feat(tactic/unify_equations): add unify_equations tactic (#4515)

`unify_equations` is a first-order unification tactic for propositional
equalities. It implements the algorithm that `cases` uses to simplify
indices of inductive types, with one extension: `unify_equations` can
derive a contradiction from 'cyclic' equations like `n = n + 1`.

`unify_equations` is unlikely to be particularly useful on its own, but
I'll use it as part of my new `induction` tactic.

docs/references.bib

@@ -440,6 +440,15 @@ @Article{FennRourke1992
   mrnumber  = {1194995}
 }
 
+@inproceedings{mcbride1996,
+  title={Inverting inductively defined relations in {LEGO}},
+  author={McBride, Conor},
+  booktitle={International Workshop on Types for Proofs and Programs},
+  pages={236--253},
+  year={1996},
+  organization={Springer}
+}
+
 @book{rudin2006real,
   title={Real and Complex Analysis},
   author={Rudin, Walter},
@@ -454,4 +463,4 @@ @book{LurieSAG
   author={Jacob Lurie},
   url={https://www.math.ias.edu/~lurie/papers/SAG-rootfile.pdf},
   year={last updated 2018},
-}
+}

src/tactic/basic.lean

@@ -34,4 +34,5 @@ import tactic.squeeze
 import tactic.suggest
 import tactic.tauto
 import tactic.trunc_cases
+import tactic.unify_equations
 import tactic.where

src/tactic/core.lean

@@ -218,14 +218,14 @@ whnf type >>= get_expl_pi_arity_aux
 meta def get_expl_arity (fn : expr) : tactic nat :=
 infer_type fn >>= get_expl_pi_arity
 
-/--
-Auxiliary function for `get_app_fn_args_whnf`.
--/
 private meta def get_app_fn_args_whnf_aux (md : transparency)
   (unfold_ginductive : bool) : list expr → expr → tactic (expr × list expr) :=
 λ args e, do
-  (expr.app t u) ← whnf e md unfold_ginductive | pure (e, args),
-  get_app_fn_args_whnf_aux (u :: args) t
+  e ← whnf e md unfold_ginductive,
+  match e with
+  | (expr.app t u) := get_app_fn_args_whnf_aux (u :: args) t
+  | _ := pure (e, args)
+  end
 
 /--
 For `e = f x₁ ... xₙ`, `get_app_fn_args_whnf e` returns `(f, [x₁, ..., xₙ])`. `e`
@@ -234,6 +234,8 @@ is normalised as necessary; for example:
 ```
 get_app_fn_args_whnf `(let f := g x in f y) = (`(g), [`(x), `(y)])
 ```
+
+The returned expression is in whnf, but the arguments are generally not.
 -/
 meta def get_app_fn_args_whnf (e : expr) (md := semireducible)
   (unfold_ginductive := tt) : tactic (expr × list expr) :=
@@ -242,12 +244,31 @@ get_app_fn_args_whnf_aux md unfold_ginductive [] e
 /--
 `get_app_fn_whnf e md unfold_ginductive` is like `expr.get_app_fn e` but `e` is
 normalised as necessary (with transparency `md`). `unfold_ginductive` controls
-whether constructors of generalised inductive types are unfolded.
+whether constructors of generalised inductive types are unfolded. The returned
+expression is in whnf.
 -/
 meta def get_app_fn_whnf : expr → opt_param _ semireducible → opt_param _ tt → tactic expr
 | e md unfold_ginductive := do
-  (expr.app f _) ← whnf e md unfold_ginductive | pure e,
-  get_app_fn_whnf f md
+  e ← whnf e md unfold_ginductive,
+  match e with
+  | (expr.app f _) := get_app_fn_whnf f md unfold_ginductive
+  | _ := pure e
+  end
+
+/--
+`get_app_fn_const_whnf e md unfold_ginductive` expects that `e = C x₁ ... xₙ`,
+where `C` is a constant, after normalisation with transparency `md`. If so, the
+name of `C` is returned. Otherwise the tactic fails. `unfold_ginductive`
+controls whether constructors of generalised inductive types are unfolded.
+-/
+meta def get_app_fn_const_whnf (e : expr) (md := semireducible)
+  (unfold_ginductive := tt) : tactic name := do
+  f ← get_app_fn_whnf e md unfold_ginductive,
+  match f with
+  | (expr.const n _) := pure n
+  | _ := fail format!
+    "expected a constant (possibly applied to some arguments), but got:\n{e}"
+  end
 
 /-- `pis loc_consts f` is used to create a pi expression whose body is `f`.
 `loc_consts` should be a list of local constants. The function will abstract these local