f9dc77673b
This PR lets recursive functions defined by well-founded recursion use a different `fix` function when the termination measure is of type `Nat`. This fix-point operator use structural recursion on “fuel”, initialized by the given measure, and is thus reasonable to reduce, e.g. in `by decide` proofs. Extra provisions are in place that the fixpoint operator only starts reducing when the fuel is fully known, to prevent “accidential” defeqs when the remaining fuel for the recursive calls match the initial fuel for that recursive argument. To opt-out, the idiom `termination_by (n,0)` can be used. We still use `@[irreducible]` as the default for such recursive definitions, to avoid unexpected `defeq` lemmas. Making these functions `@[semireducible]` by default showed performance regressions in lean. When the measure is of type `Nat`, the system will accept an explicit `@[semireducible]` without the usual warning. Fixes #5234. Fixes: #11181.
109 lines
1.7 KiB
Text
109 lines
1.7 KiB
Text
/-!
|
|
Tests that definitions by well-founded recursion (not on Nat) are irreducible.
|
|
-/
|
|
|
|
set_option pp.mvars false
|
|
|
|
def foo : Nat → Nat → Nat
|
|
| 0, m => m
|
|
| n+1, m => foo n (m + n)
|
|
termination_by n m => (n, m)
|
|
|
|
/--
|
|
error: Type mismatch
|
|
rfl
|
|
has type
|
|
?_ = ?_
|
|
but is expected to have type
|
|
foo 0 m = m
|
|
-/
|
|
#guard_msgs in
|
|
example : foo 0 m = m := rfl
|
|
|
|
/--
|
|
error: Type mismatch
|
|
rfl
|
|
has type
|
|
?_ = ?_
|
|
but is expected to have type
|
|
foo (n + 1) m = foo n (m + n)
|
|
-/
|
|
#guard_msgs in
|
|
example : foo (n+1) m = foo n (m + n) := rfl
|
|
|
|
-- also for closed terms
|
|
/--
|
|
error: Tactic `rfl` failed: The left-hand side
|
|
foo 0 0
|
|
is not definitionally equal to the right-hand side
|
|
0
|
|
|
|
⊢ foo 0 0 = 0
|
|
-/
|
|
#guard_msgs in
|
|
example : foo 0 0 = 0 := by rfl
|
|
|
|
section Unsealed
|
|
|
|
unseal foo
|
|
|
|
-- unsealing works, but does not have the desired effect
|
|
|
|
/--
|
|
error: Type mismatch
|
|
rfl
|
|
has type
|
|
?_ = ?_
|
|
but is expected to have type
|
|
foo 0 0 = 0
|
|
-/
|
|
#guard_msgs in
|
|
example : foo 0 0 = 0 := rfl
|
|
|
|
/--
|
|
error: Type mismatch
|
|
rfl
|
|
has type
|
|
?_ = ?_
|
|
but is expected to have type
|
|
foo (n + 1) m = foo n (n + m)
|
|
-/
|
|
#guard_msgs in
|
|
example : foo (n+1) m = foo n (n +m ):= rfl
|
|
|
|
end Unsealed
|
|
|
|
--should be sealed again here
|
|
|
|
/--
|
|
error: Type mismatch
|
|
rfl
|
|
has type
|
|
?_ = ?_
|
|
but is expected to have type
|
|
foo 0 m = m
|
|
-/
|
|
#guard_msgs in
|
|
example : foo 0 m = m := rfl
|
|
|
|
def bar : Nat → Nat → Nat
|
|
| 0, m => m
|
|
| n+1, m => bar n (m + n)
|
|
termination_by n m => (n, m)
|
|
|
|
-- Once unsealed, the full internals are visible. This allows one to prove, for example
|
|
-- an equality like the following
|
|
|
|
/--
|
|
error: Type mismatch
|
|
rfl
|
|
has type
|
|
?_ = ?_
|
|
but is expected to have type
|
|
foo = bar
|
|
-/
|
|
#guard_msgs in
|
|
example : foo = bar := rfl
|
|
|
|
unseal foo bar in
|
|
example : foo = bar := rfl
|