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

4 files changed, 92 insertions, 35 deletions

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<a -> 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<a -> 0<b ->
  log2 a + log2 b < 2 * log2 (a+b).
 Proof.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 8f1b8cb6e..3eb9b4870 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -351,4 +351,18 @@ Proof.
  apply crossmul_le_addsquare; order.
 Qed.
 
+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.
+
 End NZMulOrderProp.
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
index db6e86ea7..76b745bf0 100644
--- a/theories/Numbers/NatInt/NZPow.v
+++ b/theories/Numbers/NatInt/NZPow.v
@@ -166,9 +166,11 @@ Proof.
  rewrite H, pow_0_r in Hb. order.
 Qed.
 
-Lemma pow_lt_mono_r : forall a b c, 1<a -> 0<=b<c -> a^b < a^c.
+Lemma pow_lt_mono_r : forall a b c, 1<a -> 0<=c -> b<c -> a^b < a^c.
 Proof.
- intros a b c Ha (Hb,H).
+ intros a b c Ha Hc H.
+ destruct (lt_ge_cases b 0) as [Hb|Hb].
+ rewrite pow_neg_r by trivial. apply pow_pos_nonneg; order'.
  assert (H' : b<=c) by order.
  destruct (le_exists_sub _ _ H') as (d & EQ & Hd).
  rewrite EQ, pow_add_r; trivial. rewrite <- (mul_1_l (a^b)) at 1.
@@ -189,7 +191,7 @@ Proof.
  apply le_succ_l in Ha; rewrite <- one_succ in Ha.
  apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha].
  apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H].
- apply lt_le_incl, pow_lt_mono_r; now try split.
+ apply lt_le_incl, pow_lt_mono_r; order.
  nzsimpl; order.
 Qed.
 
@@ -261,25 +263,25 @@ Proof.
  order.
 Qed.
 
-Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> 0<=b -> 0<=c ->
+Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> 0<=c ->
   (b<c <-> a^b < a^c).
 Proof.
- intros a b c Ha Hb Hc.
+ intros a b c Ha Hc.
  split; intro LT.
- apply pow_lt_mono_r; try split; trivial.
+ now apply pow_lt_mono_r.
  destruct (le_gt_cases c b) as [LE|GT]; trivial.
- assert (a^c <= a^b) by (apply pow_le_mono_r; try split; order').
+ assert (a^c <= a^b) by (apply pow_le_mono_r; order').
  order.
 Qed.
 
-Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=b -> 0<=c ->
+Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=c ->
   (b<=c <-> a^b <= a^c).
 Proof.
- intros a b c Ha Hb Hc.
+ intros a b c Ha Hc.
  split; intro LE.
- apply pow_le_mono_r; try split; trivial. order'.
+ apply pow_le_mono_r; order'.
  destruct (le_gt_cases b c) as [LE'|GT]; trivial.
- assert (a^c < a^b) by (apply pow_lt_mono_r; try split; order').
+ assert (a^c < a^b) by (apply pow_lt_mono_r; order').
  order.
 Qed.
 
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index d84748ee2..276c5e9c6 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -78,14 +78,42 @@ Proof.
  order.
 Qed.
 
+(** An alternate specification *)
+
+Lemma sqrt_spec_alt : forall a, 0<=a -> exists r,
+ a == √a * √a + r /\ 0 <= r <= 2*√a.
+Proof.
+ intros a Ha.
+ destruct (sqrt_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_le_mono_r _ _ (√a * √a)).
+ rewrite <- Hr, add_comm.
+ generalize LT. nzsimpl'. now rewrite lt_succ_r, add_assoc.
+Qed.
+
+Lemma sqrt_unique' : forall a b c, 0<=c<=2*b ->
+ a == b*b + c -> sqrt a == b.
+Proof.
+ intros a b c (Hc,H) EQ.
+ apply sqrt_unique.
+ rewrite EQ.
+ split.
+ rewrite <- add_0_r at 1. now apply add_le_mono_l.
+ nzsimpl. apply lt_succ_r.
+ rewrite <- add_assoc. apply add_le_mono_l.
+ generalize H; now nzsimpl'.
+Qed.
+
 (** Sqrt is exact on squares *)
 
 Lemma sqrt_square : forall a, 0<=a -> √(a*a) == a.
 Proof.
  intros a Ha.
- apply sqrt_unique.
- split. order.
- apply mul_lt_mono_nonneg; trivial using lt_succ_diag_r.
+ apply sqrt_unique' with 0.
+ split. order. apply mul_nonneg_nonneg; order'. now nzsimpl.
 Qed.
 
 (** Sqrt is a monotone function (but not a strict one) *)
@@ -158,8 +186,7 @@ Qed.
 
 Lemma sqrt_2 : √2 == 1.
 Proof.
- apply sqrt_unique. nzsimpl. split. order'.
- apply lt_succ_r, lt_le_incl, lt_succ_r. nzsimpl'; order.
+ apply sqrt_unique' with 1. nzsimpl; split; order'. now nzsimpl'.
 Qed.
 
 Lemma sqrt_lt_lin : forall a, 1<a -> √a<a.