Satisfiability down the quasi-tableau, and the right half of the correctness of θ_r #
This file continues the development of Pdl.ClusterRho with
- Lemma 10.6: between a companion and its repeat there is a basic node,
- Lemma 10.7: if
Δ_x, ι_xis satisfiable then so isΔ_z, ι_zfor somez ∈ cycs(x), - Lemma 10.8:
Γ₂ ⊨ ¬θ_r.
Definition 10.4 (the distance d_α) and Lemma 10.5 (its properties) are in Pdl.Distance,
where they are numbered 7.47. The auxiliary notions used below — the evaluation evalQ of
Q-formulas with an assignment, the witness distance witDist, and BasicBetween — are in
Pdl.EvalQ.
Lemma 10.6 #
If x is a repeat in Q then the path from c(x) to x passes through a node with a
basic label.
The proof in the paper claims that nodes of type 1 can only succeed nodes of type 3 with a
basic label; that is not the case, see Definition 9.8. What is true, and what we use here,
is that the label of a node of type 3 with a non-basic label strictly decreases when
passing to the children: the rule applied there is a local rule. Hence if no basic node
occurred between c(x) and x then Δ_x would be strictly smaller than Δ_{c(x)},
contradicting Δ_x = Δ_{c(x)}.
The possible addresses inside a node of type 1 that is not a leaf: the node itself, its child of type 2, its grandchild of type 3, or an address inside one of the subtrees below the node of type 3.
Helper lemmas about prefixes #
Along the subtree of a node of type 1 the measure of the label does not increase, unless a node of type 3 with a basic label is passed on the way.
Lemma 10.6, by induction along the construction of the quasi-tableau: if z is a
repeat with companion c then there is a node of type 3 with a basic label between c
and z.
Lemma 10.6: if z is a repeat in Q with companion c(z), then the path from
c(z) to z passes through a node of type 3 whose label is basic.
The proof in the paper argues that a repeat is of type 1, and that in Q a node of type 1
can only succeed a node of type 3 with a basic label. In the construction of Q
(Definition 9.8) the children of a node of type 3 are of type 1 also when the label is
not basic, so that argument does not apply directly. We use instead that the labels of
the successors of a non-basic node are smaller in some measure m, so a repeat — which
has the same label as its companion — cannot be reached from its companion by non-basic
steps only.
Assumptions about the steps of the quasi-tableau #
Just like LoadedCluster.PaperFacts for Lemma 10.3, the proof of Lemma 10.7 uses facts
about the tableau tab and the sequents Λ₂[C] that are not (yet) available in this Lean
development. They are collected here in one record.
Facts about the cluster C used in the proof of Lemma 10.7.
rightLoadedsays that allΔ ∈ Λ₂[C]carry their loaded formula on the right; this is the standing assumption of Section 9 thatΓ₂is the loaded side.stepLTprovides a decreasing measure needed for Lemma 10.6 (repeat_basicBetween). A local rule applied to an unloaded formula, or the rule(◇)₂applied to the loaded formula, strictly decreases the DM ordering on sequents.basicStepdescribes the modal step at a basicΔ ∈ Λ₂[C]: there is exactly one successor sequentY, obtained by projecting along the leading atomic programaof the loaded formula and droppingafrom it.nonBasicStepdescribes the local step at a non-basicΔ ∈ Λ₂[C]: wheneverΔholds at a state, one of the successor sequents holds at the same state, with the same witness distance. In the paper this is proved by a case distinction on whether the rule was applied to an unloaded formula (local invertibility) or to the loaded formula (in which case it is Lemma 10.5(h),existsD_of_true_diamond).
- rightLoaded (Δ : Sequent) : Δ ∈ C.lambdaTwo → Δ.isRightLoaded
All sequents of
Λ₂[C]have their loaded formula on the right. The DM measure strictly decreases at the non-basic steps of the quasi-tableau.
- basicStep (Δ : 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 sequent.
- nonBasicStep (Δ : 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 sequent.
Instances For
The claim in the proof of Lemma 10.7 #
The Claim in the proof of Lemma 10.7, for the node x of the quasi-tableau: whenever
Δ_x, ι_x is satisfied at a state v, there is a repeat leaf z ∈ cycs(x) and a state
u satisfying Δ_z, ι_z with a witness distance that is not larger, and that is strictly
smaller if there is a basic node between x and z.
The internal variables of the pre-interpolants are interpreted by an assignment g; see
the module docstring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cases of the proof of the Claim #
Case k(x) = 1 where x is a repeat leaf: take z := x and u := v.
Case k(x) = 1 where x is a leaf that is not a repeat: here ι_x = θ_{Δ_x} and the
sequent Δ_x, ι_x is unsatisfiable by Lemma 9.14 (b), so the claim is vacuous.
Case k(x) = 1 where x is neither a leaf nor a companion: ι_x = ι_y and
Δ_x = Δ_y for the unique child y, and cycs(x) = cycs(y).
Case k(x) = 2: ι_x = [¬θ_Δ?]ι_y, and Δ, θ_Δ is unsatisfiable by Lemma 9.14 (b),
so ι_y holds at the same state.
Case k(x) = 3 with Δ_x basic: the loaded formula is ¬⌊a γ⃗⌋ψ with a atomic and
ι_x = [a]ι_y. Going to a state v' at minimal witness distance decreases the witness
distance by exactly one.
Case k(x) = 3 with Δ_x not basic: ι_x = ⋀ᵢ ι_{y_i} and by SatDownFacts.nonBasicStep
one of the children holds at the same state with the same witness distance.
Case k(x) = 1 where x is a companion: ι_x = gfp x ι_y. Reinterpreting the
internal variable q_x by ι_x turns ι_x into ι_y, and a repeat z ∈ cycs(y) whose
companion is x itself sends us back to x, but with a strictly smaller witness distance
by Lemma 10.6, so the secondary induction applies.
The Claim for all nodes of the quasi-tableau #
The Claim in the proof of Lemma 10.7, for all nodes of the quasi-tableau, by
leaf-to-root induction along the construction of Q (Definition 9.8).
Lemma 10.7 at the root of the quasi-tableau.
Lemma 10.8 #
Lemma 10.8: Γ₂ ⊨ ¬θ_r, i.e. the right component of the root of the cluster
together with the interpolant of Definition 9.20 is unsatisfiable.
The hypothesis Γ₁ ≠ ∅ is the one of Definition 9.20: for Γ₁ = ∅ we have θ_r = ⊤ by
Remark 9.19, and then the statement would say that Γ₂ itself is unsatisfiable.