This PR extends the notion of “fixed parameter” of a recursive function
also to parameters that come after varying function. The main benefit is
that we get nicer induction principles.
Before the definition
```lean
def app (as : List α) (bs : List α) : List α :=
match as with
| [] => bs
| a::as => a :: app as bs
```
produced
```lean
app.induct.{u_1} {α : Type u_1} (motive : List α → List α → Prop) (case1 : ∀ (bs : List α), motive [] bs)
(case2 : ∀ (bs : List α) (a : α) (as : List α), motive as bs → motive (a :: as) bs) (as bs : List α) : motive as bs
```
and now you get
```lean
app.induct.{u_1} {α : Type u_1} (motive : List α → Prop) (case1 : motive [])
(case2 : ∀ (a : α) (as : List α), motive as → motive (a :: as)) (as : List α) : motive as
```
because `bs` is fixed throughout the recursion (and can completely be
dropped from the principle).
This is a breaking change when such an induction principle is used
explicitly. Using `fun_induction` makes proof tactics robust against
this change.
The rules for when a parameter is fixed are now:
1. A parameter is fixed if it is reducibly defq to the the corresponding
argument in each recursive call, so we have to look at each such call.
2. With mutual recursion, it is not clear a-priori which arguments of
another function correspond to the parameter. This requires an analysis
with some graph algorithms to determine.
3. A parameter can only be fixed if all parameters occurring in its type
are fixed as well.
This dependency graph on parameters can be different for the different
functions in a recursive group, even leading to cycles.
4. For structural recursion, we kinda want to know the fixed parameters
before investigating which argument to actually recurs on. But once we
have that we may find that we fixed an index of the recursive
parameter’s type, and these cannot be fixed. So we have to un-fix them
5. … and all other fixed parameters that have dependencies on them.
Lean tries to identify the largest set of parameters that satisfies
these criteria.
Note that in a definition like
```lean
def app : List α → List α → List α
| [], bs => bs
| a::as, bs => a :: app as bs
```
the `bs` is not considered fixes, as it goes through the matcher
machinery.
Fixes#7027Fixes#2113
the support for mutual structural recursion (new since #4575) is
extended so that Lean tries to infer it even without annotations.
* The error message when termination checking fails looks quite
different now. Maybe a bit better, maybe with more room for
improvements.
* If there are too many combinations (with an arbitrary cut-off) for a
given argument type, it will just give up and ask the user to use
`termination_by structural`.
* It is now legal to specify `termination_by structural` on not
necessarily all functions of a clique; this simply restricts the
combinations of arguments that Lean considers.
---------
Co-authored-by: Tobias Grosser <tobias@grosser.es>
this is in preparation for #4542, and extracts from `findRecArg` the
functionality for trying one particular argument.
It also refactors the code a bit. In particular
* It reports errors in the order of the parameters, not the order of
in which they are tried (it tries non-indices first).
* For every argument it will say why it wasn't tried, even if the
reason is quite obviously (fixed prefix, or `Prop`-typed etc.)
Therefore there is some error message churn.
This didn't work before
```
def f (n : Nat) : Nat :=
match n with
| 0 => 0
| n + 1 => (f) n
```
because the `RecApp` metadata marker gets in the way. More practically
relevant, such code is to be produced when using `rw` or `simp` in
recursive theorems (see included test case).
We can fix this by preprocessing the definitions and floating the
`.mdata` marker out of applications.
For structural recursion, there already exists a `preprocess` function;
this now also floats out `.mdata` markers.
For well-founded recursion, this introduces an analogous `preprocess`
function.
Fixes#2810.
One test case output changes: With the `.mdata` out of the way, we get a
different error message. Seems fine.
Alternative approaches are:
* Leaving the `.mdata` marker where it is, and looking around it.
Tried in #2813, but not nice (many many places where `withApp` etc.
need to be adjusted).
* Moving the `.mdata` _inside_ the application, so that `withApp` still
works. Tried in #2814. Also not nice, the invariant that the `.mdata`
is around the `.const` is tedious to maintain.
