coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
*)
-- Abhishek
http://www.cs.cornell.edu/~aa755/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
- [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.