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 PDL.termProver : Lean.ParserDescr

The player who chooses tableau rules.

Equations

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

def PDL.termBuilder : Lean.ParserDescr

The player who chooses branches of local tableaux.

Equations

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

inductive PDL.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 PDL.instDecidableEqProverPos {H✝ : History} {X✝ : Sequent} : DecidableEq (ProverPos H✝ X✝)

Equations

• PDL.instDecidableEqProverPos = PDL.instDecidableEqProverPos.decEq

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

Equations

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

inductive PDL.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 PDL.instDecidableEqBuilderPos {H✝ : History} {X✝ : Sequent} : DecidableEq (BuilderPos H✝ X✝)

Equations

• PDL.instDecidableEqBuilderPos = PDL.instDecidableEqBuilderPos.decEq

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

Equations

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

@[implicit_reducible]

def PDL.GamePos : Type

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

Equations

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

@[instance_reducible]

instance PDL.instDecidableEqGamePos : DecidableEq GamePos

Equations

• PDL.instDecidableEqGamePos = PDL.instDecidableEqGamePos._aux_1

def PDL.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 PDL.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 PDL.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 PDL.Move.isModal {pos newPos : GamePos} : Move pos newPos → Prop

Whether a game move applies a modal PDL rule.

Equations

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

def PDL.move (old new : GamePos) : Prop

Existence of a legal move between two game positions.

Equations

• PDL.move old new = Nonempty (PDL.Move old new)

