Stream: Coq users

Topic: ✔ log2 in coq


view this post on Zulip Julin S (Nov 19 2021 at 13:03):

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.

view this post on Zulip Karl Palmskog (Nov 19 2021 at 13:13):

See all the different log2 in Stdlib here: https://coq.inria.fr/distrib/current/stdlib/index_global_L.html

view this post on Zulip Julin S (Nov 19 2021 at 13:19):

Thanks!

view this post on Zulip Notification Bot (Nov 19 2021 at 13:19):

Ju-sh has marked this topic as resolved.

view this post on Zulip Alexander Gryzlov (Nov 19 2021 at 16:21):

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

view this post on Zulip Alexander Gryzlov (Nov 19 2021 at 16:22):

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

view this post on Zulip Michael Soegtrop (Nov 19 2021 at 16:34):

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).

view this post on Zulip Michael Soegtrop (Nov 19 2021 at 16:35):

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


Last updated: Jan 29 2023 at 01:02 UTC