The Tableau Game (Section 6.2)

Different from the paper proof, here we directly set up the tableau game such that we also get a uniform tableau: Prover is not free to choose any local tableau: at a non-basic sequent X the only move available is the one to the canonical local tableau uniLocalTab X defined in Pdl.Interpolation.Uniformity. The gain is in gameP_general: a winning strategy for Prover yields a tableau with the property Tableau.IsUni (and hence Tableau.isUniform for the empty history) because at every loc step the canonical local tableau is used.

Prover and Builder positions

def termProver : Lean.ParserDescr

Equations

• termProver = Lean.ParserDescr.node `termProver 1024 (Lean.ParserDescr.symbol "Prover")

def termBuilder : Lean.ParserDescr

Equations

• termBuilder = Lean.ParserDescr.node `termBuilder 1024 (Lean.ParserDescr.symbol "Builder")

inductive ProverPos (H : History) (X : Sequent) : Type

Prover should make a move.

• frep {H : History} {X : Sequent} : rep H X ∧ X.isFree → ProverPos H X
• bas {H : History} {X : Sequent} : ¬flprep H X → X.basic → ProverPos H X
• nbas {H : History} {X : Sequent} : ¬flprep H X → ¬X.basic → ProverPos H X

@[instance_reducible]

instance instDecidableEqProverPos {H✝ : History} {X✝ : Sequent} : DecidableEq (ProverPos H✝ X✝)

Equations

• instDecidableEqProverPos = instDecidableEqProverPos.decEq

