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

8 files changed, 139 insertions, 132 deletions

diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v
index 4742cc6991..34c57aad9d 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 8f1b8cb6e9..3eb9b48702 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 db6e86ea7c..76b745bf01 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 d84748ee27..276c5e9c63 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.
diff --git a/theories/ZArith/Zlog_def.v b/theories/ZArith/Zlog_def.v
index 05ceca2013..588b33037d 100644
--- a/theories/ZArith/Zlog_def.v
+++ b/theories/ZArith/Zlog_def.v
@@ -12,8 +12,6 @@ Local Open Scope Z_scope.
 
 (** Definition of Zlog2 *)
 
-(** TODO: this is equal to Zlogarithm.log_inf *)
-
 Fixpoint Plog2_Z (p:positive) : Z :=
   match p with
     | 1 => Z0
@@ -32,16 +30,6 @@ Proof.
  induction p; simpl; auto with zarith.
 Qed.
 
-(** TODO : to move ... *)
-
-Lemma Zle_succ_l : forall n m, Zsucc n <= m <-> n < m.
-Proof.
- intros. split; intros H.
- rewrite (Zsucc_pred m). apply Zle_lt_succ, Zsucc_le_reg.
- now rewrite <- Zsucc_pred.
- now apply Zlt_le_succ.
-Qed.
-
 Lemma Plog2_Z_spec : forall p,
  2^(Plog2_Z p) <= Zpos p < 2^(Zsucc (Plog2_Z p)).
 Proof.
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index 7d5b41121d..7bb23db626 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -18,22 +18,16 @@
     - [Log_nearest]: [y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)]
       i.e. [Log_nearest x] is the integer nearest from [Log x] *)
 
-Require Import ZArith_base.
-Require Import Omega.
-Require Import Zcomplements.
-Require Import Zpower.
-Open Local Scope Z_scope.
+Require Import ZArith_base Omega Zcomplements Zlog_def Zpower.
+Local Open Scope Z_scope.
 
 Section Log_pos. (* Log of positive integers *)
 
   (** First we build [log_inf] and [log_sup] *)
 
-  Fixpoint log_inf (p:positive) : Z :=
-    match p with
-      | xH => 0	(* 1 *)
-      | xO q => Zsucc (log_inf q)	(* 2n *)
-      | xI q => Zsucc (log_inf q)	(* 2n+1 *)
-    end.
+  (** [log_inf] is exactly the same as the new [Plog2_Z] *)
+
+  Definition log_inf : positive -> Z := Eval red in Plog2_Z.
 
   Fixpoint log_sup (p:positive) : Z :=
     match p with
@@ -44,6 +38,9 @@ Section Log_pos. (* Log of positive integers *)
 
   Hint Unfold log_inf log_sup.
 
+  Lemma Zlog2_log_inf : forall p, Zlog2 (Zpos p) = log_inf p.
+  Proof. reflexivity. Qed.
+
   (** Then we give the specifications of [log_inf] and [log_sup]
     and prove their validity *)
 
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index ebce8ccdc7..1bd833d6fe 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -449,6 +449,14 @@ Proof.
   split; [apply Zlt_succ_le | apply Zle_lt_succ].
 Qed.
 
+Lemma Zle_succ_l : forall n m, Zsucc n <= m <-> n < m.
+Proof.
+ intros. split; intros H.
+ rewrite (Zsucc_pred m). apply Zle_lt_succ, Zsucc_le_reg.
+ now rewrite <- Zsucc_pred.
+ now apply Zlt_le_succ.
+Qed.
+
 (** Weakening order *)
 
 Lemma Zle_succ : forall n:Z, n <= Zsucc n.
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index bafee949d4..e08b7ebc34 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -44,8 +44,8 @@ Proof.
 Qed.
 
 (** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
-   deduce that the function [[n:positive](Zpower_pos z n)] is a morphism
-   for [add : positive->positive] and [Zmult : Z->Z] *)
+   deduce that the function [(Zpower_pos z)] is a morphism
+   for [Pplus : positive->positive] and [Zmult : Z->Z] *)
 
 Lemma Zpower_pos_is_exp :
   forall (n m:positive) (z:Z),
