The facts about a proper cluster used for Lemma 10.7

This file proves the four fields of LoadedCluster.SatDownFacts from Pdl.ClusterSatDown, i.e. everything that the proof of Lemma 10.7 assumes about the cluster C and the steps stepOf Δ of its quasi-tableau:

• rightLoaded: all Δ ∈ Λ₂[C] are loaded on the right (Lemma 9.4 (a)),
• stepLT: at a non-basic Δ ∈ Λ₂[C] the successors are strictly smaller in the Dershowitz-Manna ordering lt_Sequent used for the termination of local tableaux,
• basicStep: the modal step at a basic Δ ∈ Λ₂[C] (Lemma 9.7 (e)),
• nonBasicStep: 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).

The main result is LoadedCluster.satDownFacts. Its only hypothesis is Lemma 9.7 (d), i.e. that C^R_Δ is non-empty for Δ ∈ Λ₂[C], which in Pdl.ClusterInterpolation is LoadedCluster.exists_right_of_proper.

We import Pdl.Uniformity and not Pdl.ClusterInterpolation, because the latter is where LoadedCluster.satDownFacts gets used; the helper lemmas about right rules that we need are the copies in the Uniformity namespace.

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.

theorem LocalRuleApp.C_left_eq_nil {lra : LocalRuleApp} (h : lra.isRightRule = true) (hL : lra.X.left = ∅) (Y : Sequent) : Y ∈ lra.C → Y.left = ∅

If the premise of a right rule is not loaded on the left and has an empty left component, then the same holds for all conclusions.

noncomputable 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 fields

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 Δ

The stepLT field: 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) (hER : ∀ Δ ∈ C.lambdaTwo, C.nodesWithFineRight Δ ≠ []) (Δ : 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 basicStep field: the modal step at a basic Δ ∈ Λ₂[C].

theorem LoadedCluster.nonBasicStep_of {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (hER : ∀ Δ ∈ C.lambdaTwo, C.nodesWithFineRight Δ ≠ []) (Δ : 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 nonBasicStep field: the local step at a non-basic Δ ∈ Λ₂[C].

theorem LoadedCluster.satDownFacts {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (hER : ∀ Δ ∈ C.lambdaTwo, C.nodesWithFineRight Δ ≠ []) : C.SatDownFacts

All facts of SatDownFacts, from Lemma 9.7 (d).