From winning strategies to model graphs (Section 6.3)

BuildTree

theorem LoadFormula.split_splitLast_to_loadBoxes {δs : List Program} {φ : Formula} {δs_ : List Program} {δ : Program} {ξ : AnyFormula} (ξsp_def : ξ.split = (δs, φ)) (sp_def : splitLast δs = some (δs_, δ)) : ξ = AnyFormula.loadBoxes (δs_ ++ [δ]) (AnyFormula.normal φ)

def PdlRule.all (X : Sequent) : List ((Y : Sequent) × PdlRule X Y)

List of all PdlRules applicable to X. Code is based on part of theMoves This is also similar to the definitions in LocalAll.lean.

Equations

• One or more equations did not get rendered due to their size.
• PdlRule.all X = []

theorem LoadFormula.split_boxes_cons {βs : List Program} {α : Program} {φ : Formula} : (⌊⌊βs⌋⌋⌊α⌋AnyFormula.normal φ).split = (βs ++ [α], φ)

theorem PdlRule.all_spec {X Y : Sequent} (bas : X.basic) (r : PdlRule X Y) : ⟨Y, r⟩ ∈ all X

Specification that PdlRule.all is complete, almost: we demand X.basic here which is not part of the PdlRule type, but demanded by Tableau.pdl.

inductive BuildTree : GamePos → Type

Tree data type to keep track of choices made by Builder. Might still need to be tweaked.

• Choices should be labelled with the choices made by prover? TODO: Do we need to keep track of which rule is used?

• Leaf {pos : GamePos} (rp : rep pos.fst pos.snd.fst) : BuildTree pos
• Step {pos : GamePos} (YS : List GamePos) (YS_Moves : (newPos : GamePos) → newPos ∈ YS → Move pos newPos) (next : (newPos : GamePos) → newPos ∈ YS → BuildTree newPos) : BuildTree pos

def theRep {H : History} {X : Sequent} (rp : rep H X) : ℕ

Equations

• theRep rp = match h : List.findIdx? (fun (Y : Sequent) => decide (Y.setEqTo X)) H with | none => ⋯.elim | some k => k

@[irreducible]

noncomputable def buildTree (s : Strategy tableauGame Builder) {H : History} {X : Sequent} {p : ProverPos H X ⊕ BuilderPos H X} (h : winning s ⟨H, ⟨X, p⟩⟩) : BuildTree ⟨H, ⟨X, p⟩⟩

The tree generated from a winning Builder strategy

Equations

• One or more equations did not get rendered due to their size.
• buildTree s h_2 = BuildTree.Leaf rp
• buildTree s h_2 = ⋯.elim

Matches

WORRY: Where in the below is it okay/safe to work with the BuildTree type and where should we insist on the (more specific) buildTree result value?

inductive Match {pos : GamePos} : BuildTree pos → Type

Path inside a BuildTree. Analogous to PathIn for Tableau.

• stop {pos : GamePos} {bt : BuildTree pos} : Match bt
• mov {pos : GamePos} {YS : List GamePos} {Y : GamePos} {mvs : (newPos : GamePos) → newPos ∈ YS → Move pos newPos} {next : (newPos : GamePos) → newPos ∈ YS → BuildTree newPos} (Y_in : Y ∈ YS) (tail : Match (next Y Y_in)) : Match (BuildTree.Step YS mvs next)

def Match.btAt {pos : GamePos} {bt : BuildTree pos} : Match bt → (newPos : GamePos) × BuildTree newPos

Equations

• Match.stop.btAt = ⟨pos, bt⟩
• (Match.mov Y_in tail).btAt = tail.btAt

def Match.append {a✝ : GamePos} {bt : BuildTree a✝} (m1 : Match bt) (m2 : Match m1.btAt.snd) : Match bt

Equations

• Match.stop.append m2 = m2
• (Match.mov Y_in tail).append m2 = Match.mov Y_in (tail.append m2)

structure Match.edge {x✝ : GamePos} {bt : BuildTree x✝} (m n : Match bt) : Type

The parent-child relation ⋖_𝕋 in a Builder strategy tree. Similar to edge but data.

