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 Split.at_in_lt_freeVar {𝕏 : Proof} [fin_X : Fintype 𝕏.X] {n : ℕ} (h : at n ∈ 𝕏.Sequent) : n < 𝕏.freeVar

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

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

Equations

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

noncomputable def Split.unencodeVar {𝕏 : 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

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

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

The encodeVar function is injective.

@[simp]

theorem Split.encodeVar_inj' (𝕏 : 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 Split.encodeVar_inv (𝕏 : Proof) [Fintype 𝕏.X] (x : 𝕏.X) : unencodeVar (encodeVar x) ⋯ = x

unencodeVar is a left inverse of encodeVar.

theorem Split.unencodeVar_inv (𝕏 : 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 Split.at_in_not_encodeVar {𝕏 : Proof} [fin_X : Fintype 𝕏.X] {n : ℕ} (h : at n ∈ 𝕏.Sequent) (x : 𝕏.X) : ¬encodeVar x = n

theorem Split.encodeVar_eq {𝕏 : 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 Split.equation {𝕏 : Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : Formula

Equations

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

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

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

noncomputable def Split.extend {𝕏 : 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

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

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

@[simp]

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

theorem Split.extend_in {𝕏 : 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 Split.encodeVar_in_equation_imp_edge {𝕏 : Proof} [fin_X : Fintype 𝕏.X] {x y : 𝕏.X} : encodeVar y ∈ (equation x).vocab → edge 𝕏.α x y

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

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

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

theorem Split.Solution_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 Split.Solution_strong {𝕏 : 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.

theorem Split.equiv_help {C D E : Formula} (h : C≅D) (g : D = E) : C≅E

@[irreducible]

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

Proves the Solution_strong satisfies the necessary properties.

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

Equations

• Split.Interpolant 𝕏 = partial_ (Split.Solution_strong ⋯)

theorem Split.eq_chain {α : Type} {a b c d : α} {r : α → α → Prop} (h₁ : r a c) (h₂ : a = b) (h₃ : c = d) : r b d

theorem Split.Interpolant_prop {𝕏 : 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 ⊆ (f (r 𝕏.α x)).left.vocab ∩ (f (r 𝕏.α x)).right.vocab