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

10 files changed, 42 insertions, 43 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index fbe71a4c7..72e09f157 100644
--- a/theories/Numbers/Natural/Abstract/NAdd.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -22,9 +22,9 @@ intros n m; induct n.
 nzsimpl; intuition.
 intros n IH. nzsimpl.
 setoid_replace (S (n + m) == 0) with False by
- (apply -> neg_false; apply neq_succ_0).
+ (apply neg_false; apply neq_succ_0).
 setoid_replace (S n == 0) with False by
- (apply -> neg_false; apply neq_succ_0). tauto.
+ (apply neg_false; apply neq_succ_0). tauto.
 Qed.
 
 Theorem eq_add_succ :
@@ -47,11 +47,11 @@ Theorem eq_add_1 : forall n m,
 Proof.
 intros n m. rewrite one_succ. intro H.
 assert (H1 : exists p, n + m == S p) by now exists 0.
-apply -> eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
+apply eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
 left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H.
-apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
+apply eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
 right. rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H.
-apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
+apply eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
 Qed.
 
 Theorem succ_add_discr : forall n m, m ~= S (n + m).
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 7ed563be5..ac8a05220 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -41,7 +41,7 @@ nzinduct n.
 now apply eq_le_incl.
 intro n; split.
 apply le_le_succ_r.
-intro H; apply -> le_succ_r in H; destruct H as [H | H].
+intro H; apply le_succ_r in H; destruct H as [H | H].
 assumption.
 symmetry in H; false_hyp H neq_succ_0.
 Qed.
@@ -179,7 +179,7 @@ Ltac double_induct n m :=
   try intros until n;
   try intros until m;
   pattern n, m; apply double_induction; clear n m;
-  [solve_relation_wd | | | ].
+  [solve_proper | | | ].
 
 End NBaseProp.
 
diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v
index 2cb5bbc06..70f6f7945 100644
--- a/theories/Numbers/Natural/Abstract/NBits.v
+++ b/theories/Numbers/Natural/Abstract/NBits.v
@@ -303,7 +303,7 @@ Qed.
 Lemma bits_inj : forall a b, testbit a === testbit b -> a == b.
 Proof.
  intros a. pattern a.
- apply strong_right_induction with 0;[solve_predicate_wd|clear a|apply le_0_l].
+ apply strong_right_induction with 0;[solve_proper|clear a|apply le_0_l].
  intros a _ IH b H.
  destruct (eq_0_gt_0_cases a) as [EQ|LT].
  rewrite EQ in H |- *. symmetry. apply bits_inj_0.
@@ -342,7 +342,7 @@ Proof.
   exists 0. intros m. rewrite bits_0, H0; trivial. apply le_0_l.
   intros k 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.
   destruct (zero_or_succ m) as [Hm|(m', Hm)]; rewrite Hm.
diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v
index 1340e5124..1192e5cdc 100644
--- a/theories/Numbers/Natural/Abstract/NGcd.v
+++ b/theories/Numbers/Natural/Abstract/NGcd.v
@@ -97,11 +97,11 @@ Lemma gcd_bezout_pos_pos : forall n, 0<n -> forall m, 0<m ->
 Proof.
  intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn.
  pattern n. apply strong_right_induction with (z:=1); trivial.
- unfold Bezout. solve_predicate_wd.
+ unfold Bezout. solve_proper.
  clear n Hn. intros n Hn IHn.
  intros m Hm. rewrite <- le_succ_l, <- one_succ in Hm.
  pattern m. apply strong_right_induction with (z:=1); 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 *)
@@ -191,8 +191,7 @@ Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) ->
  exists q r, n == q*r /\ (q | m) /\ (r | p).
 Proof.
  intros n m p Hn H.
- assert (G := gcd_nonneg n m).
- apply le_lteq in G; destruct G as [G|G].
+ assert (G := gcd_nonneg n m). le_elim G.
  destruct (gcd_divide_l n m) as (q,Hq).
  exists (gcd n m). exists q.
  split. easy.
diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v
index f3b45e308..8a1a4def6 100644
--- a/theories/Numbers/Natural/Abstract/NLcm.v
+++ b/theories/Numbers/Natural/Abstract/NLcm.v
@@ -192,8 +192,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/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v
index 6ecdef9ef..804d1ccc0 100644
--- a/theories/Numbers/Natural/Abstract/NMulOrder.v
+++ b/theories/Numbers/Natural/Abstract/NMulOrder.v
@@ -53,7 +53,7 @@ Qed.
 Theorem lt_0_mul' : forall n m, n * m > 0 <-> n > 0 /\ m > 0.
 Proof.
 intros n m; split; [intro H | intros [H1 H2]].
-apply -> lt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. now split.
+apply lt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. now split.
  false_hyp H1 nlt_0_r.
 now apply mul_pos_pos.
 Qed.
