The interpolant of a cluster root and its correctness

This file continues the development of Pdl.PreInterpolant with

• Definition 9.20: the interpolant θ_r of the root r of the cluster C, and
• Lemma 10.1: the vocabulary of the pre-interpolants.

Definition 10.2 and Lemma 10.3 are in Pdl.ClusterRho.

Two small vocabulary lemmas

@[simp]

theorem Vocab.fromList_singleton (v : Vocab) : fromList [v] = v

@[simp]

theorem Program.voc_steps (as : List Program) : (steps as).voc = as.pvoc

Entailment from the left component of a node

def FinePathIn.leftEntails {Hist : History} {Y : Sequent} {tab : Tableau Hist Y} (t : FinePathIn tab) (φ : Formula) : Prop

Λ₁(t) ⊨ φ: the formula φ follows from the left component of the fine node t.

Equations

• t.leftEntails φ = ∀ (W : Type) (M : KripkeModel W) (w : W), (∀ ψ ∈ t.label.left, evaluate M w ψ) → evaluate M w φ

The vocabulary of a Q-formula

The pre-interpolants of Definition 9.18 are QFormulas, i.e. they contain the internal variables q_x as a separate constructor. Their vocabulary therefore splits into two parts: the ordinary vocabulary QFormula.voc, made up of the proposition letters and atomic programs occurring in the formula, and the internal variables QFormula.vars. Lemma 10.1 below bounds the two parts separately, which is exactly the statement voc(ι_x) ⊆ (voc(Γ₁) ∩ voc(Γ₂)) ∪ { q_{c(z)} | z ∈ cycs(x) } of the paper.

def QFormula.voc {Var : Type} : QFormula Var → Vocab

The ordinary vocabulary of a Q-formula, i.e. the proposition letters and atomic programs occurring in it. The internal variables are not included; they are given by QFormula.vars.

Equations

• (QFormula.fma ψ).voc = ψ.voc
• (QFormula.var a).voc = ∅
• (ι1.and ι2).voc = ι1.voc ∪ ι2.voc
• (QFormula.boxes as ι).voc = as.pvoc ∪ ι.voc

@[simp]

theorem QFormula.voc_fma {Var : Type} {ψ : Formula} : (fma ψ).voc = ψ.voc

@[simp]

theorem QFormula.voc_var {Var : Type} {q : Var} : (var q).voc = ∅

@[simp]

theorem QFormula.voc_and {Var : Type} {ι1 ι2 : QFormula Var} : (ι1.and ι2).voc = ι1.voc ∪ ι2.voc

@[simp]

theorem QFormula.voc_boxes {Var : Type} {as : List Program} {ι : QFormula Var} : (boxes as ι).voc = as.pvoc ∪ ι.voc

@[simp]

theorem QFormula.vars_fma {Var : Type} {ψ : Formula} : (fma ψ).vars = []

@[simp]

theorem QFormula.vars_var {Var : Type} {q : Var} : (var q).vars = [q]

@[simp]

theorem QFormula.vars_and {Var : Type} {ι1 ι2 : QFormula Var} : (ι1.and ι2).vars = ι1.vars ++ ι2.vars

@[simp]

theorem QFormula.vars_boxes {Var : Type} {as : List Program} {ι : QFormula Var} : (boxes as ι).vars = ι.vars

theorem QFormula.voc_subst_subset {Var : Type} {σ : Var → Formula} {V : Vocab} (hσ : ∀ (q : Var), (σ q).voc ⊆ V) (ι : QFormula Var) : (subst σ ι).voc ⊆ ι.voc ∪ V

Substituting formulas whose vocabulary is inside V for the internal variables gives a formula whose vocabulary is inside voc(ι) ∪ V.

theorem QFormula.voc_subst_top {Var : Type} (ι : QFormula Var) : (subst (fun (x : Var) => ⊤) ι).voc ⊆ ι.voc

Substituting ⊤ for all internal variables does not add anything to the vocabulary.

