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_reducible]

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 which together with D-M can be used 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 (~⌈α⌉φ)

def Olf.toForm : Olf → Multiset Formula

Equations

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

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 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.

def endNodesOf {X : Sequent} : LocalTableau X → Finset 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_reducible]

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

Equations

• instDecidableEqOpenLocalTableau X = instDecidableEqOpenLocalTableau._aux_1 X

The Dershowitz-Manna ordering on sequents

def node_to_multiset (X : Sequent) : Multiset Formula

All formulas of a sequent as a multiset, with the loaded formula (if any) unloaded.

Equations

• node_to_multiset X = X.L.val + X.R.val + X.O.toForm

def nodeMeasure (X : Sequent) : Multiset ℕ

The multiset of the local measures of all formulas in a sequent.

Equations

• nodeMeasure X = Multiset.map lmOfFormula (node_to_multiset X)

def lt_Sequent (X Y : Sequent) : Prop

The Dershowitz-Manna ordering on sequents: X is smaller than Y iff the multiset of the lmOfFormula measures of the formulas of X is smaller than the one of Y.

Equations

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

instance instIsWellFoundedSequentLt : IsWellFounded Sequent lt_Sequent

theorem lt_Sequent.trans {X Y Z : Sequent} (h1 : lt_Sequent X Y) (h2 : lt_Sequent Y Z) : lt_Sequent X Z

Local rules decrease the Dershowitz-Manna measure

The reuslts here are used for the construction of the canonical local tableau uniLocalTab.

The key facts are:

• OneSidedLocalRule.lmOfFormula_lt: every formula in a result of a one-sided local rule is smaller — in the local measure lmOfFormula — than one of the formulas the rule is applied to;
• LoadRule.lmOfFormula_lt: the same for the loaded rules, via LoadRule.unload;
• localRuleApp.decreases_DM: hence each child of a local rule application is strictly smaller than its parent in the Dershowitz-Manna ordering lt_Sequent.

@[instance_reducible]

instance instWellFoundedRelationSequent : WellFoundedRelation Sequent

The well-founded relation on sequents used for the termination of the recursive definitions of local tableaux. This would also better belong to Pdl/Local/Tableau.lean, where the commented-out termination_by of endNodesOf refers to it.

Equations

• instWellFoundedRelationSequent = { rel := lt_Sequent, wf := ⋯ }

theorem Finset.union_val_of_disjoint {α : Type u_1} [DecidableEq α] {A C : Finset α} (h : Disjoint A C) : (A ∪ C).val = A.val + C.val

The multiset of a union of two disjoint finite sets is the sum of the two multisets.

theorem Finset.union_val_sdiff {α : Type u_1} [DecidableEq α] (A B : Finset α) : (A ∪ B).val = A.val + (B \ A).val

Splitting off the new elements of a union.

theorem Finset.val_eq_sdiff_add_of_subset {α : Type u_1} [DecidableEq α] {A B : Finset α} (h : B ⊆ A) : A.val = (A \ B).val + B.val

Splitting off the condition of a rule from the sequent it is applied to.

theorem OneSidedLocalRule.lmOfFormula_lt {precond : Finset Formula} {ress : Finset (Finset Formula)} (orule : OneSidedLocalRule precond ress) (res : Finset Formula) : res ∈ ress → ∀ ψ ∈ res, ∃ φ ∈ precond, lmOfFormula ψ < lmOfFormula φ

Every formula in a result of a one-sided local rule is smaller than one of the formulas the rule is applied to.

theorem LoadRule.lmOfFormula_lt {χ : LoadFormula} {ress : Finset (Finset Formula × Option NegLoadFormula)} (lrule : LoadRule (~'χ) ress) (res : Finset Formula × Option NegLoadFormula) : res ∈ ress → ∀ ψ ∈ pairUnloadSet res, lmOfFormula ψ < lmOfFormula (~χ.unload)

Every formula in a result of a loaded rule — including the new loaded formula — is smaller than the formula the rule is applied to.

theorem lt_Sequent_of_split {X Y : Sequent} {Z A B : Multiset Formula} (hY : node_to_multiset Y = Z + A) (hX : node_to_multiset X = Z + B) (hB : B ≠ 0) (hlt : ∀ a ∈ A, ∃ b ∈ B, lmOfFormula a < lmOfFormula b) : lt_Sequent Y X

A sufficient criterion for the Dershowitz-Manna ordering on sequents: the formulas of Y are those of X, with a non-empty part B replaced by formulas that are smaller.

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

Local rules decrease the Dershowitz-Manna measure.

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

theorem mem_endNodesOf_byLocalRule_iff {X : Sequent} {lra : LocalRuleApp} {X_def : X = lra.X} {next : (Y : Sequent) → Y ∈ lra.C → LocalTableau Y} {Z : Sequent} : Z ∈ endNodesOf (LocalTableau.byLocalRule lra X_def next) ↔ ∃ (Y : Sequent) (h : Y ∈ lra.C), Z ∈ endNodesOf (next Y h)

Membership in the end nodes of a local tableau given by a local rule application.

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_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