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: i.e. we need to keep track of which rule is used.
• Maybe we also need to carry proofs in here?

• Leaf {pos : GamePos} (rp : rep pos.fst pos.snd.fst) : BuildTree pos
• Step {pos : GamePos} (YS : List GamePos) (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]

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
• move {pos : GamePos} {YS : List GamePos} {Y : GamePos} {next : (newPos : GamePos) → newPos ∈ YS → BuildTree newPos} (Y_in : Y ∈ YS) (tail : Match (next Y Y_in)) : Match (BuildTree.Step YS next)

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

Equations

• Match.stop.btAt = ⟨pos, bt⟩
• (Match.move 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.move Y_in tail).append m2 = Match.move Y_in (tail.append m2)

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

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

Equations

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

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.move Y_in tail).rewind 0 = Match.move Y_in tail
• (Match.move Y_in tail).rewind k.succ = (Match.move 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.not_mod {a✝ : GamePos} {bt : BuildTree a✝} {m n : Match bt} : m.edge n → Prop

How to say that this is not a modal step?

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⟩

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

This match ends just before an (M) application.

Equations

• Match.isJustBeforeM = sorry

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

This match ends at the result of an (M) application.

Equations

• Match.isResultOfM = sorry

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

A pre-state-part is any path in a BuildTree consisting of non-(M) edges and ending at a leaf or just before an (M) application. (There are 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.not_mod → 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 : Match bt} : Match.isJustBeforeM → PreStateP bt 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).

• fromRoot {pos : GamePos} {bt : BuildTree pos} : PreStateP bt Match.stop → PreState bt
• fromMod {pos : GamePos} {bt : BuildTree pos} {m : Match bt} : Match.isResultOfM → PreStateP bt m → PreState bt

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

Equations

• PreState.all bt = sorry

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

Collect formulas in a pre-state.

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

Equations

• PreState.forms = sorry

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

Equations

• PreState.last = sorry

theorem PreState.locConsSatBas {a✝ : GamePos} {bt : BuildTree a✝} (π : PreState bt) : saturated π.forms.toFinset ∧ locallyConsistent π.forms.toFinset ∧ π.last.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.

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.