Four facts about proper clusters (used for Lemma 10.7)

This file proves the four facts about the cluster C and the steps stepOf Δ of its quasi-tableau that the proof of Lemma 10.7 in Pdl.Interpolation.ClusterSatDown uses:

• LoadedCluster.isRightLoaded_of_mem_lambdaTwo: all Δ ∈ Λ₂[C] are loaded on the right (Lemma 9.4 (a)),
• LoadedCluster.stepOf_lt_Sequent: at a non-basic Δ ∈ Λ₂[C] the successors are strictly smaller in the Dershowitz-Manna ordering lt_Sequent used for the termination of local tableaux,
• LoadedCluster.basicStep_of: the modal step at a basic Δ ∈ Λ₂[C] (Lemma 9.7 (e)),
• LoadedCluster.nonBasicStep_of: the local step at a non-basic Δ ∈ Λ₂[C], with the witness distance preserved — the local invertibility of the rules together with Lemma 10.5 (h).

They only use properness of the cluster, via Lemma 9.7 (d), i.e. LoadedCluster.exists_right_of_proper from Pdl.Interpolation.ClusterFacts.

Splitting a boxed loaded formula

theorem LoadFormula.boxes_split (δ : List Program) (χ : LoadFormula) : (⌊⌊δ⌋⌋χ).split = (δ ++ χ.split.1, χ.split.2)

Prefixing a loaded formula with boxes prefixes its split.

Right rules applied to the right component only

A local rule that acts on the right component can also be applied to the sequent with an empty left component. This is LocalRuleApp.toContext from Pdl.Uniformity, and it lets us transfer both the decrease in the Dershowitz-Manna ordering and the local invertibility from the whole sequent to its right component.

theorem LocalRuleApp.left_nil_of_mem_ress {lra : LocalRuleApp} (h : lra.isRightRule = true) (Z : Sequent) : Z ∈ lra.ress → Z.1 = ∅

The results of a local rule acting on the right have an empty left component.

theorem LocalRuleApp.C_left_nil {lra : LocalRuleApp} (h : lra.isRightRule = true) (hL : lra.L = ∅) (Y : Sequent) : Y ∈ lra.C → Y.1 = ∅

If the premise of a right rule has an empty left component then so have all conclusions.

def LocalRuleApp.rightOnlyApp (lra : LocalRuleApp) : LocalRuleApp

The rule application lra, applied to the right component of its premise only.

Equations

• lra.rightOnlyApp = lra.toContext lra.X.rightOnly

@[simp]

theorem LocalRuleApp.rightOnlyApp_isRightRule (lra : LocalRuleApp) : lra.rightOnlyApp.isRightRule = lra.isRightRule

theorem LocalRuleApp.rightOnlyApp_X {lra : LocalRuleApp} (h : lra.isRightRule = true) : lra.rightOnlyApp.X = lra.X.rightOnly

theorem LocalRuleApp.rightOnlyApp_C {lra : LocalRuleApp} (h : lra.isRightRule = true) : lra.rightOnlyApp.C = Finset.image Sequent.rightOnly lra.C

theorem LocalRuleApp.rightOnly_lt_Sequent {lra : LocalRuleApp} (h : lra.isRightRule = true) (Y : Sequent) : Y ∈ lra.C → lt_Sequent Y.rightOnly lra.X.rightOnly

The right components of the conclusions of a right rule are strictly smaller than the right component of the premise, in the Dershowitz-Manna ordering.

Satisfaction of a sequent with an empty left component

theorem models_iff_right {W : Type} {M : KripkeModel W} {w : W} {X : Sequent} (hL : X.left = ∅) : (M, w) ⊨ X ↔ ∀ φ ∈ X.right, evaluate M w φ

The local step, with the witness distance

This is the heart of the case k(x) = 3 with Δ_x not basic in the proof of Lemma 10.7: when a right local rule is applied to a sequent that holds at v, one of the conclusions holds at v with the same witness distance. If the rule acts on an unloaded formula then the loaded formula, and hence the witness distance, is unchanged. If it acts on the loaded formula then the rule is (◇)₂ and the claim is Lemma 10.5 (h), existsD_of_true_diamond.

theorem witDist_eq_of_loadedSplit {W : Type} {M : KripkeModel W} {v : W} {Δ : Sequent} {γ : List Program} {ψ : Formula} (h : Δ.loadedSplit = (γ, ψ)) : witDist M v Δ = ⨅ (w : { w : W // evaluate M w (~ψ) }), distance_list M v (↑w) γ

The witness distance, computed from the split of the loaded formula.

theorem LocalRuleApp.rightRule_sat_witDist {lra : LocalRuleApp} (hr : lra.isRightRule = true) {W : Type} {M : KripkeModel W} {v : W} (hv : ∀ φ ∈ lra.X.right, evaluate M v φ) : ∃ Y ∈ lra.C, (∀ φ ∈ Y.right, evaluate M v φ) ∧ witDist M v Y = witDist M v lra.X

The four facts about proper clusters

theorem LoadedCluster.isRightLoaded_of_mem_lambdaTwo {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {Δ : Sequent} (hΔ : Δ ∈ C.lambdaTwo) : Δ.isRightLoaded

Every label in Λ₂[C] is loaded on the right, i.e. Lemma 9.4 (a).

theorem LoadedCluster.exists_lra_stepOf {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {Δ : Sequent} (hne : C.nodesWithFineRight Δ ≠ []) (hb : ¬Δ.basic) : ∃ (lra : LocalRuleApp), lra.isRightRule = true ∧ lra.X.rightOnly = Δ ∧ C.stepOf Δ = Finset.image Sequent.rightOnly lra.C

If a right rule is applied at some node with right component Δ, then the steps stepOf Δ are the right components of the conclusions of the local rule applied there.

Note that stepOf is a list while LocalRuleApp.C is a Finset, so we compare with lra.C.toList, matching FinePathIn.lra?_spec.

theorem LoadedCluster.stepOf_lt_Sequent {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : Δ ∈ C.lambdaTwo → ¬Δ.basic → ∀ Y ∈ C.stepOf Δ, lt_Sequent Y Δ

At a non-basic Δ ∈ Λ₂[C] the step of the quasi-tableau strictly decreases the Dershowitz-Manna ordering.

theorem LoadedCluster.basicStep_of {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : Δ ∈ C.lambdaTwo → Δ.basic → ∃ (A : ℕ) (Y : Sequent), C.stepOf Δ = {Y} ∧ Δ.loadedProg = ·A ∧ Δ.loadedProgs = ·A :: Y.loadedProgs ∧ Y.loadedFma = Δ.loadedFma ∧ ∀ (W : Type) (M : KripkeModel W) (w v : W), (∀ φ ∈ Δ.right, evaluate M w φ) → relate M (·A) w v → evaluate M v (~⌈⌈Y.loadedProgs⌉⌉Y.loadedFma) → ∀ φ ∈ Y.right, evaluate M v φ

The modal step at a basic Δ ∈ Λ₂[C].

theorem LoadedCluster.nonBasicStep_of {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Δ : Sequent) : Δ ∈ C.lambdaTwo → ¬Δ.basic → ∀ (W : Type) (M : KripkeModel W) (v : W), (∀ φ ∈ Δ.right, evaluate M v φ) → ∃ (i : ℕ) (hi : i < (C.stepOfL Δ).length), (∀ φ ∈ (C.stepOfL Δ)[i].right, evaluate M v φ) ∧ witDist M v (C.stepOfL Δ)[i] = witDist M v Δ

The local step at a non-basic Δ ∈ Λ₂[C].