3ab2c714ec
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>
87 lines
2.1 KiB
Text
87 lines
2.1 KiB
Text
|
|
def foo (n : Nat) : Nat := match n with
|
|
| 0 => 0
|
|
| n+1 => foo n
|
|
termination_by structural n
|
|
|
|
-- Test that this is indeed by structural recursion
|
|
example : foo (n + 3) = foo n := Eq.refl _
|
|
|
|
|
|
-- Check that we can still refer to a variable called `structural` in
|
|
-- the `termination_by` syntax
|
|
def bar (structural : Nat) : True := match structural with
|
|
| 0 => .intro
|
|
| structural+1 => bar structural
|
|
termination_by «structural»
|
|
|
|
namespace Errors
|
|
-- A few error conditions
|
|
|
|
/--
|
|
error: cannot use specified parameter for structural recursion:
|
|
it is unchanged in the recursive calls
|
|
-/
|
|
#guard_msgs in
|
|
def foo1 (n : Nat) : Nat := foo1 n
|
|
termination_by structural n
|
|
|
|
/--
|
|
error: cannot use specified parameter for structural recursion:
|
|
its type Nat.le is an inductive family and indices are not variables
|
|
n.succ.le 100
|
|
-/
|
|
#guard_msgs in
|
|
def foo2 (n : Nat) (h : n < 100) : Nat := match n with
|
|
| 0 => 0
|
|
| n+1 => foo2 n (by omega)
|
|
termination_by structural h
|
|
|
|
/--
|
|
error: one parameter bound in `termination_by`, but the body of Errors.foo3 only binds 0 parameters.
|
|
-/
|
|
#guard_msgs in
|
|
def foo3 (n : Nat) : Nat → Nat := match n with
|
|
| 0 => id
|
|
| n+1 => foo3 n
|
|
termination_by structural m => m
|
|
|
|
/--
|
|
error: failed to infer structural recursion:
|
|
Cannot use parameter n:
|
|
failed to eliminate recursive application
|
|
ackermann (n + 1) m
|
|
-/
|
|
#guard_msgs in
|
|
def ackermann (n m : Nat) := match n, m with
|
|
| 0, m => m + 1
|
|
| .succ n, 0 => ackermann n 1
|
|
| .succ n, .succ m => ackermann n (ackermann (n + 1) m)
|
|
termination_by structural n
|
|
|
|
/--
|
|
error: failed to infer structural recursion:
|
|
Cannot use parameter m:
|
|
failed to eliminate recursive application
|
|
ackermann2 n 1
|
|
-/
|
|
#guard_msgs in
|
|
def ackermann2 (n m : Nat) := match n, m with
|
|
| 0, m => m + 1
|
|
| .succ n, 0 => ackermann2 n 1
|
|
| .succ n, .succ m => ackermann2 n (ackermann2 (n + 1) m)
|
|
termination_by structural m
|
|
|
|
/--
|
|
error: The termination argument of a structurally recursive function must be one of the parameters 'n', but
|
|
id n + 1
|
|
isn't one of these.
|
|
-/
|
|
#guard_msgs in
|
|
def foo4 (n : Nat) : Nat → Nat := match n with
|
|
| 0 => id
|
|
| n+1 => foo4 n
|
|
termination_by structural id n + 1
|
|
|
|
|
|
end Errors
|