From 0cb098205ba6d85674659bf5d0bfc0ed942464cc Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 2 Nov 2010 15:10:47 +0000 Subject: Numbers: misc improvements - Add alternate specifications of pow and sqrt - Slightly more general pow_lt_mono_r - More explicit equivalence of Plog2_Z and log_inf - Nicer proofs in Zpower git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13607 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/NatInt/NZLog.v | 52 ++++++++++++++++++++++++++--------------- 1 file changed, 33 insertions(+), 19 deletions(-) (limited to 'theories/Numbers/NatInt/NZLog.v') diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v index 4742cc699..34c57aad9 100644 --- a/theories/Numbers/NatInt/NZLog.v +++ b/theories/Numbers/NatInt/NZLog.v @@ -50,8 +50,8 @@ Qed. Ltac order_pos := ((apply add_pos_pos || apply add_nonneg_nonneg || apply mul_pos_pos || apply mul_nonneg_nonneg || - apply pow_nonneg || apply log2_nonneg || - apply (le_le_succ_r 0)); + apply pow_nonneg || apply pow_pos_nonneg || + apply log2_nonneg || apply (le_le_succ_r 0)); order_pos) (* in case of success of an apply, we recurse *) || order'. (* otherwise *) @@ -74,14 +74,42 @@ Proof. order. Qed. +(** An alternate specification *) + +Lemma log2_spec_alt : forall a, 0 exists r, + a == 2^(log2 a) + r /\ 0 <= r < 2^(log2 a). +Proof. + intros a Ha. + destruct (log2_spec _ Ha) as (LE,LT). + destruct (le_exists_sub _ _ LE) as (r & Hr & Hr'). + exists r. + split. now rewrite add_comm. + split. trivial. + apply (add_lt_mono_r _ _ (2^log2 a)). + rewrite <- Hr. generalize LT. + rewrite pow_succ_r by order_pos. + rewrite two_succ at 1. now nzsimpl. +Qed. + +Lemma log2_unique' : forall a b c, 0<=b -> 0<=c<2^b -> + a == 2^b + c -> log2 a == b. +Proof. + intros a b c Hb (Hc,H) EQ. + apply log2_unique. trivial. + rewrite EQ. + split. + rewrite <- add_0_r at 1. now apply add_le_mono_l. + rewrite pow_succ_r by order. + rewrite two_succ at 2. nzsimpl. now apply add_lt_mono_l. +Qed. + (** log2 is exact on powers of 2 *) Lemma log2_pow2 : forall a, 0<=a -> log2 (2^a) == a. Proof. intros a Ha. - apply log2_unique; trivial. - split. order. apply pow_lt_mono_r. order'. split; trivial. - apply lt_succ_diag_r. + apply log2_unique' with 0; trivial. + split; order_pos. now nzsimpl. Qed. (** log2 and basic constants *) @@ -257,20 +285,6 @@ Qed. (** The sum of two log2 is less than twice the log2 of the sum. This can almost be seen as a convexity inequality. *) -Lemma quadmul_le_squareadd : forall a b, 0<=a -> 0<=b -> - 2*2*a*b <= (a+b)*(a+b). -Proof. - intros. - nzsimpl'. - rewrite !mul_add_distr_l, !mul_add_distr_r. - rewrite (add_comm _ (b*b)), add_assoc. - apply add_le_mono_r. - rewrite (add_shuffle0 (a*a)), (mul_comm b a). - apply add_le_mono_r. - rewrite (mul_comm a b) at 1. - now apply crossmul_le_addsquare. -Qed. - Lemma add_log2_lt : forall a b, 0 0 log2 a + log2 b < 2 * log2 (a+b). Proof. -- cgit v1.2.3