Generating all Local Tableaux

def OneSidedLocalRule.all (L : List Formula) : Option ((B : List (List Formula)) × OneSidedLocalRule L B)

Equations

• OneSidedLocalRule.all [Formula.bottom] = some ⟨∅, OneSidedLocalRule.bot⟩
• OneSidedLocalRule.all [φ1, ~φ2] = if h : φ1 = φ2 then h ▸ some ⟨∅, OneSidedLocalRule.not φ1⟩ else none
• OneSidedLocalRule.all [~~φ] = some ⟨[[φ]], OneSidedLocalRule.neg φ⟩
• OneSidedLocalRule.all [φ⋀ψ] = some ⟨[[φ, ψ]], OneSidedLocalRule.con φ ψ⟩
• OneSidedLocalRule.all [~(φ⋀ψ)] = some ⟨[[~φ], [~ψ]], OneSidedLocalRule.nCo φ ψ⟩
• OneSidedLocalRule.all [⌈α⌉φ] = if notAtm : ¬α.isAtomic then some ⟨unfoldBox α φ, OneSidedLocalRule.box α φ notAtm⟩ else none
• OneSidedLocalRule.all [~⌈α⌉φ] = if notAtm : ¬α.isAtomic then some ⟨unfoldDiamond α φ, OneSidedLocalRule.dia α φ notAtm⟩ else none
• OneSidedLocalRule.all x✝ = none

def OneSidedLocalRule.all_spec {L : List Formula} {B : List (List Formula)} (osr : OneSidedLocalRule L B) : ⟨B, osr⟩ ∈ all L

Equations

• ⋯ = ⋯

def LoadRule.the (nχ : NegLoadFormula) : Option ((ress : List (List Formula × Option NegLoadFormula)) × LoadRule nχ ress)

Given a negated loaded formula, is there a LoadRule applicable to it?

Equations

• LoadRule.the (~'⌊α⌋AnyFormula.loaded a) = if notAtom : ¬α.isAtomic then some ⟨unfoldDiamondLoaded α a, LoadRule.dia notAtom⟩ else none
• LoadRule.the (~'⌊α⌋AnyFormula.normal a) = if notAtom : ¬α.isAtomic then some ⟨unfoldDiamondLoaded' α a, LoadRule.dia' notAtom⟩ else none

def LoadRule.the_spec {χ : LoadFormula} {ress : List (List Formula × Option NegLoadFormula)} (lor : LoadRule (~'χ) ress) : some ⟨ress, lor⟩ = the (~'χ)

Equations

• ⋯ = ⋯

def LocalRule.all (cond : Sequent) : Option ((ress : List Sequent) × LocalRule cond ress)

Given a subsequent cond to be replaced, is there an applicable local rule? Note that cond are only the principal formulas, not the whole sequent.

Equations

• One or more equations did not get rendered due to their size.
• LocalRule.all ([φ1], [φ2], none) = if h : φ2 = ~φ1 then some ⟨∅, ⋯.mpr (LocalRule.LRnegL φ1)⟩ else if h : φ1 = ~φ2 then some ⟨∅, ⋯.mpr (LocalRule.LRnegR φ2)⟩ else none
• LocalRule.all x✝ = none

def LocalRule.all_spec {L : Sequent} {B : List Sequent} (lr : LocalRule L B) : ⟨B, lr⟩ ∈ all L

Equations

• ⋯ = ⋯

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

Given a sequent, return a list of all possible local rule applications.

Equations

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

theorem LocalRuleApp.all_spec (X : Sequent) (C : List Sequent) (lrA : LocalRuleApp X C) : ⟨C, lrA⟩ ∈ all X

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

At most finitely many local rule applications lead from X and to B. Note this is weaker than "only finitely many local rules apply to X, because each B gives a different type.

Equations

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

def combo {α : Type} [DecidableEq α] {q : α → Type} {L : List α} (f : (x : α) → x ∈ L → List (q x)) : List ((x : α) → x ∈ L → q x)

Convert a function returning lists into a list of functions. Helper for LocalTableau.all.

Equations

• One or more equations did not get rendered due to their size.
• combo f = [fun (x : α) (x_in : x ∈ []) => ⋯.elim]

theorem combo_mem_of_forall_in {α : Type} [DecidableEq α] {q : α → Type} {L : List α} (f : (x : α) → x ∈ L → List (q x)) (g : (x : α) → x ∈ L → q x) : (∀ (x : α) (x_in : x ∈ L), g x x_in ∈ f x x_in) → g ∈ combo f

Characterization of members of combo result. Could be strengthened to ↔ later.

@[irreducible]

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 := ⋯ }