Skip to content

First-order unification

InductiveTerms for unification#✓fully proved

For a type \(C\) of constants, a term over \(C\) is either a variable \(x\), indexed by a natural number \(x \in \mathbb{N}\), or a constant \(c \in C\), or a binary node built from two terms \(l\) and \(r\).

inductive Term (C : Type u) where
  | var (x : ℕ)
  | const (c : C)
  | node (l r : Term C)
  deriving DecidableEq, Repr
Used by 54
Used byBound-variable supremum of a type scheme · Evaluation of a type scheme · Generalization of a monotype · Generalization depends only on the free variables of the context · Generalizing in a context with fewer free variables · Renaming step of the substitution lemma · Hindley–Milner typing · let generalizes · Soundness of Algorithm W · Typing inversion for variables · Completeness of type inference for closed expressions · Instantiation of a type scheme · Instantiation commutes with substitution · The let rule under a type substitution · Substitutions agreeing on a context give the same lookups · Typing is preserved in more general contexts · No monotype is an arrow out of itself · The abstraction \(\lambda f.\, f\, f\) has no type · Type schemes · Hindley–Milner typing is stable under type substitution · Substitution into a scheme depends only on its free variables · Substituting into a generalization is more general · Monotypes as type schemes · Monotypes · Variables below a bound · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W · Eliminating a solved variable lowers the number of variables · The elimination step preserves the unification specification · Total size of a list of equations · Variables of a list of equations · Lists of equations · Variables of a substituted term · Failure is correct when the first equation has no unifier · Single-variable substitution on first-order terms · Absorbing a single-variable substitution · Size of a term · Occurs check: size bound · Substitution · Applying a substitution to a term · Substitution depends only on the variables of the term · Applying a substitution to a list of equations · A term is fixed by substituting it for a variable it avoids · Unifier of a list of equations · Soundness of unification · Martelli–Montanari unification · Completeness of unification · Most generality of unification · Variables of a term · The elimination step of unification introduces no variables · Variables of a substituted variable occur in the substituted term · Substituting for a variable that does not occur in the substituted term · Unification introduces no new variables

AbbreviationSubstitution#✓fully proved

A substitution is a map assigning a term to every variable, that is, a function from the set \(\mathbb{N}\) of variables to terms.

abbrev Subst (C : Type u) := ℕ → Term C
Uses 1 · Used by 41
Statement usesTerms for unification
Used byRenaming step of the substitution lemma · Soundness of type inference for closed expressions · Soundness of Algorithm W · Type inference for closed expressions · Completeness of type inference for closed expressions · Type inference succeeds exactly on typable closed expressions · Principal types · Instantiation commutes with substitution · The let rule under a type substitution · Substitutions agreeing on a context give the same lookups · Applying a type substitution to a context · Hindley–Milner typing is stable under type substitution · Applying a type substitution to a scheme · Substitution into a scheme depends only on its free variables · Substituting into a generalization is more general · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W · Composition of substitutions on first-order terms · Lists of equations with the same unifiers satisfy the same specification · The elimination step preserves the unification specification · Variables of a substituted term · Most general unifier · Unification returns a most general unifier · Failure is correct when the first equation has no unifier · Single-variable substitution on first-order terms · Absorbing a single-variable substitution · Occurs check: size bound · Applying a substitution to a term · Substitution depends only on the variables of the term · Applying a substitution to a list of equations · Unifier of a list of equations · Soundness of unification · Martelli–Montanari unification · Unification returns an idempotent substitution · Completeness of unification · Most generality of unification · Specification of a unification result · The elimination step of unification introduces no variables · Variables of a substituted variable occur in the substituted term · Unification introduces no new variables

DefinitionApplying a substitution to a term#✓fully proved

For a substitution \(\sigma\) and a term \(t\), the term \(t\sigma\) is obtained from \(t\) by replacing every variable \(x\) by \(\sigma(x)\): a variable \(x\) becomes \(\sigma(x)\), a constant is unchanged, and a node with subterms \(l\) and \(r\) becomes the node with subterms \(l\sigma\) and \(r\sigma\).

def subst (s : Subst C) : Term C → Term C
  | var x => s x
  | const c => const c
  | node l r => node (l.subst s) (r.subst s)
