This PR almost completely rewrites the inductive predicate recursion
algorithm; in particular `IndPredBelow` to function more consistently.
Historically, the `brecOn` generation through `IndPredBelow` has been
very error-prone -- this should be fixed now since the new algorithm is
very direct and doesn't rely on tactics or meta-variables at all.
Additionally, the new structural recursion procedure for inductive
predicates shares more code with regular structural recursion and thus
allows for mutual and nested recursion in the same way it was possible
with regular structural recursion. For example, the following works now:
```lean-4
mutual
inductive Even : Nat → Prop where
| zero : Even 0
| succ (h : Odd n) : Even n.succ
inductive Odd : Nat → Prop where
| succ (h : Even n) : Odd n.succ
end
mutual
theorem Even.exists (h : Even n) : ∃ a, n = 2 * a :=
match h with
| .zero => ⟨0, rfl⟩
| .succ h =>
have ⟨a, ha⟩ := h.exists
⟨a + 1, congrArg Nat.succ ha⟩
termination_by structural h
theorem Odd.exists (h : Odd n) : ∃ a, n = 2 * a + 1 :=
match h with
| .succ h =>
have ⟨a, ha⟩ := h.exists
⟨a, congrArg Nat.succ ha⟩
termination_by structural h
end
```
Closes#1672Closes#10004
this improves support for structural recursion over inductive
*predicates* when there are reflexive arguments.
Consider
```lean
inductive F: Prop where
| base
| step (fn: Nat → F)
-- set_option trace.Meta.IndPredBelow.search true
set_option pp.proofs true
def F.asdf1 : (f : F) → True
| base => trivial
| step f => F.asdf1 (f 0)
termination_by structural f => f`
```
Previously the search for the right induction hypothesis would fail with
```
could not solve using backwards chaining x✝¹ : F
x✝ : x✝¹.below
f : Nat → F
a✝¹ : ∀ (a : Nat), (f a).below
a✝ : Nat → True
⊢ True
```
The backchaining process will try to use `a✝ : Nat → True`, but then has
no idea what to use for `Nat`.
There are three steps here to fix this.
1. We let-bind the function's type before the whole process. Now the
goal is
```
funType : F → Prop := fun x => True
x✝ : x✝¹.below
f : Nat → F
a✝¹ : ∀ (a : Nat), (f a).below
a✝ : ∀ (a : Nat), funType (f a)
⊢ funType (f 0)
```
2. Instead of using the general purpose backchaining proof search, which
is more
powerful than we need here (we need on recursive search and no
backtracking),
we have a custom search that looks for local assumptions that
provide evidence of `funType`, and extracts the arguments from that
“type” application to construct the recursive call.
Above, it will thus unify `f a =?= f 0`.
3. In order to make progress here, we also turn on use
`withoutProofIrrelevance`,
because else `isDefEq` is happy to say “they are equal” without actually
looking
at the terms and thus assigning `?a := 0`.
This idea of let-binding the function's motive may also be useful for
the other recursion compilers, as it may simplify the FunInd
construction. This is to be investigated.
fixes#4751
Many of our tests in `tests/lean/run/` produce output from `#eval` (or
`#check`) statements, that is then ignored.
This PR tries to capture all the useful output using `#guard_msgs`. I've
only done a cursory check that the output is still sane --- there is a
chance that some "unchecked" tests have already accumulated regressions
and this just cements them!
In the other direction, I did identify two rotten tests:
* a minor one in `setStructInstNotation.lean`, where a comment says `Set
Nat`, but `#check` actually prints `?_`. Weird?
* `CompilerProbe.lean` is generating empty output, apparently indicating
that something is broken, but I don't know the signficance of this file.
In any case, I'll ask about these elsewhere.
(This started by noticing that a recent `grind` test file had an
untested `trace_state`, and then got carried away.)
@Kha The structural recursion is working :)
It is so much more powerful than the one in Lean3.
I added examples with `let rec`, nested and multiple
`match`-expressions.
I will keep testing and adding missing features tomorrow, and
will hopefully start porting stdlib to new frontend before the end of
the week.
