Generating all Local Tableaux

We show that for any X the type LocalTableau is finite.

This is needed to define BuildTree as a finite tree.

Helpers about Finset.fsort

theorem Finset.fsort_toFinset (X : Finset Formula) : X.fsort.toFinset = X

@[simp]

theorem Finset.fsort_singleton (a : Formula) : {a}.fsort = [a]

theorem Finset.length_fsort (X : Finset Formula) : X.fsort.length = X.card

theorem Finset.fsort_nodup (X : Finset Formula) : X.fsort.Nodup

theorem fsort_eq_singleton {X : Finset Formula} {a : Formula} (h : X.fsort = [a]) : X = {a}

theorem fsort_eq_pair {X : Finset Formula} {a b : Formula} (h : X.fsort = [a, b]) : X = {a, b}

theorem sublist_fsort_toFinset_subset {L : Finset Formula} {l : List Formula} (h : l.Sublist L.fsort) : l.toFinset ⊆ L

A sublist of the sorted version of L gives a subset of L.

theorem exists_sublist_fsort_of_subset {L Lcond : Finset Formula} (h : Lcond ⊆ L) : ∃ l ∈ L.fsort.sublists, l.toFinset = Lcond

Any subset of L arises from a sublist of the sorted version of L.

theorem Olf.subset_self (o : Olf) : o ⊆ o

theorem Olf.none_subset (o : Olf) : none ⊆ o

theorem Formula.ne_neg (φ : Formula) : φ ≠ ~φ

theorem Formula.ne_neg_neg (φ : Formula) : φ ≠ ~~φ

theorem pair_neg_cases {φ a b : Formula} (h : {φ, ~φ} = {a, b}) (hab : a ≠ b) : a = φ ∧ b = ~φ ∨ a = ~φ ∧ b = φ

If {φ, ~φ} = {a, b} with a ≠ b then the pair is one of the two obvious ones.

All one-sided local rules

