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
Given equ : n + m = n or equ : n = n + m with n and m natural numbers
and m a nonzero literal, this tactic produces a proof of false. More
precisely, the two sides of the equation must be of the form
nat.succ (... (nat.succ e)...) with different numbers of nat.succ
constructors. Matching is performed with transparency md.
For equ : t = u, try the following methods in order: unify_defeq,
unify_var, unify_constructor_headed, unify_cyclic. If any of them is
successful, stop and return its result. If none is successful, fail.
If equ is the display name of a local constant with type t = u or t == u,
then unify_equation_once equ simplifies it once using
unify_equations.unify_homogeneous or unify_equations.unify_heterogeneous.
Given a list of display names of local hypotheses that are (homogeneous or
heterogeneous) equations, unify_equations performs first-order unification on
each hypothesis in order. See tactic.interactive.unify_equations for an
example and an explanation of what unification does.
Returns true iff the goal has been solved during the unification process.
Note: you must make sure that the input names are unique in the context.
unify_equations eq₁ ... eqₙ performs a form of first-order unification on the
hypotheses eqᵢ. 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:
In the example, unify_equations uses the fact that every constructor is
injective to conclude n = m from h₁. Then it replaces every m with n and
moves on to h₂. The types of f and 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.
In general, unify_equations uses the following steps on each equation until
none of them applies any more: