Pre-interpolants (Definition 9.18)

Given the quasi-tableau Q of the cluster C (Def 9.8, LoadedCluster.Q) and the formulas θ_Δ of Def 9.13 (LoadedCluster.thetaOf), we define by a leaf-to-root induction a pre-interpolant ι_x for every node x of Q.

As in Pdl.InterpolationCluster a node of the quasi-tableau is given by its address, the list of child indices leading to it from the root. Hence the internal variables q_x for x ∈ K_Q are indexed by List Nat, and pre-interpolants are elements of QFormula (List Nat), the Q-formulas of Def 9.15.

The definition proceeds by recursion on the subtree, carrying along the address of its root; the address is needed to look up the companion c(x) and to decide whether x is itself a companion. Two cases of the definition presuppose facts about the quasi-tableau that are not part of the data type, namely that nodes of type 2 and basic nodes of type 3 have a unique child. For nodes without children where the paper assumes one we return the placeholder ⊤; by Remark 9.9 (QuasiTab.build_leaf_typ) this does not happen in C.Q.

The leading program of the loaded formula

def Sequent.loadedProg? : Sequent → Option Program

The leading program α of the loaded formula ~⌊α⌋ξ of a sequent, if there is one. For a basic sequent this program is atomic, see Sequent.isAtomic_of_basic_of_negLoad_mem_wForms.

Equations