@@ -65,11 +65,11 @@ Proof.
 intros n m.
 split; [| intros [H1 H2]; now rewrite H1, H2, mul_1_l].
 intro H; destruct (lt_trichotomy n 1) as [H1 | [H1 | H1]].
-apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. order'.
+apply lt_1_r in H1. rewrite H1, mul_0_l in H. order'.
 rewrite H1, mul_1_l in H; now split.
 destruct (eq_0_gt_0_cases m) as [H2 | H2].
 rewrite H2, mul_0_r in H. order'.
-apply -> (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1.
+apply (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1.
 assert (H3 : 1 < n * m) by now apply (lt_1_l m).
 rewrite H in H3; false_hyp H3 lt_irrefl.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 2816af7c4..8bba7d72b 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -17,7 +17,7 @@ Include NAddProp N.
 
 Theorem lt_wf_0 : well_founded lt.
 Proof.
-setoid_replace lt with (fun n m => 0 <= n /\ n < m).
+setoid_replace lt with (fun n m => 0 <= n < m).
 apply lt_wf.
 intros x y; split.
 intro H; split; [apply le_0_l | assumption]. now intros [_ H].
@@ -27,12 +27,12 @@ Defined.
 
 Theorem nlt_0_r : forall n, ~ n < 0.
 Proof.
-intro n; apply -> le_ngt. apply le_0_l.
+intro n; apply le_ngt. apply le_0_l.
 Qed.
 
 Theorem nle_succ_0 : forall n, ~ (S n <= 0).
 Proof.
-intros n H; apply -> le_succ_l in H; false_hyp H nlt_0_r.
+intros n H; apply le_succ_l in H; false_hyp H nlt_0_r.
 Qed.
 
 Theorem le_0_r : forall n, n <= 0 <-> n == 0.
@@ -118,9 +118,9 @@ Proof.
 intros Base Step; induct n.
 intros; apply Base.
 intros n IH m H. elim H using le_ind.
-solve_predicate_wd.
+solve_proper.
 apply Step; [| apply IH]; now apply eq_le_incl.
-intros k H1 H2. apply -> le_succ_l in H1. apply lt_le_incl in H1. auto.
+intros k H1 H2. apply le_succ_l in H1. apply lt_le_incl in H1. auto.
 Qed.
 
 Theorem lt_ind_rel :
@@ -132,7 +132,7 @@ intros Base Step; induct n.
 intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]].
 rewrite H; apply Base.
 intros n IH m H. elim H using lt_ind.
-solve_predicate_wd.
+solve_proper.
 apply Step; [| apply IH]; now apply lt_succ_diag_r.
 intros k H1 H2. apply lt_succ_l in H1. auto.
 Qed.
@@ -176,7 +176,7 @@ Theorem lt_le_pred : forall n m, n < m -> n <= P m.
 Proof.
 intro n; cases m.
 intro H; false_hyp H nlt_0_r.
-intros m IH. rewrite pred_succ; now apply -> lt_succ_r.
+intros m IH. rewrite pred_succ; now apply lt_succ_r.
 Qed.
 
 Theorem lt_pred_le : forall n m, P n < m -> n <= m.
@@ -184,7 +184,7 @@ Theorem lt_pred_le : forall n m, P n < m -> n <= m.
 Proof.
 intros n m; cases n.
 rewrite pred_0; intro H; now apply lt_le_incl.
-intros n IH. rewrite pred_succ in IH. now apply <- le_succ_l.
+intros n IH. rewrite pred_succ in IH. now apply le_succ_l.
 Qed.
 
 Theorem lt_pred_lt : forall n m, n < P m -> n < m.
@@ -201,7 +201,7 @@ Theorem pred_le_mono : forall n m, n <= m -> P n <= P m.
  (* Converse is false for n == 1, m == 0 *)
 Proof.
 intros n m H; elim H using le_ind_rel.
-solve_relation_wd.
+solve_proper.
 intro; rewrite pred_0; apply le_0_l.
 intros p q H1 _; now do 2 rewrite pred_succ.
 Qed.
@@ -209,12 +209,12 @@ Qed.
 Theorem pred_lt_mono : forall n m, n ~= 0 -> (n < m <-> P n < P m).
 Proof.
 intros n m H1; split; intro H2.
-assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n.
+assert (m ~= 0). apply neq_0_lt_0. now apply lt_lt_0 with n.
 now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2 ;
-[apply <- succ_lt_mono | | |].
-assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n).
+[apply succ_lt_mono | | |].
+assert (m ~= 0). apply neq_0_lt_0. apply lt_lt_0 with (P n).
 apply lt_le_trans with (P m). assumption. apply le_pred_l.
