Finding interpolants

Here we show that given a finite GL-split proof, we can always find suitable interpolants.

def Split.Proof.Sequent (𝕏 : Proof) [fin_X : Fintype 𝕏.X] : _root_.Sequent

Get the entire underlying sequent of a finite proof.

Equations

• 𝕏.Sequent = Fintype.elems.biUnion fun (x : 𝕏.X) => Finset.image (Sum.elim id id) (Split.f (Split.r 𝕏.α x))

def Split.Proof.freeVar (𝕏 : Proof) [fin_X : Fintype 𝕏.X] : ℕ

Find n such that for all m ≥ n, m is not in an the variables of the proof.

Equations

• 𝕏.freeVar = Sequent.freshVar 𝕏.Sequent

theorem at_in_lt_freeVar {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] {n : ℕ} (h : at n ∈ 𝕏.Sequent) : n < 𝕏.freeVar

noncomputable def encodeVar {𝕏 : Split.Proof} [Fintype 𝕏.X] : 𝕏.X → ℕ

For each x in a finite proof, find a free variable.

Equations

• encodeVar x = 𝕏.freeVar + ↑((Fintype.equivFin 𝕏.X) x)

noncomputable def unencodeVar {𝕏 : Split.Proof} [Fintype 𝕏.X] (n : ℕ) (h1 : n - 𝕏.freeVar < Fintype.card 𝕏.X) : 𝕏.X

Given n which is in the range of the free variables, unencode n back to its node in the proof.

Equations

• unencodeVar n h1 = (Fintype.equivFin 𝕏.X).symm ⟨n - 𝕏.freeVar, h1⟩

theorem encodeVar_inj (𝕏 : Split.Proof) [Fintype 𝕏.X] : Function.Injective encodeVar

The encodeVar function is injective.

@[simp]

theorem encodeVar_inj' (𝕏 : Split.Proof) [Fintype 𝕏.X] (x y : 𝕏.X) : encodeVar x = encodeVar y ↔ x = y

The encodeVar function is injective. This version works better with simp than encodeVar_inj.

theorem encodeVar_inv (𝕏 : Split.Proof) [Fintype 𝕏.X] (x : 𝕏.X) : unencodeVar (encodeVar x) ⋯ = x

unencodeVar is a left inverse of encodeVar.

theorem unencodeVar_inv (𝕏 : Split.Proof) [Fintype 𝕏.X] (n : ℕ) (h1 : n - 𝕏.freeVar < Fintype.card 𝕏.X) (h2 : n ≥ 𝕏.freeVar) : encodeVar (unencodeVar n h1) = n

encodeVar is a left inverse of unencodeVar.

theorem at_in_not_encodeVar {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] {n : ℕ} (h : at n ∈ 𝕏.Sequent) (x : 𝕏.X) : ¬encodeVar x = n

theorem encodeVar_eq {𝕏 : Split.Proof} {Fin_X : Fintype 𝕏.X} {x : 𝕏.X} {n : ℕ} {h1 : n - 𝕏.freeVar < Fintype.card 𝕏.X} {h2 : n ≥ 𝕏.freeVar} : encodeVar x = n ↔ x = unencodeVar n h1

noncomputable def equation {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : Formula

Equations

• One or more equations did not get rendered due to their size.

theorem encodeVar_helper₁ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] {Y : Finset 𝕏.X} {n : ℕ} (h : n ∈ Finset.image encodeVar Y) : n - 𝕏.freeVar < Fintype.card 𝕏.X

theorem encodeVar_helper₂ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] {Y : Finset 𝕏.X} {n : ℕ} (h : n ∈ Finset.image encodeVar Y) : unencodeVar n ⋯ ∈ Y

