The Tableau Game (Section 6.2 and 6.3) #

(∃ (newPos : ProverPos Hist X ⊕ BuilderPos Hist X), next = ⟨Hist, ⟨X, newPos⟩⟩) ∨ ∃ (Y : Sequent) (newPos : ProverPos (X :: Hist) Y ⊕ BuilderPos (X :: Hist) Y), next = ⟨X :: Hist, ⟨Y, newPos⟩⟩

source

theorem move.hist_suffix {next : GamePos} {Hist : History} {X : Sequent} {pos : ProverPos Hist X ⊕ BuilderPos Hist X} (mov : move next ⟨Hist, ⟨X, pos⟩⟩) :

Hist <:+ next.fst

source

theorem move.trans_hist_suffix {pZ pX : GamePos} (mov : Relation.TransGen move pZ pX) :

pX.fst <:+ pZ.fst

source

theorem move_iff {H : History} {X : Sequent} {p : ProverPos H X ⊕ BuilderPos H X} {next : GamePos} :

move next ⟨H, ⟨X, p⟩⟩ ↔ (∃ (nrep : ¬rep H X) (Xbasic : X.basic), p = Sum.inl (ProverPos.bas nrep Xbasic) ∧ ∃ (L : List Formula) (R : List Formula), X = (L, R, none ) ∧ ((∃ (δs : List Program) (δ : Program) (ψ : Formula), ¬ψ.isBox ∧ (~⌈⌈δs⌉⌉⌈δ⌉ψ) ∈ L ∧ next = ⟨X :: H, ⟨(L.erase (~⌈⌈δs⌉⌉⌈δ⌉ψ), R, some (Sum.inl (~'⌊⌊δs⌋⌋⌊δ⌋AnyFormula.normal ψ))), posOf (X :: H) (L.erase (~⌈⌈δs⌉⌉⌈δ⌉ψ), R, some (Sum.inl (~'⌊⌊δs⌋⌋⌊δ⌋AnyFormula.normal ψ)))⟩⟩) ∨ ∃ (δs : List Program) (δ : Program) (ψ : Formula), ¬ψ.isBox ∧ (~⌈⌈δs⌉⌉⌈δ⌉ψ) ∈ R ∧ next = ⟨X :: H, ⟨(L, R.erase (~⌈⌈δs⌉⌉⌈δ⌉ψ), some (Sum.inr (~'⌊⌊δs⌋⌋⌊δ⌋AnyFormula.normal ψ))), posOf (X :: H) (L, R.erase (~⌈⌈δs⌉⌉⌈δ⌉ψ), some (Sum.inr (~'⌊⌊δs⌋⌋⌊δ⌋AnyFormula.normal ψ)))⟩⟩) ∨ (∃ (a : ℕ) (ξ : AnyFormula), X = (L, R, some (Sum.inl (~'⌊·a⌋ξ))) ∧ ((∃ (φ : Formula), ξ = AnyFormula.normal φ ∧ next = ⟨X :: H, ⟨(~φ :: projection a L, projection a R, none ), posOf (X :: H) (~φ :: projection a L, projection a R, none )⟩⟩) ∨ (∃ (χ : LoadFormula), ξ = AnyFormula.loaded χ ∧ next = ⟨X :: H, ⟨(projection a L, projection a R, some (Sum.inl (~'χ))), posOf (X :: H) (projection a L, projection a R, some (Sum.inl (~'χ)))⟩⟩) ∨ next = ⟨X :: H, ⟨(List.insert (~(⌊·a⌋ξ).unload) L, R, none ), posOf (X :: H) (List.insert (~(⌊·a⌋ξ).unload) L, R, none )⟩⟩)) ∨ ∃ (a : ℕ) (ξ : AnyFormula), X = (L, R, some (Sum.inr (~'⌊·a⌋ξ))) ∧ ((∃ (φ : Formula), ξ = AnyFormula.normal φ ∧ next = ⟨X :: H, ⟨(projection a L, ~φ :: projection a R, none ), posOf (X :: H) (projection a L, ~φ :: projection a R, none )⟩⟩) ∨ (∃ (χ : LoadFormula), ξ = AnyFormula.loaded χ ∧ next = ⟨X :: H, ⟨(projection a L, projection a R, some (Sum.inr (~'χ))), posOf (X :: H) (projection a L, projection a R, some (Sum.inr (~'χ)))⟩⟩) ∨ next = ⟨X :: H, ⟨(L, List.insert (~(⌊·a⌋ξ).unload) R, none ), posOf (X :: H) (L, List.insert (~(⌊·a⌋ξ).unload) R, none )⟩⟩)) ∨ (∃ (nrep : ¬rep H X) (nbas : ¬X.basic), p = Sum.inl (ProverPos.nbas nrep nbas) ∧ ∃ (ltab : LocalTableau X), next = ⟨H, ⟨X, Sum.inr (BuilderPos.ltab nrep nbas ltab)⟩⟩) ∨ ∃ (nrep : ¬rep H X) (nbas : ¬X.basic) (ltab : LocalTableau X), p = Sum.inr (BuilderPos.ltab nrep nbas ltab) ∧ ∃ Y ∈ endNodesOf ltab, next = ⟨X :: H, ⟨Y, posOf (X :: H) Y⟩⟩

source

theorem move_twice_neq {A B C : GamePos} (B_C : move C B) (A_B : move B A) :

A.snd.fst ≠ C.snd.fst

After two moves we must reach a different sequent. Is this useful for termination?

Termination via finite FL closure #

Intuitively, we want to say that each step from (L,R,O) in a tableau to (L',R',O') stays in the FL of (L,R,O). Moreover, each side left/right stays within its own FL closure. This does not mean that L' must be in the FL of L, because the O may also contribute to the left part. This makes Sequent.subseteq_FL tricky to define.

Moreover, we are working with lists (or, by ignoring their order, multisets) and thus staying in the FL closure does not imply that there are only finitely many sequents reachable: by repeating the same formulas the length of the list may increase. To tackle this we want to use that rep is defined with setEqTo that ignores multiplicity, so that even if there are infinitely many different lists and thus sequents in principle reachable, we still cannot have an infinite chain because that would mean we must have a "set-repeat" that is not allowed.

source

def Sequent.multisubseteq_FL (X Y : Sequent) :

Prop

X is a component-wise multisubset of the FL-closure of Y. Implies Sequent.subseteq_FL but not vice versa, as infinitely many multisets yield the same set.

BROKEN - does not take into account X.O and Y.O on both sides. Hopefully we will never need this anyway. Use Sequent.subseteq_FL instead.

Equations

X.multisubseteq_FL Y = (↑X.R < ↑(FLL Y.R) ∧ ↑X.L < ↑(FLL Y.L))

Instances For

source

def Sequent.subseteq_FL (X Y : Sequent) :

Prop

Sequent Y is a component-wise subset of the FL-closure of X. Note that by component we mean left and right (and not L, R, O).

WORRY: Is using Sequent.O.L here a problem because it might not be injective? (Because it calls unload where both ⌊a⌋⌊b⌋p and ⌊a⌋⌈b⌉p become ⌈a⌉⌈b⌉p.)

Equations

X.subseteq_FL Y = (X.L ⊆ FLL (Y.L ++ Y.O.L) ∧ X.O.L ⊆ FLL (Y.L ++ Y.O.L) ∧ X.R ⊆ FLL (Y.R ++ Y.O.R) ∧ X.O.R ⊆ FLL (Y.R ++ Y.O.R))

Instances For

source

@[simp]

theorem Sequent.subseteq_FL_refl (X : Sequent) :

X.subseteq_FL X

source

@[simp]

theorem Sequent.subseteq_FL_trans (X Y Z : Sequent) :

X.subseteq_FL Y → Y.subseteq_FL Z → X.subseteq_FL Z

source

theorem Sequent.subseteq_FL_of_setEq_right {X Y : Sequent} (h : X.setEqTo Y) {Z : Sequent} :

Z.subseteq_FL X → Z.subseteq_FL Y

source

theorem Sequent.subseteq_FL_of_setEq_left {X Y : Sequent} (h : X.setEqTo Y) {Z : Sequent} :

X.subseteq_FL Z → Y.subseteq_FL Z

source

theorem LoadRule.stays_in_FL_left {χ : LoadFormula} {ress : List (List Formula × Option NegLoadFormula)} (lr : LoadRule (~'χ) ress) (Y : List Formula × Option NegLoadFormula) :

Y ∈ ress → Sequent.subseteq_FL (Y.1, ∅, Option.map Sum.inl Y.2) (∅, ∅, some (Sum.inl (~'χ)))

Helper for LocalRule.stays_in_FL

source

theorem LocalRule.stays_in_FL {Lcond Rcond : List Formula} {Ocond : Olf} {B : List Sequent} (rule : LocalRule (Lcond, Rcond, Ocond) B) (Y : Sequent) :

Y ∈ B → Y.subseteq_FL (Lcond, Rcond, Ocond)

Helper for move_inside_FL

source

theorem move_inside_FL {next p : GamePos} :

move next p → next.snd.fst.subseteq_FL p.snd.fst

source

def Sequent.all_subseteq_FL (Y : Sequent) :

List { X : Sequent // X.subseteq_FL Y }

A list of sequents that are all FL-subsequents of the given sequent. The list defined here is not complete because there are infinitely many such other sequents. But the list is exhaustive modulo setEqTo, as will be shown later via the Seqt quotient. Defined using List.instMonad.

Equations

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

Instances For

NOTE

The following do NOT hold / do NOT exist because there are in fact infinitely many FL-subsequents of a given sequent, so the list returned by all_subseteq_FL can never contain all.

def Sequent.all_subseteq_FL_spec (X Y : Sequent) (h : Y.subseteq_FL X) :
    ⟨Y,h⟩ ∈ Sequent.all_subseteq_FL X := sorry

instance Sequent.subseteq_FL_fintype {X : Sequent} :
    Fintype { Y // Sequent.subseteq_FL Y X } := sorry

Hence, we now define the Quotient modulo Sequent.setEqTo within which there are only finitely many FL-subsequents.

TODO move Seqt to Sequent.lean and Sequent.subseteq_FL_congr to FischerLadner.lean later?

source

instance instSetoidSequent :

Setoid Sequent

Equations

instSetoidSequent = { r := Sequent.setEqTo, iseqv := instEquivalenceSequentSetEqTo }

source

@[reducible, inline]

abbrev Seqt :

Type

Yes, it's a pun. A Sequent modulo Sequent.setEqTo.

Equations

Seqt = Quotient instSetoidSequent

Instances For

source

instance instDecidableEqSeqt :

DecidableEq Seqt

Needed to make List.toFinset work for List Seqt. Strange that this is not inferred from instDecidableRelSequentSetEqTo automatically.

Equations

instDecidableEqSeqt = Quotient.decidableEq

source

theorem Sequent.subseteq_FL_congr (a₁ b₁ a₂ b₂ : Sequent) :

a₁ ≈ a₂ → b₁ ≈ b₂ → a₁.subseteq_FL b₁ = a₂.subseteq_FL b₂

Congruence for Sequent.subseteq_FL, used to make Seqt.subseteq_FL well-defined.

source

def Seqt.subseteq_FL (X Y : Seqt) :

Prop

Equations

X.subseteq_FL Y = Quotient.lift₂ Sequent.subseteq_FL Sequent.subseteq_FL_congr X Y

Instances For

source

theorem Seqt.subseteq_FL_of_move {next p : GamePos} (hm : move next p) :

subseteq_FL (Quotient.mk' next.snd.fst) (Quotient.mk' p.snd.fst)

In the quotient the moves keep us inside the FL. UNUSED, delete this?

source

def Sequent.allSeqt_subseteq_FL (X : Sequent) :

Finset Seqt

Equations

X.allSeqt_subseteq_FL = (List.map (fun (x : { X_1 : Sequent // X_1.subseteq_FL X }) => ⟦↑x⟧) X.all_subseteq_FL).toFinset

Instances For

source

theorem Sequent.allSeqt_subseteq_FL_spec (X Y : Sequent) :

⟦Y⟧ ∈ X.allSeqt_subseteq_FL → Y.subseteq_FL X

source

theorem Sequent.allSeqt_subseteq_FL_complete (X Y : Sequent) :

Y.subseteq_FL X → ⟦Y⟧ ∈ X.allSeqt_subseteq_FL

source

theorem Sequent.allSeqt_subseteq_FL_congr (X Y : Sequent) (h : X ≈ Y) :

X.allSeqt_subseteq_FL = Y.allSeqt_subseteq_FL

source

def Seqt.all_subseteq_FL (Xs : Seqt) :

Finset Seqt

Equations

Xs.all_subseteq_FL = Quotient.lift Sequent.allSeqt_subseteq_FL Sequent.allSeqt_subseteq_FL_congr Xs

Instances For

source

theorem Seqt.all_subseteq_FL_spec {Xs Ys : Seqt} (Ys_in : Ys ∈ Xs.all_subseteq_FL) :

Ys.subseteq_FL Xs

source

theorem Seqt.all_subseteq_FL_complete {Xs Ys : Seqt} (Ys_in : Ys.subseteq_FL Xs) :

Ys ∈ Xs.all_subseteq_FL

source

def Seqt.all_subseteq_FL_attached (Xs : Seqt) :

Finset { Ys : Seqt // Ys.subseteq_FL Xs }

Equations

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

Instances For

source

def Seqt.all_subseteq_FL_attached_complete (Xs : Seqt) (x : { Ys : Seqt // Ys.subseteq_FL Xs }) :

x ∈ Xs.all_subseteq_FL_attached

Equations

⋯ = ⋯

Instances For

source

instance Seqt.subseteq_FL_instFintype {Xs : Seqt} :

Fintype { Ys : Seqt // Ys.subseteq_FL Xs }

Equations

Seqt.subseteq_FL_instFintype = { elems := Xs.all_subseteq_FL_attached, complete := ⋯ }

source

theorem Seqt.subseteq_FL_finite {Xs : Seqt} :

Finite { Ys : Seqt // Ys.subseteq_FL Xs }

In the quotient for setEqTo there are only finitely many FL-subsets for a given Seqt. This means "there are only finitely many "sequents modulo setEq" that are subseteq_FL Y.

source

theorem help {α : Type} {f : ℕ → α} {p : α → Prop} (h_p : ∀ (n : ℕ), p (f n)) (h_fin : Finite { x : α // p x }) :

∃ (k1 : ℕ) (k2 : ℕ), k1 ≠ k2 ∧ f k1 = f k2

General helper lemma: If we have an enumeration of infinitely many values, and all of them have a certain property, but we also know that there are only finitely many values with that property, then there must be identical values in the enuemration.

source

theorem move.wf :

WellFounded move

Lemma 6.10, sort of. Because the move relation is wellfounded, all matches must be finite. Note that the paper does not prove this, only says it is similar to the proof that PDL-tableaux are finite, i.e. Lemma 4.10 which uses the Fischer-Ladner closure.

Actual Game Definition #

source

def tableauGame :

Game

The game defined in Section 6.2.

Equations

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

Instances For

source

@[simp]

theorem tableauGame_turn_Prover {Hist : History} {X : Sequent} {lpr : ProverPos Hist X} :

Game.turn ⟨Hist, ⟨X, Sum.inl lpr⟩⟩ = Prover

source

@[simp]

theorem tableauGame_turn_Builder {Hist : History} {X : Sequent} {lpr : BuilderPos Hist X} :

Game.turn ⟨Hist, ⟨X, Sum.inr lpr⟩⟩ = Builder

source

@[simp]

theorem tableauGame_winner_nlpRep_eq_Builder {i : Player} {sI : Strategy tableauGame i} {sJ : Strategy tableauGame (other i)} {Hist : History} {X : Sequent} {h1 : ¬Nonempty (LoadedPathRepeat Hist X)} :

winner sI sJ ⟨Hist, ⟨X, Sum.inl (ProverPos.nlpRep h1)⟩⟩ = Builder

source

@[simp]

theorem tableauGame_winner_lpr_eq_Prover {i : Player} {sI : Strategy tableauGame i} {sJ : Strategy tableauGame (other i)} {Hist : History} {X : Sequent} {lpr : LoadedPathRepeat Hist X} :

winner sI sJ ⟨Hist, ⟨X, Sum.inr (BuilderPos.lpr lpr)⟩⟩ = Prover

From Prover winning strategies to tableau #

source

@[irreducible]

theorem gameP_general (Hist : History) (X : Sequent) (sP : Strategy tableauGame Prover) (pos : ProverPos Hist X ⊕ BuilderPos Hist X) (h : winning sP ⟨Hist, ⟨X, pos⟩⟩) :

Nonempty (Tableau Hist X)

After history Hist, if Prover has a winning strategy then there is a closed tableau. Note: we skip Definition 6.9 (Strategy Tree for Prover) and just use the Strategy type. This is the induction loading for gameP.

source

def startPos (X : Sequent) :

GamePos

The starting position for the given sequent. With an empty history and using posOf to determine the first GamePos.

Equations