Numbers: more (syntactic) changes toward new style of type classes

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

8 files changed, 71 insertions, 183 deletions

diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 60b43f0d2..02d82bacd 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -129,7 +129,7 @@ symmetry in H; false_hyp H neq_succ_0.
 Qed.
 
 Theorem induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.
 Proof.
 intros A A_wd A0 AS n; apply NZright_induction with 0; try assumption.
@@ -146,7 +146,7 @@ from NZ. *)
 Ltac induct n := induction_maker n ltac:(apply induction).
 
 Theorem case_analysis :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     A 0 -> (forall n : N, A (S n)) -> forall n : N, A n.
 Proof.
 intros; apply induction; auto.
@@ -206,12 +206,7 @@ Fibonacci numbers *)
 Section PairInduction.
 
 Variable A : N -> Prop.
-Hypothesis A_wd : predicate_wd Neq A.
-
-Add Morphism A with signature Neq ==> iff as A_morph.
-Proof.
-exact A_wd.
-Qed.
+Hypothesis A_wd : Proper (Neq==>iff) A.
 
 Theorem pair_induction :
   A 0 -> A 1 ->
@@ -230,12 +225,7 @@ End PairInduction.
 Section TwoDimensionalInduction.
 
 Variable R : N -> N -> Prop.
-Hypothesis R_wd : relation_wd Neq Neq R.
-
-Add Morphism R with signature Neq ==> Neq ==> iff as R_morph.
-Proof.
-exact R_wd.
-Qed.
+Hypothesis R_wd : Proper (Neq==>Neq==>iff) R.
 
 Theorem two_dim_induction :
    R 0 0 ->
@@ -260,12 +250,7 @@ End TwoDimensionalInduction.
 Section DoubleInduction.
 
 Variable R : N -> N -> Prop.
-Hypothesis R_wd : relation_wd Neq Neq R.
-
-Add Morphism R with signature Neq ==> Neq ==> iff as R_morph1.
-Proof.
-exact R_wd.
-Qed.
+Hypothesis R_wd : Proper (Neq==>Neq==>iff) R.
 
 Theorem double_induction :
    (forall m : N, R 0 m) ->
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index e2a6df1cc..1e1cd95c7 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -24,7 +24,7 @@ Definition def_add (x y : N) := recursion y (fun _ p => S p) x.
 
 Infix Local "++" := def_add (at level 50, left associativity).
 
-Add Morphism def_add with signature Neq ==> Neq ==> Neq as def_add_wd.
+Instance def_add_wd : Proper (Neq ==> Neq ==> Neq) as def_add.
 Proof.
 unfold def_add.
 intros x x' Exx' y y' Eyy'.
@@ -72,7 +72,7 @@ Proof.
 unfold fun2_eq; intros; apply def_add_wd; assumption.
 Qed.
 
-Add Morphism def_mul with signature Neq ==> Neq ==> Neq as def_mul_wd.
+Instance def_mul_wd : Proper (Neq ==> Neq ==> Neq) def_mul.
 Proof.
 unfold def_mul.
 intros x x' Exx' y y' Eyy'.
@@ -136,7 +136,7 @@ apply lt_step_wd.
 assumption.
 Qed.
 
-Add Morphism def_ltb with signature Neq ==> Neq ==> (@eq bool) as def_ltb_wd.
+Instance def_ltb_wd : Proper (Neq ==> Neq ==> eq) def_ltb.
 Proof.
 intros; now apply lt_curry_wd.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index da48d2fe0..6ecf7fd33 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -32,13 +32,13 @@ Definition homomorphism (f : N1 -> N2) : Prop :=
 Definition natural_isomorphism : N1 -> N2 :=
   NAxiomsMod1.recursion O2 (fun (n : N1) (p : N2) => S2 p).
 
-Add Morphism natural_isomorphism with signature Eq1 ==> Eq2 as natural_isomorphism_wd.
+Instance natural_isomorphism_wd : Proper (Eq1 ==> Eq2) natural_isomorphism.
 Proof.
 unfold natural_isomorphism.
 intros n m Eqxy.
 apply NAxiomsMod1.recursion_wd with (Aeq := Eq2).
 reflexivity.