@@ -77,11 +77,8 @@ Section Powers_of_2.
   (** * Powers of 2 *)
 
   (** For the powers of two, that will be widely used, a more direct
-      calculus is possible. We will also prove some properties such
-      as [(x:positive) x < 2^x] that are true for all integers bigger
-      than 2 but more difficult to prove and useless. *)
-
-  (** [shift n m] computes [2^n * m], or [m] shifted by [n] positions *)
+      calculus is possible. [shift n m] computes [2^n * m], i.e.
+      [m] shifted by [n] positions *)
 
   Definition shift_nat (n:nat) (z:positive) := iter_nat n positive xO z.
   Definition shift_pos (n z:positive) := iter_pos n positive xO z.
@@ -97,32 +94,30 @@ Section Powers_of_2.
 
   Lemma two_power_nat_S :
     forall n:nat, two_power_nat (S n) = 2 * two_power_nat n.
-  Proof.
-    intro; simpl in |- *; apply refl_equal.
-  Qed.
+  Proof. reflexivity. Qed.
 
   Lemma shift_nat_plus :
     forall (n m:nat) (x:positive),
       shift_nat (n + m) x = shift_nat n (shift_nat m x).
   Proof.
-    intros; unfold shift_nat in |- *; apply iter_nat_plus.
+    intros; apply iter_nat_plus.
   Qed.
 
   Theorem shift_nat_correct :
     forall (n:nat) (x:positive), Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x.
   Proof.
-    unfold shift_nat in |- *; simple induction n;
-      [ simpl in |- *; trivial with zarith
-	| intros; replace (Zpower_nat 2 (S n0)) with (2 * Zpower_nat 2 n0);
-	  [ rewrite <- Zmult_assoc; rewrite <- (H x); simpl in |- *; reflexivity
-	    | auto with zarith ] ].
+    unfold shift_nat; induction n.
+    trivial.
+    intros x. simpl.
+    change (Zpower_nat 2 (S n)) with (2 * Zpower_nat 2 n).
+    now rewrite <- Zmult_assoc, <- IHn.
   Qed.
 
   Theorem two_power_nat_correct :
     forall n:nat, two_power_nat n = Zpower_nat 2 n.
   Proof.
     intro n.
-    unfold two_power_nat in |- *.
+    unfold two_power_nat.
     rewrite (shift_nat_correct n).
     omega.
   Qed.
@@ -131,17 +126,14 @@ Section Powers_of_2.
   Lemma shift_pos_nat :
     forall p x:positive, shift_pos p x = shift_nat (nat_of_P p) x.
   Proof.
-    unfold shift_pos in |- *.
-    unfold shift_nat in |- *.
-    intros; apply iter_nat_of_P.
+    unfold shift_pos, shift_nat. intros. apply iter_nat_of_P.
   Qed.
 
   Lemma two_power_pos_nat :
     forall p:positive, two_power_pos p = two_power_nat (nat_of_P p).
   Proof.
-    intro; unfold two_power_pos in |- *; unfold two_power_nat in |- *.
-    apply f_equal with (f := Zpos).
-    apply shift_pos_nat.
+    intro. unfold two_power_pos, two_power_nat.
+    f_equal. apply shift_pos_nat.
   Qed.
 
   (** Then we deduce that [two_power_pos] is also correct *)
@@ -170,11 +162,7 @@ Section Powers_of_2.
     forall x y:positive,
       two_power_pos (x + y) = two_power_pos x * two_power_pos y.
   Proof.
