unify_equations tactic #
This module defines
unify_equations, a first-order unification tactic that
unifies one or more equations in the context. It implements the Qnify algorithm
from McBride, Inverting Inductively Defined Relations in LEGO.
The tactic takes as input some equations which it simplifies one after the
other. Each equation is simplified by applying one of several possible
unification steps. Each such step may output other (simpler) equations which are
unified recursively until no unification step applies any more. See
tactic.interactive.unify_equations for an example and an explanation of the
unify_equations eq₁ ... eqₙ performs a form of first-order unification on the
eqᵢ must be homogeneous or heterogeneous equations.
Unification means that the equations are simplified using various facts about
constructors. For instance, consider this goal:
unify_equations h₁ h₂, we get
In the example,
unify_equations uses the fact that every constructor is
injective to conclude
n = m from
h₁. Then it replaces every
moves on to
h₂. The types of
g are now equal, so the heterogeneous
equation turns into a homogeneous one and
g is replaced by
f. Note that the
equations are processed from left to right, so
unify_equations h₂ h₁ would not
simplify as much.
unify_equations uses the following steps on each equation until
none of them applies any more:
- Constructor injectivity: if
nat.succ n = nat.succ mthen
n = m.
- Substitution: if
x = efor some hypothesis
xis replaced by
nat.succ n = nat.zerois a contradiction. If we have such an equation, the goal is solved immediately.
- Cycle elimination:
n = nat.succ nis a contradiction.
- Redundancy: if
t = ubut
uare already definitionally equal, then this equation is removed.
- Downgrading of heterogeneous equations: if
t == ubut
uhave the same type (up to definitional equality), then the equation is replaced by
t = u.