Local Tableaux (Section 3)

Tableau Nodes

@[reducible, inline]

abbrev Olf : Type

In nodes we optionally have a negated loaded formula on the left or right.

Equations

• Olf = Option (NegLoadFormula ⊕ NegLoadFormula)

def Olf.voc : Olf → Vocab

Equations

• Olf.voc none = ∅
• Olf.voc (some (Sum.inl nlf)) = nlf.voc
• Olf.voc (some (Sum.inr nlf)) = nlf.voc

def Sequent : Type

A tableau node is labelled with two lists of formulas and an Olf.

Equations

• Sequent = (List Formula × List Formula × Olf)

instance instSequentDecidableEq : DecidableEq Sequent

Equations

• instSequentDecidableEq a b = instDecidableEqProd a b

instance instSequentRepr : Repr Sequent

Equations

• instSequentRepr = instReprProdOfReprTuple

def Sequent.setEqTo : Sequent → Sequent → Prop

Two Sequents are set-equal when their components are finset-equal. That is, we do not care about the order of the lists, but we do care about the side of the formula and what formual is loaded. Hint: use List.toFinset.ext_iff with this.

Equations

• Sequent.setEqTo (L, R, O) (L', R', O') = (L.toFinset = L'.toFinset ∧ R.toFinset = R'.toFinset ∧ O = O')

def Sequent.multisetEqTo : Sequent → Sequent → Prop

Equations

• Sequent.multisetEqTo (L, R, O) (L', R', O') = (↑L = ↑L' ∧ ↑R = ↑R' ∧ O = O')

@[simp]

theorem Sequent.setEqTo_refl (X : Sequent) : X.setEqTo X

theorem Sequent.setEqTo_symm (X Y : Sequent) : X.setEqTo Y ↔ Y.setEqTo X

@[simp]

theorem Sequent.multisetEqTo_refl (X : Sequent) : X.multisetEqTo X

theorem Sequent.multisetEqTo_symm (X Y : Sequent) : X.multisetEqTo Y ↔ Y.multisetEqTo X

def Sequent.toFinset : Sequent → Finset Formula

Equations

• Sequent.toFinset (L, R, O) = L.toFinset ∪ R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset

def Sequent.L : Sequent → List Formula

Equations

• Sequent.L (L, R, O) = L

def Sequent.R : Sequent → List Formula

Equations

• Sequent.R (L, R, O) = R

def Sequent.O : Sequent → Olf

Equations

• Sequent.O (L, R, O) = O

def Sequent.isLoaded : Sequent → Bool

Equations

• Sequent.isLoaded (fst, fst_1, none) = decide False
• Sequent.isLoaded (fst, fst_1, some val) = decide True

def Sequent.isFree (Γ : Sequent) : Bool

Equations

• Γ.isFree = decide ¬Γ.isLoaded = true

@[simp]

theorem Sequent.none_isFree (L R : List Formula) : isFree (L, R, none) = true

@[simp]

theorem Sequent.some_not_isFree (L R : List Formula) (olf : NegLoadFormula ⊕ NegLoadFormula) : ¬isFree (L, R, some olf) = true

theorem setEqTo_isLoaded_iff {X Y : Sequent} (h : X.setEqTo Y) : X.isLoaded = Y.isLoaded

theorem multisetEqTo_isLoaded_iff {X Y : Sequent} (h : X.multisetEqTo Y) : X.isLoaded = Y.isLoaded

Semantics of a Sequent

instance modelCanSemImplySequent {W : Type} : vDash (KripkeModel W × W) Sequent

Equations

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

instance modelCanSemImplyLLO {W : Type} : vDash (KripkeModel W × W) (List Formula × List Formula × Olf)

Equations

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

instance instSequentHasSat : HasSat Sequent

Equations

• instSequentHasSat = { satisfiable := fun (Δ : Sequent) => ∃ (W : Type) (M : KripkeModel W) (w : W), (M, w)⊨Δ }