Uses 2 · Used by 35
Statement usesSubstitution · Terms for unification
Used byGeneralization of a monotype · Generalization depends only on the free variables of the context · Generalizing in a context with fewer free variables · Renaming step of the substitution lemma · let generalizes · Soundness of Algorithm W · Completeness of type inference for closed expressions · Type inference succeeds exactly on typable closed expressions · Principal types · Instantiation commutes with substitution · The let rule under a type substitution · The abstraction \(\lambda f.\, f\, f\) has no type · Hindley–Milner typing is stable under type substitution · Applying a type substitution to a scheme · Substituting into a generalization is more general · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W · Eliminating a solved variable lowers the number of variables · Composition of substitutions on first-order terms · The elimination step preserves the unification specification · Variables of a substituted term · Failure is correct when the first equation has no unifier · Absorbing a single-variable substitution · Occurs check: size bound · Substitution depends only on the variables of the term · Applying a substitution to a list of equations · A term is fixed by substituting it for a variable it avoids · Unifier of a list of equations · Soundness of unification · Completeness of unification · Most generality of unification · The elimination step of unification introduces no variables · Variables of a substituted variable occur in the substituted term · Substituting for a variable that does not occur in the substituted term

DefinitionSize of a term#✓fully proved

The size of a term is the number of symbols in it: a variable and a constant have size \(1\), and a node with subterms \(l\) and \(r\) has size equal to the size of \(l\) plus the size of \(r\) plus \(1\).

def size : Term C → ℕ
  | var _ => 1
  | const _ => 1
  | node l r => l.size + r.size + 1
Uses 1 · Used by 8
Statement usesTerms for unification
Used byNo monotype is an arrow out of itself · Total size of a list of equations · Occurs check: size bound · Soundness of unification · Martelli–Montanari unification · Completeness of unification · Most generality of unification · Unification introduces no new variables

DefinitionVariables of a term#✓fully proved

The variables of a term form a finite set of natural numbers, defined recursively: the variable \(x\) has the variable set \(\{x\}\), a constant has no variables, and the variables of a node with subterms \(l\) and \(r\) are those of \(l\) together with those of \(r\).

def vars : Term C → Finset ℕ
  | var x => {x}
  | const _ => ∅
  | node l r => l.vars ∪ r.vars
Uses 1 · Used by 28
Statement usesTerms for unification
Used byFree type variables depend only on visible bindings · Generalizing in a context with fewer free variables · Renaming step of the substitution lemma · Substitutions agreeing on a context give the same lookups · Typing is preserved in more general contexts · More general type scheme · Contexts with the same lookups are related by generality · Substitution into a scheme depends only on its free variables · Substituting into a generalization is more general · Variables below a bound · Free type variables of a name's visible scheme · Completeness of Algorithm W · Freshness invariants of Algorithm W · Eliminating a solved variable lowers the number of variables · The elimination step preserves the unification specification · Variables of a list of equations · Variables of a substituted term · Occurs check: size bound · Substitution depends only on the variables of the term · A term is fixed by substituting it for a variable it avoids · Soundness of unification · Martelli–Montanari unification · Completeness of unification · Most generality of unification · The elimination step of unification introduces no variables · Variables of a substituted variable occur in the substituted term · Substituting for a variable that does not occur in the substituted term · Unification introduces no new variables

TheoremSubstitution depends only on the variables of the term#✓fully proved

If two substitutions \(\sigma\) and \(\tau\) agree on every variable occurring in a term \(u\), then applying \(\sigma\) to \(u\) gives the same term as applying \(\tau\) to \(u\).

theorem subst_congr {s t : Subst C} {u : Term C} (h : ∀ x ∈ u.vars, s x = t x) :
    u.subst s = u.subst t
Uses 4 · Used by 6
Statement usesSubstitution · Terms for unification · Applying a substitution to a term · Variables of a term
Used byGeneralizing in a context with fewer free variables · Renaming step of the substitution lemma · Substitution into a scheme depends only on its free variables · Substituting into a generalization is more general · Completeness of Algorithm W · A term is fixed by substituting it for a variable it avoids

TheoremVariables of a substituted term#✓fully proved

Let \(s\) be a substitution and \(t\) a term. Every variable of the term obtained by applying \(s\) to \(t\) is a variable of \(s(y)\) for some variable \(y\) of \(t\).

theorem exists_of_mem_vars_subst {s : Subst C} {t : Term C} {z : ℕ}
    (hz : z ∈ (t.subst s).vars) : ∃ y ∈ t.vars, z ∈ (s y).vars
Uses 4 · Used by 5
Statement usesSubstitution · Terms for unification · Applying a substitution to a term · Variables of a term
Used byRenaming step of the substitution lemma · Substituting into a generalization is more general · Completeness of Algorithm W · Freshness invariants of Algorithm W · The elimination step of unification introduces no variables

