From winning strategies to model graphs, part 1: BuildTree and PreState (Section 6.3)

The uniform open local tableau

def UniOpenLT (X : Sequent) : Type

Open local tableaux for X that are the uniform one, i.e. uniLocalTab X. This type has at most one element, and it is inhabited iff uniLocalTab X has an end node.

Equations

• UniOpenLT X = { lt : LocalTableau X // endNodesOf lt ≠ ∅ ∧ lt = uniLocalTab X }

@[instance_reducible]

instance UniOpenLT.instDecidableEq {X : Sequent} : DecidableEq (UniOpenLT X)

Equations

• s.instDecidableEq t = decidable_of_iff (↑s = ↑t) ⋯

def UniOpenLT.all (X : Sequent) : List (UniOpenLT X)

All uniform open local tableaux for X: the singleton list containing uniLocalTab X if that has an end node, and the empty list otherwise. Analogue of OpenLocalTableau.all.

Equations

• UniOpenLT.all X = if h : endNodesOf (uniLocalTab X) ≠ ∅ then [⟨uniLocalTab X, ⋯⟩] else []

theorem UniOpenLT.all_spec {X : Sequent} {ltX : UniOpenLT X} : ltX ∈ all X

Analogue of OpenLocalTableau.all_spec.

theorem UniOpenLT.all_ne_nil_iff {X : Sequent} : all X ≠ [] ↔ endNodesOf (uniLocalTab X) ≠ ∅

Builder Strategy Tree

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) (someLT : UniOpenLT.all X ≠ []) (next : (lt : UniOpenLT X) → BuildChoice H X (endNodesOf ↑lt)) : BuildTree H X

  Prover plays the uniform local tab, we pick an end node (which must exist as otherwise prover wins).

• pdl {H : List Sequent} {X : Sequent} (bas : X.basic) (someR : PdlRule.all X ≠ []) (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} (bas : X.basic) (noRule : PdlRule.all X = []) : BuildTree H X

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

inductive BuildChoice : History → Sequent → Finset Sequent → Type

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

noncomputable def BuildTree.size {H : History} {X : Sequent} : BuildTree H X → ℕ

Manual replacement for sizeOf (bt : BuildTree) so we also count the next parts.

Equations

• (BuildTree.loc nbas someLT next).size = 1 + (List.map (fun (lt : UniOpenLT X) => (next lt).size) (UniOpenLT.all X)).sum
• (BuildTree.pdl bas someR next).size = 1 + (List.map (fun (x : (Y : Sequent) × PdlRule X Y) => match x with | ⟨Y, r⟩ => (next Y r).size) (PdlRule.all X)).sum
• (BuildTree.freeRepeat a).size = 1
• (BuildTree.openLeaf bas noRule).size = 1

noncomputable def BuildChoice.size {H : History} {X : Sequent} {YS : Finset Sequent} : BuildChoice H X YS → ℕ

Equations

• (BuildChoice.pick a bt_Y).size = bt_Y.size

theorem BuildTree.size_lt_loc (H : History) (X : Sequent) (nbas : ¬X.basic) (next : (lt : UniOpenLT X) → BuildChoice H X (endNodesOf ↑lt)) (ltX : UniOpenLT X) (someLT : UniOpenLT.all X ≠ []) : (next ltX).6.size < (loc nbas someLT next).size

theorem BuildTree.size_lt_pdl (H : History) (X : Sequent) (bas : X.basic) (someR : PdlRule.all X ≠ []) (next : (Y : Sequent) → PdlRule X Y → BuildTree (X :: H) Y) (Y : Sequent) (r : PdlRule X Y) : (next Y r).size < (pdl bas someR next).size

@[simp]

theorem BuildChoice.fst_eq {H : History} {X : Sequent} {YS : Finset Sequent} {bc : BuildChoice H X YS} : bc.1 = H

@[simp]

theorem BuildChoice.snd_eq {H : History} {X : Sequent} {YS : Finset Sequent} {bc : BuildChoice H X YS} : bc.2 = X

@[simp]

theorem BuildChoice.thrd_eq {H : History} {X : Sequent} {YS : Finset Sequent} {bc : BuildChoice H X YS} : bc.3 = YS