The vocabulary of conjunctions, of Spl and of the fixpoint gfp

theorem QFormula.voc_conj {Var : Type} {n : ℕ ⊕ ℕ} (L : List (QFormula Var)) : n ∈ (conj L).voc → ∃ ι ∈ L, n ∈ ι.voc

theorem QFormula.vars_conj {Var : Type} {v : Var} (L : List (QFormula Var)) : v ∈ (conj L).vars → ∃ ι ∈ L, v ∈ ι.vars

@[simp]

theorem QFormula.voc_toQ_prefixBoxes' {Var : Type} (as : List Program) (s : QSimple Var) : (QSimple.prefixBoxes as s).toQ.voc = as.pvoc ∪ s.toQ.voc

@[simp]

theorem QFormula.vars_toQ_prefixBoxes {Var : Type} (as : List Program) (s : QSimple Var) : (QSimple.prefixBoxes as s).toQ.vars = s.toQ.vars

theorem QFormula.voc_of_mem_Spl {Var : Type} (ι : QFormula Var) (s : QSimple Var) : s ∈ ι.Spl → s.toQ.voc ⊆ ι.voc

The ordinary vocabulary of the simple conjuncts of ι is inside that of ι.

theorem QFormula.vars_of_mem_Spl {Var : Type} (ι : QFormula Var) (s : QSimple Var) : s ∈ ι.Spl → ∀ v ∈ s.toQ.vars, v ∈ ι.vars

The internal variables of the simple conjuncts of ι are variables of ι.

theorem QFormula.voc_dropVar {Var : Type} [DecidableEq Var] (x : Var) (ι : QFormula Var) : (dropVar x ι).voc ⊆ ι.voc

theorem QFormula.vars_dropVar {Var : Type} [DecidableEq Var] (x : Var) (ι : QFormula Var) (v : Var) : v ∈ (dropVar x ι).vars → v ∈ ι.vars

theorem QFormula.voc_unions (L : List Program) (n : ℕ ⊕ ℕ) : n ∈ (Program.unions L).voc → ∃ α ∈ L, n ∈ α.voc

theorem QFormula.voc_loopProgs {Var : Type} [DecidableEq Var] (x : Var) (ι : QFormula Var) (α : Program) : α ∈ loopProgs x ι → α.voc ⊆ ι.voc

theorem QFormula.voc_gfp {Var : Type} [DecidableEq Var] (x : Var) (ι : QFormula Var) : (gfp x ι).voc ⊆ ι.voc

The fixpoint used at companion nodes does not add anything to the vocabulary.

theorem QFormula.vars_gfp {Var : Type} [DecidableEq Var] (x : Var) (ι : QFormula Var) (v : Var) : v ∈ (gfp x ι).vars → v ∈ ι.vars

The fixpoint used at companion nodes does not add internal variables.

More facts about the nodes of a quasi-tableau

theorem QuasiTab.companion?_qlt {q : QuasiTab} {x c : List ℕ} (h : q.companion? x = some c) : qlt c x

The companion of a node is a proper ancestor of it.

theorem QuasiTab.mem_cycs_self {q : QuasiTab} {x : List ℕ} (h : q.isRepeatLeaf x = true) : x ∈ q.cycs x

A repeat leaf is one of its own cycles.

theorem QuasiTab.mem_cycs_of_qedge_of_companion_ne {q : QuasiTab} {x y z : List ℕ} (hxy : q.qedge x y) (hz : z ∈ q.cycs y) (hne : q.companion? z ≠ some x) : z ∈ q.cycs x

A generalisation of QuasiTab.cycs_subset_of_qedge: a cycle of a child y of x is a cycle of x, unless its companion is x itself.

theorem QuasiTab.isLeafAt_of_at? {q : QuasiTab} {x : List ℕ} {Δ : Sequent} {k : Typ} (h : q.at? x = some (QNode k Δ [])) : q.isLeafAt x = true

