Enrico Borba (Jan 16 2020 at 06:05):
I'm trying to define
fib over the naturals, but I can't seem to make the equation compiler happy. I tried writing
def fib : ℤ → ℤ | (int.of_nat 0) := 0 | (int.of_nat 1) := 1 | (int.of_nat (n + 2)) := fib (n + 1) + fib n | -[1+ n] := fib (-(1 + n) + 1) - fib (-(1 + n) + 2)
I need to prove a few things to have well founded recursion, one of them is
int.sizeof ↑n < n + 3. Using
int.sizeof and see that the statement I need to show is true. I couldn't find any docs on
int.sizeof though, and I also don't see it in
int.basic, what is it and why is it showing up here?
Mario Carneiro (Jan 16 2020 at 07:04):
I recommend breaking this into two definitions
Mario Carneiro (Jan 16 2020 at 07:05):
The equation compiler will accept the definition over
nat, and the definition over
int can refer to it in each branch
Mario Carneiro (Jan 16 2020 at 07:07):
If you see the equation compiler giving you subgoals about
X.sizeof, that just means it failed to prove it automatically and you need to supply your own well founded measure.
X.sizeof is almost never the measure you want to use
Enrico Borba (Jan 16 2020 at 18:42):
Splitting them up worked. Thank you for that suggestion.
Last updated: May 11 2021 at 21:10 UTC