noncomputable def extend {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] {Y : Finset 𝕏.X} (Y_sub : Y ⊆ Fintype.elems) (σ : { x : 𝕏.X // x ∈ Y } → Formula) : Formula → Formula

Extend a substitution specific to encoded variables to all formulas.

Equations

• extend Y_sub σ Formula.bottom = ⊥
• extend Y_sub σ Formula.top = ⊤
• extend Y_sub σ (at n) = if h : n ∈ Finset.image encodeVar Y then σ ⟨unencodeVar n ⋯, ⋯⟩ else at n
• extend Y_sub σ (na n) = if h : n ∈ Finset.image encodeVar Y then ~σ ⟨unencodeVar n ⋯, ⋯⟩ else na n
• extend Y_sub σ (A&B) = (extend Y_sub σ A&extend Y_sub σ B)
• extend Y_sub σ (A v B) = (extend Y_sub σ A v extend Y_sub σ B)
• extend Y_sub σ (□A) = □extend Y_sub σ A
• extend Y_sub σ (◇A) = ◇extend Y_sub σ A

theorem partial_const {p : ℕ → Prop} [DecidablePred p] (σ : Subtype p → Formula) (A : Formula) : (∀ n ∈ A.vocab, ¬p n) → A = partial_ σ A

@[simp]

theorem Finset.doubleton_subset_iff {α : Type} [DecidableEq α] {s : Finset α} {a b : α} : {a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s

theorem extend_in {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] {Y : Finset 𝕏.X} (Y_sub : Y ⊆ Fintype.elems) (σ : { x : 𝕏.X // x ∈ Y } → Formula) (A : Formula) : (∀ y ∈ Y, encodeVar y ∉ A.vocab) → A = extend Y_sub σ A

theorem encodeVar_in_equation_imp_edge {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] {x y : 𝕏.X} : encodeVar y ∈ (equation x).vocab → Split.edge 𝕏.α x y

From the paper: If py ∈ χx then x ◁ y.

theorem var_in_equation {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] {x : 𝕏.X} (n : ℕ) : n ∈ (equation x).vocab → n ∈ (Split.f (Split.r 𝕏.α x)).left.vocab ∩ (Split.f (Split.r 𝕏.α x)).right.vocab ∨ ∃ (y : 𝕏.X), encodeVar y = n ∧ Split.edge 𝕏.α x y

From the paper: If p ∈ χx then p ∈ Voc(fˡ(x)) ∩ Voc(fʳ(x)) or p = py and x ◁ y.

theorem interpolant_strong_helper {p : ℕ → Prop} [DecidablePred p] (σ : Subtype p → Formula) (n : ℕ) {B A : Formula} : single n B (partial_ σ A) = partial_ (fun (m : { m : ℕ // p m ∨ m = n }) => single n B (if h : p ↑m then σ ⟨↑m, h⟩ else at↑m)) A

Helper for Solution strong, gives interaction between single substitution and partial substitution.

@[irreducible]

noncomputable def interpolant_strong {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] {Y : Finset 𝕏.X} (Y_sub : Y ⊆ Fintype.elems) : { n : ℕ // n ∈ Finset.image encodeVar Y } → Formula

Strong solution towards finding interpolants.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

theorem interpolant_strong_prop {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (Y : Finset 𝕏.X) (Y_sub : Y ⊆ Fintype.elems) (n : { n : ℕ // n ∈ Finset.image encodeVar Y }) : (interpolant_strong Y_sub n = partial_ (interpolant_strong Y_sub) (equation (unencodeVar ↑n ⋯)) ∨ (interpolant_strong Y_sub n≅partial_ (interpolant_strong Y_sub) (equation (unencodeVar ↑n ⋯)))) ∧ (∀ m ∈ (interpolant_strong Y_sub n).vocab, m ∈ (Split.f (Split.r 𝕏.α (unencodeVar ↑n ⋯))).left.vocab ∩ (Split.f (Split.r 𝕏.α (unencodeVar ↑n ⋯))).right.vocab ∪ Finset.image encodeVar Fintype.elems \ Finset.image encodeVar Y) ∧ ∀ (y : 𝕏.X), encodeVar y ∈ (partial_ (interpolant_strong Y_sub) (at↑n)).vocab → Relation.ReflTransGen (Split.edge 𝕏.α) (unencodeVar ↑n ⋯) y

Proves that interpolant_strong satisfies the necessary properties.

noncomputable def interpolant (𝕏 : Split.Proof) [fin_X : Fintype 𝕏.X] : Formula → Formula

Equations

• interpolant 𝕏 = partial_ (interpolant_strong ⋯)

theorem interpolant_prop {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : (interpolant 𝕏 (at encodeVar x) = interpolant 𝕏 (equation x) ∨ (interpolant 𝕏 (at encodeVar x)≅interpolant 𝕏 (equation x))) ∧ (interpolant 𝕏 (at encodeVar x)).vocab ⊆ (Split.f (Split.r 𝕏.α x)).left.vocab ∩ (Split.f (Split.r 𝕏.α x)).right.vocab