Documentation

LeanPool.PDL.Local.Soundness

Local Lemmas for Soundness (part of Section 6) #

source
theorem PDL.Sequent.mem_toFinset_of_mem_left {L R : Finset Formula} {O : Olf} {f : Formula} (h : f ∈ L) :
f ∈ toFinset (L, R, O)

Formulas on the left of a sequent are in Sequent.toFinset.

source
theorem PDL.Sequent.mem_toFinset_of_mem_right {L R : Finset Formula} {O : Olf} {f : Formula} (h : f ∈ R) :
f ∈ toFinset (L, R, O)

Formulas on the right of a sequent are in Sequent.toFinset.

source
theorem PDL.mem_sup_endNodesOf {C : Finset Sequent} (next : (Y : Sequent) → Y ∈ C → LocalTableau Y) {Z : Sequent} (Z_in : Z ∈ C) {Y : Sequent} (h : Y ∈ endNodesOf (next Z Z_in)) :
Y ∈ (Finset.image (fun (x : ↥C) => endNodesOf (next ↑x ⋯)) C.attach).sup id

Helper to show that an end node of a child tableau is an end node of the whole tableau, in the unfolded form of endNodesOf for LocalTableau.byLocalRule.

source
theorem PDL.LocalRuleApp.preserve_in_side_atomic (lra : LocalRuleApp) {α : Program} {ξ : AnyFormula} {side : Side} (α_atom : α.isAtomic) (h : (AnyNegFormula.neg (AnyFormula.loaded (LoadFormula.box α ξ))).inSide side lra.X) (Y : Sequent) :
Y ∈ lra.C → (AnyNegFormula.neg (AnyFormula.loaded (LoadFormula.box α ξ))).inSide side Y

An atomic loaded diamond cannot be the principal formula of a local rule, hence any local rule application preserves it, and on the same side.

source
theorem PDL.atomicLocalLoadedDiamond (α : Program) {X : Sequent} (ltab : LocalTableau X) (α_atom : α.isAtomic) (ξ : AnyFormula) {side : Side} (negLoad_in : (AnyNegFormula.neg (AnyFormula.loaded (LoadFormula.box α ξ))).inSide side X) (Y : Sequent) :
Y ∈ endNodesOf ltab → (AnyNegFormula.neg (AnyFormula.loaded (LoadFormula.box α ξ))).inSide side Y

Helper for loadedDiamondPaths. If α is atomic, and ~''(⌊α⌋ξ) is in X, then for any local tableau ltab for X, the same loaded diamond must still be in all endNodesOf ltab, on the same side.

source
@[simp]
theorem PDL.next_exists_avoid_def_l {Y : Sequent} {B : Finset Sequent} (next : (Y : Sequent) → Y ∈ B → LocalTableau Y) :
(∃ (l : Finset Sequent), (∃ (a : Sequent) (h : a ∈ B), endNodesOf (next a h) = l) ∧ Y ∈ l) ↔ ∃ (Z : Sequent) (Z_in : Z ∈ B), Y ∈ endNodesOf (next Z Z_in)
source
theorem PDL.lra_preserves_free {Z : Sequent} (lra : LocalRuleApp) (Z_in : Z ∈ lra.C) (X_free : lra.X.isFree) :
Z.isFree
source
theorem PDL.endNodesOf_free_are_free {X Y : Sequent} (ltX : LocalTableau X) (h : X.isFree) (Y_in : Y ∈ endNodesOf ltX) :
Y.isFree
source
theorem PDL.localLoadedDiamondList (αs : List Program) {X : Sequent} (ltab : LocalTableau X) {W : Type} {M : KripkeModel W} {v w : W} (v_αs_w : relateSeq M αs v w) (v_t : vDash.SemImplies (M, v) X) (φ : Formula) {side : Side} (negLoad_in : (AnyNegFormula.neg (AnyFormula.loadBoxes αs (AnyFormula.normal φ))).inSide side X) (no_other_loading : (X.without (AnyNegFormula.neg (AnyFormula.loadBoxes αs (AnyFormula.normal φ)))).isFree) (w_nξ : vDash.SemImplies (M, w) (AnyNegFormula.neg (AnyFormula.normal φ))) :
∃ Y ∈ endNodesOf ltab, vDash.SemImplies (M, v) Y ∧ (Y.isFree ∨ ∃ (F : List Formula) (γ : List Program), (AnyNegFormula.neg (AnyFormula.loadBoxes γ (AnyFormula.normal φ))).inSide side Y ∧ relateSeq M γ v w ∧ distanceList M v w γ = distanceList M v w αs ∧ vDash.SemImplies (M, v) F ∧ (F, γ) ∈ Dl αs ∧ (Y.without (AnyNegFormula.neg (AnyFormula.loadBoxes γ (AnyFormula.normal φ)))).isFree)

Helper to deal with local tableau in loadedDiamondPaths. Takes a list of programs and φ, i.e. we want access to all loaded boxes.