-    intros.
-    rewrite (two_power_pos_correct (x + y)).
-    rewrite (two_power_pos_correct x).
-    rewrite (two_power_pos_correct y).
-    apply Zpower_pos_is_exp.
+    intros. rewrite 3 two_power_pos_correct. apply Zpower_pos_is_exp.
   Qed.
 
   (** The exponentiation [z -> 2^z] for [z] a signed integer.
@@ -190,65 +178,34 @@ Section Powers_of_2.
       | Zneg y => 0
     end.
 
-  Theorem two_p_is_exp :
-    forall x y:Z, 0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y.
+  Lemma two_p_correct : forall x, two_p x = 2^x.
   Proof.
-    simple induction x;
-      [ simple induction y; simpl in |- *; auto with zarith
-	| simple induction y;
-	  [ unfold two_p in |- *; rewrite (Zmult_comm (two_power_pos p) 1);
-	    rewrite (Zmult_1_l (two_power_pos p)); auto with zarith
-	    | unfold Zplus in |- *; unfold two_p in |- *; intros;
-	      apply two_power_pos_is_exp
-	    | intros; unfold Zle in H0; unfold Zcompare in H0;
-	      absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith ]
-	| simple induction y;
-	  [ simpl in |- *; auto with zarith
-	    | intros; unfold Zle in H; unfold Zcompare in H;
-	      absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith
-	    | intros; unfold Zle in H; unfold Zcompare in H;
-	      absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith ] ].
+   intros [|p|p]; trivial. apply two_power_pos_correct.
   Qed.
 
-  Lemma two_p_gt_ZERO : forall x:Z, 0 <= x -> two_p x > 0.
+  Theorem two_p_is_exp :
+    forall x y, 0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y.
   Proof.
-    simple induction x; intros;
-      [ simpl in |- *; omega
-	| simpl in |- *; unfold two_power_pos in |- *; apply Zorder.Zgt_pos_0
-	| absurd (0 <= Zneg p);
-	  [ simpl in |- *; unfold Zle in |- *; unfold Zcompare in |- *;
-	    do 2 unfold not in |- *; auto with zarith
-	    | assumption ] ].
+   intros. rewrite 3 two_p_correct. apply Z.pow_add_r; auto with zarith.
   Qed.
 
-  Lemma two_p_S : forall x:Z, 0 <= x -> two_p (Zsucc x) = 2 * two_p x.
+  Lemma two_p_gt_ZERO : forall x, 0 <= x -> two_p x > 0.
   Proof.
-    intros; unfold Zsucc in |- *.
-    rewrite (two_p_is_exp x 1 H (Zorder.Zle_0_pos 1)).
-    apply Zmult_comm.
+   intros. rewrite two_p_correct. now apply Zlt_gt, Z.pow_pos_nonneg.
   Qed.
 
-  Lemma two_p_pred : forall x:Z, 0 <= x -> two_p (Zpred x) < two_p x.
+  Lemma two_p_S : forall x, 0 <= x -> two_p (Zsucc x) = 2 * two_p x.
   Proof.
-    intros; apply natlike_ind with (P := fun x:Z => two_p (Zpred x) < two_p x);
-      [ simpl in |- *; unfold Zlt in |- *; auto with zarith
-	| intros; elim (Zle_lt_or_eq 0 x0 H0);
-	  [ intros;
-	    replace (two_p (Zpred (Zsucc x0))) with (two_p (Zsucc (Zpred x0)));
-	      [ rewrite (two_p_S (Zpred x0));
-		[ rewrite (two_p_S x0); [ omega | assumption ]
-		  | apply Zorder.Zlt_0_le_0_pred; assumption ]
-		| rewrite <- (Zsucc_pred x0); rewrite <- (Zpred_succ x0);
-		  trivial with zarith ]
-	    | intro Hx0; rewrite <- Hx0; simpl in |- *; unfold Zlt in |- *;
-	      auto with zarith ]
-	| assumption ].
+   intros. rewrite 2 two_p_correct. now apply Z.pow_succ_r.
   Qed.
 
-  Lemma Zlt_lt_double : forall x y:Z, 0 <= x < y -> x < 2 * y.
-    intros; omega. Qed.
+  Lemma two_p_pred : forall x, 0 <= x -> two_p (Zpred x) < two_p x.
+  Proof.
+   intros. rewrite 2 two_p_correct.
+   apply Z.pow_lt_mono_r; auto with zarith.
+  Qed.
 
-  End Powers_of_2.
+End Powers_of_2.
 
 Hint Resolve two_p_gt_ZERO: zarith.
 Hint Immediate two_p_pred two_p_S: zarith.