Local rules and local rule applications

One-sided local rules

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 α φ)

def instDecidableEqOneSidedLocalRule.decEq {a✝ : List Formula} {a✝¹ : List (List Formula)} (x✝ x✝¹ : OneSidedLocalRule a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqOneSidedLocalRule.decEq OneSidedLocalRule.bot OneSidedLocalRule.bot = isTrue instDecidableEqOneSidedLocalRule.decEq._proof_1
• instDecidableEqOneSidedLocalRule.decEq (OneSidedLocalRule.not a_2) (OneSidedLocalRule.not a_2) = isTrue ⋯
• instDecidableEqOneSidedLocalRule.decEq (OneSidedLocalRule.neg a_2) (OneSidedLocalRule.neg a_2) = isTrue ⋯
• instDecidableEqOneSidedLocalRule.decEq (OneSidedLocalRule.con a_2 a_3) (OneSidedLocalRule.con a_2 a_3) = isTrue ⋯
• instDecidableEqOneSidedLocalRule.decEq (OneSidedLocalRule.nCo a_2 a_3) (OneSidedLocalRule.nCo a_2 a_3) = isTrue ⋯
• instDecidableEqOneSidedLocalRule.decEq (OneSidedLocalRule.box a_2 a_3 a_4) (OneSidedLocalRule.box a_2 a_3 b) = ⋯ ▸ isTrue ⋯
• instDecidableEqOneSidedLocalRule.decEq (OneSidedLocalRule.dia a_2 a_3 a_4) (OneSidedLocalRule.dia a_2 a_3 b) = ⋯ ▸ isTrue ⋯

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

Equations

• instDecidableEqOneSidedLocalRule = instDecidableEqOneSidedLocalRule.decEq

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

Equations

• instReprOneSidedLocalRule = { reprPrec := instReprOneSidedLocalRule.repr }

def instReprOneSidedLocalRule.repr {a✝ : List Formula} {a✝¹ : List (List Formula)} : OneSidedLocalRule a✝ a✝¹ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprOneSidedLocalRule.repr OneSidedLocalRule.bot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OneSidedLocalRule.bot")).group prec✝

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

Loaded Rules

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' α φ)

def instDecidableEqLoadRule.decEq {a✝ : NegLoadFormula} {a✝¹ : List (List Formula × Option NegLoadFormula)} (x✝ x✝¹ : LoadRule a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqLoadRule.decEq (LoadRule.dia a_4) (LoadRule.dia b) = ⋯ ▸ isTrue ⋯
• instDecidableEqLoadRule.decEq (LoadRule.dia' a_4) (LoadRule.dia' b) = ⋯ ▸ isTrue ⋯

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

Equations

• instDecidableEqLoadRule = instDecidableEqLoadRule.decEq

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

Equations

• instReprLoadRule = { reprPrec := instReprLoadRule.repr }

def instReprLoadRule.repr {a✝ : NegLoadFormula} {a✝¹ : List (List Formula × Option NegLoadFormula)} : LoadRule a✝ a✝¹ → ℕ → Std.Format

Equations

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

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.

Local Rules

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.

The YS_def arguments in non-terminal rules enables deriving DecidableEq for LocalRule.

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

def instReprLocalRule.repr {a✝ : Sequent} {a✝¹ : List Sequent} : LocalRule a✝ a✝¹ → ℕ → Std.Format

Equations

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

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

Equations

• instReprLocalRule = { reprPrec := instReprLocalRule.repr }

def instDecidableEqLocalRule.decEq {a✝ : Sequent} {a✝¹ : List Sequent} (x✝ x✝¹ : LocalRule a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqLocalRule.decEq (LocalRule.oneSidedL orule YS_def) (LocalRule.oneSidedR orule_1 YS_def_1) = isFalse ⋯
• instDecidableEqLocalRule.decEq (LocalRule.oneSidedR orule YS_def) (LocalRule.oneSidedL orule_1 YS_def_1) = isFalse ⋯
• instDecidableEqLocalRule.decEq (LocalRule.LRnegL a_2) (LocalRule.LRnegL a_2) = isTrue ⋯
• instDecidableEqLocalRule.decEq (LocalRule.LRnegR a_2) (LocalRule.LRnegR a_2) = isTrue ⋯

instance instDecidableEqLocalRule {a✝ : Sequent} {a✝¹ : List Sequent} : DecidableEq (LocalRule a✝ a✝¹)

Equations

• instDecidableEqLocalRule = instDecidableEqLocalRule.decEq

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

def principalFormulaForLocalRule {X : Sequent} {YS : List Sequent} : LocalRule X YS → AnyFormula

Helper originally written for Lemma 6.14 but currently unused.

Equations

• principalFormulaForLocalRule (LocalRule.oneSidedL OneSidedLocalRule.bot YS_def_2) = AnyFormula.normal Formula.bottom
• principalFormulaForLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.con φ ψ) YS_def_2) = AnyFormula.normal (φ ⋀ ψ)
• principalFormulaForLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.not φ) YS_def_2) = AnyFormula.normal φ
• principalFormulaForLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.neg φ) YS_def_2) = AnyFormula.normal (~~φ)
• principalFormulaForLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.nCo φ ψ) YS_def_2) = AnyFormula.normal (~(φ ⋀ ψ))
• principalFormulaForLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.dia α φ notAtom) YS_def_2) = AnyFormula.normal (~⌈α⌉φ)
• principalFormulaForLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.box α φ notAtom) YS_def_2) = AnyFormula.normal (⌈α⌉φ)
• principalFormulaForLocalRule (LocalRule.oneSidedR OneSidedLocalRule.bot YS_def_2) = AnyFormula.normal Formula.bottom
• principalFormulaForLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.con φ ψ) YS_def_2) = AnyFormula.normal (φ ⋀ ψ)
• principalFormulaForLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.not φ) YS_def_2) = AnyFormula.normal φ
• principalFormulaForLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.neg φ) YS_def_2) = AnyFormula.normal (~~φ)
• principalFormulaForLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.nCo φ ψ) YS_def_2) = AnyFormula.normal (~(φ ⋀ ψ))
• principalFormulaForLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.dia α φ notAtom) YS_def_2) = AnyFormula.normal (~⌈α⌉φ)
• principalFormulaForLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.box α φ notAtom) YS_def_2) = AnyFormula.normal (⌈α⌉φ)
• principalFormulaForLocalRule (LocalRule.LRnegL φ) = AnyFormula.normal φ
• principalFormulaForLocalRule (LocalRule.LRnegR φ) = AnyFormula.normal φ
• principalFormulaForLocalRule (LocalRule.loadedL φ lrule YS_def) = AnyFormula.loaded φ
• principalFormulaForLocalRule (LocalRule.loadedR φ lrule YS_def) = AnyFormula.loaded φ