TheoremVariables of a substituted variable occur in the substituted term#✓fully proved

For every substitution \(s\), term \(t\) and variable \(y\) occurring in \(t\), every variable of the term \(s(y)\) occurs in the term obtained from \(t\) by applying \(s\).

theorem vars_subset_vars_subst {s : Subst C} {t : Term C} {y : ℕ}
    (hy : y ∈ t.vars) : (s y).vars ⊆ (t.subst s).vars
Uses 4 · Used by 2
Statement usesSubstitution · Terms for unification · Applying a substitution to a term · Variables of a term
Used byRenaming step of the substitution lemma · Substituting into a generalization is more general

TheoremOccurs check: size bound#✓fully proved

Let \(x\) be a variable and \(t\) a term in which \(x\) occurs, with \(t\) not the variable \(x\) itself. Then for every substitution \(\sigma\), the term \(\sigma(x)\) has strictly smaller size than \(t\sigma\), the result of applying \(\sigma\) to \(t\).

Consequently the equation \(x = t\) has no unifier when \(x\) occurs in \(t\) and \(t \ne x\) (the occurs check).

theorem size_subst_lt_of_mem {x : ℕ} {t : Term C} (hx : x ∈ t.vars) (ht : t ≠ var x)
    (s : Subst C) : (s x).size < (t.subst s).size
Uses 5 · Used by 3
Statement usesSubstitution · Terms for unification · Size of a term · Applying a substitution to a term · Variables of a term
Used bySoundness of unification · Completeness of unification · Most generality of unification

TheoremSubstituting for a variable that does not occur in the substituted term#✓fully proved

Let \(x\) be a variable and \(t\) a term in which \(x\) does not occur. For every term \(u\), every variable of the term obtained from \(u\) by replacing each occurrence of \(x\) with \(t\) is a variable of \(u\) or of \(t\), and is different from \(x\).

theorem vars_subst_single_subset {x : ℕ} {t : Term C} (hxt : x ∉ t.vars) (u : Term C) :
    (u.subst fun y ↦ if y = x then t else var y).vars ⊆ (u.vars ∪ t.vars).erase x
Uses 3 · Used by 2
Statement usesTerms for unification · Applying a substitution to a term · Variables of a term
Used byEliminating a solved variable lowers the number of variables · The elimination step of unification introduces no variables

DefinitionComposition of substitutions on first-order terms#✓fully proved

For substitutions \(s\) and \(t\), the composite \(s \gg t\) (first \(s\), then \(t\)) sends each variable \(x\) to the term obtained from \(s(x)\) by applying \(t\) to every variable of \(s(x)\).

def comp (s t : Subst C) : Subst C := fun x ↦ (s x).subst t
Uses 2 · Used by 18
Statement usesSubstitution · Applying a substitution to a term
Used bySoundness of Algorithm W · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W · Lists of equations with the same unifiers satisfy the same specification · The elimination step preserves the unification specification · Most general unifier · Unification returns a most general unifier · Failure is correct when the first equation has no unifier · Absorbing a single-variable substitution · Soundness of unification · Martelli–Montanari unification · Unification returns an idempotent substitution · Completeness of unification · Most generality of unification · Specification of a unification result · The elimination step of unification introduces no variables · Unification introduces no new variables

DefinitionSingle-variable substitution on first-order terms#✓fully proved

For a variable \(x\) and a term \(t\), the substitution \([x \mapsto t]\) sends \(x\) to \(t\) and every other variable \(y\) to the term \(y\).

def single (x : ℕ) (t : Term C) : Subst C := fun y ↦ if y = x then t else var y
Uses 2 · Used by 10
Statement usesSubstitution · Terms for unification
Used byEliminating a solved variable lowers the number of variables · The elimination step preserves the unification specification · Absorbing a single-variable substitution · A term is fixed by substituting it for a variable it avoids · Soundness of unification · Martelli–Montanari unification · Completeness of unification · Most generality of unification · The elimination step of unification introduces no variables · Unification introduces no new variables

TheoremAbsorbing a single-variable substitution#✓fully proved

Let \(x\) be a variable, \(t\) a term, and \([x \mapsto t]\) the substitution replacing \(x\) by \(t\) and fixing every other variable. If a substitution \(\sigma\) satisfies \(\sigma(x) = t\sigma\), where \(t\sigma\) is the result of applying \(\sigma\) to \(t\), then the composite substitution that applies \([x \mapsto t]\) first and \(\sigma\) second equals \(\sigma\).

