The Tableau Game (Section 6.2) #

prPdl {X Y : Sequent} {Hist : History} {nrep : ¬rep Hist X} {Xbasic : X.basic} : ∀ (a : PdlRule X Y), move ⟨Hist, ⟨X, Sum.inl (ProverPos.bas nrep Xbasic)⟩⟩ ⟨X :: Hist, ⟨Y, posOf (X :: Hist) Y⟩⟩
When the sequent is basic and no repeat, let prover apply a PDL rule.
prLocTab {Hist : History} {X : Sequent} {nrep : ¬rep Hist X} {nbas : ¬X.basic} {ltab : LocalTableau X} : move ⟨Hist, ⟨X, Sum.inl (ProverPos.nbas nrep nbas)⟩⟩ ⟨Hist, ⟨X, Sum.inr (BuilderPos.ltab nrep nbas ltab)⟩⟩
If not basic, let prover pick any ltab : LocalTableau X as new position.
buEnd {X : Sequent} {ltab : LocalTableau X} {Y : Sequent} {Hist : History} {nrep : ¬rep Hist X} {nbas : ¬X.basic} : Y ∈ endNodesOf ltab → move ⟨Hist, ⟨X, Sum.inr (BuilderPos.ltab nrep nbas ltab)⟩⟩ ⟨X :: Hist, ⟨Y, posOf (X :: Hist) Y⟩⟩
Let Builder pick an end node of ltab

Instances For

source

theorem move_then_no_rep {Hist : History} {X : Sequent} {next : GamePos} {p : ProverPos Hist X ⊕ BuilderPos Hist X} :

move ⟨Hist, ⟨X, p⟩⟩ next → ¬rep Hist X

source

def theMoves :

GamePos → Finset GamePos

The finite set of moves, given as a function instead of a relation. With move_of_mem_theMoves and mem_theMoves_of_move this agrees with move.

Equations

