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

1 files changed, 30 insertions, 44 deletions

diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index ef9057c06..3722d4727 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -15,19 +15,19 @@ Module Type NZOrderProp
 
 Instance le_wd : Proper (eq==>eq==>iff) le.
 Proof.
-intros n n' Hn m m' Hm. rewrite !lt_eq_cases, !Hn, !Hm; auto with *.
+intros n n' Hn m m' Hm. now rewrite <- !lt_succ_r, Hn, Hm.
 Qed.
 
 Ltac le_elim H := rewrite lt_eq_cases in H; destruct H as [H | H].
 
 Theorem lt_le_incl : forall n m, n < m -> n <= m.
 Proof.
-intros; apply <- lt_eq_cases; now left.
+intros. apply lt_eq_cases. now left.
 Qed.
 
 Theorem le_refl : forall n, n <= n.
 Proof.
-intro; apply <- lt_eq_cases; now right.
+intro. apply lt_eq_cases. now right.
 Qed.
 
 Theorem lt_succ_diag_r : forall n, n < S n.
@@ -97,7 +97,7 @@ intros n m; nzinduct n m.
 intros H; false_hyp H lt_irrefl.
 intro n; split; intros H H1 H2.
 apply lt_succ_r in H2. le_elim H2.
-apply H; auto. apply -> le_succ_l. now apply lt_le_incl.
+apply H; auto. apply le_succ_l. now apply lt_le_incl.
 rewrite H2 in H1. false_hyp H1 nlt_succ_diag_l.
 apply le_succ_l in H1. le_elim H1.
 apply H; auto. rewrite lt_succ_r. now apply lt_le_incl.
@@ -206,12 +206,12 @@ Qed.
 
 Theorem lt_succ_l : forall n m, S n < m -> n < m.
 Proof.
-intros n m H; apply -> le_succ_l; order.
+intros n m H; apply le_succ_l; order.
 Qed.
 
 Theorem le_le_succ_r : forall n m, n <= m -> n <= S m.
 Proof.
-intros n m LE. rewrite <- lt_succ_r in LE. order.
+intros n m LE. apply lt_succ_r in LE. order.
 Qed.
 
 Theorem lt_lt_succ_r : forall n m, n < m -> n < S m.
@@ -254,15 +254,14 @@ Proof.
 apply lt_le_incl, lt_0_2.
 Qed.
 
-Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m.
-Proof.
-intros n m H1 H2. rewrite one_succ. apply <- le_succ_l in H1. order.
-Qed.
-
 (** The order tactic enriched with some knowledge of 0,1,2 *)
 
 Ltac order' := generalize lt_0_1 lt_1_2; order.
 
+Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m.
+Proof.
+intros n m H1 H2. rewrite <- le_succ_l, <- one_succ in H1. order.
+Qed.
 
 (** More Trichotomy, decidability and double negation elimination. *)
 
@@ -364,7 +363,7 @@ Proof.
 intro z; nzinduct n z.
 order.
 intro n; split; intros IH m H1 H2.
-apply -> le_succ_r in H2. destruct H2 as [H2 | H2].
+apply le_succ_r in H2. destruct H2 as [H2 | H2].
 now apply IH. exists n. now split; [| rewrite <- lt_succ_r; rewrite <- H2].
 apply IH. assumption. now apply le_le_succ_r.
 Qed.
@@ -414,14 +413,14 @@ Qed.
 Lemma rs'_rs'' : right_step' -> right_step''.
 Proof.
 intros RS' n; split; intros H1 m H2 H3.
-apply -> lt_succ_r in H3; le_elim H3;
+apply lt_succ_r in H3; le_elim H3;
 [now apply H1 | rewrite H3 in *; now apply RS'].
 apply H1; [assumption | now apply lt_lt_succ_r].
 Qed.
 
 Lemma rbase : A' z.
 Proof.
-intros m H1 H2. apply -> le_ngt in H1. false_hyp H2 H1.
+intros m H1 H2. apply le_ngt in H1. false_hyp H2 H1.
 Qed.
 
 Lemma A'A_right : (forall n, A' n) -> forall n, z <= n -> A n.
@@ -473,28 +472,28 @@ Let left_step'' := forall n, A' n <-> A' (S n).
 Lemma ls_ls' :  A z -> left_step -> left_step'.
 Proof.
 intros Az LS n H1 H2. le_elim H1.
-apply LS; trivial. apply H2; [now apply <- le_succ_l | now apply eq_le_incl].
+apply LS; trivial. apply H2; [now apply le_succ_l | now apply eq_le_incl].
 rewrite H1; apply Az.
 Qed.
 
 Lemma ls'_ls'' : left_step' -> left_step''.
 Proof.
 intros LS' n; split; intros H1 m H2 H3.
