feat: functional induction for structural recursion (#3738)

This extends `derive_functional_induction` to work with structural
recursion as well.

It produces the less general, more concrete induction rule where the
induction hypothesis is
specialized for every argument of the recursive call, not just the the
one that the function
is recursing on.

Care is taken so that the induction principle and it's motive take the
arguments in the same
order as the original function.

While I was it, also makes sure that the order of the cases in the
induction principle matches
the order of recursive calls in the function better.

---------

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>

RELEASES.md

@@ -23,9 +23,8 @@ v4.8.0 (development in progress)
 
 * New command `derive_functional_induction`:
 
-  Derived from the definition of a (possibly mutually) recursive function
-  defined by well-founded recursion, a **functional induction principle** is
-  tailored to proofs about that function. For example from:
+  Derived from the definition of a (possibly mutually) recursive function, a **functional induction
+  principle** is created that is tailored to proofs about that function. For example from:
   ```
   def ackermann : Nat → Nat → Nat
     | 0, m => m + 1
@@ -41,6 +40,11 @@ v4.8.0 (development in progress)
     (x x : Nat) : motive x x
   ```
 
+  It can be used in the `induction` tactic using the `using` syntax:
+  ```
+  induction n, m using ackermann.induct
+  ```
+
 * The termination checker now recognizes more recursion patterns without an
   explicit `termination_by`. In particular the idiom of counting up to an upper
   bound, as in

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -291,15 +291,15 @@ def transform
     let aux1 := mkApp aux1 motive'
     let aux1 := mkAppN aux1 discrs'
     unless (← isTypeCorrect aux1) do
-      logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux1}"
+      logError m!"failed to transform matcher, type error when constructing new pre-splitter motive:{indentExpr aux1}"
       check aux1
     let origAltTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux1)
 
     let aux2 := mkAppN (mkConst splitter matcherLevels.toList) params'
     let aux2 := mkApp aux2 motive'
     let aux2 := mkAppN aux2 discrs'
     unless (← isTypeCorrect aux2) do
-      logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux2}"
+      logError m!"failed to transform matcher, type error when constructing splitter motive:{indentExpr aux2}"
       check aux2
     let altTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux2)
 
@@ -339,7 +339,6 @@ def transform
     let aux := mkApp aux motive'
     let aux := mkAppN aux discrs'
     unless (← isTypeCorrect aux) do
-      -- check aux
       logError m!"failed to transform matcher, type error when constructing new motive:{indentExpr aux}"
       check aux
     let altTypes ← arrowDomainsN matcherApp.alts.size (← inferType aux)