The Tableau Game (Section 6.2) #

prPdl {X Y : Sequent} {Hist : History} {nrep : ¬flprep Hist X} {Xbasic : X.basic} : 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 : ¬flprep 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 : ¬flprep 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

def Move.isModal {pos newPos : GamePos} :

Move pos newPos → Prop

Equations

Instances For

source

def move (old new : GamePos) :

Prop

Equations

move old new = Nonempty (Move old new)

Instances For

source

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

move ⟨H, ⟨X, p⟩⟩ next → ¬(rep H X ∧ X.isFree = true)

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.frep a)⟩⟩ = ∅
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 : ¬flprep 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 : ¬flprep 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 : ¬flprep 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 {H : History} {X : Sequent} {pos : ProverPos H X ⊕ BuilderPos H X} (h : rep H X ∧ X.isFree = true) :

theMoves ⟨H, ⟨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 use the Seqt (which is the quotient from Sequent.setEqTo) within which there are only finitely many FL-subsequents.

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 but nice to have.

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 exist_duplicates_of_infinite_among_fintype {α : Type} {f : ℕ → α} {p : α → Prop} (h_p : ∀ (n : ℕ), p (f n)) (h_fin : Finite { x : α // p x }) :

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

Helper lemma for matchesFinite: If we have enumerate 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 enumeration.

Infinite chains of moves #

Towards matchesFinite we here collect facts about an infinite chain g : ℕ → GamePos with move (g n) (g (n+1)) for all n, following the proof idea for the matchesFinite lemma:

at each position of the chain a move is possible, hence there is no forbidden repeat, i.e. ¬ flprep (see moveChain_not_flprep);
all sequents along the chain stay inside the FL closure of the first one (see moveChain_inside_FL), of which there are only finitely many modulo setEqTo (see Seqt.subseteq_FL_finite);
the history at a later position contains the sequents of all earlier positions (see moveChain_hist_accum and moveChain_hist_split);
hence a sequent that is setEqTo an earlier one must be loaded, because a free repeat would have ended the match (see moveChain_setEq_isLoaded), and thus from some point onwards all sequents in the chain are loaded (see moveChain_eventually_loaded);
a repeat in this loaded part gives a loaded-path repeat, which also ends the match (see moveChain_hist_index and moveChain_multisetEq_absurd).

This section is from aristotle.harmonic.fun

source

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

move ⟨H, ⟨X, p⟩⟩ next → ¬flprep H X

If a move from ⟨H, X, p⟩ is possible, then X is neither a free repeat nor a loaded-path repeat in H. Note this is stronger than move_then_no_frep.

source

theorem exists_spread_subsequence {P : ℕ → Prop} (hS : ∀ (N : ℕ), ∃ (n : ℕ), N ≤ n ∧ P n) :

∃ (e : ℕ → ℕ), (∀ (k : ℕ), P (e k)) ∧ ∀ (k1 k2 : ℕ), k1 < k2 → e k1 + 2 ≤ e k2

Helper lemma for matchesFinite: if a property of natural numbers holds arbitrarily late, then we can enumerate witnesses for it with gaps of at least two.

source

theorem moveChain_not_flprep {g : ℕ → GamePos} (g_rel : ∀ (n : ℕ), move (g n) (g (n + 1))) (n : ℕ) :

¬flprep (g n).fst (g n).snd.fst

Because a move is possible, no position in the chain is a forbidden repeat.

source

theorem moveChain_hist_step {g : ℕ → GamePos} (g_rel : ∀ (n : ℕ), move (g n) (g (n + 1))) (n : ℕ) :

(g (n + 1)).fst = (g n).fst ∧ (g (n + 1)).snd.fst = (g n).snd.fst ∨ (g (n + 1)).fst = (g n).snd.fst :: (g n).fst

One step in the chain either keeps history and sequent (the prLocTab case) or adds the current sequent to the history.

source

theorem moveChain_hist_accum {g : ℕ → GamePos} (g_rel : ∀ (n : ℕ), move (g n) (g (n + 1))) (m n : ℕ) :

m ≤ n → ∃ (pre : List Sequent), (g n).fst = pre ++ (g m).fst ∧ ∀ Y ∈ pre, ∃ (j : ℕ), m ≤ j ∧ j < n ∧ Y = (g j).snd.fst

The history only grows, and everything added to it are sequents from the chain.

source

theorem moveChain_hist_split {g : ℕ → GamePos} (g_rel : ∀ (n : ℕ), move (g n) (g (n + 1))) {m n : ℕ} (h : m + 2 ≤ n) :

∃ (pre : List Sequent), (g n).fst = pre ++ (g m).snd.fst :: (g m).fst ∧ ∀ Y ∈ pre, ∃ (j : ℕ), m < j ∧ j < n ∧ Y = (g j).snd.fst

After at least two moves the sequent of the earlier position is in the later history, and all newer entries of that history are sequents from strictly in between.

source

theorem moveChain_inside_FL {g : ℕ → GamePos} (g_rel : ∀ (n : ℕ), move (g n) (g (n + 1))) (n : ℕ) :

Seqt.subseteq_FL ⟦(g n).snd.fst⟧ ⟦(g 0).snd.fst⟧

All sequents in the chain stay inside the FL closure of the first sequent.

source

theorem moveChain_setEq_isLoaded {g : ℕ → GamePos} (g_rel : ∀ (n : ℕ), move (g n) (g (n + 1))) {m n : ℕ} (h : m + 2 ≤ n) (hs : (g m).snd.fst.setEqTo (g n).snd.fst) :

(g n).snd.fst.isLoaded = true

A sequent in the chain that is setEqTo an earlier one must be loaded, because otherwise we would have a free repeat and the match would have ended.

source

theorem moveChain_exists_setEq_late {g : ℕ → GamePos} (g_rel : ∀ (n : ℕ), move (g n) (g (n + 1))) (N : ℕ) :

∃ (m : ℕ) (n : ℕ), N ≤ m ∧ m + 2 ≤ n ∧ (g m).snd.fst.setEqTo (g n).snd.fst

Because there are only finitely many sequents modulo setEqTo inside the FL closure, arbitrarily late in the chain we find two positions with setEqTo sequents.

source

theorem moveChain_eventually_loaded {g : ℕ → GamePos} (g_rel : ∀ (n : ℕ), move (g n) (g (n + 1))) :

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → (g n).snd.fst.isLoaded = true

From some point onwards all sequents in the chain are loaded: there are only finitely many sequents modulo setEqTo, and free ones can never come back.

source

theorem moveChain_hist_index {g : ℕ → GamePos} (g_rel : ∀ (n : ℕ), move (g n) (g (n + 1))) {N m n : ℕ} (hN : ∀ (j : ℕ), N ≤ j → (g j).snd.fst.isLoaded = true) (hm : N ≤ m) (h : m + 2 ≤ n) :

∃ (k : Fin (List.length (g n).fst)), List.get (g n).fst k = (g m).snd.fst ∧ ∀ i ≤ k, (List.get (g n).fst i).isLoaded = true

If all sequents from N onwards are loaded and N ≤ m with m + 2 ≤ n, then the sequent of position m occurs in the history of position n at an index such that all entries up to and including that index are loaded. This is what is needed for a loaded-path repeat.

source

theorem moveChain_setEq_absurd {g : ℕ → GamePos} (g_rel : ∀ (n : ℕ), move (g n) (g (n + 1))) {N m n : ℕ} (hN : ∀ (j : ℕ), N ≤ j → (g j).snd.fst.isLoaded = true) (hm : N ≤ m) (h : m + 2 ≤ n) (hs : (g m).snd.fst.setEqTo (g n).snd.fst) :

False

A setEqTo repeat in the loaded part of the chain is impossible: it would be a loaded-path repeat, at which the match ends.

source

theorem matchesFinite :

WellFounded (Function.swap move)

Lemma 6.11. The move relation is converse wellfounded (and thus all matches must be finite). This is similar to the proof that PDL-tableaux are finite (Lemma 4.10), relying on the finiteness of the Fischer-Ladner closure. In Lean we never needed to say 4.10 because values of the inductive type Tableau are always finite by constriction. But we do need a proof here, as this lemma is about move, not Match.

The whole argument is done in the MoveChain section above.

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

instance instDecidableEqPos :

DecidableEq Game.Pos

This helps to pick up the derived instance DecidableEq GamePos above.

Equations

instDecidableEqPos = id instDecidableEqOfLawfulBEq

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} {h : rep Hist X ∧ X.isFree = true} :

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