Is there a built-in function to do logarithm to base 2 with coq?

Found https://coq.inria.fr/library/Coq.Numbers.NatInt.NZLog.html but couldn't figure how to use it.

See all the different `log2`

in Stdlib here: https://coq.inria.fr/distrib/current/stdlib/index_global_L.html

Thanks!

Ju-sh has marked this topic as resolved.

I've been looking for this in Mathcomp recently for my FAV port, found some stuff in https://github.com/thery/mathcomp-extra/blob/master/more_thm.v

So I just copied it to my prelude and added a few lemmas of my own: https://github.com/clayrat/fav-ssr/blob/trunk/src/prelude.v#L103

There are also a floor and ceil log2 function for positives at the beginning of this file : (https://github.com/coq/coq/blob/master/theories/Reals/Cauchy/QExtra.v).

(Need to clean this up and move to proper places one day).

Last updated: Sep 30 2023 at 05:01 UTC