From winning strategies to model graphs, part 2: the model graph (Section 6.3) #

This continues Pdl.Completeness.BuildTree. Here we define the model graph BuildTree.toModel obtained from a BuildTree (Definition 6.17) and provide the infrastructure that is used in Pdl.Completeness.BuildTreeExistence to prove the existence lemmas.

Defining The Model Graph #

source

def BuildTree.toModel {X : Sequent} (bt : BuildTree [] X) :

(W : Finset (Finset Formula)) × KripkeModel ↥W

Definition 6.17 to get model graph from strategy tree.

Equations

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

Instances For

source

theorem PreState.mem_toModel {X : Sequent} {bt : BuildTree [] X} {π : PreState bt} :

π.forms ∈ bt.toModel.fst

Helper lemma saying (the formula sets of) all pre-states are in the model graph.

source

@[instance_reducible]

instance instCoePreStateSubtypeFinsetFormulaMemFstKripkeModelToModel {X : Sequent} {bt : BuildTree [] X} :

Coe (PreState bt) ↥bt.toModel.fst

Equations

instCoePreStateSubtypeFinsetFormulaMemFstKripkeModelToModel = { coe := fun (π : PreState bt) => ⟨π.forms, ⋯⟩ }

Infrastructure for the existence lemmas #

The existence lemmas 6.18, 6.19 and 6.20 all have the same shape: given a pre-state π and a (possibly loaded) diamond in it, find another pre-state ρ that is reached from π by the corresponding Q relation. All of them are proven by walking through the BuildTree: we go to the last node of π (which is basic), apply some PdlRules there, and then pick a pre-state collected at the node we arrive at. The lemmas in this section provide the tools for these steps.

source

def PreState.toW {X : Sequent} {bt : BuildTree [] X} (π : PreState bt) :

↥bt.toModel.fst

The world of the model graph given by a pre-state.

Equations

π.toW = ⟨π.forms, ⋯⟩

Instances For

source

@[simp]

theorem PreState.toW_val {X : Sequent} {bt : BuildTree [] X} (π : PreState bt) :

↑π.toW = π.forms

source

theorem PreState.rel_iff {X : Sequent} {bt : BuildTree [] X} {π ρ : PreState bt} {a : ℕ} :

bt.toModel.snd.Rel a π.toW ρ.toW ↔ ∃ (φ : Formula), (~⌈·a⌉φ) ∈ π.forms ∧ Finset.projection a π.forms ∪ {~φ} ⊆ ρ.forms

Unfolding the atomic accessibility relation of BuildTree.toModel.

Formulas of a pre-state #

source