-apply -> le_succ_l in H3. apply lt_le_incl in H3. now apply H1.
+apply le_succ_l in H3. apply lt_le_incl in H3. now apply H1.
 le_elim H3.
-apply <- le_succ_l in H3. now apply H1.
+apply le_succ_l in H3. now apply H1.
 rewrite <- H3 in *; now apply LS'.
 Qed.
 
 Lemma lbase : A' (S z).
 Proof.
-intros m H1 H2. apply -> le_succ_l in H2.
-apply -> le_ngt in H1. false_hyp H2 H1.
+intros m H1 H2. apply le_succ_l in H2.
+apply le_ngt in H1. false_hyp H2 H1.
 Qed.
 
 Lemma A'A_left : (forall n, A' n) -> forall n, n <= z -> A n.
 Proof.
-intros H1 n H2. apply H1 with (n := n); [assumption | now apply eq_le_incl].
+intros H1 n H2. apply (H1 n); [assumption | now apply eq_le_incl].
 Qed.
 
 Theorem strong_left_induction: left_step' -> forall n, n <= z -> A n.
@@ -551,8 +550,8 @@ Theorem order_induction' :
     forall n, A n.
 Proof.
 intros Az AS AP n; apply order_induction; try assumption.
-intros m H1 H2. apply AP in H2; [| now apply <- le_succ_l].
-apply -> (A_wd (P (S m)) m); [assumption | apply pred_succ].
+intros m H1 H2. apply AP in H2; [|now apply le_succ_l].
+now rewrite pred_succ in H2.
 Qed.
 
 End Center.
@@ -579,8 +578,8 @@ Theorem lt_ind : forall (n : t),
    forall m, n < m -> A m.
 Proof.
 intros n H1 H2 m H3.
-apply right_induction with (S n); [assumption | | now apply <- le_succ_l].
-intros; apply H2; try assumption. now apply -> le_succ_l.
+apply right_induction with (S n); [assumption | | now apply le_succ_l].
+intros; apply H2; try assumption. now apply le_succ_l.
 Qed.
 
 (** Elimination principle for <= *)
@@ -606,8 +605,8 @@ Section WF.
 
 Variable z : t.
 
-Let Rlt (n m : t) := z <= n /\ n < m.
-Let Rgt (n m : t) := m < n /\ n <= z.
+Let Rlt (n m : t) := z <= n < m.
+Let Rgt (n m : t) := m < n <= z.
 
 Instance Rlt_wd : Proper (eq ==> eq ==> iff) Rlt.
 Proof.
@@ -619,25 +618,13 @@ Proof.
 intros x1 x2 H1 x3 x4 H2; unfold Rgt; rewrite H1; now rewrite H2.
 Qed.
 
-Instance Acc_lt_wd : Proper (eq==>iff) (Acc Rlt).
-Proof.
-intros x1 x2 H; split; intro H1; destruct H1 as [H2];
-constructor; intros; apply H2; now (rewrite H || rewrite <- H).
-Qed.
-
-Instance Acc_gt_wd : Proper (eq==>iff) (Acc Rgt).
-Proof.
-intros x1 x2 H; split; intro H1; destruct H1 as [H2];
-constructor; intros; apply H2; now (rewrite H || rewrite <- H).
-Qed.
-
 Theorem lt_wf : well_founded Rlt.
 Proof.
 unfold well_founded.
 apply strong_right_induction' with (z := z).
-apply Acc_lt_wd.
+auto with typeclass_instances.
 intros n H; constructor; intros y [H1 H2].
-apply <- nle_gt in H2. elim H2. now apply le_trans with z.
+apply nle_gt in H2. elim H2. now apply le_trans with z.
 intros n H1 H2; constructor; intros m [H3 H4]. now apply H2.
 Qed.
 
@@ -645,11 +632,11 @@ Theorem gt_wf : well_founded Rgt.
 Proof.
 unfold well_founded.
 apply strong_left_induction' with (z := z).
-apply Acc_gt_wd.
+auto with typeclass_instances.
 intros n H; constructor; intros y [H1 H2].
-apply <- nle_gt in H2. elim H2. now apply le_lt_trans with n.
+apply nle_gt in H2. elim H2. now apply le_lt_trans with n.
 intros n H1 H2; constructor; intros m [H3 H4].
-apply H2. assumption. now apply <- le_succ_l.
+apply H2. assumption. now apply le_succ_l.
 Qed.
 
 End WF.
@@ -662,4 +649,3 @@ End NZOrderProp.
 Module NZOrderedType (NZ : NZDecOrdSig')
  <: DecidableTypeFull <: OrderedTypeFull
  := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec.
-