• Sequent.loadedProg? (fst, fst_1, none) = none
• Sequent.loadedProg? (fst, fst_1, some (Sum.inl (~'⌊α⌋a))) = some α
• Sequent.loadedProg? (fst, fst_1, some (Sum.inr (~'⌊α⌋a))) = some α

def Sequent.loadedProg (X : Sequent) : Program

The leading program of the loaded formula, or ?'⊥ if the sequent is free. Only used in the case k(x) = 3 with Δₓ basic of Definition 9.18, where the sequent is loaded.

Equations

• X.loadedProg = X.loadedProg?.getD (?'⊥)

Definition 9.18

@[irreducible]

def QuasiTab.iitpAt (q : QuasiTab) (θ : Sequent → Formula) (n : QuasiTab) (x : List ℕ) : QFormula (List ℕ)

Def 9.18: the pre-interpolant ι_x of the node with address x in the quasi-tableau q, where θ gives the formulas θ_Δ of Def 9.13.

The first argument q is the whole quasi-tableau (used to find companions), the argument n is the subtree at address x, on which we recurse.

• k(x) = 1 and x is a leaf: if x is a repeat, i.e. has a companion c(x), then ι_x := q_{c(x)}; otherwise Δ_x ∈ Λ₂[C⁺] \ Λ₂[C] and ι_x := θ_{Δ_x}.
• k(x) = 1 and x is a companion: ι_x is the fixpoint QFormula.gfp x ι_y where y is the unique child of x.
• k(x) = 1 otherwise: ι_x := ι_y for the unique child y.
• k(x) = 2: ι_x := [¬θ_{Δ_x}?] ι_y for the unique child y.
• k(x) = 3 with Δ_x basic: ι_x := [a] ι_y where a is the leading atomic program of the loaded formula of Δ_x.
• k(x) = 3 with Δ_x not basic: ι_x := ⋀ { ι_y | x ⋖Q y }.

Equations

• q.iitpAt θ (QuasiTab.QNode Typ.one Δ []) x✝ = match q.companion? x✝ with | some c => QFormula.var c | none => QFormula.fma (θ Δ)
• q.iitpAt θ (QuasiTab.QNode Typ.one Δ (y :: tail)) x✝ = if x✝ ∈ q.companions then QFormula.gfp x✝ (q.iitpAt θ y (x✝ ++ [0])) else q.iitpAt θ y (x✝ ++ [0])
• q.iitpAt θ (QuasiTab.QNode Typ.two Δ (y :: tail)) x✝ = QFormula.boxes [?'~θ Δ] (q.iitpAt θ y (x✝ ++ [0]))
• q.iitpAt θ (QuasiTab.QNode Typ.two Δ []) x✝ = QFormula.fma ⊤
• q.iitpAt θ (QuasiTab.QNode Typ.three Δ []) x✝ = if Δ.basic then QFormula.fma ⊤ else QFormula.conj (q.iitpList θ [] x✝ 0)
• q.iitpAt θ (QuasiTab.QNode Typ.three Δ (y :: tail)) x✝ = if Δ.basic then QFormula.boxes [Δ.loadedProg] (q.iitpAt θ y (x✝ ++ [0])) else QFormula.conj (q.iitpList θ (y :: tail) x✝ 0)

@[irreducible]

def QuasiTab.iitpList (q : QuasiTab) (θ : Sequent → Formula) (ns : List QuasiTab) (x : List ℕ) (i : ℕ) : List (QFormula (List ℕ))

Auxiliary function for iitpAt: the pre-interpolants of a list of children, where i is the index of the first one, needed to build their addresses.

Equations

• q.iitpList θ [] x✝¹ x✝ = []
• q.iitpList θ (n :: ns) x✝¹ x✝ = q.iitpAt θ n (x✝¹ ++ [x✝]) :: q.iitpList θ ns x✝¹ (x✝ + 1)

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

Def 9.18: the pre-interpolant ι_x of the node with address x of the quasi-tableau Q of the cluster C, where θ gives the interpolants of the exit nodes of C. When there is no node at address x we return the placeholder ⊤.

Equations

• C.iitp θ x = match C.Q.at? x with | none => QFormula.fma ⊤ | some n => C.Q.iitpAt (C.thetaOf θ) n x

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

The pre-interpolant of the root of the quasi-tableau. This is the formula ι_{c_Q} that Def 9.20 turns into the interpolant of the root of the cluster.

Equations

• C.rootIitp θ = C.iitp θ QuasiTab.rootAddress

Unfolding lemmas for Definition 9.18

@[simp]

theorem QuasiTab.iitpAt_one_leaf_repeat {q : QuasiTab} {θ : Sequent → Formula} {Δ : Sequent} {x c : List ℕ} (h : q.companion? x = some c) : q.iitpAt θ (QNode Typ.one Δ []) x = QFormula.var c

@[simp]

theorem QuasiTab.iitpAt_one_leaf_exit {q : QuasiTab} {θ : Sequent → Formula} {Δ : Sequent} {x : List ℕ} (h : q.companion? x = none) : q.iitpAt θ (QNode Typ.one Δ []) x = QFormula.fma (θ Δ)

theorem QuasiTab.iitpAt_one_node {q : QuasiTab} {θ : Sequent → Formula} {Δ : Sequent} {x : List ℕ} {y : QuasiTab} {ys : List QuasiTab} : q.iitpAt θ (QNode Typ.one Δ (y :: ys)) x = if x ∈ q.companions then QFormula.gfp x (q.iitpAt θ y (x ++ [0])) else q.iitpAt θ y (x ++ [0])

theorem QuasiTab.iitpAt_two {q : QuasiTab} {θ : Sequent → Formula} {Δ : Sequent} {x : List ℕ} {y : QuasiTab} {ys : List QuasiTab} : q.iitpAt θ (QNode Typ.two Δ (y :: ys)) x = QFormula.boxes [?'~θ Δ] (q.iitpAt θ y (x ++ [0]))

theorem QuasiTab.iitpAt_three_basic {q : QuasiTab} {θ : Sequent → Formula} {Δ : Sequent} {x : List ℕ} {y : QuasiTab} {ys : List QuasiTab} (h : Δ.basic) : q.iitpAt θ (QNode Typ.three Δ (y :: ys)) x = QFormula.boxes [Δ.loadedProg] (q.iitpAt θ y (x ++ [0]))

theorem QuasiTab.iitpAt_three_not_basic {q : QuasiTab} {θ : Sequent → Formula} {Δ : Sequent} {x : List ℕ} {next : List QuasiTab} (h : ¬Δ.basic) : q.iitpAt θ (QNode Typ.three Δ next) x = QFormula.conj (q.iitpList θ next x 0)

@[simp]

theorem QuasiTab.iitpList_nil {q : QuasiTab} {θ : Sequent → Formula} {x : List ℕ} {i : ℕ} : q.iitpList θ [] x i = []

@[simp]

theorem QuasiTab.iitpList_cons {q : QuasiTab} {θ : Sequent → Formula} {n : QuasiTab} {ns : List QuasiTab} {x : List ℕ} {i : ℕ} : q.iitpList θ (n :: ns) x i = q.iitpAt θ n (x ++ [i]) :: q.iitpList θ ns x (i + 1)

theorem QuasiTab.length_iitpList {q : QuasiTab} {θ : Sequent → Formula} {ns : List QuasiTab} {x : List ℕ} {i : ℕ} : (q.iitpList θ ns x i).length = ns.length

theorem QuasiTab.iitpList_getElem {q : QuasiTab} {θ : Sequent → Formula} {ns : List QuasiTab} {x : List ℕ} {i j : ℕ} (hj : j < ns.length) : (q.iitpList θ ns x i)[j] = q.iitpAt θ ns[j] (x ++ [i + j])

The j-th element of iitpList is the pre-interpolant of the j-th child.

Unfolding Definition 9.18 at the level of addresses

The lemmas above are about the recursion on subtrees. Here we restate them for the pre-interpolants LoadedCluster.iitp of the nodes of Q, which are given by addresses.

theorem QuasiTab.at?_snoc (q : QuasiTab) (x : List ℕ) (i : ℕ) : q.at? (x ++ [i]) = (q.at? x).bind fun (n : QuasiTab) => n.children[i]?

Going to the child with index i of the node at address x.

theorem LoadedCluster.iitp_of_at? {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {θ : FinePathIn tab → Formula} {x : List ℕ} {n : QuasiTab} (h : C.Q.at? x = some n) : C.iitp θ x = C.Q.iitpAt (C.thetaOf θ) n x

theorem LoadedCluster.iitp_first_child {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {θ : FinePathIn tab → Formula} {x : List ℕ} {k : Typ} {Δ : Sequent} {y : QuasiTab} {ys : List QuasiTab} (h : C.Q.at? x = some (QuasiTab.QNode k Δ (y :: ys))) : C.iitp θ (x ++ [0]) = C.Q.iitpAt (C.thetaOf θ) y (x ++ [0])

The pre-interpolant of the first child of a node.

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

Def 9.18, case k(x) = 1 where x is a repeat leaf: ι_x = q_{c(x)}.

theorem LoadedCluster.iitp_one_leaf_exit {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {θ : FinePathIn tab → Formula} {x : List ℕ} {Δ : Sequent} (h : C.Q.at? x = some (QuasiTab.QNode Typ.one Δ [])) (hc : C.Q.companion? x = none) : C.iitp θ x = QFormula.fma (C.thetaOf θ Δ)

Def 9.18, case k(x) = 1 where x is a leaf that is not a repeat: ι_x = θ_{Δ_x}.

theorem LoadedCluster.iitp_one_companion {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {θ : FinePathIn tab → Formula} {x : List ℕ} {Δ : Sequent} {y : QuasiTab} {ys : List QuasiTab} (h : C.Q.at? x = some (QuasiTab.QNode Typ.one Δ (y :: ys))) (hx : x ∈ C.Q.companions) : C.iitp θ x = QFormula.gfp x (C.iitp θ (x ++ [0]))

Def 9.18, case k(x) = 1 where x is a companion: ι_x is the fixpoint.

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

Def 9.18, case k(x) = 1 where x is neither a leaf nor a companion: ι_x = ι_y.

theorem LoadedCluster.iitp_two {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {θ : FinePathIn tab → Formula} {x : List ℕ} {Δ : Sequent} {y : QuasiTab} {ys : List QuasiTab} (h : C.Q.at? x = some (QuasiTab.QNode Typ.two Δ (y :: ys))) : C.iitp θ x = QFormula.boxes [?'~C.thetaOf θ Δ] (C.iitp θ (x ++ [0]))

Def 9.18, case k(x) = 2: ι_x = [¬θ_{Δ_x}?] ι_y.

theorem LoadedCluster.iitp_three_basic {X : Sequent} {tab : Tableau [] X} {C : LoadedCluster tab} {θ : FinePathIn tab → Formula} {x : List ℕ} {Δ : Sequent} {y : QuasiTab} {ys : List QuasiTab} (h : C.Q.at? x = some (QuasiTab.QNode Typ.three Δ (y :: ys))) (hb : Δ.basic) : C.iitp θ x = QFormula.boxes [Δ.loadedProg] (C.iitp θ (x ++ [0]))

Def 9.18, case k(x) = 3 with Δ_x basic: ι_x = [a] ι_y.

theorem LoadedCluster.iitp_three_not_basic {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)) (hb : ¬Δ.basic) : C.iitp θ x = QFormula.conj (C.Q.iitpList (C.thetaOf θ) next x 0)

Def 9.18, case k(x) = 3 with Δ_x not basic: ι_x is the conjunction of the pre-interpolants of all children of x, see iitpList_getElem_eq_iitp.

theorem LoadedCluster.iitpList_getElem_eq_iitp {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)) {i : ℕ} (hi : i < next.length) : (C.Q.iitpList (C.thetaOf θ) next x 0)[i] = C.iitp θ (x ++ [i])

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