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

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

@[simp]

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

Entailment from the left component of a node

def PDL.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 : PDL.KripkeModel W) (w : W), (∀ ψ ∈ t.label.left, PDL.evaluate M w ψ) → PDL.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 PDL.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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem PDL.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 PDL.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 PDL.QFormula.voc_conj {Var : Type} {n : ℕ ⊕ ℕ} (L : List (QFormula Var)) : n ∈ (conj L).voc → ∃ ι ∈ L, n ∈ ι.voc

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

@[simp]

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

@[simp]

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

theorem PDL.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 PDL.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 PDL.QFormula.voc_dropVar {Var : Type} [DecidableEq Var] (x : Var) (ι : QFormula Var) : (dropVar x ι).voc ⊆ ι.voc

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

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

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

theorem PDL.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 PDL.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 PDL.QuasiTab.companionOpt_qlt {q : QuasiTab} {x c : List ℕ} (h : q.companionOpt x = some c) : qlt c x

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

theorem PDL.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 PDL.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.companionOpt 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 PDL.QuasiTab.isLeafAt_of_atOpt {q : QuasiTab} {x : List ℕ} {Δ : Sequent} {k : Typ} (h : q.atOpt 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 PDL.QuasiTab.typAt_of_atOpt {q : QuasiTab} {x : List ℕ} {n : QuasiTab} (h : q.atOpt x = some n) : q.typAt x = some n.typ

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

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

theorem PDL.QuasiTab.qedge_snoc {q : QuasiTab} {x : List ℕ} {Δ : Sequent} {k : Typ} {next : List QuasiTab} {i : ℕ} (h : q.atOpt 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 PDL.QuasiTab.iitpAt_two_leaf {q : QuasiTab} {θ : Sequent → Formula} {Δ : Sequent} {x : List ℕ} : q.iitpAt θ (QNode Typ.two Δ []) x = QFormula.fma ⊤

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

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

theorem PDL.LoadedCluster.iitp_three_basic_leaf {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {θ : FinePathIn tab → Formula} {x : List ℕ} {Δ : Sequent} (h : C.Q.atOpt 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 PDL.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 (PDL.nodeAt C.root).left = ∅ then ⊤ else PDL.QFormula.subst (fun (x : List ℕ) => ⊤) (C.rootIitp θ)

Cluster facts used to construct interpolants

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

Facts about the cluster C used in the interpolant construction. LoadedCluster.paperFacts in ClusterInterpolation proves these from tableau uniformity and cluster properness. Collecting them here keeps those later proofs separate from the construction.

• 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.pdlFvoc ⊆ (nodeAt C.root).left.pdlFvoc

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

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

  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 PDL.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 PDL.LoadedCluster.mem_iitpList {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {θ : FinePathIn tab → Formula} {x : List ℕ} {Δ : Sequent} {next : List QuasiTab} (h : C.Q.atOpt 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 PDL.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.atOpt x = some n → (C.iitp θ x).voc ⊆ jvoc (nodeAt C.root) ∧ ∀ v ∈ (C.iitp θ x).vars, ∃ z ∈ C.Q.cycs x, C.Q.companionOpt 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 PDL.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 PDL.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.companionOpt 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 PDL.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 PDL.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 Γ₂.