• YS : List GamePos
• next (newPos : GamePos) : newPos ∈ self.YS → BuildTree newPos
• mPos : GamePos
• nPos : GamePos
• nPos_in : self.nPos ∈ self.YS
• mvs (newPos : GamePos) : newPos ∈ self.YS → Move self.mPos newPos
• h : m.btAt = ⟨self.mPos, BuildTree.Step self.YS self.mvs self.next⟩
• def_n : n = m.append (⋯ ▸ mov ⋯ stop)

theorem Match.leaf_no_edge {pos : GamePos} {bt : BuildTree pos} (m : Match bt) (rp : rep m.btAt.fst.fst m.btAt.fst.snd.fst) (h : m.btAt.snd = BuildTree.Leaf rp) (n : Match bt) : ¬Nonempty (m.edge n)

If m ends at a leaf, then it cannot have an edge to any n.

def Match.rewind {a✝ : GamePos} {bt : BuildTree a✝} : Match bt → (k : ℕ) → Match bt

Go back up inside bt by k steps. FIXME: instead of Nat, use Fin like we do in PathIn.rewind.

Equations

• Match.stop.rewind x✝ = Match.stop
• (Match.mov Y_in tail).rewind 0 = Match.mov Y_in tail
• (Match.mov Y_in tail).rewind k.succ = (Match.mov Y_in tail).rewind k

def Match.companionOf {pos mPos : GamePos} {bt : BuildTree pos} (m : Match bt) (rp : rep mPos.fst mPos.snd.fst) : m.btAt = ⟨mPos, BuildTree.Leaf rp⟩ → Match bt

Equations

• m.companionOf rp x✝ = m.rewind (theRep rp)

def Match.companion {a✝ : GamePos} {bt : BuildTree a✝} (m n : Match bt) : Prop

Equations

• m.companion n = ∃ (mPos : GamePos) (rp : rep mPos.fst mPos.snd.fst) (h : m.btAt = ⟨mPos, BuildTree.Leaf rp⟩), n = m.companionOf rp h

Pre-states (Def 6.13)

As possible worlds for the model graph we want to define maximal paths inside the build tree that do not contain (M) steps.

In the paper pre-states are allowed to be of the form π;π' when π ends at a repeat and π' is a maximal prefix of the path from the companion to that repeat. Here we only store the π part of such pre-states, because the π' is then uniquely determined by π.

def Match.edge.isModal {pos : GamePos} {bt : BuildTree pos} {m n : Match bt} : m.edge n → Prop

This edge between matches is a modal step. To even say this we adjusted BuildTree to contain data which rule was used.

Equations

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

def Match.isLeaf {pos : GamePos} {bt : BuildTree pos} {m : Match bt} : Prop

Equations

• Match.isLeaf = ∃ (m_pos : GamePos) (rep : rep m_pos.fst m_pos.snd.fst), m.btAt = ⟨m_pos, BuildTree.Leaf rep⟩

inductive PreStateP {pos : GamePos} (bt : BuildTree pos) (m : Match bt) : Type

A pre-state-part starting at m is any path in bt : BuildTree consisting of non-(M) edges and stopping at a leaf or at an (M) application. (No Match.companion steps here, see note above.)

PROBLEM / QUESTION: do we also need leafs given by empty prMoves???

• edge {pos : GamePos} {bt : BuildTree pos} {m n : Match bt} (e : m.edge n) : ¬e.isModal → PreStateP bt n → PreStateP bt m
• stopLeaf {pos : GamePos} {bt : BuildTree pos} {m : Match bt} : Match.isLeaf → PreStateP bt m
• stopAtM {pos : GamePos} {bt : BuildTree pos} {m n : Match bt} (e : m.edge n) : e.isModal → PreStateP bt m

def BuildTree.allPreStatePs {pos : GamePos} (bt : BuildTree pos) (m : Match bt) : List (PreStateP bt m)

Collect all PreStatePs from a given m onwards.

Equations

• (BuildTree.Leaf rp).allPreStatePs m = [PreStateP.stopLeaf ⋯]
• (BuildTree.Step YS YS_Moves next).allPreStatePs x_2 = sorry

