Zulip Chat Archive

Stream: general

Topic: int.sizeof


view this post on Zulip 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 #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?

view this post on Zulip Mario Carneiro (Jan 16 2020 at 07:04):

I recommend breaking this into two definitions

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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