theorem single_comp_eq {x : ℕ} {t : Term C} {s : Subst C} (h : s x = t.subst s) :
    single x t ≫ s = s
Uses 5 · Used by 1
Statement usesSubstitution · Composition of substitutions on first-order terms · Single-variable substitution on first-order terms · Terms for unification · Applying a substitution to a term
Used byThe elimination step preserves the unification specification

TheoremA term is fixed by substituting it for a variable it avoids#✓fully proved

If the variable \(x\) does not occur in the term \(t\), then applying to \(t\) the substitution \([x \mapsto t]\), which replaces \(x\) by \(t\) and fixes every other variable, leaves \(t\) unchanged.

theorem subst_single_of_not_mem {x : ℕ} {t : Term C} (hxt : x ∉ t.vars) :
    t.subst (single x t) = t
Uses 5 · Used by 1
Statement usesSingle-variable substitution on first-order terms · Terms for unification · Applying a substitution to a term · Variables of a term
Proof usesSubstitution depends only on the variables of the term
Used byThe elimination step preserves the unification specification
33 fully proved

Unifiers

AbbreviationLists of equations#✓fully proved

A list of equations over constants \(C\) is a finite list of pairs \((t, u)\) of terms over \(C\), each pair standing for the equation \(t = u\).

abbrev Equations (C : Type u) := List (Term C × Term C)
Uses 1 · Used by 20
Statement usesTerms for unification
Used bySoundness of Algorithm W · Completeness of Algorithm W · Eliminating a solved variable lowers the number of variables · Lists of equations with the same unifiers satisfy the same specification · The elimination step preserves the unification specification · Total size of a list of equations · Variables of a list of equations · Most general unifier · Unification returns a most general unifier · Failure is correct when the first equation has no unifier · Applying a substitution to a list of equations · Unifier of a list of equations · Soundness of unification · Martelli–Montanari unification · Unification returns an idempotent substitution · Completeness of unification · Most generality of unification · Specification of a unification result · The elimination step of unification introduces no variables · Unification introduces no new variables

DefinitionUnifier of a list of equations#✓fully proved

A substitution \(s\) unifies a list \(E\) of equations between terms when, for every equation \((t, u)\) in \(E\), applying \(s\) to \(t\) and applying \(s\) to \(u\) give the same term.

def Unifies (s : Subst C) (E : Equations C) : Prop := ∀ e ∈ E, e.1.subst s = e.2.subst s
Uses 4 · Used by 11
Statement usesLists of equations · Substitution · Terms for unification · Applying a substitution to a term
Used bySoundness of Algorithm W · Completeness of Algorithm W · Lists of equations with the same unifiers satisfy the same specification · The elimination step preserves the unification specification · Most general unifier · Unification returns a most general unifier · Failure is correct when the first equation has no unifier · Soundness of unification · Completeness of unification · Most generality of unification · Specification of a unification result

DefinitionMost general unifier#✓fully proved

A substitution \(s\) is a most general unifier of a list of equations \(E\) when \(s\) unifies \(E\) and every unifier \(s'\) of \(E\) factors through \(s\), that is, \(s' = s \gg r\) for some substitution \(r\), where \(s \gg r\) applies first \(s\) and then \(r\).

def IsMGU (s : Subst C) (E : Equations C) : Prop :=
  Unifies s E ∧ ∀ s', Unifies s' E → ∃ r, s' = s ≫ r
Uses 4 · Used by 1
Statement usesLists of equations · Substitution · Composition of substitutions on first-order terms · Unifier of a list of equations
Used byUnification returns a most general unifier

DefinitionApplying a substitution to a list of equations#✓fully proved

For a substitution \(\sigma\) and a list \(E\) of equations between terms, the result is the list obtained by replacing each equation \(u = v\) of \(E\), in order, by \(u\sigma = v\sigma\), where \(u\sigma\) is the result of applying \(\sigma\) to \(u\).

def substEqs (s : Subst C) (E : Equations C) : Equations C :=
  E.map fun e ↦ (e.1.subst s, e.2.subst s)
Uses 4 · Used by 8
Statement usesLists of equations · Substitution · Terms for unification · Applying a substitution to a term
Used byEliminating a solved variable lowers the number of variables · The elimination step preserves the unification specification · Soundness of unification · Martelli–Montanari unification · Completeness of unification · Most generality of unification · The elimination step of unification introduces no variables · Unification introduces no new variables

