The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Because it is an instance of a more general property


https://coq.inria.fr/distrib/V8.4/stdlib/Coq.Numbers.NatInt.NZLog.html#NZLog2Prop.log2_pow2

for the case of both naturals and integers. The module system is used to 
specialize it.

On 02/19/2015 06:21 PM, Jean-Francois Monin wrote:
> The statement of Nat.log2_pow2 is very strange:
> why on the hell do they add the precondition add 0 <= nat ???
>
> My 2 cts,
> JF
>
> On Thu, Feb 19, 2015 at 11:08:05AM -0500, Abhishek Anand wrote:
> >     The official library-docs don't tell the full story :)
> >     Coq provides much more powerful ways to search for content.
> >     You might want to learn about commands lke SearchAbout, SearchPattern,
> >     SearchRewrite, e.t.c :
> >     [1]https://coq.inria.fr/distrib/current/refman/command-index.html
> >     The commands I used to find the lemma are there in the email itself.
> >     If you open CoqIDE and type the following 2 lines, Nat.log2_pow2 will show
> >     up in the RHS bottom sub-window
> >     Require Export Coq.Numbers.Natural.Peano.NPeano.
> >     SearchAbout (log2 (2^?x)).
> >     Here is a screenshot:
> >     [2]https://dl.dropboxusercontent.com/u/79447152/CoqIDESearch.png
> >     Regards,
> >     -- Abhishek
> >     [3]http://www.cs.cornell.edu/~aa755/
> >     On Thu, Feb 19, 2015 at 10:42 AM, Michel Levy
> >     
> > <[4]michel.levy1948 AT gmail.com>
> >  wrote:
> >
> >       On 19/02/2015 16:12, Abhishek Anand wrote:
> >
> >         It is already there in the standard library:
> >         Require Export Coq.Numbers.Natural.Peano.NPeano.
> >         SearchAbout (log2 (2^?x)).
> >         (*
> >         Nat.log2_pow2: forall a : nat, 0 <= a -> log2 (2 ^ a) = a
> >         *)
> >         -- Abhishek
> >         [5]http://www.cs.cornell.edu/~aa755/
> >
> >       Thank you really much for your answer.
> >       But how did you find it ? I was looking at the "official doc" in
> >
> >       
> > [6]https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.Natural.Peano.NPeano.html
> >       and I don't find Nat.log2_pow2 on this page or in the web index of the
> >       standard library.
> >
> >       Sincerely yours.