Numbers: some improvements in proofs

 - a ltac solve_proper which generalizes solve_predicate_wd and co
 - using le_elim is nicer that (apply le_lteq; destruct ...)
 - "apply ->" can now be "apply" most of the time.

 Benefit: NumPrelude is now almost empty

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13762 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 56 insertions, 63 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index 44cd08e67..641375a5c 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -347,7 +347,7 @@ Qed.
 Lemma div_pow2_bits : forall a n m, 0<=n -> 0<=m -> (a/2^n).[m] = a.[m+n].
 Proof.
  intros a n m Hn. revert a m. apply le_ind with (4:=Hn).
- solve_predicate_wd.
+ solve_proper.
  intros a m Hm. now nzsimpl.
  clear n Hn. intros n Hn IH a m Hm. nzsimpl; trivial.
  rewrite <- div_div by order_pos.
@@ -360,7 +360,7 @@ Proof.
  destruct (le_gt_cases 0 n) as [Hn|Hn].
  now rewrite <- div2_bits, mul_comm, div_mul by order'.
  rewrite (testbit_neg_r a n Hn).
- apply le_succ_l, le_lteq in Hn. destruct Hn as [Hn|Hn].
+ apply le_succ_l in Hn. le_elim Hn.
  now rewrite testbit_neg_r.
  now rewrite Hn, bit0_odd, odd_mul, odd_2.
 Qed.
@@ -373,7 +373,7 @@ Qed.
 Lemma mul_pow2_bits_add : forall a n m, 0<=n -> (a*2^n).[n+m] = a.[m].
 Proof.
  intros a n m Hn. revert a m. apply le_ind with (4:=Hn).
- solve_predicate_wd.
+ solve_proper.
  intros a m. now nzsimpl.
  clear n Hn. intros n Hn IH a m. nzsimpl; trivial.
  rewrite mul_assoc, (mul_comm _ 2), <- mul_assoc.
@@ -403,11 +403,11 @@ Lemma mod_pow2_bits_high : forall a n m, 0<=n<=m ->
 Proof.
  intros a n m (Hn,H).
  destruct (mod_pos_bound a (2^n)) as [LE LT]. order_pos.