theorem BuildChoice.frth_mem {H : History} {X : Sequent} {YS : Finset Sequent} {bc : BuildChoice H X YS} : bc.4 ∈ YS

The node picked by Builder is one of the given ones.

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

Equations

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

@[instance_reducible]

instance instDecidableIsFreeRepeat {H : History} {X : Sequent} {bt : BuildTree H X} : Decidable bt.isFreeRepeat

Equations

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

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.

def FreeRepeat.of_rep_free {H : History} {X : Sequent} (rp : rep H X) (free : ¬X.isLoaded) : FreeRepeat H X

Given the proof rep H X and that X is free, find a FreeRepeat value / data.

(Previously here we tried to go from rep H X and ¬Nonempty (LoadedPathRepeat H X) to FreeRepeat which does not work as there might still be loaded non-lpr repeats.)

Equations

• FreeRepeat.of_rep_free rp free = ⟨rp.toFin, ⋯⟩

@[irreducible]

noncomputable 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 BuildTree. 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.freeRepeat (FreeRepeat.of_rep_free ⋯ ⋯)

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} {someLT : UniOpenLT.all X ≠ []} {next : (lt : UniOpenLT X) → BuildChoice H X (endNodesOf ↑lt)} {lt : UniOpenLT X} : Match (next lt).6 → Match (BuildTree.loc nbas someLT next)
• pdl {H : List Sequent} {X : Sequent} {bas : X.basic} {someR : PdlRule.all X ≠ []} {next : (Y : Sequent) → PdlRule X Y → BuildTree (X :: H) Y} {Y : Sequent} {r : PdlRule X Y} : Match (next Y r) → Match (BuildTree.pdl bas someR next)

@[instance_reducible]

instance instDecidableEqMatch {H✝ : History} {X✝ : Sequent} {a✝ : BuildTree H✝ X✝} : DecidableEq (Match a✝)

Equations

• instDecidableEqMatch = instDecidableEqMatch.decEq