The node at address x is a leaf of type 1 when it is QNode one Δ [].

theorem QuasiTab.typAt_of_at? {q : QuasiTab} {x : List ℕ} {n : QuasiTab} (h : q.at? x = some n) : q.typAt x = some n.typ

theorem QuasiTab.at?_child {q : QuasiTab} {x : List ℕ} {Δ : Sequent} {k : Typ} {next : List QuasiTab} {i : ℕ} (h : q.at? x = some (QNode k Δ next)) (hi : i < next.length) : q.at? (x ++ [i]) = some next[i]

Going to the child with index i, at the level of addresses.

theorem QuasiTab.qedge_snoc {q : QuasiTab} {x : List ℕ} {Δ : Sequent} {k : Typ} {next : List QuasiTab} {i : ℕ} (h : q.at? x = some (QNode k Δ next)) (hi : i < next.length) : q.qedge x (x ++ [i])

Two more unfolding lemmas for Definition 9.18

These are the two cases where the data type allows a node without children although the definition of the quasi-tableau provides one; see Remark 9.9.

theorem QuasiTab.iitpAt_two_leaf {q : QuasiTab} {θ : Sequent → Formula} {Δ : Sequent} {x : List ℕ} : q.iitpAt θ (QNode Typ.two Δ []) x = QFormula.fma ⊤

theorem QuasiTab.iitpAt_three_basic_leaf {q : QuasiTab} {θ : Sequent → Formula} {Δ : Sequent} {x : List ℕ} (h : Δ.basic) : q.iitpAt θ (QNode Typ.three Δ []) x = QFormula.fma ⊤

