Local Tableaux (Section 3)

inductive PDL.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 PDL.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 PDL.testsOfProgram_sizeOf_lt (α : Program) (τ : Formula) : τ ∈ testsOfProgram α → sizeOf τ < sizeOf α

@[irreducible]

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

• One or more equations did not get rendered due to their size.
• PDL.lmOfFormula PDL.Formula.bottom = 0
• PDL.lmOfFormula PDL.Formula.bottom.neg = 0
• PDL.lmOfFormula (PDL.Formula.atom_prop a) = 0
• PDL.lmOfFormula (PDL.Formula.atom_prop a).neg = 0
• PDL.lmOfFormula φ.neg.neg = 1 + PDL.lmOfFormula φ
• PDL.lmOfFormula (φ.and ψ) = 1 + PDL.lmOfFormula φ + PDL.lmOfFormula ψ
• PDL.lmOfFormula (φ.and ψ).neg = 1 + PDL.lmOfFormula φ.neg + PDL.lmOfFormula ψ.neg
• PDL.lmOfFormula (PDL.Formula.box (PDL.Program.atom_prog a) a_1) = 0
• PDL.lmOfFormula (PDL.Formula.box (PDL.Program.atom_prog a) a_1).neg = 0

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

theorem PDL.lmOfFormula_lt_dia_of_nonAtom {φ : Formula} {α : Program} (h : ¬α.isAtomic) : lmOfFormula φ.neg < lmOfFormula (Formula.box α φ).neg

def PDL.Olf.toForm : Olf → Multiset Formula

The multiset of unloaded formulas represented by an optional loading.

Equations

• PDL.Olf.toForm none = ∅
• PDL.Olf.toForm (some (Sum.inl (PDL.NegLoadFormula.neg χ))) = {χ.unload.neg}
• PDL.Olf.toForm (some (Sum.inr (PDL.NegLoadFormula.neg χ))) = {χ.unload.neg}

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

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

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

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

theorem PDL.lmOfFormula.le_union_left (α β : Program) (φ : Formula) : lmOfFormula (Formula.box α φ).neg ≤ lmOfFormula (Formula.box (α.union β) φ).neg

theorem PDL.lmOfFormula.le_union_right (α β : Program) (φ : Formula) : lmOfFormula (Formula.box β φ).neg ≤ lmOfFormula (Formula.box (α.union β) φ).neg

theorem PDL.Dset_goes_down (α : Program) (φ : Formula) {Fs : List Formula} {δ : List Program} (in_D : (Fs, δ) ∈ Dset α) {ψ : Formula} (in_Fs : ψ ∈ Fs) : lmOfFormula ψ < lmOfFormula (Formula.box α φ).neg

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

theorem PDL.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 PDL.measureProp {α : Program} {φ φ₁ φ₂ : Formula} : lmOfFormula φ < lmOfFormula φ.neg.neg ∧ lmOfFormula φ₁ + lmOfFormula φ₂ < lmOfFormula (φ₁.and φ₂) ∧ lmOfFormula φ₁.neg < lmOfFormula (φ₁.and φ₂).neg ∧ lmOfFormula φ₂.neg < lmOfFormula (φ₁.and φ₂).neg ∧ (¬α.isAtomic → ∀ X ∈ unfoldBox α φ, ∑ ψ ∈ X.toFinset, lmOfFormula ψ < lmOfFormula (Formula.box α φ)) ∧ (¬α.isAtomic → ∀ X ∈ unfoldDiamond α φ, ∑ ψ ∈ X.toFinset, lmOfFormula ψ < lmOfFormula (Formula.box α φ).neg)

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 PDL.endNodesOf {X : Sequent} : LocalTableau X → Finset Sequent

The end sequents of a local tableau.

Equations

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

def PDL.OpenLocalTableau (X : Sequent) : Type

An open local tableau has at least one end node.

Equations

• PDL.OpenLocalTableau X = { lt : PDL.LocalTableau X // PDL.endNodesOf lt ≠ ∅ }

@[instance_reducible]

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

Equations

• PDL.instDecidableEqOpenLocalTableau X = PDL.instDecidableEqOpenLocalTableau._aux_1 X

The Dershowitz-Manna ordering on sequents

def PDL.nodeToMultiset (X : Sequent) : Multiset Formula

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

Equations

• PDL.nodeToMultiset X = X.L.val + X.R.val + X.O.toForm

def PDL.nodeMeasure (X : Sequent) : Multiset ℕ

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

Equations

• PDL.nodeMeasure X = Multiset.map PDL.lmOfFormula (PDL.nodeToMultiset X)

def PDL.ltSequent (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

• PDL.ltSequent X Y = (PDL.nodeMeasure X).IsDershowitzMannaLT (PDL.nodeMeasure Y)

instance PDL.instIsWellFoundedSequentLt : WellFounded ltSequent

theorem PDL.ltSequent.trans {X Y Z : Sequent} (h1 : ltSequent X Y) (h2 : ltSequent Y Z) : ltSequent 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 ltSequent.

@[instance_reducible]

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

• PDL.instWellFoundedRelationSequent = { rel := PDL.ltSequent, wf := PDL.instIsWellFoundedSequentLt }

theorem PDL.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 PDL.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 PDL.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 PDL.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 PDL.LoadRule.lmOfFormula_lt {χ : LoadFormula} {ress : Finset (Finset Formula × Option NegLoadFormula)} (lrule : LoadRule (NegLoadFormula.neg χ) ress) (res : Finset Formula × Option NegLoadFormula) : res ∈ ress → ∀ ψ ∈ pairUnloadSet res, lmOfFormula ψ < lmOfFormula χ.unload.neg

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 PDL.lt_Sequent_of_split {X Y : Sequent} {Z A B : Multiset Formula} (hY : nodeToMultiset Y = Z + A) (hX : nodeToMultiset X = Z + B) (hB : B ≠ 0) (hlt : ∀ a ∈ A, ∃ b ∈ B, lmOfFormula a < lmOfFormula b) : ltSequent 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 PDL.localRuleApp.decreases_DM (lra : LocalRuleApp) (Y : Sequent) (hY : Y ∈ lra.C) : ltSequent Y lra.X

Local rules decrease the Dershowitz-Manna measure.

Helper functions, relating end nodes and children

def PDL.endNodeToEndNodeOfChild {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) }

Locate a child tableau containing a given end node of the parent tableau.

Equations

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

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

theorem PDL.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 PDL.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 PDL.localTableauTruth {X : Sequent} (lt : LocalTableau X) {W : Type} (M : KripkeModel W) (w : W) : vDash.SemImplies (M, w) X ↔ ∃ Y ∈ endNodesOf lt, vDash.SemImplies (M, w) Y

theorem PDL.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 PDL.endNodesOf_basic {X Z : Sequent} {ltZ : LocalTableau Z} : X ∈ endNodesOf ltZ → X.basic

End nodes of any local tableau are basic.

theorem PDL.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 PDL.IsDershowitzMannaLT.irrefl {α : Type u_1} [Preorder α] [WellFoundedLT α] (X : Multiset α) : ¬X.IsDershowitzMannaLT X