-unfold fun2_eq. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd.
+intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd.
 assumption.
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index aee2cf8f7..a5b496ba3 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -201,21 +201,21 @@ Proof NZneq_succ_iter_l.
 in the induction step *)
 
 Theorem right_induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N, A z ->
       (forall n : N, z <= n -> A n -> A (S n)) ->
         forall n : N, z <= n -> A n.
 Proof NZright_induction.
 
 Theorem left_induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N, A z ->
       (forall n : N, n < z -> A (S n) -> A n) ->
         forall n : N, n <= z -> A n.
 Proof NZleft_induction.
 
 Theorem right_induction' :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N,
       (forall n : N, n <= z -> A n) ->
       (forall n : N, z <= n -> A n -> A (S n)) ->
@@ -223,7 +223,7 @@ Theorem right_induction' :
 Proof NZright_induction'.
 
 Theorem left_induction' :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N,
     (forall n : N, z <= n -> A n) ->
     (forall n : N, n < z -> A (S n) -> A n) ->
@@ -231,21 +231,21 @@ Theorem left_induction' :
 Proof NZleft_induction'.
 
 Theorem strong_right_induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N,
     (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) ->
        forall n : N, z <= n -> A n.
 Proof NZstrong_right_induction.
 
 Theorem strong_left_induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N,
       (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) ->
         forall n : N, n <= z -> A n.
 Proof NZstrong_left_induction.
 
 Theorem strong_right_induction' :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N,
       (forall n : N, n <= z -> A n) ->
       (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) ->
@@ -253,7 +253,7 @@ Theorem strong_right_induction' :
 Proof NZstrong_right_induction'.
 
 Theorem strong_left_induction' :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N,
     (forall n : N, z <= n -> A n) ->
     (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) ->
@@ -261,7 +261,7 @@ Theorem strong_left_induction' :
 Proof NZstrong_left_induction'.
 
 Theorem order_induction :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N, A z ->
       (forall n : N, z <= n -> A n -> A (S n)) ->
       (forall n : N, n < z  -> A (S n) -> A n) ->
@@ -269,7 +269,7 @@ Theorem order_induction :
 Proof NZorder_induction.
 
 Theorem order_induction' :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall z : N, A z ->
       (forall n : N, z <= n -> A n -> A (S n)) ->
       (forall n : N, n <= z -> A n -> A (P n)) ->
@@ -282,7 +282,7 @@ ZOrder) since they boil down to regular induction *)
 (** Elimintation principle for < *)
 
 Theorem lt_ind :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall n : N,
       A (S n) ->
       (forall m : N, n < m -> A m -> A (S m)) ->
@@ -292,7 +292,7 @@ Proof NZlt_ind.
 (** Elimintation principle for <= *)
 
 Theorem le_ind :
-  forall A : N -> Prop, predicate_wd Neq A ->
+  forall A : N -> Prop, Proper (Neq==>iff) A ->
     forall n : N,
       A n ->
       (forall m : N, n <= m -> A m -> A (S m)) ->
@@ -309,8 +309,7 @@ Proof NZgt_wf.
 
 Theorem lt_wf_0 : well_founded lt.
 Proof.
-setoid_replace lt with (fun n m : N => 0 <= n /\ n < m)
-  using relation (@relations_eq N N).
+setoid_replace lt with (fun n m : N => 0 <= n /\ n < m).
 apply lt_wf.
 intros x y; split.
 intro H; split; [apply le_0_l | assumption]. now intros [_ H].
@@ -400,13 +399,8 @@ Qed.
 
 Section RelElim.
 
-(* FIXME: Variable R : relation N. -- does not work *)
-
-Variable R : N -> N -> Prop.
-Hypothesis R_wd : relation_wd Neq Neq R.
-
-Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2.
-Proof. apply R_wd. Qed.
+Variable R : relation N.
+Hypothesis R_wd : Proper (Neq==>Neq==>iff) R.
 
 Theorem le_ind_rel :
    (forall m : N, R 0 m) ->
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index a9eec350f..dea4d664d 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -26,13 +26,7 @@ Variable Aeq : relation A.
 
 Notation Local "x ==A y" := (Aeq x y) (at level 70, no associativity).
 
