LeanPool.Lean4GlCoalgebras.Interpolation.Interpolants

Finding interpolants #

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

source

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

Lean4GlCoalgebras.Sequent

Get the entire underlying sequent of a finite proof.

Equations

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

Instances For

source

def Lean4GlCoalgebras.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 = Lean4GlCoalgebras.Sequent.freshVar 𝕏.Sequent

Instances For

source

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

n < 𝕏.freeVar

source

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

𝕏.X → ℕ

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

Equations

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

Instances For

source

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

𝕏.X

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

Equations

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

Instances For

source

theorem Lean4GlCoalgebras.encodeVar_inj (𝕏 : Split.Proof) [Fintype 𝕏.X] :

Function.Injective encodeVar

The encodeVar function is injective.

source

@[simp]

theorem Lean4GlCoalgebras.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.

source

theorem Lean4GlCoalgebras.encodeVar_inv (𝕏 : Split.Proof) [Fintype 𝕏.X] (x : 𝕏.X) :

unencodeVar (encodeVar x) ⋯ = x

unencodeVar is a left inverse of encodeVar.

source

theorem Lean4GlCoalgebras.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.

source

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

¬encodeVar x = n

source

theorem Lean4GlCoalgebras.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

source

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

Formula

Auxiliary declaration used in the GL coalgebra development.

Equations

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

Instances For

source

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

n - 𝕏.freeVar < Fintype.card 𝕏.X

source

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

unencodeVar n ⋯ ∈ Y

source

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

Formula → Formula

Extend a substitution specific to encoded variables to all formulas.

Equations

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

Instances For

source

theorem Lean4GlCoalgebras.partial_const {p : ℕ → Prop} [DecidablePred p] (σ : Subtype p → Formula) (A : Formula) :

(∀ n ∈ A.vocab, ¬p n) → A = partial_ σ A

source

@[simp]

theorem Lean4GlCoalgebras.Finset.doubleton_subset_iff {α : Type} [DecidableEq α] {s : Finset α} {a b : α} :

{a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s

source

theorem Lean4GlCoalgebras.extend_in {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] {Y : Finset 𝕏.X} (Y_sub : Y ⊆ Fintype.elems) (σ : ↥Y → Formula) (A : Formula) :

(∀ y ∈ Y, encodeVar y ∉ A.vocab) → A = extend Y_sub σ A

source

theorem Lean4GlCoalgebras.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.

source

theorem Lean4GlCoalgebras.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.

source

theorem Lean4GlCoalgebras.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.

source

@[irreducible]

noncomputable def Lean4GlCoalgebras.interpolantStrong {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] {Y : Finset 𝕏.X} (Y_sub : Y ⊆ Fintype.elems) :

↥(Finset.image encodeVar Y) → Formula

Strong solution towards finding interpolants.

Equations

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

Instances For

source

theorem Lean4GlCoalgebras.interpolant_strong_prop {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (Y : Finset 𝕏.X) (Y_sub : Y ⊆ Fintype.elems) (n : ↥(Finset.image encodeVar Y)) :

(interpolantStrong Y_sub n = partial_ (interpolantStrong Y_sub) (equation (unencodeVar ↑n ⋯)) ∨ (interpolantStrong Y_sub n≅partial_ (interpolantStrong Y_sub) (equation (unencodeVar ↑n ⋯)))) ∧ (∀ m ∈ (interpolantStrong 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_ (interpolantStrong Y_sub) (at↑n)).vocab → Relation.ReflTransGen (Split.edge 𝕏.α) (unencodeVar ↑n ⋯) y

Proves that interpolantStrong satisfies the necessary properties.

source

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

Formula → Formula

Auxiliary declaration used in the GL coalgebra development.

Equations

Lean4GlCoalgebras.interpolant 𝕏 = Lean4GlCoalgebras.partial_ (Lean4GlCoalgebras.interpolantStrong ⋯)

Instances For

source

theorem Lean4GlCoalgebras.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