Replaces `@[eliminator]` with two attributes `@[induction_eliminator]`
and `@[cases_eliminator]` for defining custom eliminators for the
`induction` and `cases` tactics, respectively.
Adds `Nat.recAux` and `Nat.casesAuxOn`, which are eliminators that are
defeq to `Nat.rec` and `Nat.casesOn`, but these use `0` and `n + 1`
rather than `Nat.zero` and `Nat.succ n`.
For example, using `induction` to prove that the factorial function is
positive now has the following goal states (thanks also to #3616 for the
goal state after unfolding).
```lean
example : 0 < fact x := by
induction x with
| zero => decide
| succ x ih =>
/-
x : Nat
ih : 0 < fact x
⊢ 0 < fact (x + 1)
-/
unfold fact
/-
...
⊢ 0 < (x + 1) * fact x
-/
simpa using ih
```
Thanks to @adamtopaz for initial work on splitting the `@[eliminator]`
attribute.
right now, the `induction` tactic accepts a custom eliminator using the
`using <ident>` syntax, but is restricted to identifiers. This
limitation becomes annoying when the elminator has explicit parameters
that are not targets, and the user (naturally) wants to be able to write
```
induction a, b, c using foo (x := …)
```
This generalizes the syntax to expressions and changes the code
accordingly.
This can be used to instantiate a multi-motive induction:
```
example (a : A) : True := by
induction a using A.rec (motive_2 := fun b => True)
case mkA b IH => exact trivial
case A => exact trivial
case mkB b IH => exact trivial
```
For this to work the term elaborator learned the `heedElabAsElim` flag,
`true` by default. But in the default setting, `A.rec (motive_2 := fun b
=> True)`
would fail to elaborate, because there is no expected type. So the
induction
tactic will elaborate in a mode where that attribute is simply ignored.
As a side effect, the “failed to infer implicit target” error message
is improved and prints the name of the implicit target that could not be
instantiated.