theorem PreState.mem_forms_of_mem {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {Z : Sequent} (hZ : Z ∈ ↑π) {f : Formula} (hf : f ∈ Z.toFinset) :

f ∈ π.forms

source

theorem PreState.mem_wForms_of_mem {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {Z : Sequent} (hZ : Z ∈ ↑π) {f : WhateverFormula} (hf : f ∈ Z.wForms) :

f ∈ π.wForms

source

theorem PreState.getLast_mem {H : History} {X : Sequent} {bt : BuildTree H X} (π : PreState bt) :

(↑π).getLast ⋯ ∈ ↑π

The last sequent of a pre-state is one of its sequents.

source

def PreState.hasAnf {H : History} {X : Sequent} {bt : BuildTree H X} (π : PreState bt) (anf : AnyNegFormula) :

Prop

A pre-state "has" an AnyNegFormula if one of its sequents contains it.

Equations

π.hasAnf anf = ∃ Z ∈ ↑π, AnyNegFormula.mem_Sequent Z anf

Instances For

source

theorem PreState.mem_forms_of_hasAnf {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {ξ : AnyFormula} (h : π.hasAnf (~''ξ)) :

~ξ.unload ∈ π.forms

If a pre-state has ~''ξ then the unloaded formula ~ξ.unload is among its formulas.

Walking down the `BuildTree` #

source

theorem Match.btAt_size_le {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) :

m.btAt.snd.snd.size ≤ bt.size

The sub-BuildTree reached by a Match is not bigger than the whole tree.

source

theorem BuildTree.exists_match_of_pdlRule {H : History} {Z : Sequent} (bt : BuildTree H Z) (bas : Z.basic) (nfr : ¬bt.isFreeRepeat) {Y : Sequent} (r : PdlRule Z Y) :

∃ (m : Match bt), m.btAt.snd.fst = Y ∧ m.btAt.snd.snd.size < bt.size

If a PdlRule is applicable at the root of a BuildTree that is basic and not a free repeat, then the tree has a corresponding child, reached by a one-step Match.

source

theorem Match.exists_step {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) (bas : m.endSeq.basic) (nfr : ¬m.btAt.snd.snd.isFreeRepeat) {Y : Sequent} (r : PdlRule m.endSeq Y) :

∃ (m' : Match bt), m'.endSeq = Y ∧ m'.btAt.snd.snd.size < m.btAt.snd.snd.size

Making a PdlRule step at the end of a Match: we get a longer Match that ends at the child sequent, and the sub-BuildTree we reach is strictly smaller.

source

theorem Match.not_isFreeRepeat_of_loaded {H : History} {X : Sequent} {bt : BuildTree H X} {m : Match bt} (hl : m.endSeq.isLoaded) :

¬m.btAt.snd.snd.isFreeRepeat

A Match ending in a loaded sequent is never at a free repeat.

source

theorem Match.exists_eq_not_freeRepeat {X : Sequent} {bt : BuildTree [] X} (m : Match bt) :

∃ (m' : Match bt), m'.endSeq = m.endSeq ∧ ¬m'.btAt.snd.snd.isFreeRepeat

Any Match can be replaced by one that ends at the same sequent and is not at a free repeat: if we are at a free repeat we go to its companion, which is strictly shorter.

source

theorem Match.exists_preState_of_not_freeRepeat {X : Sequent} {bt : BuildTree [] X} (m : Match bt) (nfr : ¬m.btAt.snd.snd.isFreeRepeat) :

∃ (ρ : PreState bt), m.endSeq ∈ ↑ρ ∧ ∃ (mρ : Match bt), mρ.endSeq = (↑ρ).getLast ⋯ ∧ mρ.btAt.snd.snd.size ≤ m.btAt.snd.snd.size

At the end of a Match that is not a free repeat we find a pre-state that starts with the sequent we are at, and whose own last sequent is reached by a Match that goes no higher up.

Free pre-states #

source

theorem BuildTree.collect_contains_root_head_of_not_freeRepeat {H : History} {X : Sequent} (bt : BuildTree H X) (h : ¬bt.isFreeRepeat) :

∃ p ∈ bt.collect, p.head? = some X

Version of BuildTree.collect_contains_root_of_not_freeRepeat saying that the root sequent is the first sequent of the collected pre-state.

source

theorem PreState.O_getLast_eq_none {H : History} {X : Sequent} {bt : BuildTree H X} (π : PreState bt) (h : ((↑π).head ⋯).O = none) :

((↑π).getLast ⋯).O = none

If the first sequent of a pre-state is free then so is its last sequent. (Generalised to an arbitrary history H, as needed for the recursion.)

source

theorem Match.exists_preState_head_of_not_freeRepeat {X : Sequent} {bt : BuildTree [] X} (m : Match bt) (nfr : ¬m.btAt.snd.snd.isFreeRepeat) :

∃ (ρ : PreState bt), (↑ρ).head ⋯ = m.endSeq ∧ ∃ (mρ : Match bt), mρ.endSeq = (↑ρ).getLast ⋯

Version of Match.exists_preState_of_not_freeRepeat where the pre-state starts at the sequent we are at.

source

theorem PdlRule.exists_modL {L R : Finset Formula} {a : ℕ} {ξ : AnyFormula} :

∃ (Y : Sequent), Nonempty (PdlRule (L, R, some (Sum.inl (~'⌊·a⌋ξ))) Y) ∧ AnyNegFormula.mem_Sequent Y (~''ξ) ∧ (∀ (f : Formula), (⌈·a⌉f) ∈ L ∪ R → f ∈ Y.toFinset) ∧ ∀ (χ : LoadFormula), ξ = AnyFormula.loaded χ → Y.isLoaded

What the modal rule (M) gives us on the left: the child contains ~''ξ and all a-successors of the boxes in the parent, and it is loaded whenever ξ is.

source

theorem PdlRule.exists_modR {L R : Finset Formula} {a : ℕ} {ξ : AnyFormula} :

∃ (Y : Sequent), Nonempty (PdlRule (L, R, some (Sum.inr (~'⌊·a⌋ξ))) Y) ∧ AnyNegFormula.mem_Sequent Y (~''ξ) ∧ (∀ (f : Formula), (⌈·a⌉f) ∈ L ∪ R → f ∈ Y.toFinset) ∧ ∀ (χ : LoadFormula), ξ = AnyFormula.loaded χ → Y.isLoaded

What the modal rule (M) gives us on the right. Mirrors PdlRule.exists_modL.

source

theorem PreState.negLoad_atomic_mem_getLast {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {a : ℕ} {ξ : AnyFormula} (h : WhateverFormula.negLoad (~'⌊·a⌋ξ) ∈ π.wForms) :

WhateverFormula.negLoad (~'⌊·a⌋ξ) ∈ ((↑π).getLast ⋯).wForms

An atomic loaded diamond in a pre-state occurs already in its last sequent. This is the loaded analogue of PreState.mem_bothSides_getLast_of_basic and the reason why the modal rule is applicable at the end of the pre-state. (Generalised from bt : BuildTree [] X to an arbitrary history H, as needed for the recursion into sub-BuildTrees.)

source

theorem PreState.exists_mem_of_mem_wForms {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {f : WhateverFormula} (h : f ∈ π.wForms) :

∃ Z ∈ ↑π, f ∈ Z.wForms

source

@[simp]

theorem PreState.hasAnf_loaded_iff {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {χ : LoadFormula} :

π.hasAnf (~''(AnyFormula.loaded χ)) ↔ WhateverFormula.negLoad (~'χ) ∈ π.wForms

source

@[simp]

theorem PreState.hasAnf_normal_iff {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {φ : Formula} :

π.hasAnf (~''(AnyFormula.normal φ)) ↔ (WhateverFormula.any ∘ AnyFormula.normal) (~φ) ∈ π.wForms

source

theorem PreState.mem_forms_of_mem_wForms {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {φ : Formula} (h : (WhateverFormula.any ∘ AnyFormula.normal) φ ∈ π.wForms) :

φ ∈ π.forms

A normal formula in π.wForms is also in π.forms.

source

theorem Sequent.isLoaded_of_negLoad_mem {Z : Sequent} {nlf : NegLoadFormula} (h : NegLoadFormula.mem_Sequent Z nlf) :

Z.isLoaded

source

theorem Sequent.box_mem_LR_of_mem_toFinset {Z : Sequent} {a : ℕ} {f : Formula} (h : (⌈·a⌉f) ∈ Z.toFinset) :

(⌈·a⌉f) ∈ Z.L ∪ Z.R

An atomic box in a sequent is on the left or on the right (it cannot come from the loaded formula, which is always negated).

source

theorem LoadFormula.box_unload {α : Program} {ξ : AnyFormula} :

(⌊α⌋ξ).unload = ⌈α⌉ξ.unload

source

theorem Match.atomicLoadedStep {X : Sequent} {bt : BuildTree [] X} (m : Match bt) (bas : m.endSeq.basic) {a : ℕ} {ξ : AnyFormula} (hload : NegLoadFormula.mem_Sequent m.endSeq (~'⌊·a⌋ξ)) :

∃ (m' : Match bt), m'.btAt.snd.snd.size < m.btAt.snd.snd.size ∧ AnyNegFormula.mem_Sequent m'.endSeq (~''ξ) ∧ (∀ (f : Formula), (⌈·a⌉f) ∈ m.endSeq.L ∪ m.endSeq.R → f ∈ m'.endSeq.toFinset) ∧ ∀ (χ : LoadFormula), ξ = AnyFormula.loaded χ → m'.endSeq.isLoaded

The modal step at the end of a Match: if the sequent we are at is basic and loaded with an atomic diamond ~'⌊·a⌋ξ, then we can go one step down, arriving at a sequent that contains ~''ξ and all a-successors of the boxes we had. Formal version of the base case of Lemma 6.18.

source

theorem Match.exists_preState_eq {X : Sequent} {bt : BuildTree [] X} (m : Match bt) :

∃ (ρ : PreState bt), ∃ Z ∈ ↑ρ, Z = m.endSeq ∧ ∃ (mρ : Match bt), mρ.endSeq = (↑ρ).getLast ⋯ ∧ (m.endSeq.isLoaded → mρ.btAt.snd.snd.size ≤ m.btAt.snd.snd.size)

After any Match there is a pre-state containing a sequent set-equal to the sequent we are at. If that sequent is loaded then the pre-state is found without going back up, so its last node is not higher up than where we are.

source

theorem PreState.atomicLoadedStep {X : Sequent} {bt : BuildTree [] X} (π : PreState bt) (mπ : Match bt) (hmπ : mπ.endSeq = (↑π).getLast ⋯) {a : ℕ} {ξ : AnyFormula} (hload : NegLoadFormula.mem_Sequent ((↑π).getLast ⋯) (~'⌊·a⌋ξ)) :

∃ (ρ : PreState bt) (mρ : Match bt), mρ.endSeq = (↑ρ).getLast ⋯ ∧ (mρ.btAt.snd.snd.size < mπ.btAt.snd.snd.size ∨ ∃ (φ : Formula), ξ = AnyFormula.normal φ) ∧ bt.toModel.snd.Rel a π.toW ρ.toW ∧ ρ.hasAnf (~''ξ)

Lemma 6.18 for an atomic program: the base case of the induction. If the last sequent of the pre-state π is loaded with ~'⌊·a⌋ξ, then there is a pre-state ρ with (Λ⁻(π), Λ⁻(ρ)) ∈ Rₐ that has ~''ξ. Unless ξ is a normal formula (in which case we may have to go back to a companion) the new pre-state also ends strictly below π.

Unfolding a loaded diamond in a pre-state #

source

theorem PreState.loadUnfold_of_nonAtom {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {α : Program} {ξ : AnyFormula} (α_notAtom : ¬α.isAtomic) (h : WhateverFormula.negLoad (~'⌊α⌋ξ) ∈ π.wForms) :

∃ Fδ ∈ Dset α, (∀ f ∈ Fδ.1, (WhateverFormula.any ∘ AnyFormula.normal) f ∈ π.wForms) ∧ π.hasAnf (~''(AnyFormula.loadBoxes Fδ.2 ξ))

Unified version of the loaded case of Lemma 6.15, for an arbitrary AnyFormula xi: if ~'⌊α⌋ξ occurs in the pre-state π and α is not atomic, then for one of the unfoldings (F,δ) ∈ Dset α all test formulas in F occur in π and π also has ~''⌊⌊δ⌋⌋ξ.