coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., michel levy, 02/19/2015
- Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Abhishek Anand, 02/19/2015
- Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Michel Levy, 02/19/2015
- Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Abhishek Anand, 02/19/2015
- Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Jean-Francois Monin, 02/19/2015
- Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Robbert Krebbers, 02/19/2015
- Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Jean-Francois Monin, 02/19/2015
- Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Abhishek Anand, 02/19/2015
- Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Michel Levy, 02/19/2015
- Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Abhishek Anand, 02/19/2015
Archive powered by MHonArc 2.6.18.