def osrCast {L L' : Finset Formula} {B : Finset (Finset Formula)} (h : L = L') (r : OneSidedLocalRule L' B) : OneSidedLocalRule L B

Transport a OneSidedLocalRule along an equality of preconditions.

Equations

• osrCast h r = ⋯.mpr r

@[simp]

theorem osrCast_self {L : Finset Formula} {B : Finset (Finset Formula)} (h : L = L) (r : OneSidedLocalRule L B) : osrCast h r = r

def OneSidedLocalRule.ofSorted (L : Finset Formula) (l : List Formula) : L.fsort = l → Option ((B : Finset (Finset Formula)) × OneSidedLocalRule L B)

Given the sorted list of the formulas in L, is there a OneSidedLocalRule for L? The pair case comes first so that the equations below hold by rfl.

Equations

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

theorem OneSidedLocalRule.ofSorted_pair {L : Finset Formula} {a b : Formula} (h : L.fsort = [a, b]) : ofSorted L [a, b] h = if hb : b = ~a then some ⟨∅, osrCast ⋯ (not a)⟩ else if ha : a = ~b then some ⟨∅, osrCast ⋯ (not b)⟩ else none

theorem OneSidedLocalRule.ofSorted_bot {L : Finset Formula} (h : L.fsort = [⊥]) : ofSorted L [⊥] h = some ⟨∅, osrCast ⋯ bot⟩

theorem OneSidedLocalRule.ofSorted_neg {L : Finset Formula} {φ : Formula} (h : L.fsort = [~~φ]) : ofSorted L [~~φ] h = some ⟨{{φ}}, osrCast ⋯ (neg φ)⟩

theorem OneSidedLocalRule.ofSorted_con {L : Finset Formula} {φ ψ : Formula} (h : L.fsort = [φ ⋀ ψ]) : ofSorted L [φ ⋀ ψ] h = some ⟨{{φ, ψ}}, osrCast ⋯ (con φ ψ)⟩

theorem OneSidedLocalRule.ofSorted_nCo {L : Finset Formula} {φ ψ : Formula} (h : L.fsort = [~(φ ⋀ ψ)]) : ofSorted L [~(φ ⋀ ψ)] h = some ⟨{{~φ}, {~ψ}}, osrCast ⋯ (nCo φ ψ)⟩

theorem OneSidedLocalRule.ofSorted_box {L : Finset Formula} {α : Program} {φ : Formula} (h : L.fsort = [⌈α⌉φ]) : ofSorted L [⌈α⌉φ] h = if notAtm : ¬α.isAtomic then some ⟨(unfoldBox α φ).toFinFin, osrCast ⋯ (box α φ notAtm)⟩ else none

theorem OneSidedLocalRule.ofSorted_dia {L : Finset Formula} {α : Program} {φ : Formula} (h : L.fsort = [~⌈α⌉φ]) : ofSorted L [~⌈α⌉φ] h = if notAtm : ¬α.isAtomic then some ⟨(unfoldDiamond α φ).toFinFin, osrCast ⋯ (dia α φ notAtm)⟩ else none

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

Is there a OneSidedLocalRule applicable to L?

Equations

• OneSidedLocalRule.all L = OneSidedLocalRule.ofSorted L L.fsort ⋯

theorem OneSidedLocalRule.all_eq_ofSorted {L : Finset Formula} {l : List Formula} (h : L.fsort = l) : all L = ofSorted L l h

theorem OneSidedLocalRule.all_spec {L : Finset Formula} {B : Finset (Finset Formula)} (osr : OneSidedLocalRule L B) : all L = some ⟨B, osr⟩

@[instance_reducible]

instance OneSidedLocalRule.fintype {L : Finset Formula} {B : Finset (Finset Formula)} : Fintype (OneSidedLocalRule L B)

Equations

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

All load rules

def LoadRule.the (nχ : NegLoadFormula) : Option ((ress : Finset (Finset 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).toFinFinOpt, LoadRule.dia notAtom⟩ else none
• LoadRule.the (~'⌊α⌋AnyFormula.normal a) = if notAtom : ¬α.isAtomic then some ⟨(unfoldDiamondLoaded' α a).toFinFinOpt, LoadRule.dia' notAtom⟩ else none

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

@[instance_reducible]

instance LoadRule.fintype {nχ : NegLoadFormula} {ress : Finset (Finset Formula × Option NegLoadFormula)} : Fintype (LoadRule nχ ress)

Equations

• LoadRule.fintype = match h_the : LoadRule.the (~'nχ.1) with | some ⟨ress', lr⟩ => { elems := if h : ress = ress' then {⋯ ▸ lr} else ∅, complete := ⋯ } | none => { elems := ∅, complete := ⋯ }

All local rules

def lrCast {c c' : Sequent} {ress : Finset Sequent} (h : c = c') (r : LocalRule c' ress) : LocalRule c ress

Transport a LocalRule along an equality of the conditions.

Equations

• lrCast h r = ⋯.mpr r

@[simp]

theorem lrCast_self {c : Sequent} {ress : Finset Sequent} (h : c = c) (r : LocalRule c ress) : lrCast h r = r

def LocalRule.negPairOf (L R : Finset Formula) (lL lR : List Formula) : L.fsort = lL → R.fsort = lR → Option ((ress : Finset Sequent) × LocalRule (L, R, none) ress)

Helper for LocalRule.all, dealing with the two closing rules LRnegL and LRnegR.

Equations

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

theorem LocalRule.negPairOf_singletons {L R : Finset Formula} {φ1 φ2 : Formula} (hL : L.fsort = [φ1]) (hR : R.fsort = [φ2]) : negPairOf L R [φ1] [φ2] hL hR = if h : φ2 = ~φ1 then some ⟨∅, lrCast ⋯ (LRnegL φ1)⟩ else if h : φ1 = ~φ2 then some ⟨∅, lrCast ⋯ (LRnegR φ2)⟩ else none

def LocalRule.all (cond : Sequent) : Option ((ress : Finset 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.

theorem LocalRule.all_none (L R : Finset Formula) : all (L, R, none) = if hR : R = ∅ then Option.map (fun (x : (B : Finset (Finset Formula)) × OneSidedLocalRule L B) => match x with | ⟨fst, orule⟩ => ⟨Finset.image (fun (res : Finset Formula) => (res, ∅, none)) fst, lrCast ⋯ (oneSidedL orule ⋯)⟩) (OneSidedLocalRule.all L) else if hL : L = ∅ then Option.map (fun (x : (B : Finset (Finset Formula)) × OneSidedLocalRule R B) => match x with | ⟨fst, orule⟩ => ⟨Finset.image (fun (res : Finset Formula) => (∅, res, none)) fst, lrCast ⋯ (oneSidedR orule ⋯)⟩) (OneSidedLocalRule.all R) else negPairOf L R L.fsort R.fsort ⋯ ⋯

theorem LocalRule.all_inl_loaded (L R : Finset Formula) (α : Program) (χ : LoadFormula) : all (L, R, some (Sum.inl (~'⌊α⌋AnyFormula.loaded χ))) = if hL : L = ∅ then if hR : R = ∅ then if notAtm : ¬α.isAtomic then some ⟨Finset.image (fun (x : Finset Formula × Option NegLoadFormula) => match x with | (X, o) => (X, ∅, Option.map Sum.inl o)) (unfoldDiamondLoaded α χ).toFinFinOpt, lrCast ⋯ (loadedL (⌊α⌋AnyFormula.loaded χ) (LoadRule.dia notAtm) ⋯)⟩ else none else none else none

theorem LocalRule.all_inl_normal (L R : Finset Formula) (α : Program) (φ : Formula) : all (L, R, some (Sum.inl (~'⌊α⌋AnyFormula.normal φ))) = if hL : L = ∅ then if hR : R = ∅ then if notAtm : ¬α.isAtomic then some ⟨Finset.image (fun (x : Finset Formula × Option NegLoadFormula) => match x with | (X, o) => (X, ∅, Option.map Sum.inl o)) (unfoldDiamondLoaded' α φ).toFinFinOpt, lrCast ⋯ (loadedL (⌊α⌋AnyFormula.normal φ) (LoadRule.dia' notAtm) ⋯)⟩ else none else none else none

theorem LocalRule.all_inr_loaded (L R : Finset Formula) (α : Program) (χ : LoadFormula) : all (L, R, some (Sum.inr (~'⌊α⌋AnyFormula.loaded χ))) = if hL : L = ∅ then if hR : R = ∅ then if notAtm : ¬α.isAtomic then some ⟨Finset.image (fun (x : Finset Formula × Option NegLoadFormula) => match x with | (X, o) => (∅, X, Option.map Sum.inr o)) (unfoldDiamondLoaded α χ).toFinFinOpt, lrCast ⋯ (loadedR (⌊α⌋AnyFormula.loaded χ) (LoadRule.dia notAtm) ⋯)⟩ else none else none else none

theorem LocalRule.all_inr_normal (L R : Finset Formula) (α : Program) (φ : Formula) : all (L, R, some (Sum.inr (~'⌊α⌋AnyFormula.normal φ))) = if hL : L = ∅ then if hR : R = ∅ then if notAtm : ¬α.isAtomic then some ⟨Finset.image (fun (x : Finset Formula × Option NegLoadFormula) => match x with | (X, o) => (∅, X, Option.map Sum.inr o)) (unfoldDiamondLoaded' α φ).toFinFinOpt, lrCast ⋯ (loadedR (⌊α⌋AnyFormula.normal φ) (LoadRule.dia' notAtm) ⋯)⟩ else none else none else none

theorem OneSidedLocalRule.precond_ne_empty {P : Finset Formula} {B : Finset (Finset Formula)} (osr : OneSidedLocalRule P B) : P ≠ ∅

theorem LocalRule.negPairOf_eq {L R : Finset Formula} {lL lR : List Formula} (hL : L.fsort = lL) (hR : R.fsort = lR) : negPairOf L R L.fsort R.fsort ⋯ ⋯ = negPairOf L R lL lR hL hR

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

@[instance_reducible]

instance LocalRule.fintype {X : Sequent} {ress : Finset Sequent} : Fintype (LocalRule X ress)

Equations

• LocalRule.fintype = match h_the : LocalRule.all X with | some ⟨ress', lr⟩ => { elems := if h : ress = ress' then {⋯ ▸ lr} else ∅, complete := ⋯ } | none => { elems := ∅, complete := ⋯ }

All local rule applications

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

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_X (X : Sequent) (lra : LocalRuleApp) : lra ∈ all X → lra.X = X

theorem LocalRuleApp.all_spec (lrA : LocalRuleApp) : lrA ∈ all lrA.X

theorem LocalRuleApp.all_nonempty_of_nonbasic {X : Sequent} (X_nonbas : ¬X.basic) : all X ≠ []

Termination measure for local tableaux

def lmOfOlf : Olf → ℕ

Equations

• lmOfOlf none = 0
• lmOfOlf (some (Sum.inl nlf)) = lmOfFormula (negUnload nlf)
• lmOfOlf (some (Sum.inr nlf)) = lmOfFormula (negUnload nlf)

def lmOfSequent (X : Sequent) : ℕ

Local measure of a sequent: the sum of lmOfFormula over all three components.

Equations

• lmOfSequent X = ∑ φ ∈ X.1, lmOfFormula φ + ∑ φ ∈ X.2.1, lmOfFormula φ + lmOfOlf X.2.2

def lmOfONlf : Option NegLoadFormula → ℕ

Local measure of an optional negated loaded formula.

Equations

• lmOfONlf none = 0
• lmOfONlf (some nlf) = lmOfFormula (negUnload nlf)

Helpers to show that local rules decrease the measure

theorem lm_sum_union_le (A B : Finset Formula) : ∑ φ ∈ A ∪ B, lmOfFormula φ ≤ ∑ φ ∈ A, lmOfFormula φ + ∑ φ ∈ B, lmOfFormula φ

The measure sum over a union is at most the sum of the measure sums.

theorem lm_sum_Dset_le_tests {α : Program} {F : List Formula} {δ : List Program} (in_D : (F, δ) ∈ Dset α) : ∑ ψ ∈ F.toFinset, lmOfFormula ψ ≤ (List.map (fun (τ : { x : Formula // x ∈ testsOfProgram α }) => lmOfFormula ↑τ) (testsOfProgram α).attach).sum

For (F,δ) ∈ Dset α the measure sum over F is at most the test measure of α.

theorem lm_dia_eq {α : Program} {φ : Formula} (h : ¬α.isAtomic) : lmOfFormula (~⌈α⌉φ) = 1 + lmOfFormula (~φ) + (List.map (fun (τ : { x : Formula // x ∈ testsOfProgram α }) => lmOfFormula ↑τ) (testsOfProgram α).attach).sum

Unfolding the measure of a diamond with a non-atomic program.

theorem OneSidedLocalRule.decreases_lm {precond : Finset Formula} {ress : Finset (Finset Formula)} (orule : OneSidedLocalRule precond ress) (res : Finset Formula) : res ∈ ress → ∑ φ ∈ res, lmOfFormula φ < ∑ φ ∈ precond, lmOfFormula φ

One-sided local rules strictly decrease the measure sum.

theorem LoadRule.decreases_lm {χ : LoadFormula} {ress : Finset (Finset Formula × Option NegLoadFormula)} (lrule : LoadRule (~'χ) ress) (Fo : Finset Formula × Option NegLoadFormula) : Fo ∈ ress → ∑ ψ ∈ Fo.1, lmOfFormula ψ + lmOfONlf Fo.2 < lmOfFormula (~χ.unload)

Loaded rules strictly decrease the measure: the new formulas together with the new loaded formula have a smaller measure than the old loaded formula.

theorem localRuleApp.decreases_lm (lra : LocalRuleApp) (Y : Sequent) (h : Y ∈ lra.C) : lmOfSequent Y < lmOfSequent lra.X

Generating all local tableaux

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 x_2 = [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.

def comboF {q : Sequent → Type} (s : Finset Sequent) (f : (x : Sequent) → x ∈ s → List (q x)) : List ((x : Sequent) → x ∈ s → q x)

Version of combo for Finsets.

Equations

• comboF s f = List.map (fun (g : (x : Sequent) → x ∈ s.seqSort → q x) (x : Sequent) (hx : x ∈ s) => g x ⋯) (combo fun (x : Sequent) (hx : x ∈ s.seqSort) => f x ⋯)

theorem comboF_mem_of_forall_in {q : Sequent → Type} {s : Finset Sequent} (f : (x : Sequent) → x ∈ s → List (q x)) (g : (x : Sequent) → x ∈ s → q x) (h : ∀ (x : Sequent) (x_in : x ∈ s), g x x_in ∈ f x x_in) : g ∈ comboF s f

@[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_nonempty (X : Sequent) : all X ≠ []

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

@[instance_reducible]

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

Equations

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

Generating all Open Local Tableaux

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

Equations

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

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