- apply le_lteq in LE; destruct LE as [LT'|EQ].
+ le_elim LE.
  apply bits_above_log2; try order.
  apply lt_le_trans with n; trivial.
  apply log2_lt_pow2; trivial.
- now rewrite <-EQ, bits_0.
+ now rewrite <- LE, bits_0.
 Qed.
 
 Lemma mod_pow2_bits_low : forall a n m, m<n ->
@@ -463,7 +463,7 @@ Proof.
  assert (AUX : forall n, 0<=n -> forall a b,
                 0<=a<2^n -> testbit a === testbit b -> a == b).
   intros n Hn. apply le_ind with (4:=Hn).
-  solve_predicate_wd.
+  solve_proper.
   intros a b Ha H. rewrite pow_0_r, one_succ, lt_succ_r in Ha.
   assert (Ha' : a == 0) by (destruct Ha; order).
   rewrite Ha' in *.
@@ -553,10 +553,10 @@ Proof.
   exists 0. intros m Hm. now rewrite bits_0, H0.
   clear k LE. intros k LE IH f Hf Hk.
   destruct (IH (fun m => f (S m))) as (n, Hn).
-  solve_predicate_wd.
+  solve_proper.
   intros m Hm. apply Hk. now rewrite <- succ_le_mono.
   exists (f 0 + 2*n). intros m Hm.
-  apply le_lteq in Hm. destruct Hm as [Hm|Hm].
+  le_elim Hm.
   rewrite <- (succ_pred m), Hn, <- div2_bits.
   rewrite mul_comm, div_add, b2z_div2, add_0_l; trivial. order'.
   now rewrite <- lt_succ_r, succ_pred.
@@ -743,10 +743,8 @@ Qed.
 
 Lemma shiftr_eq_0 : forall a n, 0<=a -> log2 a < n -> a >> n == 0.
 Proof.
- intros a n Ha H.
- apply shiftr_eq_0_iff.
- apply le_lteq in Ha. destruct Ha as [Ha|Ha].
- right. now split. now left.
+ intros a n Ha H. apply shiftr_eq_0_iff.
+ le_elim Ha. right. now split. now left.
 Qed.
 
 (** Properties of [div2]. *)
@@ -1304,7 +1302,7 @@ Qed.
 
 Lemma ones_spec_high : forall n m, 0<=n<=m -> (ones n).[m] = false.
 Proof.
- intros n m (Hn,H). apply le_lteq in Hn. destruct Hn as [Hn|Hn].
+ intros n m (Hn,H). le_elim Hn.
  apply bits_above_log2; rewrite ones_equiv.
  rewrite <-lt_succ_r, succ_pred; order_pos.
  rewrite log2_pred_pow2; trivial. now rewrite <-le_succ_l, succ_pred.
@@ -1576,7 +1574,7 @@ Lemma log2_lor : forall a b, 0<=a -> 0<=b ->
 Proof.
  assert (AUX : forall a b, 0<=a -> a<=b -> log2 (lor a b) == log2 b).
   intros a b Ha H.
-  apply le_lteq in Ha; destruct Ha as [Ha|Ha]; [|now rewrite <- Ha, lor_0_l].
+  le_elim Ha; [|now rewrite <- Ha, lor_0_l].
   apply log2_bits_unique.
   now rewrite lor_spec, bit_log2, orb_true_r by order.
   intros m Hm. assert (H' := log2_le_mono _ _ H).
@@ -1594,12 +1592,12 @@ Lemma log2_land : forall a b, 0<=a -> 0<=b ->
 Proof.
  assert (AUX : forall a b, 0<=a -> a<=b -> log2 (land a b) <= log2 a).
   intros a b Ha Hb.
-  apply le_ngt. intros H'.
-  assert (LE : 0 <= land a b) by (apply land_nonneg; now left).
-  apply le_lteq in LE. destruct LE as [LT|EQ].
-  generalize (bit_log2 (land a b) LT).
+  apply le_ngt. intros LT.
+  assert (H : 0 <= land a b) by (apply land_nonneg; now left).
+  le_elim H.
+  generalize (bit_log2 (land a b) H).
   now rewrite land_spec, bits_above_log2.
-  rewrite <- EQ in H'. apply log2_lt_cancel in H'; order.
+  rewrite <- H in LT. apply log2_lt_cancel in LT; order.
  (* main *)
  intros a b Ha Hb.
  destruct (le_ge_cases a b) as [H|H].
@@ -1612,13 +1610,13 @@ Lemma log2_lxor : forall a b, 0<=a -> 0<=b ->
 Proof.
  assert (AUX : forall a b, 0<=a -> a<=b -> log2 (lxor a b) <= log2 b).
   intros a b Ha Hb.
-  apply le_ngt. intros H'.
-  assert (LE : 0 <= lxor a b) by (apply lxor_nonneg; split; order).
-  apply le_lteq in LE. destruct LE as [LT|EQ].
-  generalize (bit_log2 (lxor a b) LT).
+  apply le_ngt. intros LT.
+  assert (H : 0 <= lxor a b) by (apply lxor_nonneg; split; order).
+  le_elim H.
+  generalize (bit_log2 (lxor a b) H).
   rewrite lxor_spec, 2 bits_above_log2; try order. discriminate.
   apply le_lt_trans with (log2 b); trivial. now apply log2_le_mono.
-  rewrite <- EQ in H'. apply log2_lt_cancel in H'; order.
+  rewrite <- H in LT. apply log2_lt_cancel in LT; order.
  (* main *)
  intros a b Ha Hb.
  destruct (le_ge_cases a b) as [H|H].
@@ -1679,13 +1677,12 @@ Lemma add_carry_bits_aux : forall n, 0<=n ->
    a+b+c0 == lxor3 a b c /\ c/2 == lnextcarry a b c /\ c.[0] = c0.
 Proof.
  intros n Hn. apply le_ind with (4:=Hn).
- solve_predicate_wd.
+ solve_proper.
  (* base *)
  intros a b c0. rewrite !pow_0_r, !one_succ, !lt_succ_r, <- !one_succ.
  intros (Ha1,Ha2) (Hb1,Hb2).
- apply le_lteq in Ha1; apply le_lteq in Hb1.
- rewrite <- le_succ_l, succ_m1 in Ha1, Hb1.
- destruct Ha1 as [Ha1|Ha1]; destruct Hb1 as [Hb1|Hb1].
+ le_elim Ha1; rewrite <- ?le_succ_l, ?succ_m1 in Ha1;
+  le_elim Hb1; rewrite <- ?le_succ_l, ?succ_m1 in Hb1.
  (* base, a = 0, b = 0 *)
  exists c0.
  rewrite (le_antisymm _ _ Ha2 Ha1), (le_antisymm _ _ Hb2 Hb1).
@@ -1727,7 +1724,7 @@ Proof.
  exists (c0 + 2*c). repeat split.
  (* step, add *)
  bitwise.
- apply le_lteq in Hm. destruct Hm as [Hm|Hm].
+ le_elim Hm.
  rewrite <- (succ_pred m), lt_succ_r in Hm.
  rewrite <- (succ_pred m), <- !div2_bits, <- 2 lxor_spec by trivial.
  apply testbit_wd; try easy.
@@ -1737,7 +1734,7 @@ Proof.
  (* step, carry *)
  rewrite add_b2z_double_div2.
  bitwise.
- apply le_lteq in Hm. destruct Hm as [Hm|Hm].
+ le_elim Hm.
  rewrite <- (succ_pred m), lt_succ_r in Hm.
  rewrite <- (succ_pred m), <- !div2_bits, IH2 by trivial.
  autorewrite with bitwise. now rewrite add_b2z_double_div2.
@@ -1801,7 +1798,7 @@ Proof.
  intros EQ. rewrite EQ, lor_0_l in H.
  apply bits_inj'. intros n Hn. rewrite bits_0.
  apply le_ind with (4:=Hn).
- solve_predicate_wd.
+ solve_proper.
  trivial.
  clear n Hn. intros n Hn IH.
  rewrite <- div2_bits, H; trivial.
@@ -1828,7 +1825,7 @@ Proof.
  assert (AUX : forall n, 0<=n ->
           forall a b, 0 <= a < 2^n -> 0<=b -> ldiff a b == 0 -> a <= b).
  intros n Hn. apply le_ind with (4:=Hn); clear n Hn.
- solve_predicate_wd.
+ solve_proper.
  intros a b Ha Hb _. rewrite pow_0_r, one_succ, lt_succ_r in Ha.
  setoid_replace a with 0 by (destruct Ha; order'); trivial.
  intros n Hn IH a b (Ha,Ha') Hb H.
diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v
index 77a7c7341..87a95e9d7 100644
--- a/theories/Numbers/Integer/Abstract/ZGcd.v
+++ b/theories/Numbers/Integer/Abstract/ZGcd.v
@@ -163,12 +163,12 @@ Proof.
  assert (aux : forall n, 0<=n -> forall m, 0<=m -> Bezout n m (gcd n m)).
   intros n Hn; pattern n.
   apply strong_right_induction with (z:=0); trivial.
-  unfold Bezout. solve_predicate_wd.
+  unfold Bezout. solve_proper.
   clear n Hn. intros n Hn IHn.
   apply le_lteq in Hn; destruct Hn as [Hn|Hn].
   intros m Hm; pattern m.
   apply strong_right_induction with (z:=0); trivial.
-  unfold Bezout. solve_predicate_wd.
+  unfold Bezout. solve_proper.
   clear m Hm. intros m Hm IHm.
   destruct (lt_trichotomy n m) as [LT|[EQ|LT]].
   (* n < m *)
diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v
index bbf7d893a..f381953fb 100644
--- a/theories/Numbers/Integer/Abstract/ZLcm.v
+++ b/theories/Numbers/Integer/Abstract/ZLcm.v
@@ -313,8 +313,8 @@ Lemma lcm_unique_alt : forall n m p, 0<=p ->
 Proof.
  intros n m p Hp H.
  apply lcm_unique; trivial.
- apply -> H. apply divide_refl.
- apply -> H. apply divide_refl.
+ apply H, divide_refl.
+ apply H, divide_refl.
  intros. apply H. now split.
 Qed.
 
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 5431b4a10..3a8e1f389 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -68,12 +68,12 @@ Qed.
 
 Theorem lt_lt_pred : forall n m, n < m -> P n < m.
 Proof.
-intros; apply <- lt_pred_le; now apply lt_le_incl.
+intros; apply lt_pred_le; now apply lt_le_incl.
 Qed.
 
 Theorem le_le_pred : forall n m, n <= m -> P n <= m.
 Proof.
-intros; apply lt_le_incl; now apply <- lt_pred_le.
+intros; apply lt_le_incl; now apply lt_pred_le.
 Qed.
 
 Theorem lt_pred_lt : forall n m, n < P m -> n < m.
@@ -83,7 +83,7 @@ Qed.
 
 Theorem le_pred_lt : forall n m, n <= P m -> n <= m.
 Proof.
-intros; apply lt_le_incl; now apply <- lt_le_pred.
+intros; apply lt_le_incl; now apply lt_le_pred.
 Qed.
 
 Theorem pred_lt_mono : forall n m, n < m <-> P n < P m.
@@ -123,9 +123,9 @@ Qed.
 
 Theorem lt_m1_r : forall n m, n < m -> m < 0 -> n < -1.
 Proof.
-intros n m H1 H2. apply -> lt_le_pred in H2.
+intros n m H1 H2. apply lt_le_pred in H2.
 setoid_replace (P 0) with (-1) in H2. now apply lt_le_trans with m.
-apply <- eq_opp_r. now rewrite one_succ, opp_pred, opp_0.
+apply eq_opp_r. now rewrite one_succ, opp_pred, opp_0.
 Qed.
 
 End ZOrderProp.
diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v
index 68eca3305..618722aa8 100644
--- a/theories/Numbers/Integer/Abstract/ZMul.v
+++ b/theories/Numbers/Integer/Abstract/ZMul.v
@@ -39,7 +39,7 @@ Qed.
 
 Theorem mul_opp_l : forall n m, (- n) * m == - (n * m).
 Proof.
-intros n m. apply -> add_move_0_r.
+intros n m. apply add_move_0_r.
 now rewrite <- mul_add_distr_r, add_opp_diag_l, mul_0_l.
 Qed.
 
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index 4c0a9a2ca..6d2fa41fc 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -94,7 +94,7 @@ Notation le_0_square := square_nonneg (only parsing).
 
 Theorem nlt_square_0 : forall n, ~ n * n < 0.
 Proof.
-intros n H. apply -> lt_nge in H. apply H. apply square_nonneg.
+intros n H. apply lt_nge in H. apply H. apply square_nonneg.
 Qed.
 
 Theorem square_lt_mono_nonpos : forall n m, n <= 0 -> m < n -> n * n < m * m.
@@ -109,42 +109,38 @@ Qed.
 
 Theorem square_lt_simpl_nonpos : forall n m, m <= 0 -> n * n < m * m -> m < n.
 Proof.
-intros n m H1 H2. destruct (le_gt_cases n 0).
-destruct (lt_ge_cases m n).
-assumption. assert (F : m * m <= n * n) by now apply square_le_mono_nonpos.
-apply -> le_ngt in F. false_hyp H2 F.
-now apply le_lt_trans with 0.
+intros n m H1 H2. destruct (le_gt_cases n 0); [|order].
+destruct (lt_ge_cases m n) as [LE|GT]; trivial.
+apply square_le_mono_nonpos in GT; order.
 Qed.
 
 Theorem square_le_simpl_nonpos : forall n m, m <= 0 -> n * n <= m * m -> m <= n.
 Proof.
-intros n m H1 H2. destruct (le_gt_cases n 0).
-destruct (le_gt_cases m n).
-assumption. assert (F : m * m < n * n) by now apply square_lt_mono_nonpos.
-apply -> lt_nge in F. false_hyp H2 F.
-apply lt_le_incl; now apply le_lt_trans with 0.
+intros n m H1 H2. destruct (le_gt_cases n 0); [|order].
+destruct (le_gt_cases m n) as [LE|GT]; trivial.
+apply square_lt_mono_nonpos in GT; order.
 Qed.
 
 Theorem lt_1_mul_neg : forall n m, n < -1 -> m < 0 -> 1 < n * m.
 Proof.
-intros n m H1 H2. apply -> (mul_lt_mono_neg_r m) in H1.
-apply <- opp_pos_neg in H2. rewrite mul_opp_l, mul_1_l in H1.
+intros n m H1 H2. apply (mul_lt_mono_neg_r m) in H1.
+apply opp_pos_neg in H2. rewrite mul_opp_l, mul_1_l in H1.
 now apply lt_1_l with (- m).
 assumption.
 Qed.
 
 Theorem lt_mul_m1_neg : forall n m, 1 < n -> m < 0 -> n * m < -1.
 Proof.
-intros n m H1 H2. apply -> (mul_lt_mono_neg_r m) in H1.
+intros n m H1 H2. apply (mul_lt_mono_neg_r m) in H1.
 rewrite mul_1_l in H1. now apply lt_m1_r with m.
 assumption.
 Qed.
 
 Theorem lt_mul_m1_pos : forall n m, n < -1 -> 0 < m -> n * m < -1.
 Proof.
-intros n m H1 H2. apply -> (mul_lt_mono_pos_r m) in H1.
+intros n m H1 H2. apply (mul_lt_mono_pos_r m) in H1.
 rewrite mul_opp_l, mul_1_l in H1.
-apply <- opp_neg_pos in H2. now apply lt_m1_r with (- m).
+apply opp_neg_pos in H2. now apply lt_m1_r with (- m).
 assumption.
 Qed.
 
diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v
index 682c680cc..53d84dce1 100644
--- a/theories/Numbers/Integer/Abstract/ZPow.v
+++ b/theories/Numbers/Integer/Abstract/ZPow.v
@@ -22,7 +22,7 @@ Module Type ZPowProp
 
 Lemma even_pow : forall a b, 0<b -> even (a^b) = even a.
 Proof.
- intros a b Hb. apply lt_ind with (4:=Hb). solve_predicate_wd.
+ intros a b Hb. apply lt_ind with (4:=Hb). solve_proper.
  now nzsimpl.
  clear b Hb. intros b Hb IH. nzsimpl; [|order].
  rewrite even_mul, IH. now destruct (even a).
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 8ed42ed8d..cad5152d7 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -23,7 +23,7 @@ Proof.
 intros A A_wd A0 AS n; apply Zind; clear n.
 assumption.
 intros; rewrite <- Zsucc_succ'. now apply -> AS.
-intros n H. rewrite <- Zpred_pred'. rewrite Zsucc_pred in H. now apply <- AS.
+intros n H. rewrite <- Zpred_pred'. rewrite Zsucc_pred in H. now apply AS.
 Qed.
 
 (** * Implementation of [ZAxiomsMiniSig] by [BinInt.Z] *)
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index ab555ca32..2b568dddc 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -13,7 +13,7 @@ Require Export Ring.
 
 Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
 Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
-Open Local Scope pair_scope.
+Local Open Scope pair_scope.
 
 Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig.
  Module Import NProp.
@@ -173,8 +173,8 @@ rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm).
 apply H2.
 rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1.
 induct p. assumption. intros p IH.
-apply -> (A_wd (0, p) (1, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l].
-rewrite one_succ in IH. now apply <- AS.
+apply (A_wd (0, p) (1, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l].
+rewrite one_succ in IH. now apply AS.
 induct p. assumption. intros p IH.
 replace 0 with (snd (p, 0)); [| reflexivity].
 replace (N.succ p) with (N.succ (fst (p, 0))); [| reflexivity]. now apply -> AS.