theorem LoadedCluster.iitp_two_leaf {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {θ : FinePathIn tab → Formula} {x : List ℕ} {Δ : Sequent} (h : C.Q.at? x = some (QuasiTab.QNode Typ.two Δ [])) : C.iitp θ x = QFormula.fma ⊤

theorem LoadedCluster.iitp_three_basic_leaf {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {θ : FinePathIn tab → Formula} {x : List ℕ} {Δ : Sequent} (h : C.Q.at? x = some (QuasiTab.QNode Typ.three Δ [])) (hb : Δ.basic) : C.iitp θ x = QFormula.fma ⊤

Definition 9.20: the interpolant of the root of the cluster

noncomputable def LoadedCluster.itp {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (θ : FinePathIn tab → Formula) : Formula

Def 9.20: the interpolant θ_r of the root r of the cluster C.

If the left component Γ₁ of the root is empty then θ_r := ⊤ (see Remark 9.19), and otherwise θ_r is the pre-interpolant ι_{r_Q} of the root of the quasi-tableau. The latter is a QFormula, i.e. it may still contain internal variables; by Lemma 10.1 (iitp_vars) it does not, so it does not matter which substitution we use to read it as a Formula, and we simply substitute ⊤.

Equations

• C.itp θ = if (nodeAt C.root).left = ∅ then ⊤ else QFormula.subst (fun (x : List ℕ) => ⊤) (C.rootIitp θ)

Facts about the cluster that are used but not yet formalised

structure LoadedCluster.PaperFacts {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) : Prop

Facts about the cluster C that the paper establishes elsewhere, but that are not available in this Lean development yet. They are collected here so that the results below can list them as a single hypothesis.

• proper says that the cluster is proper, as assumed throughout Section 9.
• exists_right is Lemma 9.7 (d): if C_Δ is non-empty then so is C^R_Δ.
• vocL and vocR are instances of the fact that the vocabulary of both components only shrinks along a tableau; here applied to the nodes of C⁺, all of which are below the root r of the cluster.
• loadedProgVoc says that the leading atomic program a of the loaded formula of a basic Δ ∈ Λ₂[C] is in the joint vocabulary of the root. That a ∈ voc(Γ₂) is again vocabulary preservation. That a ∈ voc(Γ₁) — which the paper does not mention, but which its Lemma 10.1 needs — holds when Γ₁ ≠ ∅ because by Lemma 9.7 (e) the modal rule is applied at some t ∈ C^R_Δ and its child u is again in C, so that Λ₁(u) = (Λ₁(t))_a is non-empty by Lemma 9.5 (b), which forces a box ⌈a⌉ψ in Λ₁(t). Note that for Γ₁ = ∅ the claim is false, which is why Definition 9.20 treats that case separately.

• exists_right (Δ : Sequent) : Δ ∈ C.lambdaTwo → C.nodesWithFineRight Δ ≠ []

  Lemma 9.7 (d): if C_Δ ≠ ∅ then C^R_Δ ≠ ∅.

• vocL (f : FinePathIn tab) : f ∈ C.fineCLplus → f.label.left.fvoc ⊆ (nodeAt C.root).left.fvoc

  The vocabulary of the left component only shrinks below the root of the cluster.

• vocR (f : FinePathIn tab) : f ∈ C.fineCLplus → f.label.right.fvoc ⊆ (nodeAt C.root).right.fvoc

  The vocabulary of the right component only shrinks below the root of the cluster.

• loadedProgVoc : (nodeAt C.root).left ≠ ∅ → ∀ Δ ∈ C.lambdaTwo, Δ.basic → Δ.loadedProg.voc ⊆ jvoc (nodeAt C.root)

  The leading atomic program of a basic label of Λ₂[C] is in the joint vocabulary.

• leftPropagation (Δ : Sequent) : Δ ∈ C.lambdaTwo → ∀ (φ : Formula), (∀ u ∈ C.nodesWithFineRight Δ, u.leftEntails φ) → (∀ u ∈ C.exitsWithFine Δ, u.leftEntails φ) → ∀ t ∈ C.plusNodesWithFine Δ, t.leftEntails φ

  The conclusion of the inner induction in the proof of Lemma 10.3: if a formula follows from the left component of every node of C^R_Δ and of every exit node with right component Δ, then it follows from the left component of every node of C⁺_Δ. This packages Lemma 9.7 (a) — every node of C_Δ is in C^L_Δ or in C^R_Δ — with the local invertibility of the rules applied at the nodes of C^L_Δ.

• rightRuleChildren (Δ : Sequent) : Δ ∈ C.lambdaTwo → ¬Δ.basic → ∀ t ∈ C.nodesWithFineRight Δ, ∀ Pi ∈ C.stepOf Δ, ∃ u ∈ C.plusNodesWithFine Pi, u.label.left = t.label.left

  For a non-basic Δ ∈ Λ₂[C] and every t ∈ C^R_Δ, the children of t in the tableau are the nodes Λ₁(t);Π for Π ∈ stepOf Δ, and they are in C⁺_Π. We only record what is used in the proof of Lemma 10.3: the existence of a node of C⁺_Π with the same left component as t.

• modalStep (Δ : Sequent) : Δ ∈ C.lambdaTwo → Δ.basic → ∀ t ∈ C.nodesWithFineRight Δ, ∀ Pi ∈ C.stepOf Δ, ∃ u ∈ C.plusNodesWithFine Pi, ∀ (W : Type) (M : KripkeModel W) (w v : W), (∀ ψ ∈ t.label.left, evaluate M w ψ) → relate M Δ.loadedProg w v → ∀ ψ ∈ u.label.left, evaluate M v ψ

  For a basic Δ ∈ Λ₂[C] the modal rule is applied at every t ∈ C^R_Δ, and its unique child u is in C and satisfies Λ₁(u) = (Λ₁(t))_a where a is the leading atomic program of the loaded formula of Δ. We only record the semantic consequence used in the proof of Lemma 10.3: from Λ₁(t) at a state w we get Λ₁(u) at every a-successor of w.

theorem LoadedCluster.thetaOf_voc_sub_jvoc {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (hF : C.PaperFacts) (θ : FinePathIn tab → Formula) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) (Δ : Sequent) : (C.thetaOf θ Δ).voc ⊆ jvoc (nodeAt C.root)

The vocabulary of θ_Δ is inside the joint vocabulary of the root of the cluster. This is Lemma 9.14 (c) together with vocabulary preservation.

Lemma 10.1: the vocabulary of the pre-interpolants

theorem LoadedCluster.mem_iitpList {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {θ : FinePathIn tab → Formula} {x : List ℕ} {Δ : Sequent} {next : List QuasiTab} (h : C.Q.at? x = some (QuasiTab.QNode Typ.three Δ next)) {ι : QFormula (List ℕ)} (hι : ι ∈ C.Q.iitpList (C.thetaOf θ) next x 0) : ∃ (i : ℕ) (_ : i < next.length), ι = C.iitp θ (x ++ [i])

The conjuncts in the case k(x) = 3 with Δ_x not basic are the pre-interpolants of the children of x.

theorem LoadedCluster.iitp_voc_aux {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (hF : C.PaperFacts) (θ : FinePathIn tab → Formula) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) (hΓ₁ : (nodeAt C.root).left ≠ ∅) (m : ℕ) (n : QuasiTab) : sizeOf n ≤ m → ∀ (x : List ℕ), C.Q.at? x = some n → (C.iitp θ x).voc ⊆ jvoc (nodeAt C.root) ∧ ∀ v ∈ (C.iitp θ x).vars, ∃ z ∈ C.Q.cycs x, C.Q.companion? z = some v

Lemma 10.1: the vocabulary of the pre-interpolant of a node x of the quasi-tableau consists of the joint vocabulary of the root of the cluster and of internal variables q_{c(z)} for cycles z ∈ cycs(x).

Here the two parts are stated separately: voc(ι_x) ⊆ voc(Γ₁) ∩ voc(Γ₂) for the ordinary vocabulary, and the internal variables of ι_x are companions of elements of cycs(x).

The hypothesis Γ₁ ≠ ∅ is needed: for Γ₁ = ∅ the claim would say that ι_x has no ordinary vocabulary at all, which fails at nodes of type 3 with a basic label. Definition 9.20 covers that case separately, see Remark 9.19.

theorem LoadedCluster.iitp_voc {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (hF : C.PaperFacts) (θ : FinePathIn tab → Formula) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) (hΓ₁ : (nodeAt C.root).left ≠ ∅) (x : List ℕ) : (C.iitp θ x).voc ⊆ jvoc (nodeAt C.root)

Lemma 10.1, first part: for every node x of the quasi-tableau, the ordinary vocabulary of the pre-interpolant ι_x is inside voc(Γ₁) ∩ voc(Γ₂). See LoadedCluster.iitp_voc_aux for the hypothesis Γ₁ ≠ ∅.

theorem LoadedCluster.iitp_vars {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (hF : C.PaperFacts) (θ : FinePathIn tab → Formula) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) (hΓ₁ : (nodeAt C.root).left ≠ ∅) (x v : List ℕ) : v ∈ (C.iitp θ x).vars → ∃ z ∈ C.Q.cycs x, C.Q.companion? z = some v

Lemma 10.1, second part: the internal variables occurring in the pre-interpolant ι_x are the companions q_{c(z)} of cycles z ∈ cycs(x).

theorem LoadedCluster.rootIitp_vars {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (hF : C.PaperFacts) (θ : FinePathIn tab → Formula) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) (hΓ₁ : (nodeAt C.root).left ≠ ∅) : (C.rootIitp θ).vars = []

The pre-interpolant of the root of the quasi-tableau contains no internal variables, because cycs(r_Q) = ∅ (Lemma 9.12 (b)).

theorem LoadedCluster.itp_voc {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (hF : C.PaperFacts) (θ : FinePathIn tab → Formula) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) : (C.itp θ).voc ⊆ jvoc (nodeAt C.root)

Lemma 10.1, the corollary: the interpolant of the root of the cluster only uses the joint vocabulary of Γ₁ and Γ₂.