-Hypothesis Aeq_equiv : equiv A Aeq.
-
-Add Relation A Aeq
- reflexivity proved by (proj1 Aeq_equiv)
- symmetry proved by (proj2 (proj2 Aeq_equiv))
- transitivity proved by (proj1 (proj2 Aeq_equiv))
-as Aeq_rel.
+Instance Aeq_equiv : Equivalence Aeq.
 
 Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (n : N) : A :=
 recursion
@@ -42,10 +36,7 @@ recursion
   n.
 
 Theorem strong_rec_wd :
-forall a a' : A, a ==A a' ->
-  forall f f', fun2_eq Neq (fun_eq Neq Aeq) Aeq f f' ->
-    forall n n', n == n' ->
-      strong_rec a f n ==A strong_rec a' f' n'.
+ Proper (Aeq ==> (Neq ==> (Neq ==>Aeq) ==> Aeq) ==> Neq ==> Aeq) strong_rec.
 Proof.
 intros a a' Eaa' f f' Eff' n n' Enn'.
 (* First we prove that recursion (which is on type N -> A) returns
diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v
index c5122ac08..5242826c6 100644
--- a/theories/Numbers/Natural/Binary/NBinDefs.v
+++ b/theories/Numbers/Natural/Binary/NBinDefs.v
@@ -32,34 +32,14 @@ Definition NZsub := Nminus.
 Definition NZmul := Nmult.
 
 Instance NZeq_equiv : Equivalence NZeq.
-
-Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
-Proof.
-congruence.
-Qed.
+Program Instance NZsucc_wd : Proper (eq==>eq) NZsucc.
+Program Instance NZpred_wd : Proper (eq==>eq) NZpred.
+Program Instance NZadd_wd : Proper (eq==>eq==>eq) NZadd.
+Program Instance NZsub_wd : Proper (eq==>eq==>eq) NZsub.
+Program Instance NZmul_wd : Proper (eq==>eq==>eq) NZmul.
 
 Theorem NZinduction :
-  forall A : NZ -> Prop, predicate_wd NZeq A ->
+  forall A : NZ -> Prop, Proper (NZeq==>iff) A ->
     A N0 -> (forall n, A n <-> A (NZsucc n)) -> forall n : NZ, A n.
 Proof.
 intros A A_wd A0 AS. apply Nrect. assumption. intros; now apply -> AS.
@@ -117,25 +97,10 @@ Definition NZle := Nle.
 Definition NZmin := Nmin.
 Definition NZmax := Nmax.
 
-Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
-Proof.
-unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
-Proof.
-unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.
-Proof.
-congruence.
-Qed.
+Program Instance NZlt_wd : Proper (eq==>eq==>iff) NZlt.
+Program Instance NZle_wd : Proper (eq==>eq==>iff) NZle.
+Program Instance NZmin_wd : Proper (eq==>eq==>eq) NZmin.
+Program Instance NZmax_wd : Proper (eq==>eq==>eq) NZmax.
 
 Theorem NZlt_eq_cases : forall n m : N, n <= m <-> n < m \/ n = m.
 Proof.
@@ -199,14 +164,9 @@ Proof.
 reflexivity.
 Qed.
 
-Theorem recursion_wd :
-forall (A : Type) (Aeq : relation A),
-  forall a a' : A, Aeq a a' ->
-    forall f f' : N -> A -> A, fun2_eq NZeq Aeq Aeq f f' ->
-      forall x x' : N, x = x' ->
-        Aeq (recursion a f x) (recursion a' f' x').
+Instance recursion_wd A (Aeq : relation A) :
+ Proper (Aeq==>(eq==>Aeq==>Aeq)==>eq==>Aeq) (@recursion A).
 Proof.
-unfold fun2_wd, NZeq, fun2_eq.
 intros A Aeq a a' Eaa' f f' Eff'.
 intro x; pattern x; apply Nrect.
 intros x' H; now rewrite <- H.
@@ -224,10 +184,10 @@ Qed.
 
 Theorem recursion_succ :
   forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A),
-    Aeq a a -> fun2_wd NZeq Aeq Aeq f ->
+    Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
       forall n : N, Aeq (recursion a f (Nsucc n)) (f n (recursion a f n)).
 Proof.
-unfold NZeq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n; pattern n; apply Nrect.
+unfold recursion; intros A Aeq a f EAaa f_wd n; pattern n; apply Nrect.
 rewrite Nrect_step; rewrite Nrect_base; now apply f_wd.
 clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|].
 now rewrite Nrect_step.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 38951218d..61171a43e 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -29,38 +29,14 @@ Definition NZsub := minus.
 Definition NZmul := mult.
 
 Instance NZeq_equiv : Equivalence NZeq.
