Model Graphs (Section 6.1)

Definition of Model Graphs

def Modelgraphs.Q {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) : Program → ↥W → ↥W → Prop

Definition 6.3: Given relations for all atomic programs over model graph states (i.e. sets of formulas), define relations for all PDL programs inductively as usual, but using membership to interpret the test operator.

Equations

• Modelgraphs.Q R (·c) = R c
• Modelgraphs.Q R (?'τ) = fun (v w : ↥W) => v = w ∧ τ ∈ ↑v
• Modelgraphs.Q R (α⋓β) = fun (v w : ↥W) => Modelgraphs.Q R α v w ∨ Modelgraphs.Q R β v w
• Modelgraphs.Q R (α;'β) = Relation.Comp (Modelgraphs.Q R α) (Modelgraphs.Q R β)
• Modelgraphs.Q R (∗α) = Relation.ReflTransGen (Modelgraphs.Q R α)

def ModelGraph (W : Finset (Finset Formula)) : Type

Definition 6.4. A model graph is a Kripke model over sets of formulas as states fulfilling the conditions (a) to (b). See also [Bor88] Def 19 on page 31 where (a)-(b) are named (i)-(iv). Note: In MB item (b) aka (ii) only has →. We use ↔ similar to [BdRV01] Def 4.18 and 4.84. Note: In item (c) a is atomic, but in item (d) α is any program.

Equations

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

Truth Lemma

theorem get_eq_getzip {α : Type u_1} {l : List α} {α✝ : Type u_2} {x : α✝} {δ : List α✝} {X Y : α} {i : Fin (l ++ [Y]).length} {h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length} : (X :: (l ++ [Y])).get i.castSucc = ((x, X) :: δ.zip (l ++ [Y]))[↑i].2

theorem loadClaimHelper {Worlds : Finset (Finset Formula)} {MG : ModelGraph Worlds} {X Y : ↥Worlds} {δ : List Program} {φ : Formula} {l : List ↥Worlds} (length_def : l.length + 1 = δ.length) (δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X) (lchain : List.IsChain (pairRel ↑MG) (((?'⊤) :: δ).zip (X :: l ++ [Y]))) (IHδ : ∀ d ∈ δ, ∀ (X' Y' : ↥Worlds) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y') (i : Fin (X :: l ++ [Y]).length) : (⌈⌈List.drop (↑i) δ⌉⌉φ) ∈ ↑((X :: l ++ [Y]).get i)

theorem Q_then_relate {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) (α : Program) (X Y : ↥Worlds) : Modelgraphs.Q (↑MG).Rel α X Y → relate (↑MG) α X Y

Condition C3 for the proof of Lemma 6.5. Originally MB Lemma 9, page 32, stronger version for induction loading. Now also using Q relation to overwrite tests.

theorem loadedTruthLemma {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) (X : ↥Worlds) (P : Formula) : (P ∈ ↑X → evaluate (↑MG) X P) ∧ (~P ∈ ↑X → ¬evaluate (↑MG) X P)

Conditions C1 and C2 for the proof of Lemma 6.5.

theorem loadedTruthLemmaProg {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) (α : Program) (X : ↥Worlds) (φ : Formula) : (⌈α⌉φ) ∈ ↑X → ∀ (Y : ↥Worlds), relate (↑MG) α X Y → φ ∈ ↑Y

Condition C4 for the proof of Lemma 6.5.

theorem truthLemma {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) (X : ↥Worlds) (P : Formula) : P ∈ ↑X → evaluate (↑MG) X P

Additional Q relations for the completeness proof

def Qtests {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) (F : List Formula) : ↥W → ↥W → Prop

Q_F - for a list F of tests (instead of a set in the notes).

Equations

• Qtests R F x✝¹ x✝ = ((x✝¹ == x✝) = true ∧ ∀ τ ∈ F, Modelgraphs.Q R (?'τ) x✝¹ x✝)

def Qsteps {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) : List Program → ↥W → ↥W → Prop

Q_δ for a list δ of programs.

Equations

• Qsteps R [] x✝¹ x✝ = ((x✝¹ == x✝) = true)
• Qsteps R (α :: δ) x✝¹ x✝ = Relation.Comp (Modelgraphs.Q R α) (Qsteps R δ) x✝¹ x✝

@[simp]

theorem Qsteps_single {a✝ : Finset (Finset Formula)} {R : ℕ → ↥a✝ → ↥a✝ → Prop} {α : Program} {v w : ↥a✝} : Qsteps R [α] v w ↔ Modelgraphs.Q R α v w

theorem Qsteps_append {a✝ : Finset (Finset Formula)} {R : ℕ → ↥a✝ → ↥a✝ → Prop} {δ1 δ2 : List Program} {v w : ↥a✝} : Qsteps R (δ1 ++ δ2) v w ↔ ∃ (u : ↥a✝), Qsteps R δ1 v u ∧ Qsteps R δ2 u w

def Qcombo {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) (F : List Formula) (δ : List Program) : ↥W → ↥W → Prop

Q_Fδ for a list of tests F and a list or programs δ.

Equations

• Qcombo R F δ = Relation.Comp (Qtests R F) (Qsteps R δ)

theorem cpHelpA {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) (α : Program) (Fδ : List Formula × List Program) : Fδ ∈ Dset α → ∀ (v w : ↥W), Qcombo R Fδ.1 Fδ.2 v w → Modelgraphs.Q R α v w

Q_Fδ v w implies Q v w.