Stream: Coq users

Topic: Why does N.log2_up 1 = 0 and not 1?

view this post on Zulip Rodolphe Lepigre (Nov 02 2023 at 10:49):

I just stumbled on this, and this looks very surprising to me. I would expect N.log2_up n to answer the question: how many bits do I need to represent n in binary, but that does not work for 1.

However, given the existence of N.log_2_up1 : N.log2_up 1 = 0 that seems to be done on purpose. Is there a good reason?

view this post on Zulip Gaëtan Gilbert (Nov 02 2023 at 10:59):

Lemma log2_up_pow2 : forall a, 0<=a -> log2_up (2^a) == a. only works with log2_up 1 = 0

Last updated: Jun 23 2024 at 04:03 UTC