From NNF formulas to alternating Büchi automata

We construct, for every negation normal form formula, an alternating Büchi automaton (ABW) accepting the same language, establishing exists_ABW_lang_for_LTL.

@[reducible, inline]

abbrev LeanModelChecking.Iic {α : Type u_1} [LE α] (v : α) : Type u_1

The subtype { x // x ≤ v } of elements bounded above by v.

Equations

• LeanModelChecking.Iic v = { x : α // x ≤ v }

@[reducible, inline]

abbrev Subtype.embedLe {α : Type u_1} [Preorder α] {x y : α} (hle : x ≤ y) : LeanModelChecking.Iic x → LeanModelChecking.Iic y

The inclusion of LeanModelChecking.Iic x into LeanModelChecking.Iic y induced by a bound x ≤ y. Lives in the Subtype namespace so that dot notation v.embedLe hle works on subtype elements.

Equations

• Subtype.embedLe hle v = ⟨↑v, ⋯⟩

theorem LeanModelChecking.subtype_val_injective {α : Sort u_1} {P : α → Prop} : Function.Injective Subtype.val

theorem LeanModelChecking.antitone_nat_eventually_constant {f : ℕ → ℕ} (hf : Antitone f) : ∃ (N : ℕ) (c : ℕ), (∀ n ≥ N, f n = c) ∧ c ≤ f 0

def LeanModelChecking.NNF.repeatAndNext {AP : Type} (f g : NNF AP) : ℕ → NNF AP

f.repeatAndNext g n is the formula f ∧ X (f ∧ X (… ∧ X g)) with n nested next operators, used to unfold f until g to depth n.

Equations

• f.repeatAndNext g 0 = g
• f.repeatAndNext g n.succ = f.and (f.repeatAndNext g n).next

theorem LeanModelChecking.release_expand {AP : Type} (f g : NNF AP) : (f.release g).language = (g.and (f.or (f.release g).next)).language

theorem LeanModelChecking.until_expand_repeat {AP : Type} (f g : NNF AP) (w : ℕ → Letter AP) : (f.until g).language w ↔ ∃ (n : ℕ), (f.repeatAndNext g n).language w

theorem LeanModelChecking.PositiveBool.Sat.and_union {Q : Type} (f g : PositiveBool Q) {A B : Set Q} : Sat A f → Sat B g → Sat (A ∪ B) (f.and g)

def LeanModelChecking.PositiveBool.map {Q P : Type} (f : Q → P) : PositiveBool Q → PositiveBool P

Functorial action on positive Boolean formulas: rename the atoms of ψ along f, leaving the Boolean structure unchanged.

Equations

• LeanModelChecking.PositiveBool.map f (LeanModelChecking.PositiveBool.atom q) = LeanModelChecking.PositiveBool.atom (f q)
• LeanModelChecking.PositiveBool.map f LeanModelChecking.PositiveBool.true = LeanModelChecking.PositiveBool.true
• LeanModelChecking.PositiveBool.map f LeanModelChecking.PositiveBool.false = LeanModelChecking.PositiveBool.false
• LeanModelChecking.PositiveBool.map f (ψ₁.and ψ₂) = (LeanModelChecking.PositiveBool.map f ψ₁).and (LeanModelChecking.PositiveBool.map f ψ₂)
• LeanModelChecking.PositiveBool.map f (ψ₁.or ψ₂) = (LeanModelChecking.PositiveBool.map f ψ₁).or (LeanModelChecking.PositiveBool.map f ψ₂)

@[implicit_reducible]

instance LeanModelChecking.PositiveBool.instFunctor : Functor PositiveBool

Equations

• LeanModelChecking.PositiveBool.instFunctor = { map := fun {α β : Type} => LeanModelChecking.PositiveBool.map }

def LeanModelChecking.PositiveBool.Forall {α : Type} (p : α → Prop) : PositiveBool α → Prop

ψ.Forall p holds when every atom occurring in the positive Boolean formula ψ satisfies the predicate p.

Equations

• LeanModelChecking.PositiveBool.Forall p (LeanModelChecking.PositiveBool.atom q) = p q
• LeanModelChecking.PositiveBool.Forall p LeanModelChecking.PositiveBool.true = True
• LeanModelChecking.PositiveBool.Forall p LeanModelChecking.PositiveBool.false = True
• LeanModelChecking.PositiveBool.Forall p (ψ₁.and ψ₂) = (LeanModelChecking.PositiveBool.Forall p ψ₁ ∧ LeanModelChecking.PositiveBool.Forall p ψ₂)
• LeanModelChecking.PositiveBool.Forall p (ψ₁.or ψ₂) = (LeanModelChecking.PositiveBool.Forall p ψ₁ ∧ LeanModelChecking.PositiveBool.Forall p ψ₂)

theorem LeanModelChecking.PositiveBool.Forall.imp {α : Type} {p q : α → Prop} (h : ∀ (x : α), p x → q x) {φ : PositiveBool α} (pf : Forall p φ) : Forall q φ

def LeanModelChecking.PositiveBool.mapSubtype {α : Type} {p : α → Prop} (ψ : PositiveBool α) (pf : Forall p ψ) : PositiveBool (Subtype p)

Refine the atoms of ψ to the subtype Subtype p, given a proof pf that every atom of ψ satisfies p.

Equations

• (LeanModelChecking.PositiveBool.atom q).mapSubtype h = LeanModelChecking.PositiveBool.atom ⟨q, h⟩
• LeanModelChecking.PositiveBool.true.mapSubtype x = LeanModelChecking.PositiveBool.true
• LeanModelChecking.PositiveBool.false.mapSubtype x = LeanModelChecking.PositiveBool.false
• (ψ₁.and ψ₂).mapSubtype pf_2 = (ψ₁.mapSubtype ⋯).and (ψ₂.mapSubtype ⋯)
• (ψ₁.or ψ₂).mapSubtype pf_2 = (ψ₁.mapSubtype ⋯).or (ψ₂.mapSubtype ⋯)

def LeanModelChecking.PositiveBool.mapSubtypeImp {α : Type} {p q : α → Prop} (ψ : PositiveBool (Subtype p)) (h : ∀ (x : α), p x → q x) : PositiveBool (Subtype q)

Weaken the atom subtype of ψ from Subtype p to Subtype q along an implication p x → q x.

Equations

• ψ.mapSubtypeImp h = (fun (x : Subtype p) => ⟨↑x, ⋯⟩) <$> ψ

@[simp]

theorem LeanModelChecking.PositiveBool.mapSubtypeImp_collapse {α : Type} {p q : α → Prop} (ψ : PositiveBool α) {pf : Forall p ψ} {h : ∀ (x : α), p x → q x} : (ψ.mapSubtype pf).mapSubtypeImp h = ψ.mapSubtype ⋯

theorem LeanModelChecking.PositiveBool.mapSubtype_contract {α : Type} {P Q : α → Prop} {φ : PositiveBool α} {Y : Set (Subtype P)} {fq : Forall Q φ} {fp : Forall P φ} (hsat : Sat Y (φ.mapSubtype fp)) (f : Subtype P → Subtype Q) (hf : ∀ (x : Subtype P), Q ↑x → ↑(f x) = ↑x) : Sat (f '' Y) (φ.mapSubtype fq)

theorem LeanModelChecking.PositiveBool.map_sat_le {T : Type} {Q Q' : T} [Preorder T] (hle : Q' ≤ Q) {ψ : PositiveBool (Iic Q')} {Y : Set (Iic Q)} (Hsat : Sat Y (ψ.mapSubtypeImp ⋯)) : Sat {q : Iic Q' | Subtype.embedLe hle q ∈ Y} ψ

theorem LeanModelChecking.PositiveBool.mapSubtypeImp_embed {T : Type} [PartialOrder T] {x y : T} (hle : x ≤ y) (ψ : PositiveBool { q : T // q ≤ x }) (Y : Set { q : T // q ≤ x }) : Sat (Subtype.embedLe hle '' Y) (ψ.mapSubtypeImp ⋯) ↔ Sat Y ψ

theorem LeanModelChecking.PositiveBool.sat_map_image {T : Type} [PartialOrder T] {Q' Q : T} (hq : Q' ≤ Q) {ψ : PositiveBool T} {Y : Set { q : T // q ≤ Q' }} (H2 : Forall (fun (x : T) => x ≤ Q') ψ) : Sat Y (ψ.mapSubtype H2) ↔ Sat (Subtype.embedLe hq '' Y) (ψ.mapSubtype ⋯)

theorem LeanModelChecking.PositiveBool.mapSubtype_restrict {T : Type} {α β : T → Prop} {ψ : PositiveBool T} {Y : Set (Subtype α)} (all_α : Forall α ψ) (all_β : Forall β ψ) (hle : ∀ {q : T}, β q → α q) (p_sat : Sat Y (ψ.mapSubtype all_α)) : Sat {q : Subtype β | ⟨↑q, ⋯⟩ ∈ Y} (ψ.mapSubtype all_β)

@[implicit_reducible]

instance LeanModelChecking.DAG.instFunctor : Functor DAG

Equations

• One or more equations did not get rendered due to their size.

theorem LeanModelChecking.DAG.path_mapped {α β : Type u_1} [Nonempty α] (G : DAG α) (f : α → β) (f_inj : Function.Injective f) (p : ℕ → β) (p_path : (f <$> G).path p) : G.path (Function.invFun f ∘ p)

theorem LeanModelChecking.DAG.path_elems_prop {α : Type u_1} {P : α → Prop} {G : DAG (Subtype P)} {p : ℕ → α} (p_path : (Subtype.val <$> G).path p) (i : ℕ) : P (p i)

def LeanModelChecking.replaceRoot.base {T : Type} [PartialOrder T] [DecidableEq T] {φ₁ φ₂ : T} (hle : φ₁ ≤ φ₂) (r₁ : Iic φ₁) (r₂ : Iic φ₂) (G : DAG (Iic φ₁)) : DAG.Base { q : T // q ≤ φ₂ }

Underlying vertex/edge data of the replaceRoot construction: the DAG G re-rooted, with its root r₁ relabelled to r₂ and embedded into Iic φ₂.

Equations

• One or more equations did not get rendered due to their size.

def LeanModelChecking.replaceRoot.dag {T : Type} [PartialOrder T] [DecidableEq T] {φ₁ φ₂ : T} (hle : φ₁ ≤ φ₂) (r₁ : Iic φ₁) (r₂ : Iic φ₂) (G : DAG (Iic φ₁)) : DAG { q : T // q ≤ φ₂ }

The replaceRoot.base data assembled into a DAG.

Equations

• LeanModelChecking.replaceRoot.dag hle r₁ r₂ G = { toBase := LeanModelChecking.replaceRoot.base hle r₁ r₂ G, edge_closure := ⋯ }

theorem LeanModelChecking.replaceRoot.path_after_1_prop {T : Type} [PartialOrder T] [DecidableEq T] {φ₁ φ₂ : T} (hle : φ₁ ≤ φ₂) (r₁ : Iic φ₁) (r₂ : Iic φ₂) (G : DAG (Iic φ₁)) (p : ℕ → { q : T // q ≤ φ₂ }) (p_path : (dag hle r₁ r₂ G).path p) (i : ℕ) : i > 0 → ↑(p i) ≤ φ₁

theorem LeanModelChecking.replaceRoot.preserves_path {T : Type} [PartialOrder T] [DecidableEq T] {φ₁ φ₂ : T} (hle : φ₁ ≤ φ₂) (r₁ : Iic φ₁) (r₂ : Iic φ₂) (G : DAG (Iic φ₁)) (p : ℕ → { q : T // q ≤ φ₂ }) (p_path : (dag hle r₁ r₂ G).path p) : G.path fun (i : ℕ) => ⟨↑(p (i + 1)), ⋯⟩

def LeanModelChecking.replaceRoot.runDag {T : Type} [PartialOrder T] [DecidableEq T] {φ₁ φ₂ : T} (hle : φ₁ ≤ φ₂) {S : Type} {M : ABW S (Iic φ₁)} {M' : ABW S (Iic φ₂)} {w : ℕ → S} (G : RunDAG M w) (h_delta_root : ∀ (Q : Set (Iic φ₁)), PositiveBool.Sat Q (M.δ M.q₀ (w 0)) → PositiveBool.Sat (Subtype.embedLe hle '' Q) (M'.δ M'.q₀ (w 0))) (h_delta_eq : ∀ (q : Iic φ₁) (i : ℕ), M'.δ (Subtype.embedLe hle q) (w i) = (M.δ q (w i)).mapSubtypeImp ⋯) : RunDAG M' w

Transport a run DAG of M to a run DAG of M' along the replaceRoot construction, given that the transitions of M' extend those of M.

Equations

• LeanModelChecking.replaceRoot.runDag hle G h_delta_root h_delta_eq = { toDAG := LeanModelChecking.replaceRoot.dag hle M.q₀ M'.q₀ G.toDAG, p_root := ⋯, p_sat := ⋯ }

theorem LeanModelChecking.replaceRoot.runDag_accepting {T : Type} [PartialOrder T] [DecidableEq T] {φ₁ φ₂ : T} (hle : φ₁ ≤ φ₂) {S : Type} {M : ABW S (Iic φ₁)} {M' : ABW S (Iic φ₂)} {w : ℕ → S} {G : RunDAG M w} (G_acc : G.accepting) (h_delta_root : ∀ (Q : Set (Iic φ₁)), PositiveBool.Sat Q (M.δ M.q₀ (w 0)) → PositiveBool.Sat (Subtype.embedLe hle '' Q) (M'.δ M'.q₀ (w 0))) (h_delta_eq : ∀ (q : Iic φ₁) (i : ℕ), M'.δ (Subtype.embedLe hle q) (w i) = (M.δ q (w i)).mapSubtypeImp ⋯) (hF : ∀ (q : Iic φ₁), Subtype.embedLe hle q ∈ M'.F ↔ q ∈ M.F) : (runDag hle G h_delta_root h_delta_eq).accepting

If the source run DAG G is accepting and the embedding embedLe hle reflects the acceptance condition (hF), then the transported replaceRoot.runDag is accepting too.

def LeanModelChecking.shiftDag.dag {T : Type} [PartialOrder T] {φ₁ φ₂ : T} (hle : φ₁ ≤ φ₂) (r₁ : { q : T // q ≤ φ₁ }) (r₂ : { q : T // q ≤ φ₂ }) (G : DAG (Iic φ₁)) (hrx : (r₁, 0) ∈ G.V) : DAG (Iic φ₂)

Shift the DAG G down by one level and prepend a fresh root r₂ at level 0 pointing to the old root r₁, embedding everything into Iic φ₂.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanModelChecking.shiftDag.path_after_1_prop {T : Type} [PartialOrder T] {φ₁ φ₂ : T} (hle : φ₁ ≤ φ₂) (r₁ : { q : T // q ≤ φ₁ }) (r₂ : { q : T // q ≤ φ₂ }) (G : DAG (Iic φ₁)) (hrx : (r₁, 0) ∈ G.V) (p : ℕ → Iic φ₂) (p_path : (dag hle r₁ r₂ G hrx).path p) (i : ℕ) : i > 0 → ↑(p i) ≤ φ₁

theorem LeanModelChecking.shiftDag.preserves_path {T : Type} [PartialOrder T] {φ₁ φ₂ : T} (hle : φ₁ ≤ φ₂) (r₁ : { q : T // q ≤ φ₁ }) (r₂ : { q : T // q ≤ φ₂ }) (G : DAG (Iic φ₁)) (hrx : (r₁, 0) ∈ G.V) (p : ℕ → Iic φ₂) (p_path : (dag hle r₁ r₂ G hrx).path p) : G.path fun (i : ℕ) => ⟨↑(p (i + 1)), ⋯⟩

def LeanModelChecking.shiftDag.runDag {T : Type} [PartialOrder T] {φ₁ φ₂ : T} (hle : φ₁ ≤ φ₂) {S : Type} {M : ABW S (Iic φ₁)} {M' : ABW S (Iic φ₂)} {w : ℕ → S} (G : RunDAG M fun (j : ℕ) => w (j + 1)) (h_root : PositiveBool.Sat {⟨↑M.q₀, ⋯⟩} (M'.δ M'.q₀ (w 0))) (h_delta_eq : ∀ (q : Iic φ₁) (i : ℕ), M'.δ (Subtype.embedLe hle q) (w i) = (M.δ q (w i)).mapSubtypeImp ⋯) : RunDAG M' w

Turn a run DAG of M on the shifted word into a run DAG of M' on the original word, by shiftDag.dag with the old root threaded through the new one.

Equations

• LeanModelChecking.shiftDag.runDag hle G h_root h_delta_eq = { toDAG := LeanModelChecking.shiftDag.dag hle M.q₀ M'.q₀ G.toDAG ⋯, p_root := ⋯, p_sat := ⋯ }

def LeanModelChecking.conjoinDag.base {T : Type} [PartialOrder T] [DecidableEq T] {φ₁ φ₂ Φ : T} (leφ₁ : φ₁ ≤ Φ) (leφ₂ : φ₂ ≤ Φ) (r₁ : Iic φ₁) (r₂ : Iic φ₂) (R : Iic Φ) (G₁ : DAG (Iic φ₁)) (G₂ : DAG (Iic φ₂)) : DAG.Base (Iic Φ)

Vertex/edge data conjoining two DAGs G₁ and G₂ under a common fresh root R on level 0, embedding their states into the shared bound Iic Φ.

Equations

• One or more equations did not get rendered due to their size.

def LeanModelChecking.conjoinDag.dag {T : Type} [PartialOrder T] [DecidableEq T] {φ₁ φ₂ Φ : T} (leφ₁ : φ₁ ≤ Φ) (leφ₂ : φ₂ ≤ Φ) (r₁ : Iic φ₁) (r₂ : Iic φ₂) (R : Iic Φ) (G₁ : DAG (Iic φ₁)) (G₂ : DAG (Iic φ₂)) : DAG (Iic Φ)

The conjoinDag.base data assembled into a DAG.

Equations

• LeanModelChecking.conjoinDag.dag leφ₁ leφ₂ r₁ r₂ R G₁ G₂ = { toBase := LeanModelChecking.conjoinDag.base leφ₁ leφ₂ r₁ r₂ R G₁ G₂, edge_closure := ⋯ }

theorem LeanModelChecking.conjoinDag.preserves_path {T : Type} [PartialOrder T] [DecidableEq T] {φ₁ φ₂ Φ : T} (leφ₁ : φ₁ ≤ Φ) (leφ₂ : φ₂ ≤ Φ) (r₁ : Iic φ₁) (r₂ : Iic φ₂) (R : Iic Φ) (G₁ : DAG (Iic φ₁)) (G₂ : DAG (Iic φ₂)) (op : ℕ → Iic Φ) (op_path : (dag leφ₁ leφ₂ r₁ r₂ R G₁ G₂).path op) : (∃ (k : ℕ), (Subtype.val <$> G₁).path fun (i : ℕ) => ↑(op (k + i))) ∨ (Subtype.val <$> G₂).path fun (i : ℕ) => ↑(op (i + 1))

theorem LeanModelChecking.conjoinDag.runDag_p_sat {T : Type} [PartialOrder T] [DecidableEq T] {φ₁ φ₂ Φ : T} (leφ₁ : φ₁ ≤ Φ) (leφ₂ : φ₂ ≤ Φ) {S : Type} {M₁ : ABW S (Iic φ₁)} {M₂ : ABW S (Iic φ₂)} {M : ABW S (Iic Φ)} {w : ℕ → S} (G₁ : RunDAG M₁ w) (G₂ : RunDAG M₂ w) (delta_eq_1 : ∀ (q : Iic φ₁) (i : ℕ), M.δ (Subtype.embedLe leφ₁ q) (w i) = (M₁.δ q (w i)).mapSubtypeImp ⋯) (delta_eq_2 : ∀ (q : Iic φ₂) (i : ℕ), M.δ (Subtype.embedLe leφ₂ q) (w i) = (M₂.δ q (w i)).mapSubtypeImp ⋯) (delta_root : ∀ (Y₁ : Set (Iic φ₁)) (Y₂ : Set (Iic φ₂)), PositiveBool.Sat Y₁ (M₁.δ M₁.q₀ (w 0)) → PositiveBool.Sat Y₂ (M₂.δ M₂.q₀ (w 0)) → PositiveBool.Sat (Subtype.embedLe leφ₁ '' Y₁ ∪ Subtype.embedLe leφ₂ '' Y₂) (M.δ M.q₀ (w 0))) (v : Iic Φ × ℕ) : v ∈ (dag leφ₁ leφ₂ M₁.q₀ M₂.q₀ M.q₀ G₁.toDAG G₂.toDAG).V → match v with | (q, i) => ∃ (Y : Set (Iic Φ)), PositiveBool.Sat Y (M.δ q (w i)) ∧ {(q, i)} ×ˢ Y ⊆ (dag leφ₁ leφ₂ M₁.q₀ M₂.q₀ M.q₀ G₁.toDAG G₂.toDAG).E

The p_sat obligation of conjoinDag.runDag, extracted as a standalone lemma: every vertex of the conjoined DAG has a satisfying set of successors.

def LeanModelChecking.conjoinDag.runDag {T : Type} [PartialOrder T] [DecidableEq T] {φ₁ φ₂ Φ : T} (leφ₁ : φ₁ ≤ Φ) (leφ₂ : φ₂ ≤ Φ) {S : Type} {M₁ : ABW S (Iic φ₁)} {M₂ : ABW S (Iic φ₂)} {M : ABW S (Iic Φ)} {w : ℕ → S} (G₁ : RunDAG M₁ w) (G₂ : RunDAG M₂ w) (delta_eq_1 : ∀ (q : Iic φ₁) (i : ℕ), M.δ (Subtype.embedLe leφ₁ q) (w i) = (M₁.δ q (w i)).mapSubtypeImp ⋯) (delta_eq_2 : ∀ (q : Iic φ₂) (i : ℕ), M.δ (Subtype.embedLe leφ₂ q) (w i) = (M₂.δ q (w i)).mapSubtypeImp ⋯) (delta_root : ∀ (Y₁ : Set (Iic φ₁)) (Y₂ : Set (Iic φ₂)), PositiveBool.Sat Y₁ (M₁.δ M₁.q₀ (w 0)) → PositiveBool.Sat Y₂ (M₂.δ M₂.q₀ (w 0)) → PositiveBool.Sat (Subtype.embedLe leφ₁ '' Y₁ ∪ Subtype.embedLe leφ₂ '' Y₂) (M.δ M.q₀ (w 0))) : RunDAG M w

Conjoin run DAGs of M₁ and M₂ into a run DAG of M, witnessing that M runs both component automata in parallel from the shared root.

Equations

• One or more equations did not get rendered due to their size.

def LeanModelChecking.shiftConjoinDag.runDag {S T : Type} [PartialOrder T] [DecidableEq T] {φ₁ φ₂ : T} (leφ₁ : φ₁ ≤ φ₂) {M₁ : ABW S (Iic φ₁)} {M₂ : ABW S (Iic φ₂)} {w : ℕ → S} (G₁ : RunDAG M₁ w) (G₂ : RunDAG M₂ fun (j : ℕ) => w (j + 1)) (delta_eq_1 : ∀ (q : Iic φ₁) (i : ℕ), M₂.δ (Subtype.embedLe leφ₁ q) (w i) = (M₁.δ q (w i)).mapSubtypeImp ⋯) (delta_root : ∀ (Y₁ : Set (Iic φ₁)), PositiveBool.Sat Y₁ (M₁.δ M₁.q₀ (w 0)) → PositiveBool.Sat (Subtype.embedLe leφ₁ '' Y₁ ∪ {M₂.q₀}) (M₂.δ M₂.q₀ (w 0))) : RunDAG M₂ w

Conjoin a run DAG of M₁ on the current word with a run DAG of M₂ on the shifted word into a single run DAG, the construction underlying the until/ release "next" steps.

Equations

• One or more equations did not get rendered due to their size.

def LeanModelChecking.filterDag.dag {T : Type} [PartialOrder T] {φ Φ : T} (leφ : φ ≤ Φ) (G : DAG (Iic Φ)) (rΦ : Iic Φ) (rφ : Iic φ) (shift : ℕ) : DAG (Iic φ)

Extract from G the sub-DAG of states below φ, restarting it from a fresh root rφ at the given shift and re-embedding into Iic φ.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanModelChecking.filterDag.preserves_path {T : Type} [PartialOrder T] {φ Φ : T} (leφ : φ ≤ Φ) (G : DAG (Iic Φ)) (rΦ : Iic Φ) (rφ : Iic φ) (shift : ℕ) {p : ℕ → Iic φ} (p_path : (dag leφ G rΦ rφ shift).path p) : G.path fun (i : ℕ) => Subtype.embedLe leφ (p (i + 1))

def LeanModelChecking.filterDag.runDag {T : Type} [PartialOrder T] {φ Φ : T} (leφ : φ ≤ Φ) {S : Type} {M : ABW S (Iic Φ)} {M' : ABW S (Iic φ)} {w : ℕ → S} (G : RunDAG M w) (rΦ : Iic Φ) (shift : ℕ) (h_root : ∃ (Y : Set (Iic φ)), PositiveBool.Sat Y (M'.δ M'.q₀ (w shift)) ∧ Y ⊆ {q : Iic φ | ((rΦ, shift), Subtype.embedLe leφ q) ∈ G.E}) (h_delta_eq : ∀ (q : Iic φ) (i : ℕ), M.δ (Subtype.embedLe leφ q) (w i) = (M'.δ q (w i)).mapSubtypeImp ⋯) : RunDAG M' fun (j : ℕ) => w (j + shift)

Build a run DAG of M' (the sub-automaton below φ) from a run DAG of M, restricting to the descendants of a chosen vertex (rΦ, shift).

Equations

• LeanModelChecking.filterDag.runDag leφ G rΦ shift h_root h_delta_eq = { toDAG := LeanModelChecking.filterDag.dag leφ G.toDAG rΦ M'.q₀ shift, p_root := ⋯, p_sat := ⋯ }

def LeanModelChecking.alwaysDag.Vb {T : Type} [PartialOrder T] {φ : T} (G : ℕ → DAG (Iic φ)) : Set (Iic φ × ℕ)

The "below" vertex set: the union over k of the k-th DAG G k with its levels shifted up by k, used to stitch the family G into one run.

Equations

• LeanModelChecking.alwaysDag.Vb G = ⋃ (k : ℕ), {x : LeanModelChecking.Iic φ × ℕ | ∃ (q : LeanModelChecking.Iic φ) (i : ℕ) (_ : (q, i) ∈ (G k).V), (q, i + k) = x}

def LeanModelChecking.alwaysDag.V {T : Type} [PartialOrder T] {φ Φ : T} (ltφ : φ < Φ) (G : ℕ → DAG (Iic φ)) : Set (Iic Φ × ℕ)

The vertex set of the combined always DAG: the persistent root at Φ on every level, together with the embedded vertices of Vb.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanModelChecking.alwaysDag.mini {T : Type} [PartialOrder T] {φ : T} (G : ℕ → DAG (Iic φ)) (v : Iic φ × ℕ) : ℕ

The least shift i ≤ v.2 for which the vertex v already appears in G i; this is the DAG of the family that first "owns" v.

Equations

• LeanModelChecking.alwaysDag.mini G v = sInf {i : ℕ | i ≤ v.2 ∧ (v.1, v.2 - i) ∈ (G i).V}

theorem LeanModelChecking.alwaysDag.mini_le {T : Type} [PartialOrder T] {φ : T} (G : ℕ → DAG (Iic φ)) (q : Iic φ) (l : ℕ) (H : (q, l) ∈ Vb G) : mini G (q, l) ≤ l

theorem LeanModelChecking.alwaysDag.mini_in {T : Type} [PartialOrder T] {φ : T} (G : ℕ → DAG (Iic φ)) (q : Iic φ) (l : ℕ) (H : (q, l) ∈ Vb G) : have i' := mini G (q, l); (q, l - i') ∈ (G i').V

def LeanModelChecking.alwaysDag.E {T : Type} [PartialOrder T] {φ Φ : T} (G : ℕ → DAG (Iic φ)) : Set ((Iic Φ × ℕ) × Iic Φ)

The edge set of the combined always DAG: the root Φ loops on itself and spawns a fresh copy of each G l at every level, while non-root vertices follow the edges of the DAG G (mini …) that owns them.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanModelChecking.alwaysDag.mini_not_increasing {T : Type} [PartialOrder T] {φ Φ : T} (ltφ : φ < Φ) (G : ℕ → DAG (Iic φ)) (q : Iic φ) (l : ℕ) (q' : Iic φ) (He : ((Subtype.embedLe ⋯ q, l), Subtype.embedLe ⋯ q') ∈ E G) : mini G (q', l + 1) ≤ mini G (q, l)

def LeanModelChecking.alwaysDag.base {T : Type} [PartialOrder T] {φ Φ : T} (ltφ : φ < Φ) (G : ℕ → DAG (Iic φ)) : DAG.Base (Iic Φ)

The vertex/edge data of the always construction.

Equations

• LeanModelChecking.alwaysDag.base ltφ G = { V := LeanModelChecking.alwaysDag.V ltφ G, E := LeanModelChecking.alwaysDag.E G }

def LeanModelChecking.alwaysDag.dag {T : Type} [PartialOrder T] {φ Φ : T} (ltφ : φ < Φ) (G : ℕ → DAG (Iic φ)) : DAG (Iic Φ)

The alwaysDag.base data assembled into a DAG.

Equations

• LeanModelChecking.alwaysDag.dag ltφ G = { toBase := LeanModelChecking.alwaysDag.base ltφ G, edge_closure := ⋯ }

theorem LeanModelChecking.alwaysDag.preserves_path {T : Type} [PartialOrder T] {φ Φ : T} (ltφ : φ < Φ) (G : ℕ → DAG (Iic φ)) (op : ℕ → Iic Φ) (op_path : (dag ltφ G).path op) : (op = fun (x : ℕ) => ⟨Φ, ⋯⟩) ∨ ∃ (i : ℕ) (k : ℕ), (Subtype.val <$> G i).path fun (i : ℕ) => ↑(op (k + i))

def LeanModelChecking.alwaysDag.runDag {T : Type} [PartialOrder T] {φ Φ : T} (ltφ : φ < Φ) {S : Type} {M : ABW S (Iic Φ)} {M' : ABW S (Iic φ)} {w : ℕ → S} (G : (i : ℕ) → RunDAG M' fun (j : ℕ) => w (j + i)) (h_M_root : M.q₀ = ⟨Φ, ⋯⟩) (h_M'_root : M'.q₀ = ⟨φ, ⋯⟩) (h_delta_root : ∀ (Y : Set (Iic φ)) (l : ℕ), PositiveBool.Sat Y (M'.δ M'.q₀ (w l)) → PositiveBool.Sat (Subtype.embedLe ⋯ '' Y ∪ {M.q₀}) (M.δ ⟨Φ, ⋯⟩ (w l))) (h_delta_eq : ∀ (q : Iic φ) (i : ℕ), M.δ (Subtype.embedLe ⋯ q) (w i) = (M'.δ q (w i)).mapSubtypeImp ⋯) : RunDAG M w

Combine the family of run DAGs G i of M' on every shifted word into one run DAG of M, realising the release/always semantics where the obligation is restarted at each level.

Equations

• LeanModelChecking.alwaysDag.runDag ltφ G h_M_root h_M'_root h_delta_root h_delta_eq = { toDAG := LeanModelChecking.alwaysDag.dag ltφ fun (i : ℕ) => (G i).toDAG, p_root := ⋯, p_sat := ⋯ }

inductive LeanModelChecking.sub {AP : Type} : NNF AP → NNF AP → Prop

Subformula relation: φ ≤ ψ means φ is a subformula of ψ

• refl {AP : Type} {φ : NNF AP} : sub φ φ
• and_left {AP : Type} {φ f g : NNF AP} : sub φ f → sub φ (f.and g)
• and_right {AP : Type} {φ f g : NNF AP} : sub φ g → sub φ (f.and g)
• or_left {AP : Type} {φ f g : NNF AP} : sub φ f → sub φ (f.or g)
• or_right {AP : Type} {φ f g : NNF AP} : sub φ g → sub φ (f.or g)
• next {AP : Type} {φ f : NNF AP} : sub φ f → sub φ f.next
• until_left {AP : Type} {φ f g : NNF AP} : sub φ f → sub φ (f.until g)
• until_right {AP : Type} {φ f g : NNF AP} : sub φ g → sub φ (f.until g)
• release_left {AP : Type} {φ f g : NNF AP} : sub φ f → sub φ (f.release g)
• release_right {AP : Type} {φ f g : NNF AP} : sub φ g → sub φ (f.release g)

@[implicit_reducible]

instance LeanModelChecking.instLENNF {AP : Type} : LE (NNF AP)

Equations

• LeanModelChecking.instLENNF = { le := LeanModelChecking.sub }

def LeanModelChecking.size {AP : Type} : NNF AP → ℕ

A structural size measure on NNF formulas, used to bound the subformula order and prove finiteness of the state space.

Equations

• LeanModelChecking.size (LeanModelChecking.NNF.atom p) = 1
• LeanModelChecking.size (LeanModelChecking.NNF.not_atom p) = 1
• LeanModelChecking.size φ₁.next = LeanModelChecking.size φ₁ + 1
• LeanModelChecking.size (φ₁.and φ₂) = max (LeanModelChecking.size φ₁) (LeanModelChecking.size φ₂) + 1
• LeanModelChecking.size (φ₁.or φ₂) = max (LeanModelChecking.size φ₁) (LeanModelChecking.size φ₂) + 1
• LeanModelChecking.size (φ₁.until φ₂) = max (LeanModelChecking.size φ₁) (LeanModelChecking.size φ₂) + 1
• LeanModelChecking.size (φ₁.release φ₂) = max (LeanModelChecking.size φ₁) (LeanModelChecking.size φ₂) + 1

theorem LeanModelChecking.size_le_of_sub {AP : Type} {φ ψ : NNF AP} (h : φ ≤ ψ) : size φ ≤ size ψ

theorem LeanModelChecking.size_lt_of_sub {AP : Type} {φ ψ : NNF AP} (h : φ ≤ ψ) (hne : ψ ≠ φ) : size φ < size ψ

theorem LeanModelChecking.sub_antisymm {AP : Type} {φ₁ φ₂ : NNF AP} (h1 : φ₁ ≤ φ₂) (h2 : φ₂ ≤ φ₁) : φ₁ = φ₂

theorem LeanModelChecking.sub_trans {AP : Type} {a b c : NNF AP} (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c

@[implicit_reducible]

instance LeanModelChecking.instPartialOrderNNF {AP : Type} : PartialOrder (NNF AP)

Equations

• One or more equations did not get rendered due to their size.

instance LeanModelChecking.instNonemptySubtypeNNFLe {AP : Type} {ψ : NNF AP} : Nonempty { q : NNF AP // q ≤ ψ }

def LeanModelChecking.subFinset {AP : Type} [DecidableEq AP] : NNF AP → Finset (NNF AP)

The finite set of subformulas of an NNF formula (including the formula itself), witnessing that the subformula order has a finite carrier.

Equations

• LeanModelChecking.subFinset (LeanModelChecking.NNF.atom p) = {LeanModelChecking.NNF.atom p}
• LeanModelChecking.subFinset (LeanModelChecking.NNF.not_atom p) = {LeanModelChecking.NNF.not_atom p}
• LeanModelChecking.subFinset φ₁.next = insert φ₁.next (LeanModelChecking.subFinset φ₁)
• LeanModelChecking.subFinset (φ₁.and φ₂) = insert (φ₁.and φ₂) (LeanModelChecking.subFinset φ₁ ∪ LeanModelChecking.subFinset φ₂)
• LeanModelChecking.subFinset (φ₁.or φ₂) = insert (φ₁.or φ₂) (LeanModelChecking.subFinset φ₁ ∪ LeanModelChecking.subFinset φ₂)
• LeanModelChecking.subFinset (φ₁.until φ₂) = insert (φ₁.until φ₂) (LeanModelChecking.subFinset φ₁ ∪ LeanModelChecking.subFinset φ₂)
• LeanModelChecking.subFinset (φ₁.release φ₂) = insert (φ₁.release φ₂) (LeanModelChecking.subFinset φ₁ ∪ LeanModelChecking.subFinset φ₂)

theorem LeanModelChecking.mem_sub_finset {AP : Type} [DecidableEq AP] {q f : NNF AP} : q ≤ f → q ∈ subFinset f

theorem LeanModelChecking.sub_finite {AP : Type} (f : NNF AP) : Finite { q : NNF AP // q ≤ f }

def LeanModelChecking.delta {AP : Type} (φ : NNF AP) (σ : Letter AP) [DecidablePred fun (x : AP) => x ∈ σ] : PositiveBool (NNF AP)

The one-step transition formula of the alternating automaton for φ on the letter σ: a positive Boolean formula over subformulas describing which obligations the successors must satisfy.

Equations

• LeanModelChecking.delta (LeanModelChecking.NNF.atom p) σ = if p ∈ σ then LeanModelChecking.PositiveBool.true else LeanModelChecking.PositiveBool.false
• LeanModelChecking.delta (LeanModelChecking.NNF.not_atom p) σ = if p ∈ σ then LeanModelChecking.PositiveBool.false else LeanModelChecking.PositiveBool.true
• LeanModelChecking.delta (φ₁.and φ₂) σ = (LeanModelChecking.delta φ₁ σ).and (LeanModelChecking.delta φ₂ σ)
• LeanModelChecking.delta (φ₁.or φ₂) σ = (LeanModelChecking.delta φ₁ σ).or (LeanModelChecking.delta φ₂ σ)
• LeanModelChecking.delta φ₁.next σ = LeanModelChecking.PositiveBool.atom φ₁
• LeanModelChecking.delta (φ₁.until φ₂) σ = (LeanModelChecking.delta φ₂ σ).or ((LeanModelChecking.delta φ₁ σ).and (LeanModelChecking.PositiveBool.atom (φ₁.until φ₂)))
• LeanModelChecking.delta (φ₁.release φ₂) σ = (LeanModelChecking.delta φ₂ σ).and ((LeanModelChecking.delta φ₁ σ).or (LeanModelChecking.PositiveBool.atom (φ₁.release φ₂)))

theorem LeanModelChecking.delta_forall {AP : Type} {φ : NNF AP} {σ : Letter AP} [DecidablePred fun (x : AP) => x ∈ σ] : PositiveBool.Forall (fun (x : NNF AP) => x ≤ φ) (delta φ σ)

noncomputable def LeanModelChecking.NNF.toABW {AP : Type} (ψ : NNF AP) : ABW (Letter AP) { x : NNF AP // x ≤ ψ }

The alternating Büchi automaton recognising the language of the NNF formula ψ: its states are the subformulas of ψ, its initial state is ψ, and its transitions are given by delta.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanModelChecking.subformula_toABW_lang {S : Type} {Φ φ : NNF S} (leφ : φ ≤ Φ) {w : ℕ → Letter S} {G : RunDAG Φ.toABW w} (G_acc : G.accepting) {k : ℕ} {q : Iic Φ} {Y : Set (Iic Φ)} (p_sat : PositiveBool.Sat Y (Φ.toABW.δ ⟨φ, leφ⟩ (w k))) (p_sub : {(q, k)} ×ˢ Y ⊆ G.E) : φ.toABW.language fun (j : ℕ) => w (j + k)

theorem LeanModelChecking.and_mp.left {S : Type} {φ₁ φ₂ : NNF S} {w : ℕ → Letter S} : (φ₁.and φ₂).toABW.language w → φ₁.toABW.language w

theorem LeanModelChecking.and_mp.right {S : Type} {φ₁ φ₂ : NNF S} {w : ℕ → Letter S} : (φ₁.and φ₂).toABW.language w → φ₂.toABW.language w

theorem LeanModelChecking.and_mpr {AP : Type} {φ₁ φ₂ : NNF AP} {w : ℕ → Letter AP} (H1 : φ₁.toABW.language w) (H2 : φ₂.toABW.language w) : (φ₁.and φ₂).toABW.language w

theorem LeanModelChecking.or_mp {S : Type} {φ₁ φ₂ : NNF S} {w : ℕ → Letter S} : (φ₁.or φ₂).toABW.language w → φ₁.toABW.language w ∨ φ₂.toABW.language w

theorem LeanModelChecking.or_mpr.left {S : Type} {φ₁ φ₂ : NNF S} {w : ℕ → Letter S} : φ₁.toABW.language w → (φ₁.or φ₂).toABW.language w

theorem LeanModelChecking.or_mpr.right {S : Type} {φ₁ φ₂ : NNF S} {w : ℕ → Letter S} : φ₂.toABW.language w → (φ₁.or φ₂).toABW.language w

theorem LeanModelChecking.next_mp {AP : Type} {φ : NNF AP} {w : ℕ → Letter AP} : φ.next.toABW.language w → φ.toABW.language fun (j : ℕ) => w (j + 1)

theorem LeanModelChecking.next_mpr {AP : Type} {φ : NNF AP} {w : ℕ → Letter AP} : (φ.toABW.language fun (j : ℕ) => w (j + 1)) → φ.next.toABW.language w

theorem LeanModelChecking.until_mp {S : Type} {φ₁ φ₂ : NNF S} {w : ℕ → Letter S} (H : (φ₁.until φ₂).toABW.language w) : ∃ (n : ℕ), (φ₂.toABW.language fun (j : ℕ) => w (j + n)) ∧ ∀ k < n, φ₁.toABW.language fun (j : ℕ) => w (j + k)

theorem LeanModelChecking.until_mpr.base {S : Type} {φ₁ φ₂ : NNF S} {w : ℕ → Letter S} (h2 : φ₂.toABW.language w) : (φ₁.until φ₂).toABW.language w

theorem LeanModelChecking.until_mpr.next {S : Type} {φ₁ φ₂ : NNF S} {w : ℕ → Letter S} (h1 : φ₁.toABW.language w) (h2 : (φ₁.until φ₂).toABW.language fun (j : ℕ) => w (j + 1)) : (φ₁.until φ₂).toABW.language w

theorem LeanModelChecking.release_mp.right {S : Type} {φ₁ φ₂ : NNF S} {w : ℕ → Letter S} {G : RunDAG (φ₁.release φ₂).toABW w} (G_acc : G.accepting) {l : ℕ} (H : (⟨φ₁.release φ₂, ⋯⟩, l) ∈ G.V) : φ₂.toABW.language fun (j : ℕ) => w (j + l)

theorem LeanModelChecking.release_mp.left {S : Type} {φ₁ φ₂ : NNF S} {w : ℕ → Letter S} {G : RunDAG (φ₁.release φ₂).toABW w} (G_acc : G.accepting) {l : ℕ} (H₁ : (⟨φ₁.release φ₂, ⋯⟩, l) ∈ G.V) (H₂ : (⟨φ₁.release φ₂, ⋯⟩, l + 1) ∉ G.V) : φ₁.toABW.language fun (j : ℕ) => w (j + l)

theorem LeanModelChecking.release_mpr.always {S : Type} {φ₁ φ₂ : NNF S} {w : ℕ → Letter S} (hg : ∀ (i : ℕ), φ₂.toABW.language fun (j : ℕ) => w (j + i)) : (φ₁.release φ₂).toABW.language w

theorem LeanModelChecking.release_mpr.base {S : Type} {φ₁ φ₂ : NNF S} {w : ℕ → Letter S} (h1 : φ₁.toABW.language w) (h2 : φ₂.toABW.language w) : (φ₁.release φ₂).toABW.language w

theorem LeanModelChecking.release_mpr.next {S : Type} {φ₁ φ₂ : NNF S} {w : ℕ → Letter S} (h2 : φ₂.toABW.language w) (h3 : (φ₁.release φ₂).toABW.language fun (j : ℕ) => w (j + 1)) : (φ₁.release φ₂).toABW.language w

theorem LeanModelChecking.NNF.toABW_lang {AP : Type} (ψ : NNF AP) : ψ.toABW.language = ψ.language

theorem LeanModelChecking.exists_ABW_lang_for_LTL {AP : Type} (f : LTL AP) : ∃ (Q : Type) (_ : Finite Q) (A : ABW (Letter AP) Q), f.language = A.language