Unification

[EwenBC]

Creation of unification algorithm which update context by solving a telescopic equality

Algorithm:

Input:

• a context Γ and a telescope equality ΔEq.

Output:

• a new context Γ' ⊆ Γ where some variables of Γ have been replaced by their value from the unification
• an equivalence between (Γ, ΔEq) and Γ'.

Example:

Input:

• Γ := (m n : ℕ)(x y : A)(xs : Vec A m)(ys : Vec A n)
• ΔEq := (e₁ : suc m ≡ suc n)(e₂ : cons m x xs ≡(Vec A e₁) cons n y ys)

Output:

• Γ' := (m : ℕ)(x : A)(xs : Vec A m)
• σ : (Γ, ΔEq) → Γ'
• τ : Γ' → (Γ, ΔEq)
• (maybe) e: ∀ x, σ τ x = x
• (maybe) e': ∀ x, τ σ x = x

For more:

Implementation based on Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory by Jesper Cockk and Dominique Devriese.