dede354e77
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.
41 lines
728 B
Text
41 lines
728 B
Text
/-!
|
|
Test that parentheses don't get in the way of structural recursion.
|
|
https://github.com/leanprover/lean4/issues/2810
|
|
-/
|
|
|
|
def f (n : Nat) : Nat :=
|
|
match n with
|
|
| 0 => 0
|
|
| n + 1 => (f) n
|
|
|
|
-- with beta-reduction
|
|
def f2 (n : Nat) : Nat :=
|
|
match n with
|
|
| 0 => 0
|
|
| n + 1 => (fun n' => (f2) n') n
|
|
|
|
-- structural recursion
|
|
def f3 (n : Nat) : Nat :=
|
|
match n with
|
|
| 0 => 0
|
|
| n + 1 => (f3) n
|
|
termination_by f3 n => n
|
|
|
|
-- Same with rewrite
|
|
|
|
theorem f_zero (n : Nat) : f n = 0 := by
|
|
match n with
|
|
| .zero => rfl
|
|
| .succ n =>
|
|
unfold f
|
|
rewrite [f_zero]
|
|
rfl
|
|
|
|
-- Same with simp
|
|
|
|
theorem f_zero' (n : Nat) : f n = 0 := by
|
|
match n with
|
|
| .zero => rfl
|
|
| .succ n =>
|
|
unfold f
|
|
simp only [f_zero']
|