DefinitionVariables of a list of equations#✓fully proved

The variables of a list of equations form the finite set of all variables that occur on either side of any of its equations.

def eqVars : Equations C → Finset ℕ
  | [] => ∅
  | e :: E => e.1.vars ∪ e.2.vars ∪ eqVars E
Uses 3 · Used by 8
Statement usesLists of equations · Terms for unification · Variables of a term
Used byFreshness invariants of Algorithm W · Eliminating a solved variable lowers the number of variables · Soundness of unification · Martelli–Montanari unification · Completeness of unification · Most generality of unification · The elimination step of unification introduces no variables · Unification introduces no new variables

DefinitionTotal size of a list of equations#✓fully proved

The total size of a list of equations is the sum, over all its equations, of the sizes of the two sides, where the size of a term is its number of variable, constant and node symbols.

def eqSize : Equations C → ℕ
  | [] => 0
  | e :: E => e.1.size + e.2.size + eqSize E
Uses 3 · Used by 5
Statement usesLists of equations · Terms for unification · Size of a term
Used bySoundness of unification · Martelli–Montanari unification · Completeness of unification · Most generality of unification · Unification introduces no new variables

TheoremEliminating a solved variable lowers the number of variables#✓fully proved

Let \(x\) be a variable, \(t\) a term in which \(x\) does not occur, and \(E\) a list of equations. Applying the substitution that replaces \(x\) by \(t\) (and fixes every other variable) to both sides of every equation of \(E\) gives a list of equations with strictly fewer distinct variables than the list obtained by putting the equation \(x = t\) in front of \(E\).

theorem card_eqVars_elim_lt {x : ℕ} {t : Term C} (hxt : x ∉ t.vars) (E : Equations C) :
    (eqVars (substEqs (single x t) E)).card < (eqVars ((var x, t) :: E)).card
Uses 8 · Used by 5
Statement usesLists of equations · Single-variable substitution on first-order terms · Terms for unification · Variables of a term · Variables of a list of equations · Applying a substitution to a list of equations
Proof usesApplying a substitution to a term · Substituting for a variable that does not occur in the substituted term
Used bySoundness of unification · Martelli–Montanari unification · Completeness of unification · Most generality of unification · Unification introduces no new variables

The algorithm

DefinitionMartelli–Montanari unification#✓fully proved

The algorithm takes a list of equations between terms and returns a substitution or fails. On the empty list it returns the identity substitution. Otherwise it looks at the first equation \(t = u\) and the remaining list \(E\). If \(t\) and \(u\) are the same variable, or the same constant, the equation is dropped and the algorithm continues on \(E\); if they are two different constants, it fails. If \(t\) is a variable \(x\) and \(u \ne x\), or else \(u\) is a variable \(x\) and \(t\) is not a variable, let \(v\) be the other side: the algorithm fails when \(x\) occurs in \(v\), and otherwise substitutes \(v\) for \(x\) on both sides of every equation of \(E\) and unifies the result; if that returns \(s\), it returns the substitution that applies first the replacement of \(x\) by \(v\) and then \(s\), and if that fails, it fails. If \(t\) and \(u\) are nodes with children \(l_1, r_1\) and \(l_2, r_2\), it continues on the list \(l_1 = l_2\), \(r_1 = r_2\) followed by \(E\). If one side is a constant and the other a node, it fails.

Cslib.Unification.unify · 38 lines 
def unify : Equations C → Option (Subst C)
  | [] => some var
  | (var x, var y) :: E =>
    if x = y then unify E
    else (unify (substEqs (single x (var y)) E)).map fun s ↦ single x (var y) ≫ s
  | (var x, t) :: E =>
    if x ∈ t.vars then none
    else (unify (substEqs (single x t) E)).map fun s ↦ single x t ≫ s
  | (t, var x) :: E =>
    if x ∈ t.vars then none
    else (unify (substEqs (single x t) E)).map fun s ↦ single x t ≫ s
  | (const c, const d) :: E => if c = d then unify E else none
  | (node l₁ r₁, node l₂ r₂) :: E => unify ((l₁, l₂) :: (r₁, r₂) :: E)
  | (const _, node _ _) :: _ => none
  | (node _ _, const _) :: _ => none
