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

Match

Here we define paths inside a BuildTree, similar to PathIn for Tableau.

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

Inspired by PathIn

• 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 → ℕ → Match bt

Equations

• Match.rewind = sorry

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

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

Equations

• m.cEdge n = (m.edge n ∨ m.companion n)

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 will probably only store the π part of such pre-states, because the π' is uniquely determined by π then.

def Match.edge.not_mod {a✝ : GamePos} {a✝¹ : BuildTree a✝} {m n : Match a✝¹} : m.edge n → Prop

How to say that this is not a modal step?

Equations

• Match.edge.not_mod = sorry

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

A pre-state-part is a path in a BuildTree starting at a Match, going along any non-(M) edge or companion steps and ending at a leaf or just before an (M) application.

• edge {Pos : GamePos} {bt : BuildTree Pos} {m n : Match bt} (e : m.edge n) : e.not_mod → PreStateP bt n → PreStateP bt m
• companion {Pos : GamePos} {bt : BuildTree Pos} {m n : Match bt} : m.companion n → PreStateP bt n → PreStateP bt m
• stop {Pos : GamePos} {bt : BuildTree Pos} {m : Match bt} : false = true → PreStateP bt m

inductive PreState {Pos : GamePos} (bt : BuildTree Pos) (m : Match bt) : Type

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

def PreState.all {Pos : GamePos} (bt : BuildTree Pos) : List ((m : Match bt) × PreState bt m)

Equations

• PreState.all bt = sorry

def PreState.forms {a✝ : GamePos} {bt : BuildTree a✝} {m : Match bt} : PreState bt m → 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✝} {n : Match bt} : PreState bt n → Sequent

Equations

• PreState.last = sorry

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

def BuildTree.toModel {Pos : GamePos} (bt : BuildTree Pos) : (W : Finset (Finset Formula)) × KripkeModel { x : Finset Formula // x ∈ 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), X.toFinset ∈ WS

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