Satisfiability down the quasi-tableau, and the right half of the correctness of θ_r

This file continues the development of Pdl.Interpolation.ClusterRho with

• Lemma 10.6: between a companion and its repeat there is a basic node,
• Lemma 10.7: if Δ_x, ι_x is satisfiable then so is Δ_z, ι_z for some z ∈ cycs(x),
• Lemma 10.8: Γ₂ ⊨ ¬θ_r.

Definition 10.4 (the distance d_α) and Lemma 10.5 (its properties) are in Pdl.Local.Distance. The auxiliary notions used below — the evaluation evalQ of Q-formulas with an assignment, the witness distance witDist, and BasicBetween — are in Pdl.Interpolation.EvalQ.

The facts about the cluster C and the steps stepOf Δ of its quasi-tableau that are used here are proved in Pdl.Interpolation.ClusterSatDownFacts.

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.

theorem QuasiTab.at?_in_typeOneNode {Δ : Sequent} {next : List QuasiTab} {t : List ℕ} {n : QuasiTab} (h : (QNode Typ.one Δ [QNode Typ.two Δ [QNode Typ.three Δ next]]).at? t = some n) : t = [] ∨ t = [0] ∨ t = [0, 0] ∨ ∃ (i : ℕ) (t' : List ℕ) (hi : i < next.length), t = 0 :: 0 :: i :: t' ∧ next[i].at? t' = some n

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

theorem prefix_sandwich {α : Type u_1} {x c u : List α} (h1 : x <+: c) (h2 : c <+: x ++ u) : ∃ (s : List α), s <+: u ∧ c = x ++ s

If x is a prefix of c and c is a prefix of x ++ u then c = x ++ s for a prefix s of u.

theorem length_lt_of_mem_inits_dropLast {α : Type u_1} {x z : List α} : z ∈ x.inits.dropLast → z.length < x.length

theorem prefix_ne_of_mem_inits_dropLast {α : Type u_1} {x z : List α} (h : z ∈ x.inits.dropLast) : z <+: x ∧ z ≠ x

The addresses searched by QuasiTab.companion? are the proper prefixes.

theorem QuasiTab.companion?_spec {q : QuasiTab} {z c : List ℕ} (h : q.companion? z = some c) : c <+: z ∧ c ≠ z ∧ q.labelAt c = q.labelAt z ∧ q.typAt c = some Typ.one

The companion of a repeat leaf is a proper ancestor with the same label and type 1.

theorem LoadedCluster.measure_le_or_basicBetween {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Hist : List Sequent) (Δ : Sequent) (x : List ℕ) : C.Q.at? x = some (QuasiTab.build C.lambdaTwo C.stepOfL Hist Δ) → ∀ (t : List ℕ) (n : QuasiTab), (QuasiTab.build C.lambdaTwo C.stepOfL Hist Δ).at? t = some n → (n.label = Δ ∨ lt_Sequent n.label Δ) ∨ C.Q.BasicBetween x (x ++ t)

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.

theorem LoadedCluster.build_repeat_basicBetween {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (Hist : List Sequent) (Δ : Sequent) (x : List ℕ) : C.Q.at? x = some (QuasiTab.build C.lambdaTwo C.stepOfL Hist Δ) → ∀ (z c : List ℕ), x <+: z → C.Q.isRepeatLeaf z = true → C.Q.companion? z = some c → x <+: c → C.Q.BasicBetween c z

Induction for Lemma 10.6, 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.

theorem LoadedCluster.repeat_basicBetween {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) {z c : List ℕ} (hz : C.Q.isRepeatLeaf z = true) (hc : C.Q.companion? z = some c) : C.Q.BasicBetween c 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.

We use that the labels of the successors of a non-basic node are smaller in the Dershowitz-Manna ordering (LoadedCluster.stepOf_lt_Sequent), so a repeat — which has the same label as its companion — cannot be reached from its companion by non-basic steps only.

The claim in the proof of Lemma 10.7

def LoadedCluster.SatDown {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (θ : FinePathIn tab → Formula) (x : List ℕ) : Prop

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.

The cases of the proof of the Claim

theorem LoadedCluster.satDown_one_leaf_repeat {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {x : List ℕ} {θ : FinePathIn tab → Formula} {Δ : Sequent} {c : List ℕ} (hx : C.Q.at? x = some (QuasiTab.QNode Typ.one Δ [])) (hc : C.Q.companion? x = some c) : C.SatDown θ x

Case k(x) = 1 where x is a repeat leaf: take z := x and u := v.

theorem LoadedCluster.satDown_one_leaf_exit {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {x : List ℕ} {θ : FinePathIn tab → Formula} {Δ : Sequent} (hx : C.Q.at? x = some (QuasiTab.QNode Typ.one Δ [])) (hc : C.Q.companion? x = none) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) : C.SatDown θ x

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.

theorem LoadedCluster.satDown_one_inner {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {x : List ℕ} {θ : FinePathIn tab → Formula} {Δ : Sequent} {y : QuasiTab} {ys : List QuasiTab} (hx : C.Q.at? x = some (QuasiTab.QNode Typ.one Δ (y :: ys))) (hcomp : x ∉ C.Q.companions) (hylab : C.Q.labelAt (x ++ [0]) = some Δ) (IH : C.SatDown θ (x ++ [0])) : C.SatDown θ x

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).

theorem LoadedCluster.satDown_two {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {x : List ℕ} {θ : FinePathIn tab → Formula} {Δ : Sequent} {y : QuasiTab} {ys : List QuasiTab} (hx : C.Q.at? x = some (QuasiTab.QNode Typ.two Δ (y :: ys))) (hylab : C.Q.labelAt (x ++ [0]) = some Δ) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) (IH : C.SatDown θ (x ++ [0])) : C.SatDown θ x

Case k(x) = 2: ι_x = [¬θ_Δ?]ι_y, and Δ, θ_Δ is unsatisfiable by Lemma 9.14 (b), so ι_y holds at the same state.

theorem LoadedCluster.satDown_three_basic {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {x : List ℕ} {θ : FinePathIn tab → Formula} {Δ Y : Sequent} {y : QuasiTab} {ys : List QuasiTab} (hΔ : Δ ∈ C.lambdaTwo) (hb : Δ.basic) (hx : C.Q.at? x = some (QuasiTab.QNode Typ.three Δ (y :: ys))) (hstep : C.stepOf Δ = {Y}) (hylab : C.Q.labelAt (x ++ [0]) = some Y) (IH : C.SatDown θ (x ++ [0])) : C.SatDown θ x

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.

theorem LoadedCluster.satDown_three_not_basic {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {x : List ℕ} {θ : FinePathIn tab → Formula} {Δ : Sequent} {next : List QuasiTab} (hΔ : Δ ∈ C.lambdaTwo) (hb : ¬Δ.basic) (hx : C.Q.at? x = some (QuasiTab.QNode Typ.three Δ next)) (hlen : next.length = (C.stepOfL Δ).length) (hlab : ∀ (i : ℕ) (hi : i < (C.stepOfL Δ).length), C.Q.labelAt (x ++ [i]) = some (C.stepOfL Δ)[i]) (IH : ∀ i < next.length, C.SatDown θ (x ++ [i])) : C.SatDown θ x

Case k(x) = 3 with Δ_x not basic: ι_x = ⋀ᵢ ι_{y_i} and by LoadedCluster.nonBasicStep_of one of the children holds at the same state with the same witness distance.

theorem LoadedCluster.satDown_one_companion {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {x : List ℕ} {θ : FinePathIn tab → Formula} {Δ : Sequent} {y : QuasiTab} {ys : List QuasiTab} (hx : C.Q.at? x = some (QuasiTab.QNode Typ.one Δ (y :: ys))) (hcomp : x ∈ C.Q.companions) (hylab : C.Q.labelAt (x ++ [0]) = some Δ) (IH : C.SatDown θ (x ++ [0])) : C.SatDown θ x

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

theorem LoadedCluster.satDown_build {X : Sequent} {tab : Tableau [] X} {θ : FinePathIn tab → Formula} (C : LoadedCluster tab) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) (Hist : List Sequent) (Δ : Sequent) (x : List ℕ) : C.Q.at? x = some (QuasiTab.build C.lambdaTwo C.stepOfL Hist Δ) → C.SatDown θ x

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).

theorem LoadedCluster.satDown_root {X : Sequent} {tab : Tableau [] X} {θ : FinePathIn tab → Formula} (C : LoadedCluster tab) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) : C.SatDown θ QuasiTab.rootAddress

Lemma 10.7 at the root of the quasi-tableau.

Lemma 10.8

theorem LoadedCluster.right_unsat_itp {X : Sequent} {tab : Tableau [] X} {θ : FinePathIn tab → Formula} (C : LoadedCluster tab) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) (hΓ₁ : (nodeAt C.root).left ≠ ∅) : ¬HasSat.satisfiable ({C.itp θ} ∪ (nodeAt C.root).right)

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.5, and then the statement would say that Γ₂ itself is unsatisfiable.