int.sizeof

Stream: general

[Enrico Borba]

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 #print I can see the definition of 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]

I recommend breaking this into two definitions

[Mario Carneiro]

The equation compiler will accept the definition over nat, and the definition over int can refer to it in each branch

[Mario Carneiro]

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]

Splitting them up worked. Thank you for that suggestion.