def instDecidableEqMatch.decEq {H✝ : History} {X✝ : Sequent} {a✝ : BuildTree H✝ X✝} (x✝ x✝¹ : Match a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqMatch.decEq Match.nil Match.nil = isTrue ⋯
• instDecidableEqMatch.decEq Match.nil a_1.loc = isFalse ⋯
• instDecidableEqMatch.decEq Match.nil a_1.pdl = isFalse ⋯
• instDecidableEqMatch.decEq a_1.loc Match.nil = isFalse ⋯
• instDecidableEqMatch.decEq a_1.pdl Match.nil = isFalse ⋯

@[implicit_reducible]

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 is a combination of a prover and a builder move.

Equations

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

@[implicit_reducible]

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

The sequent reached at the end of a match.

Equations

• m.endSeq = m.btAt.snd.fst

@[irreducible]

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

Equations

• Match.all (BuildTree.loc nbas someLT next) = Match.nil :: do let ltX ← UniOpenLT.all X let __do_lift ← Match.all (next ltX).6 pure __do_lift.loc
• Match.all (BuildTree.pdl bas someR next) = Match.nil :: do let x ← PdlRule.all X match x with | ⟨Y, r⟩ => do let __do_lift ← Match.all (next Y r) pure __do_lift.pdl
• Match.all (BuildTree.freeRepeat a) = [Match.nil]
• Match.all (BuildTree.openLeaf bas noRule) = [Match.nil]

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

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 bas noRule⟩⟩ => True | x => False

@[instance_reducible]

instance instDecidableIsOpenLeaf {a✝ : History} {a✝¹ : Sequent} {bt : BuildTree a✝ a✝¹} {m : Match bt} : Decidable Match.isOpenLeaf

Equations

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

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

@[instance_reducible]

instance instMatchDecidableIsFreeRepeat {H : History} {X : Sequent} {bt : BuildTree H X} {m : Match bt} : Decidable m.isFreeRepeat

Equations

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

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

def Match.getFreeRepeat {X : Sequent} {bt : BuildTree [] X} (m : Match bt) (h : m.isFreeRepeat) : FreeRepeat m.btAt.fst m.btAt.snd.fst

Get the FreeRepeat (rewind-index and same-sequent proof) of a Match.

Equations

• m.getFreeRepeat h = BuildTree.getFreeRepeat ⋯

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

theorem Match.btAt_append {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) (c : Match m.btAt.snd.snd) : (m.append c).btAt = c.btAt

Appending matches: the node reached is the one reached by the second match.

theorem Match.endSeq_append {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) (c : Match m.btAt.snd.snd) : (m.append c).endSeq = c.endSeq

Appending matches: the sequent reached is the one reached by the second match.

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 x_2 = Match.nil
• 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

@[simp]

theorem Match.rewind_zero {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) : m.rewind 0 = m

Rewinding 0 steps does nothing.

theorem Match.rewind_length_lt_length_of_pos {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) (k : Fin (m.length + 1)) (k_pos : 0 < k) : (m.rewind k).length < m.length

Inspired by PathIn.rewind_length_lt_length_of_gt_zero.

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

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. The + 1 is there because the FreeRepeat values are indices of the history starting with 0, but Match.rewind 0 would do nothing. (Same as the .succ in companionOf for PathIn.)

Equations

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

@[implicit_reducible]

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

The sequents visited by a Match, in reverse order and not including the last one. Analogous to PathIn.toHistory.

Equations

• Match.nil.toHistory = []
• tail.loc.toHistory = tail.toHistory ++ [X]
• tail.pdl.toHistory = tail.toHistory ++ [X]

@[simp]

theorem Match.toHistory_length {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) : List.length m.toHistory = m.length

theorem Match.toHistory_append_eq_btAt_fst {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) : m.toHistory ++ H = m.btAt.fst

The history reached by a Match consists of the sequents visited, then the old history.

@[simp]

theorem Match.rewind_last {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) : m.rewind (Fin.last m.length) = nil

theorem Match.btAt_rewind_eq_toHistory_get {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) (k : Fin (m.length + 1)) : (m.rewind k).btAt.snd.fst = (m.btAt.snd.fst :: m.toHistory).get (Fin.cast ⋯ k)

Rewinding a Match by k steps gives the k-th element of the history, where the end sequent of the match itself is counted as the 0-th element. Inspired by PathIn.nodeAt_rewind_eq_toHistory_get.

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

theorem Match.companionOf_setEqTo_sequent {a✝ : Sequent} {bt : BuildTree [] a✝} (m : Match bt) (h : m.isFreeRepeat) : (m.companionOf h).btAt.snd.fst = m.btAt.snd.fst

The sequent at the companion is the same as the sequent at the repeat. Similar to nodeAt_companionOf_setEq.

theorem Match.companionOf_length_lt {X : Sequent} {bt : BuildTree [] X} (m : Match bt) (h : m.isFreeRepeat) : (m.companionOf h).length < m.length

Going to the companion of a free repeat gives a strictly shorter Match.

Collecting Sequents for Pre-states

As possible worlds for the model graph we want to define maximal paths inside the build tree that do not contain (M), (L+) or (L-) steps.

We collect the sequents along such paths directly by induction on the BuildTree.

@[irreducible]

def BuildTree.collect {H : History} {X : Sequent} (bt : BuildTree H X) : Finset (List Sequent)

Collect pre-states in the whole BuildTree. The local pre-states come from paths in a local tableau, and PDL pre-states each consist of just a single node.

Equations

• (BuildTree.loc nbas someLT next).collect = (UniOpenLT.all X).toFinset.sup fun (lt : UniOpenLT X) => (↑lt).pathsTo (next lt).4 ∪ (next lt).6.collect
• (BuildTree.pdl bas someR next).collect = {[X]} ∪ (PdlRule.all X).toFinset.sup fun (x : (Y : Sequent) × PdlRule X Y) => match x with | ⟨Y, r⟩ => (next Y r).collect
• (BuildTree.freeRepeat a).collect = ∅
• (BuildTree.openLeaf bas noRule).collect = {[X]}

The following four simp lemmas describe membership in BuildTree.collect. They are the Finset replacements of the old list-based unfolding of collect.

@[simp]

theorem BuildTree.mem_collect_loc {H : History} {X : Sequent} {nbas : ¬X.basic} {someLT : UniOpenLT.all X ≠ []} {next : (lt : UniOpenLT X) → BuildChoice H X (endNodesOf ↑lt)} {p : List Sequent} : p ∈ (loc nbas someLT next).collect ↔ ∃ lt ∈ UniOpenLT.all X, p ∈ (↑lt).pathsTo (next lt).4 ∨ p ∈ (next lt).6.collect

@[simp]

theorem BuildTree.mem_collect_pdl {H : List Sequent} {X : Sequent} {bas : X.basic} {someR : PdlRule.all X ≠ []} {next : (Y : Sequent) → PdlRule X Y → BuildTree (X :: H) Y} {p : List Sequent} : p ∈ (pdl bas someR next).collect ↔ p = [X] ∨ ∃ (Y : Sequent) (r : PdlRule X Y), ⟨Y, r⟩ ∈ PdlRule.all X ∧ p ∈ (next Y r).collect

@[simp]

theorem BuildTree.mem_collect_freeRepeat {H : History} {X : Sequent} {fr : FreeRepeat H X} {p : List Sequent} : p ∈ (freeRepeat fr).collect ↔ False

@[simp]

theorem BuildTree.mem_collect_openLeaf {H : History} {X : Sequent} {bas : X.basic} {noRule : PdlRule.all X = []} {p : List Sequent} : p ∈ (openLeaf bas noRule).collect ↔ p = [X]

theorem BuildTree.collect_contains_root_of_not_freeRepeat {H : History} {X : Sequent} (bt : BuildTree H X) (h : ¬bt.isFreeRepeat) : ∃ π ∈ bt.collect, X ∈ π

Any BuildTree that is not a free repeat collects at least one list containing its root. Generalisation of BuildTree.collect_contains_root to non-empty histories.

theorem BuildTree.not_isFreeRepeat_nil {X : Sequent} (bt : BuildTree [] X) : ¬bt.isFreeRepeat

theorem BuildTree.collect_contains_root {X : Sequent} (bt : BuildTree [] X) : ∃ π ∈ bt.collect, X ∈ π

theorem BuildTree.collect_nonempty {X : Sequent} (bt : BuildTree [] X) : bt.collect ≠ ∅

Pre-states (Def 6.13)

def PreState {H : History} {X : Sequent} (bt : BuildTree H X) : Type

A pre-state is a list of sequents collected from a BuildTree.

Equations

• PreState bt = ↥bt.collect

theorem PreState.nonempty {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} : ↑π ≠ []

Collecting Formulas in Pre-state Sequents

def PreState.wForms {H : History} {X : Sequent} {bt : BuildTree H X} (π : PreState bt) : Finset WhateverFormula

Λ(π) gets all formulas for a pre-state but keep the information what is loaded. Returns the WhateverFormula type so that lemmas like 6.15 and 6.18 are sayable.

Equations

• π.wForms = pathWForms ↑π

def PreState.forms {H : History} {X : Sequent} {bt : BuildTree H X} (π : PreState bt) : Finset Formula

Λ⁻(π) gets all formulas from a pre-state π, via unloading if needed.

Equations

• π.forms = pathForms ↑π

@[simp]

theorem PreState.mem_wForms {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {f : WhateverFormula} : f ∈ π.wForms ↔ ∃ Z ∈ ↑π, f ∈ Z.wForms

@[simp]

theorem PreState.mem_forms {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {f : Formula} : f ∈ π.forms ↔ ∃ Z ∈ ↑π, f ∈ Z.toFinset

theorem PreState.mem_forms_iff {H : History} {X : Sequent} {bt : BuildTree H X} {φ : Formula} {π : PreState bt} : φ ∈ π.forms ↔ WhateverFormula.any (AnyFormula.normal φ) ∈ π.wForms ∨ (∃ (χ : LoadFormula), χ.unload = φ ∧ WhateverFormula.any (AnyFormula.loaded χ) ∈ π.wForms) ∨ ∃ (ψ : NegLoadFormula), negUnload ψ = φ ∧ WhateverFormula.negLoad ψ ∈ π.wForms

Characterizing three different ways in which a formula can be in PreState.forms.

theorem BuildTree.exists_mem_attach_forms_eq {H : Sequent} {bt : BuildTree [] H} {ρ : PreState bt} : ∃ a ∈ bt.collect.attach, PreState.forms a = ρ.forms

theorem PreState.forms_saturated {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} : saturated π.forms

theorem PreState.forms_locallyConsistent {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} : locallyConsistent π.forms

theorem PreState.forms_last_basic {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} : ((↑π).getLast ⋯).basic

PreStates to Matches and back again

To prove the existence lemmas we first make some helper definitions and lemmas that allow us to switch between PreStates & Matches.

theorem Match.collect_btAt_subset {H : History} {X : Sequent} {bt : BuildTree H X} (m : Match bt) (π : List Sequent) : π ∈ m.btAt.snd.snd.collect → π ∈ bt.collect

The result of BuildTree.collect in any sub-BuildTree reached by a Match is also part of BuildTree.collect applied to the bigger BuildTree.

theorem Match.existsPreState {X : Sequent} {bt : BuildTree [] X} (m : Match bt) : ∃ (π : PreState bt), ∃ Z ∈ ↑π, m.btAt.snd.fst = Z

For any Match there exists a PreState containing the sequent at the end of the Match.

def Match.fitsPreState {X : Sequent} {bt : BuildTree [] X} (m : Match bt) (π : List Sequent) : Bool

The Boolean predicate used by Match.toPreState: does the given list of sequents contain the sequent at the end of the given Match?

Equations

• m.fitsPreState π = π.any fun (Z : Sequent) => decide (m.btAt.snd.fst = Z)

theorem Match.fitsPreState_iff {X : Sequent} {bt : BuildTree [] X} {m : Match bt} {π : List Sequent} : m.fitsPreState π = true ↔ ∃ Z ∈ π, m.btAt.snd.fst = Z

theorem Match.exists_fitsPreState {X : Sequent} {bt : BuildTree [] X} (m : Match bt) : ∃ π ∈ bt.collect.toList, m.fitsPreState π = true

Reformulation of Match.existsPreState using Match.fitsPreState. Note that we use Finset.toList here to be able to use List.find? below.

theorem Match.find?_fitsPreState_isSome {X : Sequent} {bt : BuildTree [] X} (m : Match bt) : (List.find? m.fitsPreState bt.collect.toList).isSome = true

Thanks to Match.existsPreState the search for a fitting pre-state succeeds.

noncomputable def Match.toPreState {X : Sequent} {bt : BuildTree [] X} (m : Match bt) : PreState bt

Pick a PreState for a given Match, using Match.existsPreState and List.find?. Noncomputable because Finset.toList is.

Equations

• m.toPreState = ⟨(List.find? m.fitsPreState bt.collect.toList).get ⋯, ⋯⟩

theorem Match.toPreState_spec {X : Sequent} {bt : BuildTree [] X} (m : Match bt) : ∃ Z ∈ ↑m.toPreState, m.btAt.snd.fst = Z

The result of Match.toPreState indeed contains the sequent at the end of the Match.

@[irreducible]

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

Search for the node in bt at which the list p of sequents is collected, and return the Match leading to that node. Auxiliary function for PreState.toMatch, defined for all lists p of sequents. If p is not collected anywhere, then we return Match.nil as a dummy value.

Equations

• One or more equations did not get rendered due to their size.
• (BuildTree.freeRepeat a).toMatchAux x✝ = Match.nil
• (BuildTree.openLeaf bas noRule).toMatchAux x✝ = Match.nil

theorem BuildTree.toMatchAux_mem_collect {H : History} {X : Sequent} (bt : BuildTree H X) (p : List Sequent) : p ∈ bt.collect → p ∈ (bt.toMatchAux p).btAt.snd.snd.collect

A collected list of sequents is still collected in the sub-BuildTree found for it.

theorem BuildTree.toMatchAux_head? {H : History} {X : Sequent} (bt : BuildTree H X) (p : List Sequent) : p ∈ bt.collect → p.head? = some (bt.toMatchAux p).btAt.snd.fst

A collected list of sequents starts with the sequent of the node where it is collected.

def PreState.toMatch {H : History} {X : Sequent} {bt : BuildTree H X} (π : PreState bt) : Match bt

Every pre-state comes from a Match: this is the Match that leads to the node of the BuildTree at which the pre-state π was collected. (Defined for any history, not only for H = [].)

Equations

• π.toMatch = bt.toMatchAux ↑π

theorem PreState.toMatch_mem_collect {H : History} {X : Sequent} {bt : BuildTree H X} (π : PreState bt) : ↑π ∈ π.toMatch.btAt.snd.snd.collect

Specification of PreState.toMatch, part one: the pre-state is collected already in the sub-BuildTree reached by the match.

theorem PreState.toMatch_head {H : History} {X : Sequent} {bt : BuildTree H X} (π : PreState bt) : (↑π).head ⋯ = π.toMatch.btAt.snd.fst

Specification of PreState.toMatch, part two: the pre-state starts with the sequent at the node reached by the match.

theorem PreState.toMatch_endSeq {H : History} {X : Sequent} {bt : BuildTree H X} (π : PreState bt) : π.toMatch.endSeq = (↑π).head ⋯

Specification of PreState.toMatch, part three: the sequent at the node reached by the match is the head of the pre-state. (Reformulation of PreState.toMatch_head.)

theorem PreState.exists_match_endSeq_eq_last {H : History} {X : Sequent} {bt : BuildTree H X} (π : PreState bt) : ∃ (m : Match bt), m.endSeq = (↑π).getLast ⋯

Not only the first sequent of a pre-state is reached by a Match (this is PreState.toMatch), also the last sequent of a pre-state is reached by some Match.

theorem PreState.exists_endMatch {H : History} {X : Sequent} {bt : BuildTree H X} (π : PreState bt) : ∃ (c : Match π.toMatch.btAt.snd.snd), π.toMatch.endSeq = (↑π).head ⋯ ∧ (π.toMatch.append c).endSeq = (↑π).getLast ⋯

Both ends of a pre-state are reached by matches, and the match reaching the last sequent extends the one reaching the first sequent: the continuation c is a Match inside the sub-BuildTree at which π was collected, and appending it to π.toMatch gives a Match in the whole tree that ends at the last sequent of π.

theorem PreState.setEqTo_mem_toMatch_toPreState {X : Sequent} {bt : BuildTree [] X} (π : PreState bt) : ∃ Z ∈ ↑π.toMatch.toPreState, (↑π).head ⋯ = Z

Weak round-trip that always holds: going from a pre-state to a match and back gives a pre-state that contains the first sequent of π.

theorem PreState.toMatch_toPreState {X : Sequent} {bt : BuildTree [] X} (π : PreState bt) (uniq : ∀ ρ ∈ bt.collect, (∃ Z ∈ ρ, (↑π).head ⋯ = Z) → ρ = ↑π) : π.toMatch.toPreState = π

Round-trip: under the assumption that π is the only collected list that contains a sequent set-equal to the sequent at the node where π is collected, going to the match and back gives π again.

theorem PreState.toMatch_toPreState_openLeaf {X : Sequent} (bas : X.basic) (noRule : PdlRule.all X = []) (π : PreState (BuildTree.openLeaf bas noRule)) : π.toMatch.toPreState = π

Example where the uniq assumption of PreState.toMatch_toPreState is satisfied: an open leaf collects only one pre-state, so there the round-trip does hold.

Properties of Formula (Sets? Lists?) obtained from Pre-States

theorem PreState.mem_bothSides_getLast_of_basic {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {φ : Formula} (φ_basic : φ.basic = true) (φ_in : φ ∈ π.forms) : φ ∈ ((↑π).getLast ⋯).toFinset

Every basic formula of a pre-state already occurs in the last (basic) sequent of that pre-state. Note that bothSides is used here, so this also covers formulas from the loaded part of a sequent.

theorem PreState.formsCases {a✝ : History} {a✝¹ : Sequent} {bt : BuildTree a✝ a✝¹} {φ : Formula} {π : PreState bt} (φ_in : φ ∈ π.forms) : φ.basic = true ∧ φ ∈ ((↑π).getLast ⋯).toFinset ∨ ¬φ.basic = true

Lemma 6.14, weakened version. The original statement says that φ is principal in a rule applied later on. We do not have the rule applications available along a pre-state, so instead we make the case distinction on whether φ is basic, and give the actual content for the first case: any basic formula of a pre-state occurs already in its last sequent. (We also use Sequent.toFinset instead of ∈ to include the loaded formula.)

Lemma 6.15 free case.

The helper lemmas needed for it are in Pdl/Sequent.lean, Pdl/LocalRules.lean and Pdl/LocalTableauPaths.lean.

theorem PreState.freeUnfoldDiaMem_of_nonAtom {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {α : Program} {φ : Formula} : ¬α.isAtomic → (WhateverFormula.any ∘ AnyFormula.normal) (~⌈α⌉φ) ∈ π.wForms → ∃ Xδ ∈ Dset α, ((Xδ.1 ∪ [~⌈⌈Xδ.2⌉⌉φ]).all fun (x : Formula) => decide ((WhateverFormula.any ∘ AnyFormula.normal) x ∈ π.wForms)) = true

Lemma 6.15 free case. (Generalised from bt : BuildTree [] X to an arbitrary history H, as needed for the recursion into sub-BuildTrees.)

Lemma 6.15 loaded cases.

The helper lemmas needed for these are in Pdl/Sequent.lean, Pdl/LocalRules.lean and Pdl/LocalTableauPaths.lean.

theorem PreState.loadUnfoldMem_of_nonAtom {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {α : Program} {ξ : AnyFormula} : ¬α.isAtomic → WhateverFormula.negLoad (~'⌊α⌋ξ) ∈ π.wForms → ∃ (ress : Finset (Finset Formula × Option NegLoadFormula)), Nonempty (LoadRule (~'⌊α⌋ξ) ress) ∧ ∃ Fo ∈ ress, ((Fo.1.sort fun (a b : Formula) => a ≤ b).all fun (f : Formula) => decide ((WhateverFormula.any ∘ AnyFormula.normal) f ∈ π.wForms)) = true ∧ (Fo.2.toList.all fun (nl : NegLoadFormula) => decide (WhateverFormula.negLoad nl ∈ π.wForms)) = true

Generic version of the loaded case of Lemma 6.15: a non-atomic loaded diamond in a pre-state must have been unfolded by a LoadRule somewhere in the pre-state. The two versions below are the special cases for AnyFormula.loaded and AnyFormula.normal. (Generalised from bt : BuildTree [] X to an arbitrary history H, as needed for the recursion into sub-BuildTrees.)

theorem PreState.loadUnfoldDiaMem_of_nonAtom {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {α : Program} (χ : LoadFormula) : ¬α.isAtomic → WhateverFormula.negLoad (~'⌊α⌋AnyFormula.loaded χ) ∈ π.wForms → ∃ Xδ ∈ Dset α, (Xδ.1.all fun (x : Formula) => decide ((WhateverFormula.any ∘ AnyFormula.normal) x ∈ π.wForms)) = true ∧ ((YsetLoad Xδ χ).2.toList.all fun (x : NegLoadFormula) => decide (WhateverFormula.negLoad x ∈ π.wForms)) = true

Lemma 6.15 loaded case with more than one loaded box

theorem PreState.loadUnfoldDiaMem_of_nonAtom' {H : History} {X : Sequent} {bt : BuildTree H X} {π : PreState bt} {α : Program} {φ : Formula} : ¬α.isAtomic → WhateverFormula.negLoad (~'⌊α⌋AnyFormula.normal φ) ∈ π.wForms → ∃ Xδ ∈ Dset α, (Xδ.1.all fun (x : Formula) => decide ((WhateverFormula.any ∘ AnyFormula.normal) x ∈ π.wForms)) = true ∧ ((YsetLoad' Xδ φ).2.toList.all fun (x : NegLoadFormula) => decide (WhateverFormula.negLoad x ∈ π.wForms)) = true

Lemma 6.15 loaded case with only one loaded box.

theorem PreState.locConsSatBas {X : Sequent} {bt : BuildTree [] X} (π : PreState bt) : saturated π.forms ∧ locallyConsistent π.forms ∧ ((↑π).getLast ⋯).basic

Lemma 6.16: pre-states are saturated and locally consistent, their last node is basic.