One or more equations did not get rendered due to their size.
theMoves ⟨H, ⟨X, Sum.inl (ProverPos.nlpRep a a_1)⟩⟩ = ∅
theMoves ⟨H, ⟨(L, R, some (Sum.inl (~'⌊α;'β⌋χ))), Sum.inl (ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
theMoves ⟨H, ⟨(L, R, some (Sum.inl (~'⌊?'τ⌋χ))), Sum.inl (ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
theMoves ⟨H, ⟨(L, R, some (Sum.inl (~'⌊α⋓β⌋χ))), Sum.inl (ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
theMoves ⟨H, ⟨(L, R, some (Sum.inl (~'⌊∗α⌋χ))), Sum.inl (ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
theMoves ⟨H, ⟨(L, R, some (Sum.inr (~'⌊α;'β⌋χ))), Sum.inl (ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
theMoves ⟨H, ⟨(L, R, some (Sum.inr (~'⌊?'τ⌋χ))), Sum.inl (ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
theMoves ⟨H, ⟨(L, R, some (Sum.inr (~'⌊α⋓β⌋χ))), Sum.inl (ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
theMoves ⟨H, ⟨(L, R, some (Sum.inr (~'⌊∗α⌋χ))), Sum.inl (ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
theMoves ⟨H, ⟨X, Sum.inl (ProverPos.nbas nrep nbas)⟩⟩ = Finset.image (fun (ltab : LocalTableau X) => ⟨H, ⟨X, Sum.inr (BuilderPos.ltab nrep nbas ltab)⟩⟩) Fintype.elems
theMoves ⟨H, ⟨X, Sum.inr (BuilderPos.lpr lpr)⟩⟩ = ∅
theMoves ⟨H, ⟨X, Sum.inr (BuilderPos.ltab a a_1 ltab)⟩⟩ = (List.map (fun (Y : Sequent) => ⟨X :: H, ⟨Y, posOf (X :: H) Y⟩⟩) (endNodesOf ltab)).toFinset

Instances For

source

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

next ∈ theMoves ⟨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⟩⟩

Characterization of theMoves.

source

theorem no_moves_of_rep {Hist : History} {X : Sequent} {pos : ProverPos Hist X ⊕ BuilderPos Hist X} (h : rep Hist X) :

theMoves ⟨Hist, ⟨X, pos⟩⟩ = ∅

source

theorem move_of_mem_theMoves {pos next : GamePos} :

next ∈ theMoves pos → move pos next

The finite set given by theMoves indeed agrees with the relation move. Other direction is mem_theMoves_of_move.

source

theorem mem_theMoves_of_move {pos next : GamePos} :

move pos next → next ∈ theMoves pos

source

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

(∃ (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 {Hist : History} {X : Sequent} {pos : ProverPos Hist X ⊕ BuilderPos Hist X} {next : GamePos} (mov : move ⟨Hist, ⟨X, pos⟩⟩ next) :

Hist <:+ next.fst

source

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

pX.fst <:+ pZ.fst

source

theorem move.trans_hist {pX pY : GamePos} (movt : Relation.TransGen move pX pY) :

pX.fst = pY.fst ∧ pX.snd.fst = pY.snd.fst ∨ pX.snd.fst :: pX.fst <:+ pY.fst

Along the transitive closure of move either the history stays the same or the old sequent and history form a prefix of the new history (where "prefix" is actually "suffix" because the history has the newest element first).

Lemmas about double moves #

source

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

List.length A.fst < List.length C.fst

After two moves the history must grow.

source

@[reducible, inline]

abbrev movemove (a c : GamePos) :

Prop

Insert obligatory "We like to move it move it" joke here.

Equations

movemove = Relation.Comp move move

Instances For

source

theorem movemove.hist {A B C : GamePos} (A_B : move A B) (B_C : move B C) :

A.snd.fst :: A.fst <:+ C.fst

source

theorem movemove_trans_hist {A B : GamePos} (A_B : Relation.TransGen movemove A B) :

A.snd.fst :: A.fst <:+ B.fst

After any number of double moves the history gets extended.

Termination via finite FL closure #

See also StayingInFL.lean whereSequent.subseteq_FL is defined.

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

theorem move_inside_FL {p next : GamePos} (mov : move p next) :

next.snd.fst.subseteq_FL p.snd.fst

source

def Formula.allNegLoads :

Formula → List NegLoadFormula

Given ~⌈α₁⌉…⌈αₙ⌉φ, return the list of ~⌊α₁⌋…⌊αₖ⌋⌈αₖ₊₁⌉…⌈αₙ⌉φ for all k.

Equations

One or more equations did not get rendered due to their size.
x✝.allNegLoads = []

Instances For

source

theorem Formula.allNegLoads_spec {nχ : NegLoadFormula} {φ : Formula} :

nχ ∈ φ.allNegLoads → negUnload nχ = φ

source

theorem Formula.allNegLoads_complete {nχ : NegLoadFormula} {φ : Formula} :

negUnload nχ = φ → nχ ∈ φ.allNegLoads

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_complete (X Y : Sequent) (h : Y.subseteq_FL X) :
    ⟨Y,h⟩ ∈ Sequent.all_subseteq_FL X := ...

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

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 {p next : GamePos} (hm : move p next) :

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 exists_mem_sublists_toFinsetEq_of_Subset {α : Type u_1} [DecidableEq α] {A B : List α} :

A ⊆ B → ∃ C ∈ B.sublists, C.toFinset = A.toFinset

Small helper function. Mathlib this?

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 matchesFinite :

WellFounded (Function.swap move)

Lemma 6.10. The move relation is converse wellfounded (and thus 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 : rep Hist X} {h2 : ¬Nonempty (LoadedPathRepeat Hist X)} :

winner sI sJ ⟨Hist, ⟨X, Sum.inl (ProverPos.nlpRep h1 h2)⟩⟩ = 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