termination_by E => ((eqVars E).card, eqSize E)
decreasing_by
  · -- `x = x`: the same variables or fewer, smaller size
    refine lex_of_le_of_lt (Finset.card_le_card ?_) ?_
    · intro z hz
      simp [eqVars, hz]
    · simp only [eqSize, size]
      omega
  · exact Prod.Lex.left _ _ (card_eqVars_elim_lt (by simpa [vars] using ‹¬x = y›) _)
  · exact Prod.Lex.left _ _ (card_eqVars_elim_lt ‹_› _)
  · rw [eqVars_cons_swap]
    exact Prod.Lex.left _ _ (card_eqVars_elim_lt ‹_› _)
  · refine lex_of_le_of_lt (Finset.card_le_card ?_) ?_
    · intro z hz
      simp [eqVars, hz]
    · simp only [eqSize, size]
      omega
  · refine lex_of_le_of_lt (Finset.card_le_card ?_) ?_
    · intro z hz
      simp only [eqVars, vars, Finset.mem_union] at hz ⊢
      tauto
    · simp only [eqSize, size]
      omega
Uses 11 · Used by 10
Statement usesLists of equations · Substitution · Composition of substitutions on first-order terms · Single-variable substitution on first-order terms · Terms for unification · Size of a term · Variables of a term · Eliminating a solved variable lowers the number of variables · Total size of a list of equations · Variables of a list of equations · Applying a substitution to a list of equations
Used bySoundness of Algorithm W · Algorithm W · Completeness of Algorithm W · Freshness invariants of Algorithm W · Unification returns a most general unifier · Soundness of unification · Unification returns an idempotent substitution · Completeness of unification · Most generality of unification · Unification introduces no new variables

Correctness

DefinitionSpecification of a unification result#✓fully proved

Let \(E\) be a list of equations between terms and \(r\) either a substitution or failure. The specification holds for \(E\) and \(r\) when, if \(r\) is a substitution \(s\), then \(s\) unifies \(E\) and every substitution \(s'\) that unifies \(E\) equals the composite substitution that applies first \(s\) and then \(s'\); and, if \(r\) is failure, then no substitution unifies \(E\).

def UnifySpec (E : Equations C) (r : Option (Subst C)) : Prop :=
  (∀ s, r = some s → Unifies s E ∧ ∀ s', Unifies s' E → s' = s ≫ s') ∧
    (r = none → ∀ s', ¬ Unifies s' E)
Uses 4 · Used by 6
Statement usesLists of equations · Substitution · Composition of substitutions on first-order terms · Unifier of a list of equations
Used byLists of equations with the same unifiers satisfy the same specification · The elimination step preserves the unification specification · Failure is correct when the first equation has no unifier · Soundness of unification · Completeness of unification · Most generality of unification

TheoremLists of equations with the same unifiers satisfy the same specification#✓fully proved

Let \(E\) and \(E'\) be lists of equations such that a substitution unifies \(E\) exactly when it unifies \(E'\). If an optional substitution \(r\) satisfies the unification specification for \(E'\) (a returned substitution \(s\) unifies the list and every unifier \(s'\) of it satisfies \(s' = s \gg s'\), where \(s \gg s'\) applies first \(s\) and then \(s'\), and failure means the list has no unifier), then \(r\) satisfies the unification specification for \(E\).