theorem BuildTree.allPreStatePs_spec {pos : GamePos} {bt : BuildTree pos} {m : Match bt} (π : PreStateP bt m) : π ∈ bt.allPreStatePs m

inductive PreState {pos : GamePos} (bt : BuildTree pos) : Type

A pre-state is a maximal pre-state-part, i.e. starting at the root or just after (M).

WORRY: should fromRoot also have a condition about pos being the start of the game?

• fromRoot {pos : GamePos} {bt : BuildTree pos} : PreStateP bt Match.stop → PreState bt
• fromMod {pos : GamePos} {bt : BuildTree pos} {o m : Match bt} (e : o.edge m) : e.isModal → PreStateP bt m → PreState bt

def BuildTree.allPreStates {pos : GamePos} (bt : BuildTree pos) : List (PreState bt)

Collect all PreStates for a given BuildTree.

Equations

• bt.allPreStates = List.map PreState.fromRoot (bt.allPreStatePs Match.stop)

theorem BuildTree.allPreStates_spec {pos : GamePos} {bt : BuildTree pos} (π : PreState bt) : π ∈ bt.allPreStates

def PreState.forms {a✝ : GamePos} {bt : BuildTree a✝} : PreState bt → List Formula

Collect formulas in a pre-state. The non-loaded part of Λ(π) in paper.

TODO: If the pre-state ends in a repeat, also include formulas in the path from companion to (M).

QUESTION: Can we collect loaded formulas here by unloading them? Or would that make the loaded case of PreState.pdlFormCase unsayable?

Equations

• PreState.forms = sorry

def PreState.lforms {a✝ : GamePos} {bt : BuildTree a✝} : PreState bt → List NegLoadFormula

Collect formulas in a pre-state. The loaded part of Λ(π) in paper.

Equations

• PreState.lforms = sorry

def PreState.last {a✝ : GamePos} {bt : BuildTree a✝} : PreState bt → Sequent

Equations

• PreState.last = sorry

theorem PreState.formsCases {a✝ : GamePos} {bt : BuildTree a✝} {φ : Formula} {π : PreState bt} : φ ∈ π.forms → φ.basic = true ∧ φ ∈ π.last ∨ sorry

TODO Lemma 6.14

theorem PreState.pdlFormCase {a✝ : GamePos} {bt : BuildTree a✝} {α : Program} {φ : Formula} {δ : List Program} {π : PreState bt} : ¬α.isAtomic → (~⌈α⌉φ) ∈ π.forms → ∃ Xδ ∈ H α, Xδ.1 ∪ [~⌈⌈δ⌉⌉φ] ⊆ π.forms

WIP Lemma 6.15 (unloaded case only)

theorem PreState.locConsSatBas {a✝ : GamePos} {bt : BuildTree a✝} (π : PreState bt) : saturated π.forms.toFinset ∧ locallyConsistent π.forms.toFinset ∧ π.last.basic

WIP Lemma 6.16: pre-states are saturated and locally consistent, their last node is basic.

def BuildTree.toModel {Pos : GamePos} (bt : BuildTree Pos) : (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.

theorem PreState.diamondExistence {a✝ : GamePos} {bt : BuildTree a✝} {α : Program} {φ : AnyFormula} {π : PreState bt} : (~'⌊α⌋φ) ∈ π.lforms → ∃ (t : Match bt), AnyNegFormula.mem_Sequent t.btAt.fst.snd.fst (~''φ) ∧ ∃ (ρ : PreState bt) (u : Match bt), Modelgraphs.Q sorry α ⟨π.forms.toFinset, ⋯⟩ ⟨ρ.forms.toFinset, ⋯⟩

WIP Lemma 6.18

QUESTION: which R can we use here in order to use Modelgraphs.Q?

Model graph of pre-states

theorem strmg (X : Sequent) (s : Strategy tableauGame Builder) (h : winning s (startPos X)) : ∃ (WS : Finset (Finset Formula)) (mg : ModelGraph WS), ∃ Z ∈ WS, X.toFinset ⊆ Z

Theorem 6.21: If Builder has a winning strategy then there is a model graph.