Local Tableaux (Section 3)

inductive LocalTableau (X : Sequent) : Type

Local tableau for X, maximal by definition.

• byLocalRule {X : Sequent} (lra : LocalRuleApp) (X_def : X = lra.X) (next : (Y : Sequent) → Y ∈ lra.C → LocalTableau Y) : LocalTableau X
• sim {X : Sequent} : X.basic → LocalTableau X

instance LocalTableau.instDecidableEq {X : Sequent} {lt1 lt2 : LocalTableau X} : Decidable (lt1 = lt2)

Equations

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

Termination of LocalTableau

theorem testsOfProgram_sizeOf_lt (α : Program) (τ : Formula) : τ ∈ testsOfProgram α → sizeOf τ < sizeOf α

@[irreducible]

def lmOfFormula (f : Formula) : ℕ

The local measure we use together with D-M to show that LocalTableau are finite. Note that different from the paper here we also add lmOfFormula (~φ) in the ~⌈α⌉φ case. This is needed to get lmOfFormula_lt_dia_of_nonAtom.

Equations

• lmOfFormula Formula.bottom = 0
• lmOfFormula (~Formula.bottom) = 0
• lmOfFormula (·a) = 0
• lmOfFormula (~·a) = 0
• lmOfFormula (~~φ) = 1 + lmOfFormula φ
• lmOfFormula (φ ⋀ ψ) = 1 + lmOfFormula φ + lmOfFormula ψ
• lmOfFormula (~(φ ⋀ ψ)) = 1 + lmOfFormula (~φ) + lmOfFormula (~ψ)
• lmOfFormula (⌈·a⌉a_1) = 0
• lmOfFormula (~⌈·a⌉a_1) = 0
• lmOfFormula (⌈α⌉φ) = 1 + lmOfFormula φ + (List.map (fun (τ : { x : Formula // x ∈ testsOfProgram α }) => lmOfFormula (~↑τ)) (testsOfProgram α).attach).sum
• lmOfFormula (~⌈α⌉φ) = 1 + lmOfFormula (~φ) + (List.map (fun (τ : { x : Formula // x ∈ testsOfProgram α }) => lmOfFormula ↑τ) (testsOfProgram α).attach).sum

theorem lmOfFormula_lt_box_of_nonAtom {φ : Formula} {α : Program} (h : ¬α.isAtomic) : lmOfFormula φ < lmOfFormula (⌈α⌉φ)

theorem lmOfFormula_lt_dia_of_nonAtom {φ : Formula} {α : Program} (h : ¬α.isAtomic) : lmOfFormula (~φ) < lmOfFormula (~⌈α⌉φ)

instance Formula.WellFoundedLT : _root_.WellFoundedLT Formula

instance Formula.instPreorderFormula : Preorder Formula

Equations

• Formula.instPreorderFormula = Preorder.lift lmOfFormula

def node_to_multiset : Sequent → Multiset Formula

Equations

• node_to_multiset (L, R, none) = ↑L + ↑R
• node_to_multiset (L, R, some (Sum.inl (~'χ))) = ↑L + ↑R + ↑[~χ.unload]
• node_to_multiset (L, R, some (Sum.inr (~'χ))) = ↑L + ↑R + ↑[~χ.unload]

def Olf.toForm : Olf → Multiset Formula

Equations

• Olf.toForm none = ∅
• Olf.toForm (some (Sum.inl (~'χ))) = {~χ.unload}
• Olf.toForm (some (Sum.inr (~'χ))) = {~χ.unload}

theorem node_to_multiset_eq {L R : List Formula} {O : Olf} : node_to_multiset (L, R, O) = ↑L + ↑R + O.toForm

theorem node_to_multiset_eq_of_three_eq {L L' R R' : List Formula} {O O' : Olf} (hL : L = L') (hR : R = R') (hO : O = O') : node_to_multiset (L, R, O) = node_to_multiset (L', R', O')

If each three parts are the same then node_to_multiset is the same.

theorem List.Subperm.append {α : Type u_1} {l₁ l₂ r₁ r₂ : List α} : l₁.Subperm l₂ → r₁.Subperm r₂ → (l₁ ++ r₁).Subperm (l₂ ++ r₂)

theorem preconP_to_submultiset {Lcond L Rcond R : List Formula} {Ocond O : Olf} (preconditionProof : Lcond.Subperm L ∧ Rcond.Subperm R ∧ Ocond ⊆ O) : node_to_multiset (Lcond, Rcond, Ocond) ≤ node_to_multiset (L, R, O)

theorem Multiset.sub_of_le {α : Type u_1} [DecidableEq α] {M N X Y : Multiset α} (h : N ≤ M) : M - N + Y = X ↔ M + Y = X + N

theorem Multiset_diff_append_of_le {α : Type u_1} [DecidableEq α] {R Rcond Rnew : List α} : ↑(R.diff Rcond ++ Rnew) = ↑R - ↑Rcond + ↑Rnew

theorem List.Perm_diff_append_of_Subperm {α : Type u_1} [DecidableEq α] {L M : List α} (h : M.Subperm L) : L.Perm (L.diff M ++ M)

theorem List.count_eq_diff_of_subperm {α : Type u_1} [DecidableEq α] {L M : List α} (h : M.Subperm L) (φ : α) : count φ L = count φ (L.diff M) + count φ M

theorem node_to_multiset_of_precon {L R Lcond Rcond Lnew Rnew : List Formula} {O Ocond Onew : Olf} (precon : Lcond.Subperm L ∧ Rcond.Subperm R ∧ Ocond ⊆ O) (O_extracon : O ≠ none → Ocond = none → Onew = none) : node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond) + node_to_multiset (Lnew, Rnew, Onew) = node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O.change Ocond Onew)

Applying node_to_multiset before or after applyLocalRule gives the same.

def lt_Sequent (X Y : Sequent) : Prop

Equations

• lt_Sequent X Y = (node_to_multiset X).IsDershowitzMannaLT (node_to_multiset Y)

instance instWellFoundedRelationSequent : WellFoundedRelation Sequent

Equations

• instWellFoundedRelationSequent = { rel := lt_Sequent, wf := instWellFoundedRelationSequent._proof_1 }

theorem LocalRule.cond_non_empty {Lcond Rcond : List Formula} {Ocond : Olf} {X : List Sequent} (rule : LocalRule (Lcond, Rcond, Ocond) X) : node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅

theorem Multiset.sub_add_of_subset_eq {α : Type u_1} {X : Multiset α} [DecidableEq α] {M : Multiset α} (h : X ≤ M) : M = M - X + X

theorem unfoldBox.decreases_lmOf_nonAtomic {ψ : Formula} {α : Program} {φ : Formula} {X : List Formula} (α_non_atomic : ¬α.isAtomic) (X_in : X ∈ unfoldBox α φ) (ψ_in_X : ψ ∈ X) : lmOfFormula ψ < lmOfFormula (⌈α⌉φ)

theorem lmOfFormula.le_union_left (α β : Program) (φ : Formula) : lmOfFormula (~⌈α⌉φ) ≤ lmOfFormula (~⌈α⋓β⌉φ)

theorem lmOfFormula.le_union_right (α β : Program) (φ : Formula) : lmOfFormula (~⌈β⌉φ) ≤ lmOfFormula (~⌈α⋓β⌉φ)

theorem Dset_goes_down (α : Program) (φ : Formula) {Fs : List Formula} {δ : List Program} (in_D : (Fs, δ) ∈ Dset α) {ψ : Formula} (in_Fs : ψ ∈ Fs) : lmOfFormula ψ < lmOfFormula (~⌈α⌉φ)

theorem unfoldDiamond.decreases_lmOf_nonAtomic {ψ : Formula} {α : Program} {φ : Formula} {X : List Formula} (α_non_atomic : ¬α.isAtomic) (X_in : X ∈ unfoldDiamond α φ) (ψ_in_X : ψ ∈ X) : lmOfFormula ψ < lmOfFormula (~⌈α⌉φ)

theorem finset_sum_trichotomy {A : Type u_1} [DecidableEq A] (f : A → ℕ) (X : List A) (a : A) (bs : List A) (h : ∀ x ∈ X, x = a ∨ x ∈ bs ∨ f x = 0) : ∑ x ∈ X.toFinset, f x ≤ f a + (List.map f bs).sum

This is a helper for measureProp parts (d) and (e). If each element of a list X is either a, belongs to a list bs, or has f value 0, then the sum of f over X.toFinset is at most f a + (bs.map f).sum.

theorem measureProp {α : Program} {φ φ₁ φ₂ : Formula} : lmOfFormula φ < lmOfFormula (~~φ) ∧ lmOfFormula φ₁ + lmOfFormula φ₂ < lmOfFormula (φ₁ ⋀ φ₂) ∧ lmOfFormula (~φ₁) < lmOfFormula (~(φ₁ ⋀ φ₂)) ∧ lmOfFormula (~φ₂) < lmOfFormula (~(φ₁ ⋀ φ₂)) ∧ (¬α.isAtomic → ∀ X ∈ unfoldBox α φ, ∑ ψ ∈ X.toFinset, lmOfFormula ψ < lmOfFormula (⌈α⌉φ)) ∧ (¬α.isAtomic → ∀ X ∈ unfoldDiamond α φ, ∑ ψ ∈ X.toFinset, lmOfFormula ψ < lmOfFormula (~⌈α⌉φ))

This is a summary lemma and not used as a whole anywhere. Note that parts (d) and (e) are about the measure sum over X and not single formulas, so for example (e) is not the same as unfoldDiamond.decreases_lmOf_nonAtomic. Also note that we use List.toFinset here to ignore duplicates in the list X.

theorem LocalRuleDecreases {X : Sequent} {ress : List Sequent} (rule : LocalRule X ress) (Y : Sequent) : Y ∈ ress → ∀ y ∈ node_to_multiset Y, ∃ x ∈ node_to_multiset X, y < x

def MultisetLT' {α : Type u_1} [Preorder α] (M N : Multiset α) : Prop

Equations

• MultisetLT' M N = ∃ (X : Multiset α) (Y : Multiset α) (Z : Multiset α), Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y

theorem MultisetDMLT.iff_MultisetLT' {α : Type u_1} [Preorder α] {M N : Multiset α} : M.IsDershowitzMannaLT N ↔ MultisetLT' M N

theorem localRuleApp.decreases_DM (lra : LocalRuleApp) (Y : Sequent) : Y ∈ lra.C → lt_Sequent Y lra.X

@[irreducible]

def endNodesOf {X : Sequent} : LocalTableau X → List Sequent

Equations

• One or more equations did not get rendered due to their size.
• endNodesOf (LocalTableau.sim a) = [x✝]

def OpenLocalTableau (X : Sequent) : Type

An open local tableau has at least one end node.

Equations

• OpenLocalTableau X = { lt : LocalTableau X // endNodesOf lt ≠ [] }

instance instDecidableEqOpenLocalTableau (X : Sequent) : DecidableEq (OpenLocalTableau X)

Equations

• instDecidableEqOpenLocalTableau X a b = a.instDecidableEq b

Helper functions, relating end nodes and children

def endNode_to_endNodeOfChild {X : Sequent} {lrA : LocalRuleApp} (def_X : X = lrA.X) (subTabs : (Y : Sequent) → Y ∈ lrA.C → LocalTableau Y) {E : Sequent} (E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA def_X subTabs)) : { x : Sequent // ∃ (h : x ∈ lrA.C), E ∈ endNodesOf (subTabs x h) }

Equations

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

theorem endNodeIsEndNodeOfChild {X : Sequent} {self✝ : LocalRuleApp} {subTabs : (Y : Sequent) → Y ∈ self✝.C → LocalTableau Y} {E : Sequent} (def_X : X = self✝.X) (E_in : E ∈ endNodesOf (LocalTableau.byLocalRule self✝ def_X subTabs)) : ∃ (Y : Sequent) (h : Y ∈ self✝.C), E ∈ endNodesOf (subTabs Y h)

theorem endNodeOfChild_to_endNode {Y : Sequent} (lrA : LocalRuleApp) {ltX : LocalTableau lrA.X} (subTabs : (Y : Sequent) → Y ∈ lrA.C → LocalTableau Y) (h : ltX = LocalTableau.byLocalRule lrA ⋯ subTabs) (Y_in : Y ∈ lrA.C) {Z : Sequent} (Z_in : Z ∈ endNodesOf (subTabs Y Y_in)) : Z ∈ endNodesOf ltX

Overall Soundness and Invertibility of LocalTableau

theorem localTableauTruth {X : Sequent} (lt : LocalTableau X) {W : Type} (M : KripkeModel W) (w : W) : (M, w) ⊨ X ↔ ∃ Y ∈ endNodesOf lt, (M, w) ⊨ Y

theorem localTableauSat {X : Sequent} (lt : LocalTableau X) : HasSat.satisfiable X ↔ ∃ Y ∈ endNodesOf lt, HasSat.satisfiable Y

Local Tableaux make progress

These lemmas are used to show soundness, in particular loadedDiamondPaths.

theorem endNodesOf_basic {X Z : Sequent} {ltZ : LocalTableau Z} : X ∈ endNodesOf ltZ → X.basic

End nodes of any local tableau are basic.

theorem endNodesOf_nonbasic_lt_Sequent {X Y : Sequent} (lt : LocalTableau X) (X_nonbas : ¬X.basic) : Y ∈ endNodesOf lt → lt_Sequent Y X

If X is not basic, then all end nodes Y of a local tableau lt for X are strictly lower than X according to the DM-ordering of their multisets.

theorem non_eq_of_ltSequent {X Y : Sequent} : lt_Sequent X Y → X ≠ Y

If a sequent is lower according the DM-ordering, then it is different.

theorem endNodesOf_nonbasic_non_eq {X Y : Sequent} (lt : LocalTableau X) (X_nonbas : ¬X.basic) : Y ∈ endNodesOf lt → Y ≠ X

If X is not basic, then for all end nodes Y of a local tableau lt for X we have that Y ≠ X.

theorem IsDershowitzMannaLT.irrefl {α : Type u_1} [Preorder α] [WellFoundedLT α] (X : Multiset α) : ¬X.IsDershowitzMannaLT X

theorem non_multisetEqTo_of_ltSequent {X Y : Sequent} : lt_Sequent X Y → ¬X.multisetEqTo Y

If a sequent is lower according to the DM-ordering, then they are multiset-different. (The analogue with finset instead of multiset does not hold.)