Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it.


Chronological Thread 
  • From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it.
  • Date: Thu, 19 Feb 2015 18:36:44 +0100

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.



Archive powered by MHonArc 2.6.18.

Top of Page