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: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it.
  • Date: Thu, 19 Feb 2015 10:12:49 -0500

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




On Thu, Feb 19, 2015 at 9:09 AM, michel levy <michel.levy1948 AT gmail.com> wrote:
I want to prove some property of power like
  Lemma log2_power2 : forall x:nat, log2(2^x)=x.
It seems to me that I need the monotonicity properties written in Coq.Numbers.Natural.Abstract.NPow but
I don't know how to use these properties.
With  "Locate pow_l_r." I have the (sad) answer "No object of basename pow_l_r".

Can you help me ?

-- 
email : michel.levy AT imag.fr
http://membres-liglab.imag.fr/michel.levy 




Archive powered by MHonArc 2.6.18.

Top of Page