The Tableau Game (Section 6.2 and 6.3)

Defining the Tableau Game (Section 6.2)

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

• nlpRep {H : History} {X : Sequent} : ¬Nonempty (LoadedPathRepeat H X) → rep H X → ProverPos H X
• bas {H : History} {X x : Sequent} : ¬rep H x → X.basic → ProverPos H X
• nbas {H : History} {X x : Sequent} : ¬rep H x → ¬X.basic → ProverPos H X

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

Equations

• instDecidableEqProverPos = decEqProverPos✝

instance instDecidableEqLoadedPathRepeat {H : History} {X : Sequent} : DecidableEq (LoadedPathRepeat H X)

Equations

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

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

Equations

• BuilderPos H X = (LoadedPathRepeat H X ⊕ LocalTableau X)

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

Equations

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

def GamePos : Type

Equations

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

instance instGamePosDecidableEq : DecidableEq GamePos

Equations

• instGamePosDecidableEq a b = a.instDecidableEqSigma b

def LoadedPathRepeat.choice {H : History} {X : Sequent} (ne : Nonempty (LoadedPathRepeat H X)) : LoadedPathRepeat H X

Equations

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

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.

def LocalRuleApp.all (X : Sequent) : List ((B : List Sequent) × LocalRuleApp X B)

Equations

• LocalRuleApp.all X = sorry

theorem LocalRuleApp.all_spec (X : Sequent) (B : List Sequent) (lra : LocalRuleApp X B) : ⟨B, lra⟩ ∈ all X

instance LocalRuleApp.fintype {B : List Sequent} {X : Sequent} : Fintype (LocalRuleApp X B)

Equations

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

def LocalTableau.all (X : Sequent) : List (LocalTableau X)

Equations

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

theorem LocalTableau.all_spec {X : Sequent} {ltX : LocalTableau X} : ltX ∈ all X

instance LocalTableau.fintype {X : Sequent} : Fintype (LocalTableau X)

Equations

• LocalTableau.fintype = { elems := (LocalTableau.all X).toFinset, complete := ⋯ }

def tableauGame : Game

WORK-IN-PROGRESS. This is the game defined in Section 6.2 in the paper. In particular tableauGame.wf and tableauGame.move_rel together are Lemma 6.10: because the wellfounded relation decreases with every move of the game, all matches must be finite. Note that the paper does not prove Lemma 6.10 but says it is similar to Lemma 4.10 which uses the Fischer-Ladner closure.

Equations

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

def startPos (X : Sequent) : GamePos

Equations

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

theorem gameP (X : Sequent) (s : Strategy tableauGame Prover) (h : winning s (startPos X)) : Nonempty (Tableau [] X)

If Prover has a winning strategy then there is a closed tableau.

From winning strategies to model graphs (Section 6.3)

theorem strmg (X : Sequent) (s : Strategy tableauGame Builder) (h : winning s (startPos X)) : ∃ (WS : Finset (Finset Formula)) (mg : ModelGraph WS), X.toFinset ∈ WS

If Builder has a winning strategy then there is a model graph.