From winning strategies to model graphs (Section 6.3)

Lessons learned while working on this file:

• Not all leafs in the BuildTree are backpointers. We want open leafs (where builder wins the game) to actually build worlds :-) Moreover, free repeats also let builder win.

BuildTree

def FreeRepeat (Hist : History) (X : Sequent) : Type

A free repeat is a non-loaded sequent that occured before.

Equations

• FreeRepeat Hist X = { k : Fin (List.length Hist) // (List.get Hist k).multisetEqTo X ∧ ¬X.isLoaded = true }

inductive BuildTree : History → Sequent → Type

Winning Strategy Tree for Builder. At each step, we consider

• ALL rules R that prover may choose, followed immediately by
• ONE of the children then chosen by Builder

The type is actually similar to Tableau, as it also uses a history, but it does allow open leaves. For choosing a local tableau end node the mutual RuleChoice is needed to avoid the error "nested inductive datatypes parameters cannot contain local variables". Instead of the .lpr constructor here we have .fpr because we only make a RuleTree when Builder wins and thus we can never reach an lpr where Prover would win, but do allow free repeats. As in Tableau note that the history is stored in reverse.

• loc {H : History} {X : Sequent} (nbas : ¬X.basic) (next : (lt : LocalTableau X) → BuildChoice H X (endNodesOf lt)) : BuildTree H X

  Prover chooses local tab, we pick one end node.

• pdl {H : List Sequent} {X : Sequent} (bas : X.basic) (next : (Y : Sequent) → PdlRule X Y → BuildTree (X :: H) Y) : BuildTree H X

  Prover chooses PDL rule, never branches, so continue with unique child.

• freeRepeat {H : History} {X : Sequent} : FreeRepeat H X → BuildTree H X

  Free repeat means builder wins.

• openLeaf {H : History} {X : Sequent} : BuildTree H X

  Leaf that is (might be?!) not a repeat, but no rules can be applied.

inductive BuildChoice : History → Sequent → List Sequent → Type

• pick {H : List Sequent} {X : Sequent} {YS : List Sequent} {Y : Sequent} : Y ∈ YS → BuildTree (X :: H) Y → BuildChoice H X YS

@[simp]

theorem BuildChoice.fst_eq_H {H : History} {X : Sequent} {YS : List Sequent} {bc : BuildChoice H X YS} : bc.1 = H

@[irreducible]

def buildTree (s : Strategy tableauGame Builder) {H : History} {X : Sequent} {p : ProverPos H X} (h : winning s ⟨H, ⟨X, Sum.inl p⟩⟩) : BuildTree H X

Given a winning Builder strategy, compute its RuleTree. NEW: note the Sum.inl p here. This ensure we start tree building from a Prover position, i.e.

• not allowing BuilderPos.lpr here (easy, was forbidden already anyway as prover wins there.)
• not allowing BuilderPos.ltab because we cannot use BuildTree.loc for a single fixed local tab.

Equations

• One or more equations did not get rendered due to their size.
• buildTree s h_2 = BuildTree.openLeaf

Matches

inductive Match {H : History} {X : Sequent} : BuildTree H X → Type

A match is a path inside a BuildTree. Analogous to PathIn for Tableau. In Game Theory this could be called a "rollout", but note that it stays within the given Builder strategy tree and it is not tracking all intermediate game positions.

• nil {H : History} {X : Sequent} {bt : BuildTree H X} : Match bt
• loc {H : History} {X : Sequent} {nbas : ¬X.basic} {next : (lt : LocalTableau X) → BuildChoice H X (endNodesOf lt)} {lt : LocalTableau X} : Match (next lt).6 → Match (BuildTree.loc nbas next)
• pdl {H : List Sequent} {X : Sequent} {bas : X.basic} {next : (Y : Sequent) → PdlRule X Y → BuildTree (X :: H) Y} {Y : Sequent} {r : PdlRule X Y} : Match (next Y r) → Match (BuildTree.pdl bas next)

@[irreducible]

def Match.all {H : History} {X : Sequent} (bt : BuildTree H X) : List (Match bt)

Equations

• One or more equations did not get rendered due to their size.
• Match.all (BuildTree.loc nbas next) = do let ltX ← LocalTableau.all X let __do_lift ← Match.all (next ltX).6 pure __do_lift.loc
• Match.all (BuildTree.freeRepeat fr) = [Match.nil]
• Match.all BuildTree.openLeaf = [Match.nil]

theorem Match.all_spec {H : History} {X : Sequent} (bt : BuildTree H X) (m : Match bt) : m ∈ all bt

def Match.length {H : History} {X : Sequent} {bt : BuildTree H X} : Match bt → ℕ

Inspired by PathIn.length. Counting the steps made by a Match in a BuildTree. Note that such a step may be combinations of a prover and a builder move.

Equations

• Match.nil.length = 0
• tail.loc.length = tail.length + 1
• tail.pdl.length = tail.length + 1

def Match.btAt {H : History} {X : Sequent} {bt : BuildTree H X} : Match bt → (H' : History) × (Y : Sequent) × BuildTree H' Y

Equations

• Match.nil.btAt = ⟨H, ⟨X, bt⟩⟩
• tail.loc.btAt = tail.btAt
• tail.pdl.btAt = tail.btAt

def Match.append {H : History} {X : Sequent} {bt : BuildTree H X} (m1 : Match bt) (m2 : Match m1.btAt.snd.snd) : Match bt

Equations

• Match.nil.append m2 = m2
• tail.loc.append m2 = (tail.append m2).loc
• tail.pdl.append m2 = (tail.append m2).pdl

structure Match.locEdge {x✝ : History} {x✝¹ : Sequent} {bt : BuildTree x✝ x✝¹} (m n : Match bt) : Type

• H : History
• mY : Sequent
• nbas : ¬self.mY.basic
• next (lt : LocalTableau self.mY) : BuildChoice self.H self.mY (endNodesOf lt)
• lt : LocalTableau self.mY
• btAt_m_def : m.btAt = ⟨self.H, ⟨self.mY, BuildTree.loc ⋯ self.next⟩⟩
• btAt_n_def : n.btAt = ⟨(self.next self.lt).2 :: (self.next self.lt).1, ⟨(self.next self.lt).4, (self.next self.lt).6⟩⟩

structure Match.pdlEdge {x✝ : History} {x✝¹ : Sequent} {bt : BuildTree x✝ x✝¹} (m n : Match bt) : Type

• H : History
• mX : Sequent
• nY : Sequent
• bas : self.mX.basic
• next (Y : Sequent) (_r : PdlRule self.mX Y) : BuildTree (self.mX :: self.H) Y
• r : PdlRule self.mX self.nY
• btAt_m_def : m.btAt = ⟨self.H, ⟨self.mX, BuildTree.pdl ⋯ self.next⟩⟩
• btAt_n_def : n.btAt = ⟨self.mX :: self.H, ⟨self.nY, self.next self.nY self.r⟩⟩

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

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

Equations

• m.Edge n = (m.locEdge n ⊕ m.pdlEdge n)

def Match.Edge.isModal {H : History} {X : Sequent} {bt : BuildTree H X} {m n : Match bt} : m.Edge n → Prop

This edge between matches is a modal step. To even say this BuildTree must contain the rule data.

Equations

• Match.Edge.isModal (Sum.inl val) = False
• Match.Edge.isModal (Sum.inr { H := H_1, mX := mX, nY := nY, bas := bas, next := next, r := r, btAt_m_def := btAt_m_def, btAt_n_def := btAt_n_def }) = r.isModal

def Match.isOpenLeaf {H : History} {X : Sequent} {bt : BuildTree H X} {m : Match bt} : Prop

Equations

• Match.isOpenLeaf = match m.btAt with | ⟨fst, ⟨fst_1, BuildTree.openLeaf⟩⟩ => True | x => False

def Match.isFreeRepeat {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) : Prop

Equations

• m.isFreeRepeat = match m.btAt with | ⟨fst, ⟨fst_1, BuildTree.freeRepeat a⟩⟩ => True | x => False

theorem Match.isOpenLeaf_no_edge {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) (h : isOpenLeaf) (n : Match bt) : ¬Nonempty (m.Edge n)

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

def Match.rewind {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) (k : Fin (m.length + 1)) : Match bt

Rewind a Match, i.e. go back up inside bt by k steps. The + 1 is there because going back 0 steps does nothing.

Equations

• Match.nil.rewind ⟨0, ⋯⟩ = Match.nil
• Match.nil.rewind ⟨k.succ, k_h⟩ = ⋯.elim
• tail.loc.rewind k = Fin.lastCases Match.nil (Match.loc ∘ tail.rewind) k
• tail.pdl.rewind k = Fin.lastCases Match.nil (Match.pdl ∘ tail.rewind) k

def BuildTree.isFreeRepeat {H : History} {X : Sequent} : BuildTree H X → Prop

Equations

• (BuildTree.freeRepeat a).isFreeRepeat = True
• x✝.isFreeRepeat = False

def BuildTree.getFreeRepeat {H : History} {X : Sequent} {bt : BuildTree H X} (h : bt.isFreeRepeat) : FreeRepeat H X

Equations

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

@[irreducible]

theorem Match.btAt_newHist_length_eq_length_plus_oldHist {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) : List.length m.btAt.fst = m.length + List.length H

theorem Match.isFreeRepeat_iff {H : History} {X : Sequent} {bt : BuildTree H X} {m : Match bt} : m.isFreeRepeat ↔ m.btAt.snd.snd.isFreeRepeat

def Match.companionOf {X : Sequent} {bt : BuildTree [] X} (m : Match bt) (h : m.isFreeRepeat) : Match bt

Roll back to the companion. Only possibe if we started with H=[] so we know the root.

Equations

• m.companionOf h = match BuildTree.getFreeRepeat ⋯ with | ⟨⟨k, k_lt⟩, same_and_free⟩ => m.rewind ⟨k, ⋯⟩

def Match.companion {X : Sequent} {bt : BuildTree [] X} (m n : Match bt) : Prop

The repeat ♥ companion relation on Match.

Equations

• m.companion n = ∃ (h : m.isFreeRepeat), 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 in PreState and PreStateP we only store the π part of such pre-states, because the π' is then uniquely determined by π.

inductive PreStatePart {H : History} {X : Sequent} (bt : BuildTree H X) (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.)

• edge {H : History} {X : Sequent} {bt : BuildTree H X} {m n : Match bt} (e : m.Edge n) : ¬e.isModal → PreStatePart bt n → PreStatePart bt m
• stopAtM {H : History} {X : Sequent} {bt : BuildTree H X} {m n : Match bt} (e : m.Edge n) : e.isModal → PreStatePart bt m
• stopAtOpenLeaf {H : History} {X : Sequent} {bt : BuildTree H X} {m : Match bt} : Match.isOpenLeaf → PreStatePart bt m
• stopAtFreeRepeat {H : History} {X : Sequent} {bt : BuildTree H X} {m : Match bt} : m.isFreeRepeat → PreStatePart bt m

def BuildTree.allPreStateParts {H : History} {X0 : Sequent} (bt : BuildTree H X0) (m : Match bt) : List (PreStatePart bt m)

Collect all PreStatePs from a given m onwards.

Equations

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

theorem BuildTree.allPreStateParts_spec {H : History} {X : Sequent} {bt : BuildTree H X} {m : Match bt} (π : PreStatePart bt m) : π ∈ bt.allPreStateParts m

inductive PreState {H : History} {X : Sequent} (bt : BuildTree H X) : 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 H being empty, i.e. the start of the game?

• fromRoot {H : History} {X : Sequent} {bt : BuildTree H X} : PreStatePart bt Match.nil → PreState bt
• fromMod {H : History} {X : Sequent} {bt : BuildTree H X} {o m : Match bt} (e : o.Edge m) : e.isModal → PreStatePart bt m → PreState bt

def BuildTree.allPreStates {H : History} {X : Sequent} (bt : BuildTree H X) : List (PreState bt)

Collect all PreStates for a given BuildTree.

Equations

• bt.allPreStates = sorry

theorem BuildTree.allPreStates_spec {H : History} {X : Sequent} {bt : BuildTree H X} (π : PreState bt) : π ∈ bt.allPreStates

def PreState.forms {a✝ : History} {a✝¹ : Sequent} {bt : BuildTree a✝ 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✝ : History} {a✝¹ : Sequent} {bt : BuildTree a✝ 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✝ : History} {a✝¹ : Sequent} {bt : BuildTree a✝ a✝¹} : PreState bt → Sequent

Equations

• PreState.last = sorry

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

TODO Lemma 6.14

theorem PreState.pdlFormCase {a✝ : History} {a✝¹ : Sequent} {bt : BuildTree a✝ 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✝ : History} {a✝¹ : Sequent} {bt : BuildTree a✝ 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 {H : History} {X : Sequent} (bt : BuildTree H X) : (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✝ : History} {a✝¹ : Sequent} {bt : BuildTree a✝ a✝¹} {α : Program} {φ : AnyFormula} {π : PreState bt} : (~'⌊α⌋φ) ∈ π.lforms → ∃ (t : Match bt), AnyNegFormula.mem_Sequent t.btAt.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. Uses BuildTree.toModel.