-
-(* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat NZeq"
-then the theorem generated for succ_wd below is forall x, succ x = succ x,
-which does not match the axioms in NAxiomsSig *)
-
-Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
-Proof.
-congruence.
-Qed.
+Program Instance NZsucc_wd : Proper (eq==>eq) NZsucc.
+Program Instance NZpred_wd : Proper (eq==>eq) NZpred.
+Program Instance NZadd_wd : Proper (eq==>eq==>eq) NZadd.
+Program Instance NZsub_wd : Proper (eq==>eq==>eq) NZsub.
+Program Instance NZmul_wd : Proper (eq==>eq==>eq) NZmul.
 
 Theorem NZinduction :
-  forall A : nat -> Prop, predicate_wd (@eq nat) A ->
+  forall A : nat -> Prop, Proper (eq==>iff) A ->
     A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n.
 Proof.
 intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS.
@@ -108,25 +84,10 @@ Definition NZle := le.
 Definition NZmin := min.
 Definition NZmax := max.
 
-Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
-Proof.
-unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
-Proof.
-unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.
-Proof.
-congruence.
-Qed.
-
-Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.
-Proof.
-congruence.
-Qed.
+Program Instance NZlt_wd : Proper (eq==>eq==>iff) NZlt.
+Program Instance NZle_wd : Proper (eq==>eq==>iff) NZle.
+Program Instance NZmin_wd : Proper (eq==>eq==>eq) NZmin.
+Program Instance NZmax_wd : Proper (eq==>eq==>eq) NZmax.
 
 Theorem NZlt_eq_cases : forall n m : nat, n <= m <-> n < m \/ n = m.
 Proof.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 596603b6f..81893d9af 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -41,26 +41,26 @@ Definition NZmul := N.mul.
 
 Instance NZeq_equiv : Equivalence N.eq.
 
-Add Morphism NZsucc with signature N.eq ==> N.eq as NZsucc_wd.
+Instance NZsucc_wd : Proper (N.eq==>N.eq) NZsucc.
 Proof.
-unfold N.eq; intros; rewrite 2 N.spec_succ; f_equal; auto.
+unfold N.eq; repeat red; intros; rewrite 2 N.spec_succ; f_equal; auto.
 Qed.
 
-Add Morphism NZpred with signature N.eq ==> N.eq as NZpred_wd.
+Instance NZpred_wd : Proper (N.eq==>N.eq) NZpred.
 Proof.
-unfold N.eq; intros.
+unfold N.eq; repeat red; intros.
 generalize (N.spec_pos y) (N.spec_pos x) (N.spec_eq_bool x 0).
 destruct N.eq_bool; rewrite N.spec_0; intros.
 rewrite 2 N.spec_pred0; congruence.
 rewrite 2 N.spec_pred; f_equal; auto; try omega.
 Qed.
 
-Add Morphism NZadd with signature N.eq ==> N.eq ==> N.eq as NZadd_wd.
+Instance NZadd_wd : Proper (N.eq==>N.eq==>N.eq) NZadd.
 Proof.
-unfold N.eq; intros; rewrite 2 N.spec_add; f_equal; auto.
+unfold N.eq; repeat red; intros; rewrite 2 N.spec_add; f_equal; auto.
 Qed.
 
-Add Morphism NZsub with signature N.eq ==> N.eq ==> N.eq as NZsub_wd.
+Instance NZsub_wd : Proper (N.eq==>N.eq==>N.eq) NZsub.
 Proof.
 unfold N.eq; intros x x' Hx y y' Hy.
 destruct (Z_lt_le_dec [x] [y]).
