Documentation

Pdl.Local.Soundness

Local Lemmas for Soundness (part of Section 5) #

source
theorem 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 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 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 LocalRuleApp.preserve_in_side_atomic (lra : LocalRuleApp) {α : Program} {ξ : AnyFormula} {side : Side} (α_atom : α.isAtomic) (h : (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side lra.X) (Y : Sequent) :
Y ∈ lra.C → (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side 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 atomicLocalLoadedDiamond (α : Program) {X : Sequent} (ltab : LocalTableau X) (α_atom : α.isAtomic) (ξ : AnyFormula) {side : Side} (negLoad_in : (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side X) (Y : Sequent) :
Y ∈ endNodesOf ltab → (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side 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 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 lra_preserves_free {Z : Sequent} (lra : LocalRuleApp) (Z_in : Z ∈ lra.C) (X_free : lra.X.isFree) :
Z.isFree
source
theorem endNodesOf_free_are_free {X Y : Sequent} (ltX : LocalTableau X) (h : X.isFree) (Y_in : Y ∈ endNodesOf ltX) :
Y.isFree
source
theorem 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 : (M, v) ⊨ X) (φ : Formula) {side : Side} (negLoad_in : (~''(AnyFormula.loadBoxes αs (AnyFormula.normal φ))).in_side side X) (no_other_loading : (X.without (~''(AnyFormula.loadBoxes αs (AnyFormula.normal φ)))).isFree) (w_nξ : (M, w) ⊨ ~''(AnyFormula.normal φ)) :
∃ Y ∈ endNodesOf ltab, (M, v) ⊨ Y ∧ (Y.isFree ∨ ∃ (F : List Formula) (γ : List Program), (~''(AnyFormula.loadBoxes γ (AnyFormula.normal φ))).in_side side Y ∧ relateSeq M γ v w ∧ distance_list M v w γ = distance_list M v w αs ∧ (M, v) ⊨ F ∧ (F, γ) ∈ Dl αs ∧ (Y.without (~''(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.