theorem oneSidedL_preserves_right {LRO : Sequent} {Lcond : List Formula} (Lpreproof : Lcond ⊆ LRO.L) {Lres : List (List Formula)} (orule : OneSidedLocalRule Lcond Lres) {YS : List Sequent} (YS_def : YS = List.map (fun (res : List Formula) => (res, ∅, none)) Lres) (c : Sequent) : c ∈ applyLocalRule (LocalRule.oneSidedL orule YS_def) LRO → c.right = LRO.right

theorem oneSidedR_preserves_left {LRO : Sequent} {Rcond : List Formula} (Rpreproof : Rcond ⊆ LRO.R) {Rres : List (List Formula)} (orule : OneSidedLocalRule Rcond Rres) {YS : List Sequent} (YS_def : YS = List.map (fun (res : List Formula) => (∅, res, none)) Rres) (c : Sequent) : c ∈ applyLocalRule (LocalRule.oneSidedR orule YS_def) LRO → c.left = LRO.left

theorem oneSidedL_sat_down (LRO : Sequent) {Lcond : List Formula} (Lpreproof : Lcond ⊆ LRO.L) {Lres : List (List Formula)} (orule : OneSidedLocalRule Lcond Lres) {YS : List Sequent} (YS_def : YS = List.map (fun (res : List Formula) => (res, ∅, none)) Lres) {X : List Formula} (LX_sat : HasSat.satisfiable (LRO.left ∪ X)) : ∃ c ∈ applyLocalRule (LocalRule.oneSidedL orule YS_def) LRO, HasSat.satisfiable (c.left ∪ X)