theorem PDL.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 PDL.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.
• PDL.theMoves ⟨H, ⟨X, Sum.inl (PDL.ProverPos.frep a)⟩⟩ = ∅
• PDL.theMoves ⟨H, ⟨(L, R, some (Sum.inl (PDL.NegLoadFormula.neg (PDL.LoadFormula.box (α.sequence β) χ)))), Sum.inl (PDL.ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
• PDL.theMoves ⟨H, ⟨(L, R, some (Sum.inl (PDL.NegLoadFormula.neg (PDL.LoadFormula.box (PDL.Program.test τ) χ)))), Sum.inl (PDL.ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
• PDL.theMoves ⟨H, ⟨(L, R, some (Sum.inl (PDL.NegLoadFormula.neg (PDL.LoadFormula.box (α.union β) χ)))), Sum.inl (PDL.ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
• PDL.theMoves ⟨H, ⟨(L, R, some (Sum.inl (PDL.NegLoadFormula.neg (PDL.LoadFormula.box α.star χ)))), Sum.inl (PDL.ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
• PDL.theMoves ⟨H, ⟨(L, R, some (Sum.inr (PDL.NegLoadFormula.neg (PDL.LoadFormula.box (α.sequence β) χ)))), Sum.inl (PDL.ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
• PDL.theMoves ⟨H, ⟨(L, R, some (Sum.inr (PDL.NegLoadFormula.neg (PDL.LoadFormula.box (PDL.Program.test τ) χ)))), Sum.inl (PDL.ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
• PDL.theMoves ⟨H, ⟨(L, R, some (Sum.inr (PDL.NegLoadFormula.neg (PDL.LoadFormula.box (α.union β) χ)))), Sum.inl (PDL.ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
• PDL.theMoves ⟨H, ⟨(L, R, some (Sum.inr (PDL.NegLoadFormula.neg (PDL.LoadFormula.box α.star χ)))), Sum.inl (PDL.ProverPos.bas a_2 Xbasic_2)⟩⟩ = ⋯.elim
• PDL.theMoves ⟨H, ⟨X, Sum.inl (PDL.ProverPos.nbas nrep nbas)⟩⟩ = {⟨H, ⟨X, Sum.inr (PDL.BuilderPos.ltab nrep nbas (PDL.uniLocalTab X))⟩⟩}
• PDL.theMoves ⟨H, ⟨X, Sum.inr (PDL.BuilderPos.lpr lpr)⟩⟩ = ∅
• PDL.theMoves ⟨H, ⟨X, Sum.inr (PDL.BuilderPos.ltab a a_1 ltab)⟩⟩ = Finset.image (fun (Y : PDL.Sequent) => ⟨X :: H, ⟨Y, PDL.posOf (X :: H) Y⟩⟩) (PDL.endNodesOf ltab)

theorem PDL.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 ∧ (Formula.boxes δs (Formula.box δ ψ)).neg ∈ L ∧ next = ⟨X :: H, ⟨(L.erase (Formula.boxes δs (Formula.box δ ψ)).neg, R, some (Sum.inl (NegLoadFormula.neg (LoadFormula.boxes δs (LoadFormula.box δ (AnyFormula.normal ψ)))))), posOf (X :: H) (L.erase (Formula.boxes δs (Formula.box δ ψ)).neg, R, some (Sum.inl (NegLoadFormula.neg (LoadFormula.boxes δs (LoadFormula.box δ (AnyFormula.normal ψ))))))⟩⟩) ∨ ∃ (δs : List Program) (δ : Program) (ψ : Formula), ¬ψ.isBox ∧ (Formula.boxes δs (Formula.box δ ψ)).neg ∈ R ∧ next = ⟨X :: H, ⟨(L, R.erase (Formula.boxes δs (Formula.box δ ψ)).neg, some (Sum.inr (NegLoadFormula.neg (LoadFormula.boxes δs (LoadFormula.box δ (AnyFormula.normal ψ)))))), posOf (X :: H) (L, R.erase (Formula.boxes δs (Formula.box δ ψ)).neg, some (Sum.inr (NegLoadFormula.neg (LoadFormula.boxes δs (LoadFormula.box δ (AnyFormula.normal ψ))))))⟩⟩) ∨ (∃ (a : ℕ) (ξ : AnyFormula), X = (L, R, some (Sum.inl (NegLoadFormula.neg (LoadFormula.box (Program.atom_prog a) ξ)))) ∧ ((∃ (φ : Formula), ξ = AnyFormula.normal φ ∧ next = ⟨X :: H, ⟨({φ.neg} ∪ Finset.pdlProjection a L, Finset.pdlProjection a R, none), posOf (X :: H) ({φ.neg} ∪ Finset.pdlProjection a L, Finset.pdlProjection a R, none)⟩⟩) ∨ (∃ (χ : LoadFormula), ξ = AnyFormula.loaded χ ∧ next = ⟨X :: H, ⟨(Finset.pdlProjection a L, Finset.pdlProjection a R, some (Sum.inl (NegLoadFormula.neg χ))), posOf (X :: H) (Finset.pdlProjection a L, Finset.pdlProjection a R, some (Sum.inl (NegLoadFormula.neg χ)))⟩⟩) ∨ next = ⟨X :: H, ⟨(L ∪ {(LoadFormula.box (Program.atom_prog a) ξ).unload.neg}, R, none), posOf (X :: H) (L ∪ {(LoadFormula.box (Program.atom_prog a) ξ).unload.neg}, R, none)⟩⟩)) ∨ ∃ (a : ℕ) (ξ : AnyFormula), X = (L, R, some (Sum.inr (NegLoadFormula.neg (LoadFormula.box (Program.atom_prog a) ξ)))) ∧ ((∃ (φ : Formula), ξ = AnyFormula.normal φ ∧ next = ⟨X :: H, ⟨(Finset.pdlProjection a L, {φ.neg} ∪ Finset.pdlProjection a R, none), posOf (X :: H) (Finset.pdlProjection a L, {φ.neg} ∪ Finset.pdlProjection a R, none)⟩⟩) ∨ (∃ (χ : LoadFormula), ξ = AnyFormula.loaded χ ∧ next = ⟨X :: H, ⟨(Finset.pdlProjection a L, Finset.pdlProjection a R, some (Sum.inr (NegLoadFormula.neg χ))), posOf (X :: H) (Finset.pdlProjection a L, Finset.pdlProjection a R, some (Sum.inr (NegLoadFormula.neg χ)))⟩⟩) ∨ next = ⟨X :: H, ⟨(L, R ∪ {(LoadFormula.box (Program.atom_prog a) ξ).unload.neg}, none), posOf (X :: H) (L, R ∪ {(LoadFormula.box (Program.atom_prog a) ξ).unload.neg}, 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 PDL.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 PDL.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 PDL.mem_theMoves_of_move {pos next : GamePos} : move pos next → next ∈ theMoves pos

theorem PDL.move.hist {X : Sequent} {Hist : History} {next : GamePos} {pos : ProverPos Hist X ⊕ BuilderPos Hist X} (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 PDL.move.hist_suffix {X : Sequent} {Hist : History} {next : GamePos} {pos : ProverPos Hist X ⊕ BuilderPos Hist X} (mov : move ⟨Hist, ⟨X, pos⟩⟩ next) : Hist <:+ next.fst

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

theorem PDL.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 PDL.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 PDL.movemove (a c : GamePos) : Prop

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

Equations

• PDL.movemove = Relation.Comp PDL.move PDL.move

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

theorem PDL.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.subseteqFL 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 PDL.move_inside_FL {p next : GamePos} (mov : move p next) : next.snd.fst.subseteqFL p.snd.fst

def PDL.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 PDL.Formula.allNegLoads_spec {nχ : NegLoadFormula} {φ : Formula} : nχ ∈ φ.allNegLoads → negUnload nχ = φ

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

noncomputable def PDL.Sequent.allSubseteqFL (Y : Sequent) : Finset { X : Sequent // X.subseteqFL 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 PDL.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.allSubseteqFL generates all Olf values.

theorem PDL.Sequent.all_subseteq_FL_complete (X Y : Sequent) (h : Y.subseteqFL X) : ⟨Y, h⟩ ∈ X.allSubseteqFL

@[instance_reducible]

noncomputable instance PDL.Sequent.subseteqFLFintype {X : Sequent} : Fintype { Y : Sequent // Y.subseteqFL X }

Equations

• PDL.Sequent.subseteqFLFintype = { elems := X.allSubseteqFL, complete := ⋯ }

noncomputable def PDL.Sequent.allSeqtSubseteqFL (X : Sequent) : Finset Sequent

The finite set of sequents contained in the Fischer-Ladner closure of a sequent.

Equations

• X.allSeqtSubseteqFL = Finset.image (fun (x : { X_1 : PDL.Sequent // X_1.subseteqFL X }) => ↑x) X.allSubseteqFL

New stuff, now about Sequent instead of Seqt

theorem PDL.Seqt.subseteq_FL_finite {X : Sequent} : Finite { Y : Sequent // Y.subseteqFL 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 subseteqFL Y.

theorem PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.moveChain_inside_FL {g : ℕ → GamePos} (g_rel : ∀ (n : ℕ), move (g n) (g (n + 1))) (n : ℕ) : (g n).snd.fst.subseteqFL (g 0).snd.fst

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

theorem PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.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 PDL.tableauGame : Lean4GlCoalgebras.Game

The game defined in Section 6.2.

Equations

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

@[instance_reducible]

instance PDL.instDecidableEqPos : DecidableEq Lean4GlCoalgebras.Game.Pos

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

Equations

• PDL.instDecidableEqPos = id instDecidableEqOfLawfulBEq

@[simp]

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

@[simp]

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

@[simp]

theorem PDL.tableauGame_winner_nlpRep_eq_Builder {i : Lean4GlCoalgebras.Player} {Hist : History} {X : Sequent} {h : rep Hist X ∧ X.isFree} {sI : Lean4GlCoalgebras.Strategy tableauGame i} {sJ : Lean4GlCoalgebras.Strategy tableauGame (Lean4GlCoalgebras.other i)} : Lean4GlCoalgebras.winner sI sJ ⟨Hist, ⟨X, Sum.inl (ProverPos.frep h)⟩⟩ = Lean4GlCoalgebras.Player.B

@[simp]

theorem PDL.tableauGame_winner_lpr_eq_Prover {i : Lean4GlCoalgebras.Player} {X : Sequent} {Hist : History} {lpr : LoadedPathRepeat Hist X} {sI : Lean4GlCoalgebras.Strategy tableauGame i} {sJ : Lean4GlCoalgebras.Strategy tableauGame (Lean4GlCoalgebras.other i)} : Lean4GlCoalgebras.winner sI sJ ⟨Hist, ⟨X, Sum.inr (BuilderPos.lpr lpr)⟩⟩ = Lean4GlCoalgebras.Player.A

From Prover winning strategies to tableau

def PDL.GamePos.IsUni : GamePos → Prop

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

Equations

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

theorem PDL.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 PDL.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 PDL.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 PDL.gameP_general (Hist : History) (X : Sequent) (sP : Lean4GlCoalgebras.Strategy tableauGame Lean4GlCoalgebras.Player.A) (pos : ProverPos Hist X ⊕ BuilderPos Hist X) (pos_uni : GamePos.IsUni ⟨Hist, ⟨X, pos⟩⟩) (h : Lean4GlCoalgebras.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 PDL.startPos (X : Sequent) : GamePos

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

Equations

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

theorem PDL.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 PDL.gameP (X : Sequent) (s : Lean4GlCoalgebras.Strategy tableauGame Lean4GlCoalgebras.Player.A) (h : Lean4GlCoalgebras.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 PDL.gameP_isUniform (X : Sequent) (s : Lean4GlCoalgebras.Strategy tableauGame Lean4GlCoalgebras.Player.A) (h : Lean4GlCoalgebras.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.