def instDecidableEqProverPos.decEq {H✝ : History} {X✝ : Sequent} (x✝ x✝¹ : ProverPos H✝ X✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqProverPos.decEq (ProverPos.frep a) (ProverPos.frep b) = ⋯ ▸ isTrue ⋯
• instDecidableEqProverPos.decEq (ProverPos.frep a) (ProverPos.bas a_1 a_2) = isFalse ⋯
• instDecidableEqProverPos.decEq (ProverPos.frep a) (ProverPos.nbas a_1 a_2) = isFalse ⋯
• instDecidableEqProverPos.decEq (ProverPos.bas a a_1) (ProverPos.frep a_2) = isFalse ⋯
• instDecidableEqProverPos.decEq (ProverPos.bas a a_1) (ProverPos.bas b b_1) = ⋯ ▸ have h := ⋯; h ▸ isTrue ⋯
• instDecidableEqProverPos.decEq (ProverPos.bas a a_1) (ProverPos.nbas a_2 a_3) = isFalse ⋯
• instDecidableEqProverPos.decEq (ProverPos.nbas a a_1) (ProverPos.frep a_2) = isFalse ⋯
• instDecidableEqProverPos.decEq (ProverPos.nbas a a_1) (ProverPos.bas a_2 a_3) = isFalse ⋯
• instDecidableEqProverPos.decEq (ProverPos.nbas a a_1) (ProverPos.nbas b b_1) = ⋯ ▸ have h := ⋯; h ▸ isTrue ⋯

inductive BuilderPos (H : History) (X : Sequent) : Type

Builder should make a move.

• lpr {H : History} {X : Sequent} : LoadedPathRepeat H X → BuilderPos H X
• ltab {H : History} {X : Sequent} : ¬flprep H X → ¬X.basic → LocalTableau X → BuilderPos H X

@[instance_reducible]

instance instDecidableEqBuilderPos {H✝ : History} {X✝ : Sequent} : DecidableEq (BuilderPos H✝ X✝)

Equations

• instDecidableEqBuilderPos = instDecidableEqBuilderPos.decEq

def instDecidableEqBuilderPos.decEq {H✝ : History} {X✝ : Sequent} (x✝ x✝¹ : BuilderPos H✝ X✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqBuilderPos.decEq (BuilderPos.lpr a) (BuilderPos.lpr b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqBuilderPos.decEq (BuilderPos.lpr a) (BuilderPos.ltab a_1 a_2 a_3) = isFalse ⋯
• instDecidableEqBuilderPos.decEq (BuilderPos.ltab a a_1 a_2) (BuilderPos.lpr a_3) = isFalse ⋯
• instDecidableEqBuilderPos.decEq (BuilderPos.ltab a a_1 a_2) (BuilderPos.ltab b b_1 b_2) = ⋯ ▸ have h := ⋯; h ▸ if h : a_2 = b_2 then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

def GamePos : Type

Game position where either Prover (isLeft) or Builder (isRight) should make a move.

Equations

• GamePos = ((H : History) × (X : Sequent) × (ProverPos H X ⊕ BuilderPos H X))

@[instance_reducible]

instance instDecidableEqGamePos : DecidableEq GamePos

Equations

• instDecidableEqGamePos = instDecidableEqGamePos._aux_1

def posOf (H : History) (X : Sequent) : ProverPos H X ⊕ BuilderPos H X

If we reach this sequent, what is the next game position? Includes winning positions.

Equations

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

theorem posOf_eq_inr_then_lpr {H : History} {X : Sequent} {p : BuilderPos H X} : posOf H X = Sum.inr p → ∃ (lpr : LoadedPathRepeat H X), p = BuilderPos.lpr lpr

Moves

inductive Move (old new : GamePos) : Type

The relation Move old next says that we can move from old to next. There are three kinds of moves.

Note that in the prLocTab move Prover has no choice: the local tableau must be the canonical uniform one, uniLocalTab X.

• 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} : Move ⟨Hist, ⟨X, Sum.inl (ProverPos.nbas nrep nbas)⟩⟩ ⟨Hist, ⟨X, Sum.inr (BuilderPos.ltab nrep nbas (uniLocalTab X))⟩⟩

  If not basic, Prover must move to the uniform local tableau uniLocalTab X.

• 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

def Move.isModal {pos newPos : GamePos} : Move pos newPos → Prop

Equations

• (Move.prPdl r).isModal = r.isModal
• Move.prLocTab.isModal = False
• (Move.buEnd a).isModal = False

def move (old new : GamePos) : Prop

Equations

• move old new = Nonempty (Move old new)

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)

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)⟩⟩ = {⟨H, ⟨X, Sum.inr (BuilderPos.ltab nrep nbas (uniLocalTab X))⟩⟩}
• theMoves ⟨H, ⟨X, Sum.inr (BuilderPos.lpr lpr)⟩⟩ = ∅
• theMoves ⟨H, ⟨X, Sum.inr (BuilderPos.ltab a a_1 ltab)⟩⟩ = Finset.image (fun (Y : Sequent) => ⟨X :: H, ⟨Y, posOf (X :: H) Y⟩⟩) (endNodesOf ltab)

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 : Finset Formula) (R : Finset 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, ⟨({~φ} ∪ Finset.projection a L, Finset.projection a R, none), posOf (X :: H) ({~φ} ∪ Finset.projection a L, Finset.projection a R, none)⟩⟩) ∨ (∃ (χ : LoadFormula), ξ = AnyFormula.loaded χ ∧ next = ⟨X :: H, ⟨(Finset.projection a L, Finset.projection a R, some (Sum.inl (~'χ))), posOf (X :: H) (Finset.projection a L, Finset.projection a R, some (Sum.inl (~'χ)))⟩⟩) ∨ next = ⟨X :: H, ⟨(L ∪ {~(⌊·a⌋ξ).unload}, R, none), posOf (X :: H) (L ∪ {~(⌊·a⌋ξ).unload}, R, none)⟩⟩)) ∨ ∃ (a : ℕ) (ξ : AnyFormula), X = (L, R, some (Sum.inr (~'⌊·a⌋ξ))) ∧ ((∃ (φ : Formula), ξ = AnyFormula.normal φ ∧ next = ⟨X :: H, ⟨(Finset.projection a L, {~φ} ∪ Finset.projection a R, none), posOf (X :: H) (Finset.projection a L, {~φ} ∪ Finset.projection a R, none)⟩⟩) ∨ (∃ (χ : LoadFormula), ξ = AnyFormula.loaded χ ∧ next = ⟨X :: H, ⟨(Finset.projection a L, Finset.projection a R, some (Sum.inr (~'χ))), posOf (X :: H) (Finset.projection a L, Finset.projection a R, some (Sum.inr (~'χ)))⟩⟩) ∨ next = ⟨X :: H, ⟨(L, R ∪ {~(⌊·a⌋ξ).unload}, none), posOf (X :: H) (L, R ∪ {~(⌊·a⌋ξ).unload}, none)⟩⟩)) ∨ (∃ (nrep : ¬flprep H X) (nbas : ¬X.basic), p = Sum.inl (ProverPos.nbas nrep nbas) ∧ next = ⟨H, ⟨X, Sum.inr (BuilderPos.ltab nrep nbas (uniLocalTab X))⟩⟩) ∨ ∃ (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.

theorem no_moves_of_rep {H : History} {X : Sequent} {pos : ProverPos H X ⊕ BuilderPos H X} (h : rep H X ∧ X.isFree) : theMoves ⟨H, ⟨X, pos⟩⟩ = ∅

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.

theorem mem_theMoves_of_move {pos next : GamePos} : move pos next → next ∈ theMoves pos

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⟩⟩

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

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

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

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.

@[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

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

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.

theorem move_inside_FL {p next : GamePos} (mov : move p next) : next.snd.fst.subseteq_FL p.snd.fst

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 = []

theorem Formula.allNegLoads_spec {nχ : NegLoadFormula} {φ : Formula} : nχ ∈ φ.allNegLoads → negUnload nχ = φ

theorem Formula.allNegLoads_complete {nχ : NegLoadFormula} {φ : Formula} : negUnload nχ = φ → nχ ∈ φ.allNegLoads

noncomputable def Sequent.all_subseteq_FL (Y : Sequent) : Finset { X : Sequent // X.subseteq_FL Y }

A list of sequents that are all FL-subsequents of the given sequent. Defined using Finset.instMonad.

Equations

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

The following only hold because there we are now working with Finset.

theorem Olf.mem_allNegLoads_of_L_R (YO : Olf) : YO ∈ ({none} ∪ YO.L.sup fun (φ : Formula) => Finset.image (some ∘ Sum.inl) φ.allNegLoads.toFinset) ∪ YO.R.sup fun (φ : Formula) => Finset.image (some ∘ Sum.inr) φ.allNegLoads.toFinset

Any Olf is among those generated from its own left and right parts. This is the key step to show that Sequent.all_subseteq_FL generates all Olf values.

theorem Sequent.all_subseteq_FL_complete (X Y : Sequent) (h : Y.subseteq_FL X) : ⟨Y, h⟩ ∈ X.all_subseteq_FL

@[instance_reducible]

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

Equations

• Sequent.subseteq_FL_fintype = { elems := X.all_subseteq_FL, complete := ⋯ }

noncomputable def Sequent.allSeqt_subseteq_FL (X : Sequent) : Finset Sequent

Equations

• X.allSeqt_subseteq_FL = Finset.image (fun (x : { X_1 : Sequent // X_1.subseteq_FL X }) => ↑x) X.all_subseteq_FL

New stuff, now about Sequent instead of Seqt

theorem Seqt.subseteq_FL_finite {X : Sequent} : Finite { Y : Sequent // Y.subseteq_FL X }

There are only finitely many FL-subset Sequents for a given Sequent. This means "there are only finitely many "sequents modulo setEq" that are subseteq_FL Y.

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

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.

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.

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.

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.

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.

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.

theorem moveChain_inside_FL {g : ℕ → GamePos} (g_rel : ∀ (n : ℕ), move (g n) (g (n + 1))) (n : ℕ) : (g n).snd.fst.subseteq_FL (g 0).snd.fst

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

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 = (g n).snd.fst) : (g n).snd.fst.isLoaded

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.

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 = (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.

theorem moveChain_eventually_loaded {g : ℕ → GamePos} (g_rel : ∀ (n : ℕ), move (g n) (g (n + 1))) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → (g n).snd.fst.isLoaded

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.

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) (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

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.

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) (hm : N ≤ m) (h : m + 2 ≤ n) (hs : (g m).snd.fst = (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.

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

@[instance_reducible]

def tableauGame : Game

The game defined in Section 6.2.

Equations

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

@[instance_reducible]

instance instDecidableEqPos : DecidableEq Game.Pos

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

Equations

• instDecidableEqPos = id instDecidableEqOfLawfulBEq

@[simp]

theorem tableauGame_turn_Prover {Hist : History} {X : Sequent} {lpr : ProverPos Hist X} : Game.turn ⟨Hist, ⟨X, Sum.inl lpr⟩⟩ = Prover

@[simp]

theorem tableauGame_turn_Builder {Hist : History} {X : Sequent} {lpr : BuilderPos Hist X} : Game.turn ⟨Hist, ⟨X, Sum.inr lpr⟩⟩ = Builder

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

@[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

def GamePos.IsUni : GamePos → Prop

A game position is uniform if any local tableau in it is the canonical one.

Equations

• GamePos.IsUni ⟨fst, ⟨X, Sum.inr (BuilderPos.ltab a a_1 lt)⟩⟩ = (lt = uniLocalTab X)
• x✝.IsUni = True

theorem posOf_isUni (H : History) (X : Sequent) : GamePos.IsUni ⟨H, ⟨X, posOf H X⟩⟩

Positions given by posOf are uniform: they are never ltab positions.

theorem theMoves_isUni {p next : GamePos} (h : next ∈ theMoves p) : next.IsUni

All moves lead to uniform positions.

From Prover winning strategies to uniform tableaux

theorem exists_isUni_of_pdl {Hist : History} {X Y : Sequent} (nrep : ¬flprep Hist X) (bas : X.basic) (r : PdlRule X Y) {next : Tableau (X :: Hist) Y} (h : next.IsUni) : ∃ (tab : Tableau Hist X), tab.IsUni

Helper for gameP_general: prefixing a uniform tableau with a PDL rule keeps it uniform.

theorem gameP_general (Hist : History) (X : Sequent) (sP : Strategy tableauGame Prover) (pos : ProverPos Hist X ⊕ BuilderPos Hist X) (pos_uni : GamePos.IsUni ⟨Hist, ⟨X, pos⟩⟩) (h : winning sP ⟨Hist, ⟨X, pos⟩⟩) : ∃ (tab : Tableau Hist X), tab.IsUni

After history Hist, if Prover has a winning strategy then there is a closed tableau, and moreover that tableau is uniform in the sense of Tableau.IsUni, because Prover has to play the canonical local tableau uniLocalTab. Note: we skip Definition 6.9 (Strategy Tree for Prover) and just use the Strategy type. This is the induction loading for gameP.

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

• startPos X = ⟨[], ⟨X, posOf [] X⟩⟩

theorem posOf_for_startPos (X : Sequent) : ∃ (proPos : ProverPos [] X), posOf [] X = Sum.inl proPos

We start with a prover position, because when the history is empty we can't have any repeat.

theorem gameP (X : Sequent) (s : Strategy tableauGame Prover) (h : winning s (startPos X)) : ∃ (tab : Tableau [] X), tab.IsUni

If Prover has a winning strategy then there is a closed tableau, and it is uniform.

theorem gameP_isUniform (X : Sequent) (s : Strategy tableauGame Prover) (h : winning s (startPos X)) : ∃ (tab : Tableau [] X), tab.isUniform

If Prover has a winning strategy then there is a uniform closed tableau, i.e. one satisfying the conditions U1 and U2.