-apply -> succ_lt_mono in H2. now do 2 rewrite succ_pred in H2.
+apply succ_lt_mono in H2. now do 2 rewrite succ_pred in H2.
 Qed.
 
 Theorem lt_succ_lt_pred : forall n m, S n < m <-> n < P m.
@@ -225,13 +225,13 @@ Qed.
 Theorem le_succ_le_pred : forall n m, S n <= m -> n <= P m.
  (* Converse is false for n == m == 0 *)
 Proof.
-intros n m H. apply lt_le_pred. now apply -> le_succ_l.
+intros n m H. apply lt_le_pred. now apply le_succ_l.
 Qed.
 
 Theorem lt_pred_lt_succ : forall n m, P n < m -> n < S m.
  (* Converse is false for n == m == 0 *)
 Proof.
-intros n m H. apply <- lt_succ_r. now apply lt_pred_le.
+intros n m H. apply lt_succ_r. now apply lt_pred_le.
 Qed.
 
 Theorem le_pred_le_succ : forall n m, P n <= m <-> n <= S m.
diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v
index 68976624e..67ed77981 100644
--- a/theories/Numbers/Natural/Abstract/NPow.v
+++ b/theories/Numbers/Natural/Abstract/NPow.v
@@ -146,7 +146,7 @@ Proof. wrap pow_add_upper. Qed.
 Lemma even_pow : forall a b, b~=0 -> even (a^b) = even a.
 Proof.
  intros a b Hb. rewrite neq_0_lt_0 in Hb.
- apply lt_ind with (4:=Hb). solve_predicate_wd.
+ apply lt_ind with (4:=Hb). solve_proper.
  now nzsimpl.
  clear b Hb. intros b Hb IH.
  rewrite pow_succ_r', even_mul, IH. now destruct (even a).
diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v
index 4232ecbfa..d7143c677 100644
--- a/theories/Numbers/Natural/Abstract/NSub.v
+++ b/theories/Numbers/Natural/Abstract/NSub.v
@@ -35,7 +35,7 @@ Qed.
 Theorem sub_gt : forall n m, n > m -> n - m ~= 0.
 Proof.
 intros n m H; elim H using lt_ind_rel; clear n m H.
-solve_relation_wd.
+solve_proper.
 intro; rewrite sub_0_r; apply neq_succ_0.
 intros; now rewrite sub_succ.
 Qed.
@@ -45,8 +45,8 @@ Proof.
 intros n m p; induct p.
 intro; now do 2 rewrite sub_0_r.
 intros p IH H. do 2 rewrite sub_succ_r.
-rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l).
-rewrite add_pred_r by (apply sub_gt; now apply -> le_succ_l).
+rewrite <- IH by (apply lt_le_incl; now apply le_succ_l).
+rewrite add_pred_r by (apply sub_gt; now apply le_succ_l).
 reflexivity.
 Qed.
 
@@ -242,10 +242,10 @@ intros n IH. destruct (le_gt_cases m n) as [H | H].
 rewrite sub_succ_l by assumption. do 2 rewrite mul_succ_l.
 rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p).
 rewrite <- (add_sub_assoc p (n * p) (m * p)) by now apply mul_le_mono_r.
-now apply <- add_cancel_l.
-assert (H1 : S n <= m); [now apply <- le_succ_l |].
-setoid_replace (S n - m) with 0 by now apply <- sub_0_le.
-setoid_replace ((S n * p) - m * p) with 0 by (apply <- sub_0_le; now apply mul_le_mono_r).
+now apply add_cancel_l.
+assert (H1 : S n <= m); [now apply le_succ_l |].
+setoid_replace (S n - m) with 0 by now apply sub_0_le.
+setoid_replace ((S n * p) - m * p) with 0 by (apply sub_0_le; now apply mul_le_mono_r).
 apply mul_0_l.
 Qed.
 
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index d2979bcf0..82380e9b4 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -77,7 +77,7 @@ Theorem min_r : forall n m, m <= n -> Nmin n m = m.
 Proof.
 unfold Nmin, Nle; intros n m H.
 case_eq (n ?= m); intro H1; try reflexivity.
-now apply -> Ncompare_eq_correct.
+now apply Ncompare_eq_correct.
 rewrite <- Ncompare_antisym, H1 in H; elim H; auto.
 Qed.
 
@@ -85,7 +85,7 @@ Theorem max_l : forall n m, m <= n -> Nmax n m = n.
 Proof.
 unfold Nmax, Nle; intros n m H.
 case_eq (n ?= m); intro H1; try reflexivity.
-symmetry; now apply -> Ncompare_eq_correct.
+symmetry; now apply Ncompare_eq_correct.
 rewrite <- Ncompare_antisym, H1 in H; elim H; auto.
 Qed.