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.length {pos : GamePos} {bt : BuildTree pos} : Match bt → ℕ

Inspired by PathIn.length. Note that this counts all steps, even the prLocTab ones where pos.1 does not get longer.

Equations

• Match.nil.length = 0
• tail.bu.length = tail.length + 1
• (Match.pr newPos mov tail).length = tail.length + 1

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.

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.toHistory {pos : GamePos} {bt : BuildTree pos} (m : Match bt) : History

Convert a Match to a History. Inspired by PathIn.toHistory. Does not include the last node. The history of .nil is [] because this will not go into pos.1.

Equations

• Match.nil.toHistory = []
• tail.bu.toHistory = tail.toHistory ++ [pos.snd.fst]
• (Match.pr newPos mov tail).toHistory = tail.toHistory ++ [pos.snd.fst]

def Match.rewind {a✝ : GamePos} {bt : BuildTree a✝} (m : Match bt) (k : Fin (m.length + 1)) : Match bt

Rewind a Match, i.e. go back up inside bt by k steps. This used to use Nat but now we take a Fin like in PathIn.rewind, and for that we needed to define Match.length first. IDEA: also use Match.toHistory here?

Equations

• Match.nil.rewind x_2 = Match.nil
• tail.bu.rewind k = Fin.lastCases Match.nil (Match.bu ∘ tail.rewind) k
• (Match.pr newPos mov tail).rewind k = Fin.lastCases Match.nil (Match.pr newPos mov ∘ tail.rewind) k

def rep.toFin {H : History} {X : Sequent} (rp : rep H X) : Fin (List.length H)

Given a rep H X, determine the index of the companion in H using List.findIdx?. Note that we do not care about loading here.

Equations

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

theorem Move.fst_length_succ {newPos : GamePos} {H : History} {X : Sequent} {p : ProverPos H X ⊕ BuilderPos H X} (mov : Move ⟨H, ⟨X, p⟩⟩ newPos) : Game.turn ⟨H, ⟨X, p⟩⟩ = Builder → List.length newPos.fst = List.length H + 1

The extra condition that it is the turn of Builder is needed because otherwise the prLocTab case would falsify.

theorem Match.btAt_fst_fst_length_eq_length {pos : GamePos} {bt : BuildTree pos} {m : Match bt} : List.length m.btAt.fst.fst = m.length + List.length pos.fst

This is NOT TRUE, because history only records different steps and will not count Move.prLocTab steps, though these are steps in the Match.

WAIT, but Match.toHistory DOES count all steps, so the length statement here should be true. ??

?? are we sure about this one ?? Note that the history from pos needs to be added on the right side.

?? Or better restrict pos to be a starting position of the game!?!? (Analogous to how many things in TableauPath are only the Hist = [] case.)

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

Equations

• m.companionOf h = sorry

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

The repeat ♥ companion relation on Match.

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.