theorem tautImp_iff_SequentUnsat {φ ψ : Formula} {X : Sequent} : X = ([φ], [~ψ], none) → (tautology (~φ⋀(~ψ)) ↔ ¬HasSat.satisfiable X)

theorem vDash_setEqTo_iff {W : Type} {X Y : Sequent} (h : X.setEqTo Y) (M : KripkeModel W) (w : W) : (M, w)⊨X ↔ (M, w)⊨Y

theorem vDash_multisetEqTo_iff {W : Type} {X Y : Sequent} (h : X.multisetEqTo Y) (M : KripkeModel W) (w : W) : (M, w)⊨X ↔ (M, w)⊨Y

Different kinds of formulas as elements of Sequent

instance instMembershipFormulaSequent : Membership Formula Sequent

Equations

• instMembershipFormulaSequent = { mem := fun (X : Sequent) (φ : Formula) => φ ∈ X.L ∨ φ ∈ X.R }

def NegLoadFormula.mem_Sequent (X : Sequent) (nlf : NegLoadFormula) : Prop

Equations

• NegLoadFormula.mem_Sequent X nlf = (X.O = some (Sum.inl nlf) ∨ X.O = some (Sum.inr nlf))

instance instDecidableMem_SequentMkListFormulaProdOlf {L R : List Formula} {O : Olf} {nlf : NegLoadFormula} : Decidable (NegLoadFormula.mem_Sequent (L, R, O) nlf)

Equations

• instDecidableMem_SequentMkListFormulaProdOlf = if h : O = some (Sum.inl nlf) then isTrue ⋯ else if h2 : O = some (Sum.inr nlf) then isTrue ⋯ else isFalse ⋯

def Sequent.without (LRO : Sequent) (naf : AnyNegFormula) : Sequent

Equations

