From winning strategies to model graphs, part 3: the existence lemmas (Section 6.3)

This continues Pdl/BuildTreeModel.lean. Here we prove the existence lemmas 6.18, 6.19 and 6.20 that are needed for Theorem 6.21 (strmg).

The loaded diamond existence lemma (Lemma 6.18)

theorem PreState.atomicLoadedStep_wForms {X : Sequent} {bt : BuildTree [] X} (π : PreState bt) (mπ : Match bt) (hmπ : mπ.endSeq = (↑π).getLast ⋯) {a : ℕ} {ξ : AnyFormula} (h : WhateverFormula.negLoad (~'⌊·a⌋ξ) ∈ π.wForms) : ∃ (ρ : 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 (~''ξ)

Version of PreState.atomicLoadedStep with the loaded diamond given in π.wForms.

def LoadedExistsB {X : Sequent} (bt : BuildTree [] X) (α : Program) (n : ℕ) : Prop

The claim of Lemma 6.18 for a fixed program α, where the size of the sub-BuildTree we are currently at (mπ.btAt) is bounded by n. This n is used for the inner induction. Here π is the pre-state we start at and mπ is a Match witnessing where it ends, and ρ is the pre-state we reach. Note that we use Rel from BuildTree.toModel as the R to use Modelgraphs.Q.

Equations

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

def LoadedExists {X : Sequent} (bt : BuildTree [] X) (α : Program) : Prop

Lemma 6.18 for the program α, without any bound on where we are in the BuildTree.

Equations

• LoadedExists bt α = ∀ (n : ℕ), LoadedExistsB bt α n

theorem loadedChain {X : Sequent} {bt : BuildTree [] X} (γs : List Program) : (∀ γ ∈ γs, LoadedExists bt γ) → ∀ (π : PreState bt) (mπ : Match bt), mπ.endSeq = (↑π).getLast ⋯ → ∀ (ξ : AnyFormula), π.hasAnf (~''(AnyFormula.loadBoxes γs ξ)) → ∃ (ρ : PreState bt) (mρ : Match bt), mρ.endSeq = (↑ρ).getLast ⋯ ∧ (∀ (χ : LoadFormula), ξ = AnyFormula.loaded χ → mρ.btAt.snd.snd.size ≤ mπ.btAt.snd.snd.size) ∧ Qsteps bt.toModel.snd.Rel γs π.toW ρ.toW ∧ ρ.hasAnf (~''ξ)

Iterating Lemma 6.18 along a list of programs.

@[irreducible]

theorem PreState.loadedExists {X : Sequent} {bt : BuildTree [] X} (α : Program) : LoadedExists bt α

Lemma 6.18, the loaded diamond existence lemma. If the loaded diamond ~'⌊α⌋ξ occurs in the pre-state π, then there is a pre-state ρ with Q α (Λ⁻ π) (Λ⁻ ρ) that has ~''ξ. Moreover, if ξ is still loaded then ρ is reached without going up in the BuildTree. Note that the claim is abbreviated by LoadedExists bt α. The proof is by an outer induction on the length of α and an inner induction on the size of the sub-BuildTree we are at.

theorem PreState.loadedDiamondExistence {X : Sequent} {bt : BuildTree [] X} {α : Program} {φ : AnyFormula} {π : PreState bt} (h : WhateverFormula.negLoad (~'⌊α⌋φ) ∈ π.wForms) : ∃ (ρ : PreState bt), Modelgraphs.Q bt.toModel.snd.Rel α π.toW ρ.toW ∧ ρ.hasAnf (~''φ)

If ~'⌊α⌋φ occurs in the pre-state π then there is a pre-state ρ reached from π by Q α that contains ~''φ. This is a consequence of Lemma 6.18 PreState.loadedExists, but omits the bound-related claims used for induction loading. Again note that we use Rel from BuildTree.toModel as the R to use Modelgraphs.Q.

The free diamond existence lemma (Lemma 6.19)

To load a free diamond ~⌌·a⌍chi with the rule (L+) we first have to make the sequent free using (L-), and on the way we may have to go to the companion of a free repeat.

theorem Sequent.O_eq_of_setEqTo {Z Z' : Sequent} (h : Z.setEqTo Z') : Z.O = Z'.O

Set-equal sequents have the same loaded formula.

theorem Sequent.not_closed_of_sub {L R L' R' : List Formula} {O O' : Olf} (hL : ∀ f ∈ L', f ∈ L) (hR : ∀ f ∈ R', f ∈ R) (h : ¬closed (L, R, O)) : ¬closed (L', R', O')

A sequent with fewer formulas on the two sides is not closed either.

theorem PdlRule.exists_freeStep {Z : Sequent} (hZ : Z.O ≠ none) : ∃ (Y : Sequent), Nonempty (PdlRule Z Y) ∧ Y.O = none ∧ ∀ f ∈ Z.bothSides, f ∈ Y.bothSides

Applying the rule (L-) to free the loaded formula: all formulas we had are kept.

theorem PdlRule.exists_loadStep {L R : List Formula} {a : ℕ} {χ : Formula} (bas : Sequent.basic (L, R, none)) (hmem : (~⌈·a⌉χ) ∈ L ++ R) : ∃ (Y : Sequent), Nonempty (PdlRule (L, R, none) Y) ∧ Y.basic ∧ NegLoadFormula.mem_Sequent Y (~'⌊·a⌋AnyFormula.loadBoxes (boxesOf χ).1 (AnyFormula.normal (boxesOf χ).2)) ∧ ∀ (g : Formula), (g ≠ ~⌈·a⌉χ) → g ∈ L ++ R → g ∈ Y.L ++ Y.R

Applying the rule (L+) to load a free diamond ~⌌·a⌍chi maximally, using boxesOf.

theorem Match.exists_free_basic {X : Sequent} {bt : BuildTree [] X} (m : Match bt) (bas : m.endSeq.basic) : ∃ (m' : Match bt), m'.endSeq.basic ∧ m'.endSeq.O = none ∧ ¬m'.btAt.snd.snd.isFreeRepeat ∧ ∀ (f : Formula), f.basic = true → f ∈ m.endSeq.bothSides → f ∈ m'.endSeq.bothSides

Getting to a Match at a free and basic sequent that is not a free repeat, keeping all basic formulas we had. Preparation for the (L+) rule in Lemma 6.19.

theorem Match.modalStepToPreState {X : Sequent} {bt : BuildTree [] X} (m : Match bt) (bas : m.endSeq.basic) {a : ℕ} {ξ : AnyFormula} (hload : NegLoadFormula.mem_Sequent m.endSeq (~'⌊·a⌋ξ)) : ∃ (ρ : PreState bt), ρ.hasAnf (~''ξ) ∧ ∀ (f : Formula), (⌈·a⌉f) ∈ m.endSeq.L ++ m.endSeq.R → f ∈ ρ.forms

The modal step at the end of a Match, landing in a pre-state: if we are at a basic sequent loaded with ~'⌊·a⌋ξ then there is a pre-state that has ~''ξ and all a-successors of the boxes we had.

theorem PreState.freeAtomicStep {X : Sequent} {bt : BuildTree [] X} (π : PreState bt) {a : ℕ} {χ : Formula} (h : (WhateverFormula.any ∘ AnyFormula.normal) (~⌈·a⌉χ) ∈ π.wForms) : ∃ (ρ : PreState bt), bt.toModel.snd.Rel a π.toW ρ.toW ∧ ρ.hasAnf (~''(AnyFormula.loadBoxes (boxesOf χ).1 (AnyFormula.normal (boxesOf χ).2)))

Lemma 6.19: If a free diamond ~⌈·a⌉χ with an atomic program occurs in the pre-state π, then there is an a-successor pre-state ρ of π that has ~''χ, maximally loaded.

The free diamond existence lemma (Lemma 6.20)

theorem PreState.chainFromLoadBoxes {X : Sequent} {bt : BuildTree [] X} (γs : List Program) (ξ : AnyFormula) (π : PreState bt) (h : π.hasAnf (~''(AnyFormula.loadBoxes γs ξ))) : ∃ (ρ : PreState bt), Qsteps bt.toModel.snd.Rel γs π.toW ρ.toW ∧ ρ.hasAnf (~''ξ)

Iterating Lemma 6.18 along a list of programs, formulated with Qsteps. From a pre-state that has ~''(loadBoxes γs ξ) we reach one that has ~''ξ.

theorem PreState.freeAtomicChain {X : Sequent} {bt : BuildTree [] X} {π : PreState bt} {a : ℕ} {γs : List Program} {φ : Formula} (h : (WhateverFormula.any ∘ AnyFormula.normal) (~⌈·a⌉⌈⌈γs⌉⌉φ) ∈ π.wForms) : ∃ (ρ : PreState bt), Qsteps bt.toModel.snd.Rel (·a :: γs) π.toW ρ.toW ∧ ~φ ∈ ρ.forms

Combining Lemma 6.19 with Lemma 6.18: if the free diamond ~⌈·a⌉⌈⌈γs⌉⌉φ is in the pre-state π, then we can make the ·a step and then follow γs to reach a pre-state containing ~φ.

theorem PreState.freeExists {X : Sequent} {bt : BuildTree [] X} (α : Program) {φ : Formula} {π : PreState bt} (h : (WhateverFormula.any ∘ AnyFormula.normal) (~⌈α⌉φ) ∈ π.wForms) : ∃ (ρ : PreState bt), Modelgraphs.Q bt.toModel.snd.Rel α π.toW ρ.toW ∧ ~φ ∈ ρ.forms

The claim used to prove Lemma 6.20: if the free diamond ~⌈α⌉φ occurs in the pre-state π, then there is a pre-state ρ with Q α (Λ⁻ π) (Λ⁻ ρ) that contains ~φ.

theorem freeDiamondExistenceInduction {X : Sequent} {bt : BuildTree [] X} {ψ : Formula} {α : Program} {ηs : List Program} {π : PreState bt} : (WhateverFormula.any ∘ AnyFormula.normal) (~⌈α⌉⌈⌈ηs⌉⌉ψ) ∈ π.wForms → ∃ (π' : PreState bt), (~⌈⌈ηs⌉⌉ψ) ∈ π'.forms ∧ Modelgraphs.Q bt.toModel.snd.Rel α ⟨π.forms, ⋯⟩ ⟨π'.forms, ⋯⟩

Induction loading for 6.20. (Note that ψ may even be boxed here, because PreState.freeExists holds for all formulas.)

theorem freeDiamondExistence {X : Sequent} {bt : BuildTree [] X} {α : Program} {φ : Formula} {π : PreState bt} : (WhateverFormula.any ∘ AnyFormula.normal) (~⌈α⌉φ) ∈ π.wForms → ∃ (π' : PreState bt), ~φ ∈ π'.forms ∧ Modelgraphs.Q bt.toModel.snd.Rel α ⟨π.forms, ⋯⟩ ⟨π'.forms, ⋯⟩

Lemma 6.20: free diamond existence lemma for pre-states