@@ -68,14 +68,14 @@ rewrite 2 N.spec_sub0; f_equal; congruence.
 rewrite 2 N.spec_sub; f_equal; congruence.
 Qed.
 
-Add Morphism NZmul with signature N.eq ==> N.eq ==> N.eq as NZmul_wd.
+Instance NZmul_wd : Proper (N.eq==>N.eq==>N.eq) NZmul.
 Proof.
-unfold N.eq; intros; rewrite 2 N.spec_mul; f_equal; auto.
+unfold N.eq; repeat red; intros; rewrite 2 N.spec_mul; f_equal; auto.
 Qed.
 
 Theorem NZpred_succ : forall n, N.pred (N.succ n) == n.
 Proof.
-unfold N.eq; intros.
+unfold N.eq; repeat red; intros.
 rewrite N.spec_pred; rewrite N.spec_succ.
 omega.
 generalize (N.spec_pos n); omega.
@@ -86,13 +86,10 @@ Definition N_of_Z z := N.of_N (Zabs_N z).
 Section Induction.
 
 Variable A : N.t -> Prop.
-Hypothesis A_wd : predicate_wd N.eq A.
+Hypothesis A_wd : Proper (N.eq==>iff) A.
 Hypothesis A0 : A 0.
 Hypothesis AS : forall n, A n <-> A (N.succ n).
 
-Add Morphism A with signature N.eq ==> iff as A_morph.
-Proof. apply A_wd. Qed.
-
 Let B (z : Z) := A (N_of_Z z).
 
 Lemma B0 : B 0.
@@ -211,30 +208,30 @@ Proof.
  rewrite spec_compare_alt; destruct Zcompare; auto.
 Qed.
 
-Add Morphism N.compare with signature N.eq ==> N.eq ==> (@eq comparison) as compare_wd.
+Instance compare_wd : Proper (N.eq ==> N.eq ==> eq) N.compare.
 Proof.
 intros x x' Hx y y' Hy.
 rewrite 2 spec_compare_alt. unfold N.eq in *. rewrite Hx, Hy; intuition.
 Qed.
 
-Add Morphism N.lt with signature N.eq ==> N.eq ==> iff as NZlt_wd.
+Instance NZlt_wd : Proper (N.eq ==> N.eq ==> iff) N.lt.
 Proof.
 intros x x' Hx y y' Hy; unfold N.lt; rewrite Hx, Hy; intuition.
 Qed.
 
-Add Morphism N.le with signature N.eq ==> N.eq ==> iff as NZle_wd.
+Instance NZle_wd : Proper (N.eq ==> N.eq ==> iff) N.le.
 Proof.
 intros x x' Hx y y' Hy; unfold N.le; rewrite Hx, Hy; intuition.
 Qed.
 
-Add Morphism N.min with signature N.eq ==> N.eq ==> N.eq as NZmin_wd.
+Instance NZmin_wd : Proper (N.eq ==> N.eq ==> N.eq) N.min.
 Proof.
-intros; red; rewrite 2 spec_min; congruence.
+repeat red; intros; rewrite 2 spec_min; congruence.
 Qed.
 
-Add Morphism N.max with signature N.eq ==> N.eq ==> N.eq as NZmax_wd.
+Instance NZmax_wd : Proper (N.eq ==> N.eq ==> N.eq) N.max.
 Proof.
-intros; red; rewrite 2 spec_max; congruence.
+repeat red; intros; rewrite 2 spec_max; congruence.
 Qed.
 
 Theorem NZlt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
@@ -313,10 +310,10 @@ Qed.
 
 Theorem recursion_succ :
   forall (A : Type) (Aeq : relation A) (a : A) (f : N.t -> A -> A),
-    Aeq a a -> fun2_wd N.eq Aeq Aeq f ->
+    Aeq a a -> Proper (N.eq==>Aeq==>Aeq) f ->
       forall n, Aeq (recursion a f (N.succ n)) (f n (recursion a f n)).
 Proof.
-unfold N.eq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n.
+unfold N.eq, recursion; intros A Aeq a f EAaa f_wd n.
 replace (N.to_N (N.succ n)) with (Nsucc (N.to_N n)).
 rewrite Nrect_step.
 apply f_wd; auto.