• Sequent.without (L, R, O) (~''(AnyFormula.normal f)) = (L \ {~f}, R \ {~f}, O)
• Sequent.without (L, R, O) (~''(AnyFormula.loaded lf)) = if NegLoadFormula.mem_Sequent (L, R, O) (~'lf) then (L, R, none) else (L, R, O)

instance instMembershipNegLoadFormulaSequent : Membership NegLoadFormula Sequent

Equations

• instMembershipNegLoadFormulaSequent = { mem := NegLoadFormula.mem_Sequent }

def AnyNegFormula.mem_Sequent (X : Sequent) (anf : AnyNegFormula) : Prop

Equations

• AnyNegFormula.mem_Sequent x✝ (~''(AnyFormula.normal φ)) = ((~φ) ∈ x✝)
• AnyNegFormula.mem_Sequent x✝ (~''(AnyFormula.loaded χ)) = NegLoadFormula.mem_Sequent x✝ (~'χ)

instance instMembershipAnyNegFormulaSequent : Membership AnyNegFormula Sequent

Equations

• instMembershipAnyNegFormulaSequent = { mem := AnyNegFormula.mem_Sequent }

@[simp]

theorem Sequent.without_normal_isFree_iff_isFree {φ : Formula} (LRO : Sequent) : (LRO.without (~''(AnyFormula.normal φ))).isFree = true ↔ LRO.isFree = true

@[simp]

theorem Sequent.isFree_then_without_isFree (LRO : Sequent) : LRO.isFree = true → ∀ (anf : AnyNegFormula), (LRO.without anf).isFree = true

theorem Sequent.without_loadBoxes_isFree_of_eq_inl {αs : List Program} {d : Program} {L R : List Formula} {δs : List Program} {χ : LoadFormula} {φ : Formula} (h : AnyFormula.loaded χ = AnyFormula.loadBoxes αs (AnyFormula.normal φ)) : (without (L, R, some (Sum.inl (~'⌊⌊d :: δs⌋⌋χ))) (~''(AnyFormula.loadBoxes (d :: (δs ++ αs)) (AnyFormula.normal φ)))).isFree = true

theorem Sequent.without_loadBoxes_isFree_of_eq_inr {αs : List Program} {d : Program} {L R : List Formula} {δs : List Program} {χ : LoadFormula} {φ : Formula} (h : AnyFormula.loaded χ = AnyFormula.loadBoxes αs (AnyFormula.normal φ)) : (without (L, R, some (Sum.inr (~'⌊⌊d :: δs⌋⌋χ))) (~''(AnyFormula.loadBoxes (d :: (δs ++ αs)) (AnyFormula.normal φ)))).isFree = true

theorem Sequent.without_loadMulti_isFree_of_splitLast_cons_inl {d : Program} {δ_β : List Program × Program} {L R : List Formula} {δs : List Program} {φ : Formula} (h : splitLast (d :: δs) = some δ_β) : (without (L, R, some (Sum.inl (~'loadMulti δ_β.1 δ_β.2 φ))) (~''(AnyFormula.loadBoxes (d :: δs) (AnyFormula.normal φ)))).isFree = true

theorem Sequent.without_loadMulti_isFree_of_splitLast_cons_inr {d : Program} {δ_β : List Program × Program} {L R : List Formula} {δs : List Program} {φ : Formula} (h : splitLast (d :: δs) = some δ_β) : (without (L, R, some (Sum.inr (~'loadMulti δ_β.1 δ_β.2 φ))) (~''(AnyFormula.loadBoxes (d :: δs) (AnyFormula.normal φ)))).isFree = true

inductive Side : Type

• LL : Side
• RR : Side

def sideOf {α : Type u_1} : α ⊕ α → Side

Equations

• sideOf (Sum.inl val) = Side.LL
• sideOf (Sum.inr val) = Side.RR

def AnyNegFormula.in_side (anf : AnyNegFormula) : Side → (X : Sequent) → Prop

Equations

• (~''(AnyFormula.normal φ)).in_side Side.LL (L, fst, snd) = ((~φ) ∈ L)
• (~''(AnyFormula.normal φ)).in_side Side.RR (fst, R, snd) = ((~φ) ∈ R)
• (~''(AnyFormula.loaded χ)).in_side Side.LL (fst, fst_1, O) = (O = some (Sum.inl (~'χ)))
• (~''(AnyFormula.loaded χ)).in_side Side.RR (fst, fst_1, O) = (O = some (Sum.inr (~'χ)))

theorem AnyNegFormula.in_side_of_setEqTo {side : Side} {X Y : Sequent} (h : X.setEqTo Y) {anf : AnyNegFormula} : anf.in_side side X ↔ anf.in_side side Y

theorem AnyNegFormula.in_side_of_multisetEqTo {side : Side} {X Y : Sequent} (h : X.multisetEqTo Y) {anf : AnyNegFormula} : anf.in_side side X ↔ anf.in_side side Y

theorem LoadFormula.in_side_of_lf_inl {X : Sequent} (lf : LoadFormula) (O_def : X.2.2 = some (Sum.inl (~'lf))) : (~''(AnyFormula.loaded lf)).in_side Side.LL X

theorem LoadFormula.in_side_of_lf_inr {X : Sequent} (lf : LoadFormula) (O_def : X.2.2 = some (Sum.inr (~'lf))) : (~''(AnyFormula.loaded lf)).in_side Side.RR X

theorem Sequent.isLoaded_of_negAnyFormula_loaded {α : Program} {ξ : AnyFormula} {side : Side} {X : Sequent} (negLoad_in : (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side X) : X.isLoaded = true

@[simp]

theorem Sequent.without_loaded_in_side_isFree (LRO : Sequent) (ξ : LoadFormula) (side : Side) : (~''(AnyFormula.loaded ξ)).in_side side LRO → (LRO.without (~''(AnyFormula.loaded ξ))).isFree = true

Local Tableaux

inductive OneSidedLocalRule : List Formula → List (List Formula) → Type

Local rules replace a given set of formulas by other sets, one for each branch. The list of resulting branches can be empty, representing that the given set is closed. In the Haskell prover this is done in "ruleFor" in the Logic.PDL.Prove.Tree module.

• bot : OneSidedLocalRule [⊥] ∅
• not (φ : Formula) : OneSidedLocalRule [φ, ~φ] ∅
• neg (φ : Formula) : OneSidedLocalRule [~~φ] [[φ]]
• con (φ ψ : Formula) : OneSidedLocalRule [φ⋀ψ] [[φ, ψ]]
• nCo (φ ψ : Formula) : OneSidedLocalRule [~φ⋀ψ] [[~φ], [~ψ]]
• box (α : Program) (φ : Formula) (notAtom : ¬α.isAtomic) : OneSidedLocalRule [⌈α⌉φ] (unfoldBox α φ)
• dia (α : Program) (φ : Formula) (notAtom : ¬α.isAtomic) : OneSidedLocalRule [~⌈α⌉φ] (unfoldDiamond α φ)

instance instDecidableEqOneSidedLocalRule {a✝ : List Formula} {a✝¹ : List (List Formula)} : DecidableEq (OneSidedLocalRule a✝ a✝¹)

Equations

• instDecidableEqOneSidedLocalRule = decEqOneSidedLocalRule✝

instance instReprOneSidedLocalRule {a✝ : List Formula} {a✝¹ : List (List Formula)} : Repr (OneSidedLocalRule a✝ a✝¹)

Equations

• instReprOneSidedLocalRule = { reprPrec := reprOneSidedLocalRule✝ }

theorem oneSidedLocalRuleTruth {X : List Formula} {B : List (List Formula)} (lr : OneSidedLocalRule X B) : Con X≡discon B

inductive LoadRule : NegLoadFormula → List (List Formula × Option NegLoadFormula) → Type

The loaded diamond rule, given by unfoldDiamondLoaded. In MB page 19 these were multiple rules ¬u, ¬; ¬* and ¬?. It replaces the loaded formula by up to one loaded formula and a list of normal formulas. It's a bit annoying to need the rule twice here due to the definition of LoadFormula and the extra definition of unfoldDiamondLoaded'.

• dia {α : Program} {χ : LoadFormula} (notAtom : ¬α.isAtomic) : LoadRule (~'⌊α⌋AnyFormula.loaded χ) (unfoldDiamondLoaded α χ)
• dia' {α : Program} {φ : Formula} (notAtom : ¬α.isAtomic) : LoadRule (~'⌊α⌋AnyFormula.normal φ) (unfoldDiamondLoaded' α φ)

instance instDecidableEqLoadRule {a✝ : NegLoadFormula} {a✝¹ : List (List Formula × Option NegLoadFormula)} : DecidableEq (LoadRule a✝ a✝¹)

Equations

• instDecidableEqLoadRule = decEqLoadRule✝

instance instReprLoadRule {a✝ : NegLoadFormula} {a✝¹ : List (List Formula × Option NegLoadFormula)} : Repr (LoadRule a✝ a✝¹)

Equations

• instReprLoadRule = { reprPrec := reprLoadRule✝ }

def LoadRule.unload {χ : LoadFormula} {B : List (List Formula × Option NegLoadFormula)} : LoadRule (~'χ) B → OneSidedLocalRule [~χ.unload] (List.map pairUnload B)

Given a LoadRule application, define the equivalent unloaded rule application. This allows re-using oneSidedLocalRuleTruth to prove loadRuleTruth.

Equations

• (LoadRule.dia notAtom).unload = ⋯ ▸ OneSidedLocalRule.dia α χ_2.unload notAtom
• (LoadRule.dia' notAtom).unload = ⋯ ▸ OneSidedLocalRule.dia α φ notAtom

theorem loadRuleTruth {χ : LoadFormula} {B : List (List Formula × Option NegLoadFormula)} (lr : LoadRule (~'χ) B) : (~χ.unload)≡dis (List.map (Con ∘ pairUnload) B)

The loaded unfold rule is sound and invertible. In the notes this is part of localRuleTruth.

inductive LocalRule : Sequent → List Sequent → Type

A local rule is a OneSidedLocalRule, a left-right contradiction, or a LoadRule. Note that formulas can be in four places: left, right, loaded left, loaded right.

We do not have neg/contradiction rules between loaded and unloaded formulas (i.e. between ({unload χ}, ∅, some (Sum.inl ~χ)) and (∅, {unload χ}, some (Sum.inr ~χ))) because in any such case we could also close the tableau before or without loading.

• oneSidedL {precond : List Formula} {ress : List (List Formula)} (orule : OneSidedLocalRule precond ress) : LocalRule (precond, ∅, none) (List.map (fun (res : List Formula) => (res, ∅, none)) ress)
• oneSidedR {precond : List Formula} {ress : List (List Formula)} (orule : OneSidedLocalRule precond ress) : LocalRule (∅, precond, none) (List.map (fun (res : List Formula) => (∅, res, none)) ress)
• LRnegL (ϕ : Formula) : LocalRule ([ϕ], [~ϕ], none) ∅
• LRnegR (ϕ : Formula) : LocalRule ([~ϕ], [ϕ], none) ∅
• loadedL {ress : List (List Formula × Option NegLoadFormula)} (χ : LoadFormula) (lrule : LoadRule (~'χ) ress) : LocalRule (∅, ∅, some (Sum.inl (~'χ))) (List.map (fun (x : List Formula × Option NegLoadFormula) => match x with | (X, o) => (X, ∅, Option.map Sum.inl o)) ress)
• loadedR {ress : List (List Formula × Option NegLoadFormula)} (χ : LoadFormula) (lrule : LoadRule (~'χ) ress) : LocalRule (∅, ∅, some (Sum.inr (~'χ))) (List.map (fun (x : List Formula × Option NegLoadFormula) => match x with | (X, o) => (∅, X, Option.map Sum.inr o)) ress)

instance instReprLocalRule {a✝ : Sequent} {a✝¹ : List Sequent} : Repr (LocalRule a✝ a✝¹)

Equations

• instReprLocalRule = { reprPrec := reprLocalRule✝ }

instance Option.instHasSubsetOption {α : Type u_1} : HasSubset (Option α)

Equations

• Option.instHasSubsetOption = { Subset := fun (o1 o2 : Option α) => match o1, o2 with | none, x => True | some val, none => False | some f, some g => f = g }

@[simp]

theorem Option.some_subseteq {α : Type u_1} {x : α} {O : Option α} : some x ⊆ O ↔ some x = O

instance Option.insHasSdiff {α : Type u_1} [DecidableEq α] : SDiff (Option α)

Instance that is used to say (O : Olf) \ (O' : Olf).

Equations

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

def Option.overwrite {α : Type u_1} : Option α → Option α → Option α

Equations

• x✝.overwrite none = x✝
• x✝.overwrite (some x_3) = some x_3

def Olf.change (oldO Ocond newO : Olf) : Olf

Equations

• oldO.change Ocond newO = Option.overwrite (oldO \ Ocond) newO

@[simp]

theorem Olf.change_none_none {oldO : Olf} : oldO.change none none = oldO

@[simp]

theorem Olf.change_some_some_none {wnlf : NegLoadFormula ⊕ NegLoadFormula} : change (some wnlf) (some wnlf) none = none

@[simp]

theorem Olf.change_some {oldO whatever : Olf} {wnlf : NegLoadFormula ⊕ NegLoadFormula} : oldO.change whatever (some wnlf) = some wnlf

def applyLocalRule {Lcond Rcond : List Formula} {Ocond : Olf} {ress : List Sequent} : LocalRule (Lcond, Rcond, Ocond) ress → Sequent → List Sequent

Equations

• applyLocalRule x✝ (L, R, O) = List.map (fun (x : Sequent) => match x with | (Lnew, Rnew, Onew) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O.change Ocond Onew)) ress

inductive LocalRuleApp : Sequent → List Sequent → Type

• mk {L R : List Formula} {C ress : List Sequent} {O : Olf} (Lcond Rcond : List Formula) (Ocond : Olf) (rule : LocalRule (Lcond, Rcond, Ocond) ress) {hC : C = applyLocalRule rule (L, R, O)} (preconditionProof : Lcond.Subperm L ∧ Rcond.Subperm R ∧ Ocond ⊆ O) : LocalRuleApp (L, R, O) C

theorem localRuleTruth {X : Sequent} {C : List Sequent} (lrA : LocalRuleApp X C) {W : Type} (M : KripkeModel W) (w : W) : (M, w)⊨X ↔ ∃ Ci ∈ C, (M, w)⊨Ci

def Formula.basic : Formula → Bool

A basic formula is of the form ¬⊥, p, ¬p, [a]_ or ¬[a]_. Note: in the article also ⊥ is basic, but not here because then OneSidedLocalRule.bot can be applied to it.

Equations

• Formula.bottom.basic = decide False
• (~Formula.bottom).basic = decide True
• (·a).basic = decide True
• (~·a).basic = decide True
• (⌈·a⌉a_1).basic = decide True
• (~⌈·a⌉a_1).basic = decide True
• x✝.basic = decide False

def Sequent.closed (X : Sequent) : Prop

A sequent is closed iff it contains ⊥ or contains a formula and its negation.

Equations

• X.closed = (⊥ ∈ X ∨ ∃ f ∈ X, (~f) ∈ X)

def Sequent.basic : Sequent → Prop

A sequent is basic iff it only contains basic formulas and is not closed.

Equations

• Sequent.basic (L, R, O) = ((∀ f ∈ L ++ R ++ (Option.map (Sum.elim negUnload negUnload) O).toList, f.basic = true) ∧ ¬Sequent.closed (L, R, O))

inductive LocalTableau (X : Sequent) : Type

Local tableau for X, maximal by definition.

• byLocalRule {X : Sequent} {B : List Sequent} : LocalRuleApp X B → (next : (Y : Sequent) → Y ∈ B → LocalTableau Y) → LocalTableau X
• sim {X : Sequent} : X.basic → LocalTableau X

theorem mem_of_two_subperm {α : Type u_1} {l : List α} {a b : α} [DecidableEq α] : [a, b].Subperm l → a ∈ l ∧ b ∈ l

theorem nonbasic_of_localRuleApp {X : Sequent} {B : List Sequent} (lrA : LocalRuleApp X B) : ¬X.basic

If we can apply a local rule to a sequent then it cannot be basic.

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.

Equations

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

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_31 }

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 H_goes_down (α : Program) (φ : Formula) {Fs : List Formula} {δ : List Program} (in_H : (Fs, δ) ∈ H α) {ψ : 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 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 {X : Sequent} {B : List Sequent} (lrA : LocalRuleApp X B) (Y : Sequent) : Y ∈ B → lt_Sequent Y X

@[irreducible]

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

Equations

• endNodesOf (LocalTableau.byLocalRule _lr next) = (List.map (fun (x : { x : Sequent // x ∈ B }) => match x with | ⟨Y, h⟩ => endNodesOf (next Y h)) B.attach).flatten
• endNodesOf (LocalTableau.sim a) = [x✝]

Helper functions, relating end nodes and children

noncomputable def endNode_to_endNodeOfChildNonComp {X : Sequent} {a✝ : List Sequent} {subTabs : (Y : Sequent) → Y ∈ a✝ → LocalTableau Y} {E : Sequent} (lrA : LocalRuleApp X a✝) (E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)) : { x : Sequent // ∃ (h : x ∈ a✝), E ∈ endNodesOf (subTabs x h) }

Equations

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

theorem endNodeIsEndNodeOfChild {X : Sequent} {a✝ : List Sequent} {subTabs : (Y : Sequent) → Y ∈ a✝ → LocalTableau Y} {E : Sequent} (lrA : LocalRuleApp X a✝) (E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)) : ∃ (Y : Sequent) (h : Y ∈ a✝), E ∈ endNodesOf (subTabs Y h)

theorem endNodeOfChild_to_endNode {X Y : Sequent} {ltX : LocalTableau X} {C : List Sequent} (lrA : LocalRuleApp X C) (subTabs : (Y : Sequent) → Y ∈ C → LocalTableau Y) (h : ltX = LocalTableau.byLocalRule lrA subTabs) (Y_in : Y ∈ 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.)