The interpolant of a cluster root and its vocabulary

This file continues the development of Pdl.Interpolation.PreInterpolant and Pdl.Interpolation.ClusterFacts with:

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

Definition 10.2 and Lemma 10.3 are in Pdl.Interpolation.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

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.5), 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 θ)

theorem LoadedCluster.thetaOf_voc_sub_jvoc {X : Sequent} {tab : Tableau [] X} (C : LoadedCluster tab) (θ : 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) (θ : 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) (θ : 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) (θ : 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) (θ : 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) (θ : FinePathIn tab → Formula) (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.label (θ f)) : (C.itp θ).voc ⊆ jvoc (nodeAt C.root)

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