From winning strategies to model graphs (Section 6.3)

Lessons learned while working on this file:

• Are actually all leafs in the BuildTree backpointers? No, we also want all other leafs where builder wins the game to actually build some model :-)

BuildTree

inductive BuildTree : GamePos → Type

Winning Strategy Tree for Builder. At a BuStep it is the turn of Builder and we have a single child for the Move they make. At a PrStep it is the turn of Prover, and we have children for all possible Move.

In the paper "a leaf is either labeled with a sequent to which no rule is applicable, or it is a (free) repeat". Here we make leafs with PrStep because at such a position it is the turn of Prover but there are no moves so Prover loses.

GOAL: The BuildTree type should carry all information we need, so later we should not care about how a specific strategy tree for builder gets made/computer, but just that there is one.

• BuStep {pos : Game.Pos} {newPos : GamePos} (hturn : Game.turn pos = Builder) (m : Move pos newPos) (next : BuildTree newPos) : BuildTree pos
• PrStep {pos : Game.Pos} (hturn : Game.turn pos = Prover) (next : (newPos : GamePos) → Move pos newPos → BuildTree newPos) : BuildTree pos

def BuildTree.isLeaf {pos : GamePos} : BuildTree pos → Prop

Equations

• (BuildTree.BuStep hturn m next).isLeaf = (false = true)
• (BuildTree.PrStep hturn next).isLeaf = (theMoves pos = ∅)

def BuildTree.isFreeRepLeaf {pos : GamePos} : BuildTree pos → Prop

Equations

• (BuildTree.BuStep hturn m next).isFreeRepLeaf = (false = true)
• (BuildTree.PrStep hturn_4 next_4).isFreeRepLeaf = True
• (BuildTree.PrStep hturn_4 next_4).isFreeRepLeaf = False
• (BuildTree.PrStep hturn_4 next_4).isFreeRepLeaf = False
• (BuildTree.PrStep hturn_3 next_3).isFreeRepLeaf = ⋯.elim

theorem BuildTree.rep_of_isFreeRepLeaf {pos : GamePos} {bt : BuildTree pos} : bt.isFreeRepLeaf → rep pos.fst pos.snd.fst

@[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⟩⟩

Given a winning Builder strategy, compute its BuildTree.

Equations

• One or more equations did not get rendered due to their size.
• buildTree s h_2 = BuildTree.PrStep ⋯ fun (newPos : GamePos) (mov : Move ⟨H, ⟨X, Sum.inl (ProverPos.bas nrep bas)⟩⟩ newPos) => buildTree s ⋯
• buildTree s h_2 = BuildTree.PrStep ⋯ fun (newPos : GamePos) (mov : Move ⟨H, ⟨X, Sum.inl (ProverPos.nbas nrep nbas)⟩⟩ newPos) => buildTree s ⋯
• buildTree s h_2 = ⋯.elim

Matches

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

Path inside a BuildTree. Analogous to PathIn for Tableau.

• nil {pos : GamePos} {bt : BuildTree pos} : Match bt
• bu {pos : Game.Pos} {x✝ : GamePos} {next : BuildTree x✝} {hturn : Game.turn pos = Builder} {m : Move pos x✝} : Match next → Match (BuildTree.BuStep hturn m next)
• pr {pos : GamePos} {next : (newPos : GamePos) → Move pos newPos → BuildTree newPos} {hturn : Game.turn pos = Prover} (newPos : GamePos) (mov : Move pos newPos) : Match (next newPos mov) → Match (BuildTree.PrStep hturn next)

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

Equations

• Match.nil.btAt = ⟨pos, bt⟩
• tail.bu.btAt = tail.btAt
• (Match.pr newPos mov tail).btAt = tail.btAt

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

Equations

• Match.nil.append m2 = m2
• tail.bu.append m2 = (tail.append m2).bu
• (Match.pr newPos mov tail).append m2 = Match.pr newPos mov (tail.append m2)

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

• mPos : GamePos
• hturn : Game.turn self.mPos = Builder
• mov : Move self.mPos n.btAt.fst
• h : m.btAt = ⟨self.mPos, BuildTree.BuStep ⋯ self.mov n.btAt.snd⟩

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

• mPos : GamePos
• hturn : Game.turn self.mPos = Prover
• mov : Move self.mPos n.btAt.fst
• next (newPos : GamePos) (_m : Move self.mPos newPos) : BuildTree newPos
• btAt_m_def : m.btAt = ⟨self.mPos, BuildTree.PrStep ⋯ self.next⟩
• next_n_def {n_in : Move self.mPos n.btAt.fst} : self.next n.btAt.fst n_in = n.btAt.snd

def Match.Edge {a✝ : GamePos} {bt : BuildTree a✝} (m n : Match bt) : Type

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

Equations

• m.Edge n = (m.BuEdge n ⊕ m.PrEdge n)

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 BuildTree must contain Move and thus rule data.

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.btAt.snd.isLeaf

theorem Match.isLeaf_no_edge {pos : GamePos} {bt : BuildTree pos} (m : Match bt) (h : isLeaf) (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. TODO: to correctly do this, replace Nat with a Fin like we do in PathIn.rewind. For that we need Match.length and maybe Match.toHistory first.

Equations

• Match.nil.rewind x✝ = Match.nil
• a.bu.rewind 0 = sorry
• (Match.pr newPos mov a).rewind 0 = sorry
• a.bu.rewind k.succ = sorry
• (Match.pr newPos mov a).rewind k.succ = sorry

def Match.companionOf {pos : GamePos} {bt : BuildTree pos} (m : Match bt) (h : m.btAt.snd.isFreeRepLeaf) : Match bt

Equations

• m.companionOf h = m.rewind (theRep ⋯)

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

Equations

• m.companion n = ∃ (h : m.btAt.snd.isFreeRepLeaf), n = m.companionOf 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 π.

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.PrStep hturn next).allPreStatePs m = sorry
• (BuildTree.BuStep hturn mov 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.nil → 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.nil)

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.