theorem oneSidedR_sat_down (LRO : Sequent) {Rcond : List Formula} (Rpreproof : Rcond ⊆ LRO.R) {Rres : List (List Formula)} (orule : OneSidedLocalRule Rcond Rres) {YS : List Sequent} (YS_def : YS = List.map (fun (res : List Formula) => (∅, res, none)) Rres) {X : List Formula} (RX_sat : HasSat.satisfiable (LRO.right ∪ X)) : ∃ c ∈ applyLocalRule (LocalRule.oneSidedR orule YS_def) LRO, HasSat.satisfiable (c.right ∪ X)

theorem loadedL_preserves_right {LRO : Sequent} (χ : LoadFormula) (Opreproof : LRO.O = some (Sum.inl (~'χ))) {ress : List (List Formula × Option NegLoadFormula)} (lrule : LoadRule (~'χ) ress) {YS : List Sequent} (YS_def : YS = List.map (fun (x : List Formula × Option NegLoadFormula) => match x with | (X, o) => (X, ∅, Option.map Sum.inl o)) ress) (c : Sequent) : c ∈ applyLocalRule (LocalRule.loadedL χ lrule YS_def) LRO → c.right = LRO.right

Applying a LoadRule on the left will leave the right unchanged.

theorem loadedR_preserves_left {LRO : Sequent} (χ : LoadFormula) (Opreproof : LRO.O = some (Sum.inr (~'χ))) {ress : List (List Formula × Option NegLoadFormula)} (lrule : LoadRule (~'χ) ress) {YS : List Sequent} (YS_def : YS = List.map (fun (x : List Formula × Option NegLoadFormula) => match x with | (X, o) => (∅, X, Option.map Sum.inr o)) ress) (c : Sequent) : c ∈ applyLocalRule (LocalRule.loadedR χ lrule YS_def) LRO → c.left = LRO.left

Applying a LoadRule on the right will leave the left unchanged.

theorem loadedL_sat_down (LRO : Sequent) (χ : LoadFormula) (Opreproof : LRO.O = some (Sum.inl (~'χ))) {ress : List (List Formula × Option NegLoadFormula)} (lrule : LoadRule (~'χ) ress) {YS : List Sequent} (YS_def : YS = List.map (fun (x : List Formula × Option NegLoadFormula) => match x with | (X, o) => (X, ∅, Option.map Sum.inl o)) ress) {X : List Formula} (LX_sat : HasSat.satisfiable (LRO.left ∪ X)) : ∃ c ∈ applyLocalRule (LocalRule.loadedL χ lrule YS_def) LRO, HasSat.satisfiable (c.left ∪ X)

Applying a LoadRule on the left preserves satisfiability of the left, even together with any other list of formulas as context.

theorem loadedR_sat_down (LRO : Sequent) (χ : LoadFormula) (Opreproof : LRO.O = some (Sum.inr (~'χ))) {ress : List (List Formula × Option NegLoadFormula)} (lrule : LoadRule (~'χ) ress) {YS : List Sequent} (YS_def : YS = List.map (fun (x : List Formula × Option NegLoadFormula) => match x with | (X, o) => (∅, X, Option.map Sum.inr o)) ress) {X : List Formula} (RX_sat : HasSat.satisfiable (LRO.right ∪ X)) : ∃ c ∈ applyLocalRule (LocalRule.loadedR χ lrule YS_def) LRO, HasSat.satisfiable (c.right ∪ X)

Applying a LoadRule on the right preserves satisfiability of the right, even together with any other list of formulas as context.

Local Rule Applications

structure LocalRuleApp : Type

A local rule application going from ⟨L,R,O⟩ to C consists of a local rule lr replacing ⟨Lcond, Rcond, Ocond⟩ by ress and proofs that ⟨Lcond, Rcond, Ocond⟩ is a subsequent of ⟨L,R,O⟩ and that C are the results of applying lr to ⟨L,R,O⟩.

• L : List Formula
• R : List Formula
• O : Olf
• Lcond : List Formula
• Rcond : List Formula
• Ocond : Olf
• ress : List Sequent
• lr : LocalRule (self.Lcond, self.Rcond, self.Ocond) self.ress
• C : List Sequent
• hC : self.C = applyLocalRule self.lr (self.L, self.R, self.O)
• preconditionProof : self.Lcond.Subperm self.L ∧ self.Rcond.Subperm self.R ∧ self.Ocond ⊆ self.O

instance instDecidableEqLocalRuleApp : DecidableEq LocalRuleApp

Equations

• instDecidableEqLocalRuleApp = instDecidableEqLocalRuleApp.decEq

def instDecidableEqLocalRuleApp.decEq (x✝ x✝¹ : LocalRuleApp) : Decidable (x✝ = x✝¹)

Equations

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

@[reducible, inline]

abbrev LocalRuleApp.X (lra : LocalRuleApp) : Sequent

Equations

• lra.X = (lra.L, lra.R, lra.O)

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

Any local rule application is sound and invertible.

theorem nonbasic_of_localRuleApp (lra : LocalRuleApp) : ¬lra.X.basic

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

def localRuleApp_of_nonbasic_in_L (L R : List Formula) (O : Olf) (f : Formula) (f_in : f ∈ L) (f_nonBas : f.basic = false) : { lra : LocalRuleApp // lra.X = (L, R, O) }

For a given non-basic formula in the left list L, construct a LocalRuleApp using an appropriate OneSidedLocalRule.

Equations

• One or more equations did not get rendered due to their size.
• localRuleApp_of_nonbasic_in_L L R O (·n) f_in_2 f_nonBas_2 = ⋯.elim
• localRuleApp_of_nonbasic_in_L L R O (~Formula.bottom) f_in_3 f_nonBas_3 = ⋯.elim
• localRuleApp_of_nonbasic_in_L L R O (~·n) f_in_3 f_nonBas_3 = ⋯.elim

def localRuleApp_of_nonbasic_in_R (L R : List Formula) (O : Olf) (f : Formula) (f_in : f ∈ R) (f_nonBas : f.basic = false) : { lra : LocalRuleApp // lra.X = (L, R, O) }

For a given non-basic formula in the right list R, construct a LocalRuleApp using an appropriate OneSidedLocalRule.

Equations

• One or more equations did not get rendered due to their size.
• localRuleApp_of_nonbasic_in_R L R O (·n) f_in_2 f_nonBas_2 = ⋯.elim
• localRuleApp_of_nonbasic_in_R L R O (~Formula.bottom) f_in_3 f_nonBas_3 = ⋯.elim
• localRuleApp_of_nonbasic_in_R L R O (~·n) f_in_3 f_nonBas_3 = ⋯.elim

theorem basic_iff_noLocalRuleApp {Y : Sequent} : Y.basic ↔ ¬∃ (lra : LocalRuleApp), lra.X = Y

A sequent is basic iff no local rule can be applied. Note that in the paper (L+) and (L-) are also local rules and had to be excluded here, but here in the Lean formalization they are PdlRules anyway.

Local rule applications preserve atomic formulas

theorem LocalRuleApp.preserve_bottom_down (lra : LocalRuleApp) (Y : Sequent) : Y ∈ lra.C → ⊥ ∈ lra.X.bothSides → ⊥ ∈ Y.bothSides

theorem LocalRuleApp.preserve_atom_down (lra : LocalRuleApp) (Y : Sequent) : Y ∈ lra.C → ∀ (p : ℕ), ·p ∈ lra.X.bothSides → ·p ∈ Y.bothSides

theorem LocalRuleApp.preserve_neg_atom_down (lra : LocalRuleApp) (Y : Sequent) : Y ∈ lra.C → ∀ (p : ℕ), ~·p ∈ lra.X.bothSides → ~·p ∈ Y.bothSides

theorem LocalRuleApp.preserve_local_atom_down (lra : LocalRuleApp) (Y : Sequent) : Y ∈ lra.C → ∀ (f : Formula), (f = ⊥ ∨ ∃ (p : ℕ), f = ·p ∨ f = ~·p) → f ∈ lra.X.bothSides → f ∈ Y.bothSides

theorem mem_child_left_of_pairUnload_mem {w : List Formula} {o : Option NegLoadFormula} {f : Formula} (h : f ∈ pairUnload (w, o)) : f ∈ w ∨ f ∈ Olf.L (Option.map Sum.inl o)

theorem mem_child_right_of_pairUnload_mem {w : List Formula} {o : Option NegLoadFormula} {f : Formula} (h : f ∈ pairUnload (w, o)) : f ∈ w ∨ f ∈ Olf.R (Option.map Sum.inr o)

theorem loaded_unfold_child_closes_left {α : Program} {χ : LoadFormula} {w : List Formula} {o : Option NegLoadFormula} (h : (w, o) ∈ unfoldDiamondLoaded α χ) : ∃ Fδ ∈ Dset α, ∀ f ∈ Yset Fδ χ.unload, f ∈ w ∨ f ∈ Olf.L (Option.map Sum.inl o)

theorem loaded_unfold'_child_closes_left {α : Program} {φ : Formula} {w : List Formula} {o : Option NegLoadFormula} (h : (w, o) ∈ unfoldDiamondLoaded' α φ) : ∃ Fδ ∈ Dset α, ∀ f ∈ Yset Fδ φ, f ∈ w ∨ f ∈ Olf.L (Option.map Sum.inl o)

theorem loaded_unfold_child_closes_right {α : Program} {χ : LoadFormula} {w : List Formula} {o : Option NegLoadFormula} (h : (w, o) ∈ unfoldDiamondLoaded α χ) : ∃ Fδ ∈ Dset α, ∀ f ∈ Yset Fδ χ.unload, f ∈ w ∨ f ∈ Olf.R (Option.map Sum.inr o)

theorem loaded_unfold'_child_closes_right {α : Program} {φ : Formula} {w : List Formula} {o : Option NegLoadFormula} (h : (w, o) ∈ unfoldDiamondLoaded' α φ) : ∃ Fδ ∈ Dset α, ∀ f ∈ Yset Fδ φ, f ∈ w ∨ f ∈ Olf.R (Option.map Sum.inr o)

theorem LocalRuleApp.formula_preserved_or_expanded (lra : LocalRuleApp) {Y : Sequent} (hY : Y ∈ lra.C) (f : Formula) : f ∈ lra.X.bothSides → f ∈ Y.bothSides ∨ ∀ (φ ψ : Formula) (α : Program), (f = ~~φ → φ ∈ Y.bothSides) ∧ (f = φ ⋀ ψ → φ ∈ Y.bothSides ∧ ψ ∈ Y.bothSides) ∧ (f = ~(φ ⋀ ψ) → ~φ ∈ Y.bothSides ∨ ~ψ ∈ Y.bothSides) ∧ ((f = ⌈α⌉φ) → ∃ (l : TP α), ((Bset α l φ).all fun (x : Formula) => decide (x ∈ Y.bothSides)) = true) ∧ ((f = ~⌈α⌉φ) → ∃ Fδ ∈ Dset α, ((Yset Fδ φ).all fun (x : Formula) => decide (x ∈ Y.bothSides)) = true)

Every formula at the source of a local rule is either retained by a chosen child or is the principal formula and has the closure data required for saturatedness in that child.

Saturated and Locally Consistent Sets of Formulas

def saturated : Finset Formula → Prop

A set of formulas is saturated if it is closed under: removing double negations, splitting (negated) conjunctions, unfolding boxes using any test profile, and unfolding diamonds using H. Part of Def 6.2

Equations

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

theorem Sequent.basic_then_saturated {X : Sequent} : X.basic → saturated X.toFinset

Any basic sequent is also saturated.

def locallyConsistent (X : Finset Formula) : Prop

A set of formulas is lcoally consistent iff it does not contain ⊥ and for all atoms p ∈ X we do not have ~p ∈ X. Part of Def 6.2

Equations

• locallyConsistent X = (⊥ ∉ X.val ∧ ∀ (pp : ℕ), ·pp ∈ X.val → ~·pp ∉ X.val)

theorem Sequent.basic_to_locallyConsistent {X : Sequent} (bas : X.basic) : locallyConsistent X.toFinset

theorem LocalRuleApp.preserve_saturated_up (lra : LocalRuleApp) (Y : Sequent) : Y ∈ lra.C → ∀ (rest : List Sequent), Y ∈ rest → saturated (List.map Sequent.bothSides rest).flatten.toFinset → saturated (List.map Sequent.bothSides (lra.X :: rest)).flatten.toFinset

LocalRuleApp preserves saturatedness backwards.

theorem LocalRuleApp.wForms_negBox_preserved_or_unfolded (lra : LocalRuleApp) {Y : Sequent} (hY : Y ∈ lra.C) {α : Program} {φ : Formula} (h : (WhateverFormula.any ∘ AnyFormula.normal) (~⌈α⌉φ) ∈ lra.X.wForms) : (WhateverFormula.any ∘ AnyFormula.normal) (~⌈α⌉φ) ∈ Y.wForms ∨ ∃ Fδ ∈ Dset α, ((Yset Fδ φ).all fun (f : Formula) => decide ((WhateverFormula.any ∘ AnyFormula.normal) f ∈ Y.wForms)) = true

A free diamond at the source of a local rule application is either kept in the chosen child, or it is the principal formula, and then the child contains one of its unfoldings. Analogous to LocalRuleApp.formula_preserved_or_expanded, but for Sequent.wForms, i.e. here we also know that the formulas in the child occur unloaded. (This is why we cannot obtain this lemma from LocalRuleApp.formula_preserved_or_expanded: the latter uses Sequent.bothSides, where a formula may also come from unloading the loaded formula of a sequent.)

theorem LocalRuleApp.wForms_negLoad_preserved_or_unfolded (lra : LocalRuleApp) {Y : Sequent} (hY : Y ∈ lra.C) {nlf : NegLoadFormula} (h : WhateverFormula.negLoad nlf ∈ lra.X.wForms) : WhateverFormula.negLoad nlf ∈ Y.wForms ∨ ∃ (ress : List (List Formula × Option NegLoadFormula)), Nonempty (LoadRule nlf ress) ∧ ∃ Fo ∈ ress, (Fo.1.all fun (f : Formula) => decide ((WhateverFormula.any ∘ AnyFormula.normal) f ∈ Y.wForms)) = true ∧ (Fo.2.toList.all fun (nl : NegLoadFormula) => decide (WhateverFormula.negLoad nl ∈ Y.wForms)) = true

A loaded diamond at the source of a local rule application is either kept in the chosen child, or it is the principal formula, and then the child contains one of the results of the LoadRule that was applied to it. This is the loaded analogue of LocalRuleApp.wForms_negBox_preserved_or_unfolded.

theorem LoadRule.eq_unfoldDiamondLoaded {α : Program} {χ : LoadFormula} {ress : List (List Formula × Option NegLoadFormula)} (lr : LoadRule (~'⌊α⌋AnyFormula.loaded χ) ress) : ress = unfoldDiamondLoaded α χ

The only LoadRule applicable to ~'⌊α⌋χ for a loaded χ is LoadRule.dia.

theorem LoadRule.eq_unfoldDiamondLoaded' {α : Program} {φ : Formula} {ress : List (List Formula × Option NegLoadFormula)} (lr : LoadRule (~'⌊α⌋AnyFormula.normal φ) ress) : ress = unfoldDiamondLoaded' α φ

The only LoadRule applicable to ~'⌊α⌋φ for a normal φ is LoadRule.dia'.

theorem LocalRuleApp.preserve_basic_down (lra : LocalRuleApp) (Y : Sequent) : Y ∈ lra.C → ∀ (f : Formula), f.basic = true → f ∈ lra.X.bothSides → f ∈ Y.bothSides

Local rule applications preserve basic formulas: no local rule with children can have a basic formula as its principal formula. Note that ⊥ is not basic, for that case see LocalRuleApp.preserve_bottom_down.

theorem LocalRuleApp.preserve_free (lra : LocalRuleApp) (hfree : lra.O = none) (Y : Sequent) : Y ∈ lra.C → Y.O = none

Local rules never load a formula: if the sequent we apply a local rule to is free, then so are all children. (The rules loadedL and loadedR are not applicable to a free sequent, and all other local rules leave the Olf component unchanged.)