theorem UnifySpec.congr {E E' : Equations C} {r : Option (Subst C)}
    (h : ∀ s, Unifies s E ↔ Unifies s E') (hE' : UnifySpec E' r) : UnifySpec E r
Uses 5 · Used by 3
Statement usesLists of equations · Substitution · Unifier of a list of equations · Specification of a unification result
Proof usesComposition of substitutions on first-order terms
Used bySoundness of unification · Completeness of unification · Most generality of unification

TheoremFailure is correct when the first equation has no unifier#✓fully proved

Let \(E\) be a list of equations between terms and let \(u = v\) be a further equation, where \(u\sigma\) denotes the result of applying a substitution \(\sigma\) to \(u\). If \(u\sigma \ne v\sigma\) for every substitution \(\sigma\), then returning no substitution meets the unification specification for the list obtained by putting \(u = v\) in front of \(E\): no substitution unifies that list.

theorem UnifySpec.none_of_head {e : Term C × Term C} {E : Equations C}
    (h : ∀ s : Subst C, e.1.subst s ≠ e.2.subst s) : UnifySpec (e :: E) none
Uses 7 · Used by 3
Statement usesLists of equations · Substitution · Terms for unification · Applying a substitution to a term · Specification of a unification result
Proof usesComposition of substitutions on first-order terms · Unifier of a list of equations
Used bySoundness of unification · Completeness of unification · Most generality of unification

TheoremThe elimination step preserves the unification specification#✓fully proved

Let \(x\) be a variable, \(t\) a term in which \(x\) does not occur, \(e\) an equation and \(E\) a list of equations. Suppose that for every substitution \(s\), the two sides of \(e\) become equal under \(s\) exactly when \(s(x)\) equals the result of applying \(s\) to \(t\). Let \(\sigma\) be the substitution that replaces \(x\) by \(t\) and fixes every other variable, and let \(E'\) be the list obtained by applying \(\sigma\) to both sides of every equation of \(E\). Suppose an optional substitution \(r\) satisfies the unification specification for \(E'\). Define the result \(r'\) by: when \(r\) returns a substitution \(s\), \(r'\) returns \(\sigma \gg s\), the composite that applies first \(\sigma\) and then \(s\); when \(r\) is failure, \(r'\) is failure. Then \(r'\) satisfies the unification specification for the list with head \(e\) and tail \(E\).

theorem UnifySpec.elim {x : ℕ} {t : Term C} {e : Term C × Term C} {E : Equations C}
    {r : Option (Subst C)} (hxt : x ∉ t.vars)
    (he : ∀ s : Subst C, e.1.subst s = e.2.subst s ↔ s x = t.subst s)
    (ih : UnifySpec (substEqs (single x t) E) r) :
    UnifySpec (e :: E) (r.map fun s ↦ single x t ≫ s)
Uses 12 · Used by 3
Statement usesLists of equations · Substitution · Composition of substitutions on first-order terms · Single-variable substitution on first-order terms · Terms for unification · Applying a substitution to a term · Variables of a term · Specification of a unification result · Applying a substitution to a list of equations
Proof usesAbsorbing a single-variable substitution · A term is fixed by substituting it for a variable it avoids · Unifier of a list of equations
Used bySoundness of unification · Completeness of unification · Most generality of unification

TheoremSoundness of unification#✓fully proved

For every list \(E\) of equations between terms, if the Martelli–Montanari algorithm returns a substitution \(s\) on \(E\), then \(s\) unifies \(E\): applying \(s\) to the two sides of any equation of \(E\) gives the same term.

theorem unifies_unify {E : Equations C} {s : Subst C} (h : unify E = some s) : Unifies s E
Uses 19 · Used by 4
Statement usesLists of equations · Substitution · Unifier of a list of equations · Martelli–Montanari unification
Proof usesComposition of substitutions on first-order terms · Single-variable substitution on first-order terms · Terms for unification · Size of a term · Occurs check: size bound · Applying a substitution to a term · Variables of a term · Specification of a unification result · Lists of equations with the same unifiers satisfy the same specification · The elimination step preserves the unification specification · Failure is correct when the first equation has no unifier · Eliminating a solved variable lowers the number of variables · Total size of a list of equations · Variables of a list of equations · Applying a substitution to a list of equations
Used bySoundness of Algorithm W · Unification returns a most general unifier · Unification returns an idempotent substitution · Completeness of unification

TheoremMost generality of unification#✓fully proved

For every list \(E\) of equations between terms, if the Martelli–Montanari algorithm returns a substitution \(s\) on \(E\), then every substitution \(s'\) that unifies \(E\) equals the composite substitution that applies first \(s\) and then \(s'\).

theorem unify_eq_some_comp {E : Equations C} {s : Subst C} (h : unify E = some s)
    {s' : Subst C} (hs' : Unifies s' E) : s' = s ≫ s'
Uses 19 · Used by 3
Statement usesLists of equations · Substitution · Composition of substitutions on first-order terms · Unifier of a list of equations · Martelli–Montanari unification
Proof usesSingle-variable substitution on first-order terms · Terms for unification · Size of a term · Occurs check: size bound · Applying a substitution to a term · Variables of a term · Specification of a unification result · Lists of equations with the same unifiers satisfy the same specification · The elimination step preserves the unification specification · Failure is correct when the first equation has no unifier · Eliminating a solved variable lowers the number of variables · Total size of a list of equations · Variables of a list of equations · Applying a substitution to a list of equations
Used byCompleteness of Algorithm W · Unification returns a most general unifier · Unification returns an idempotent substitution

TheoremUnification returns a most general unifier#✓fully proved

If the Martelli-Montanari unification algorithm, run on a list of equations \(E\), returns a substitution \(s\), then \(s\) is a most general unifier of \(E\).

theorem isMGU_unify {E : Equations C} {s : Subst C} (h : unify E = some s) : IsMGU s E
Uses 8
Statement usesLists of equations · Most general unifier · Substitution · Martelli–Montanari unification
Proof usesComposition of substitutions on first-order terms · Unifier of a list of equations · Soundness of unification · Most generality of unification

TheoremUnification returns an idempotent substitution#✓fully proved

For every list \(E\) of equations between terms, if the Martelli–Montanari algorithm returns a substitution \(s\) on \(E\), then \(s\) is idempotent: the composite substitution that applies first \(s\) and then \(s\) equals \(s\).

theorem unify_comp_self {E : Equations C} {s : Subst C} (h : unify E = some s) : s ≫ s = s
Uses 6
Statement usesLists of equations · Substitution · Composition of substitutions on first-order terms · Martelli–Montanari unification
Proof usesSoundness of unification · Most generality of unification

TheoremCompleteness of unification#✓fully proved

For every list \(E\) of equations between terms, the Martelli–Montanari algorithm fails on \(E\) if and only if no substitution unifies \(E\).

theorem unify_eq_none_iff {E : Equations C} : unify E = none ↔ ∀ s, ¬ Unifies s E
Uses 20 · Used by 1
Statement usesLists of equations · Substitution · Unifier of a list of equations · Martelli–Montanari unification
Proof usesComposition of substitutions on first-order terms · Single-variable substitution on first-order terms · Terms for unification · Size of a term · Occurs check: size bound · Applying a substitution to a term · Variables of a term · Specification of a unification result · Lists of equations with the same unifiers satisfy the same specification · The elimination step preserves the unification specification · Failure is correct when the first equation has no unifier · Eliminating a solved variable lowers the number of variables · Total size of a list of equations · Variables of a list of equations · Applying a substitution to a list of equations · Soundness of unification
Used byCompleteness of Algorithm W

Variables of the result

TheoremThe elimination step of unification introduces no variables#✓fully proved

Write \(V(F)\) for the set of variables of a list \(F\) of equations. Let \(x_0\) be a variable, \(t\) a term in which \(x_0\) does not occur, \(e = (e_1, e_2)\) an equation such that every variable of \(t\) occurs in \(e_1\) or \(e_2\), and \(E\) a list of equations, and let \(E'\) be obtained from \(E\) by substituting \(t\) for \(x_0\) on both sides of every equation. Let \(s_0\) be a substitution such that, for every variable \(x\), every variable of \(s_0(x)\) is \(x\) or lies in \(V(E')\), and let \(\sigma\) be the substitution that applies first the replacement of \(x_0\) by \(t\) and then \(s_0\). Then for every variable \(x\), every variable of \(\sigma(x)\) is \(x\), occurs in \(e_1\) or \(e_2\), or lies in \(V(E)\).

theorem vars_single_comp_subset {x₀ : ℕ} {t : Term C} {e : Term C × Term C}
    {E : Equations C} (hxt : x₀ ∉ t.vars) (hhead : t.vars ⊆ e.1.vars ∪ e.2.vars)
    {s₀ : Subst C} (ih : ∀ x, (s₀ x).vars ⊆ insert x (eqVars (substEqs (single x₀ t) E)))
    (x : ℕ) : ((single x₀ t ≫ s₀) x).vars ⊆ insert x (eqVars (e :: E))
Uses 11 · Used by 1
Statement usesLists of equations · Substitution · Composition of substitutions on first-order terms · Single-variable substitution on first-order terms · Terms for unification · Variables of a term · Variables of a list of equations · Applying a substitution to a list of equations
Proof usesVariables of a substituted term · Applying a substitution to a term · Substituting for a variable that does not occur in the substituted term
Used byUnification introduces no new variables

TheoremUnification introduces no new variables#✓fully proved

Let \(E\) be a list of equations between terms. If the unification algorithm succeeds on \(E\) and returns the substitution \(s\), then for every variable \(x\), each variable of the term \(s(x)\) is either \(x\) itself or a variable occurring in some equation of \(E\).

theorem vars_unify_subset (E : Equations C) :
    ∀ s, unify E = some s → ∀ x, (s x).vars ⊆ insert x (eqVars E)
Uses 13 · Used by 1
Statement usesLists of equations · Substitution · Variables of a term · Variables of a list of equations · Martelli–Montanari unification
Proof usesComposition of substitutions on first-order terms · Single-variable substitution on first-order terms · Terms for unification · Size of a term · Eliminating a solved variable lowers the number of variables · Total size of a list of equations · Applying a substitution to a list of equations · The elimination step of unification introduces no variables
Used byFreshness invariants of Algorithm W

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.