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

7 files changed, 67 insertions, 143 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index 917e3fc123..5f68b2bb15 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -350,9 +350,7 @@ Qed.
 Section PosNeg.
 
 Variable P : Z -> Prop.
-Hypothesis P_wd : predicate_wd Zeq P.
-
-Add Morphism P with signature Zeq ==> iff as P_morph. Proof. exact P_wd. Qed.
+Hypothesis P_wd : Proper (Zeq ==> iff) P.
 
 Theorem Z0_pos_neg :
   P 0 -> (forall n : Z, 0 < n -> P n /\ P (- n)) -> forall n : Z, P n.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 7b3c0ba6e8..00e34a5b55 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -64,7 +64,7 @@ Theorem Zeq_dne : forall n m : Z, ~ ~ n == m <-> n == m.
 Proof NZeq_dne.
 
 Theorem Zcentral_induction :
-forall A : Z -> Prop, predicate_wd Zeq A ->
+forall A : Z -> Prop, Proper (Zeq==>iff) A ->
   forall z : Z, A z ->
     (forall n : Z, A n <-> A (S n)) ->
       forall n : Z, A n.
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index 4d927cb3b6..500dd9f535 100644
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -10,22 +10,17 @@
 
 (*i $Id$ i*)
 
+Require Import Bool.
 Require Export NumPrelude.
 
 Module Type ZDomainSignature.
 
 Parameter Inline Z : Set.
 Parameter Inline Zeq : Z -> Z -> Prop.
-Parameter Inline e : Z -> Z -> bool.
+Parameter Inline Zeqb : Z -> Z -> bool.
 
-Axiom eq_equiv_e : forall x y : Z, Zeq x y <-> e x y.
-Axiom eq_equiv : equiv Z Zeq.
-
-Add Relation Z Zeq
- reflexivity proved by (proj1 eq_equiv)
- symmetry proved by (proj2 (proj2 eq_equiv))
- transitivity proved by (proj1 (proj2 eq_equiv))
-as eq_rel.
+Axiom eqb_equiv_eq : forall x y : Z, Zeqb x y = true <-> Zeq x y.
+Instance eq_equiv : Equivalence Zeq.
 
 Delimit Scope IntScope with Int.
 Bind Scope IntScope with Z.
@@ -37,16 +32,11 @@ End ZDomainSignature.
 Module ZDomainProperties (Import ZDomainModule : ZDomainSignature).
 Open Local Scope IntScope.
 
-Add Morphism e with signature Zeq ==> Zeq ==> eq_bool as e_wd.
+Instance Zeqb_wd : Proper (Zeq ==> Zeq ==> eq) Zeqb.
 Proof.
 intros x x' Exx' y y' Eyy'.
-case_eq (e x y); case_eq (e x' y'); intros H1 H2; trivial.
-assert (x == y); [apply <- eq_equiv_e; now rewrite H2 |
-assert (x' == y'); [rewrite <- Exx'; now rewrite <- Eyy' |
-rewrite <- H1; assert (H3 : e x' y'); [now apply -> eq_equiv_e | now inversion H3]]].
-assert (x' == y'); [apply <- eq_equiv_e; now rewrite H1 |
-assert (x == y); [rewrite Exx'; now rewrite Eyy' |
-rewrite <- H2; assert (H3 : e x y); [now apply -> eq_equiv_e | now inversion H3]]].
+apply eq_true_iff_eq.
+rewrite 2 eqb_equiv_eq, Exx', Eyy'; auto with *.
 Qed.
 
 Theorem neq_sym : forall n m, n # m -> m # n.
@@ -62,7 +52,7 @@ Qed.
 Declare Left Step ZE_stepl.
 
 (* The right step lemma is just transitivity of Zeq *)
-Declare Right Step (proj1 (proj2 eq_equiv)).
+Declare Right Step (@Equivalence_Transitive _ _ eq_equiv).
 
 End ZDomainProperties.
 
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 1b8bdda408..efd1f0da39 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -221,21 +221,21 @@ Proof NZneq_succ_iter_l.
 in the induction step *)
 
 Theorem Zright_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z, A z ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
         forall n : Z, z <= n -> A n.
 Proof NZright_induction.
 
 Theorem Zleft_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z, A z ->
       (forall n : Z, n < z -> A (S n) -> A n) ->
         forall n : Z, n <= z -> A n.
 Proof NZleft_induction.
 
 Theorem Zright_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
       (forall n : Z, n <= z -> A n) ->
       (forall n : Z, z <= n -> A n -> A (S n)) ->
@@ -243,7 +243,7 @@ Theorem Zright_induction' :
 Proof NZright_induction'.
 
 Theorem Zleft_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
     (forall n : Z, z <= n -> A n) ->
     (forall n : Z, n < z -> A (S n) -> A n) ->
@@ -251,21 +251,21 @@ Theorem Zleft_induction' :
 Proof NZleft_induction'.
 
 Theorem Zstrong_right_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
     (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
        forall n : Z, z <= n -> A n.
 Proof NZstrong_right_induction.
 
 Theorem Zstrong_left_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
       (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
         forall n : Z, n <= z -> A n.
 Proof NZstrong_left_induction.
 
 Theorem Zstrong_right_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
       (forall n : Z, n <= z -> A n) ->
       (forall n : Z, z <= n -> (forall m : Z, z <= m -> m < n -> A m) -> A n) ->
@@ -273,7 +273,7 @@ Theorem Zstrong_right_induction' :
 Proof NZstrong_right_induction'.
 
 Theorem Zstrong_left_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z,
     (forall n : Z, z <= n -> A n) ->
     (forall n : Z, n <= z -> (forall m : Z, m <= z -> S n <= m -> A m) -> A n) ->
@@ -281,7 +281,7 @@ Theorem Zstrong_left_induction' :
 Proof NZstrong_left_induction'.
 
 Theorem Zorder_induction :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z, A z ->
     (forall n : Z, z <= n -> A n -> A (S n)) ->
     (forall n : Z, n < z -> A (S n) -> A n) ->
@@ -289,7 +289,7 @@ Theorem Zorder_induction :
 Proof NZorder_induction.
 
 Theorem Zorder_induction' :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall z : Z, A z ->
     (forall n : Z, z <= n -> A n -> A (S n)) ->
     (forall n : Z, n <= z -> A n -> A (P n)) ->
@@ -297,7 +297,7 @@ Theorem Zorder_induction' :
 Proof NZorder_induction'.
 
 Theorem Zorder_induction_0 :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     A 0 ->
     (forall n : Z, 0 <= n -> A n -> A (S n)) ->
     (forall n : Z, n < 0 -> A (S n) -> A n) ->
@@ -305,7 +305,7 @@ Theorem Zorder_induction_0 :
 Proof NZorder_induction_0.
 
 Theorem Zorder_induction'_0 :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     A 0 ->
     (forall n : Z, 0 <= n -> A n -> A (S n)) ->
     (forall n : Z, n <= 0 -> A n -> A (P n)) ->
@@ -317,7 +317,7 @@ Ltac Zinduct n := induction_maker n ltac:(apply Zorder_induction_0).
 (** Elimintation principle for < *)
 
 Theorem Zlt_ind :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall n : Z, A (S n) ->
       (forall m : Z, n < m -> A m -> A (S m)) -> forall m : Z, n < m -> A m.
 Proof NZlt_ind.
@@ -325,7 +325,7 @@ Proof NZlt_ind.
 (** Elimintation principle for <= *)
 
 Theorem Zle_ind :
-  forall A : Z -> Prop, predicate_wd Zeq A ->
+  forall A : Z -> Prop, Proper (Zeq==>iff) A ->
     forall n : Z, A n ->
       (forall m : Z, n <= m -> A m -> A (S m)) -> forall m : Z, n <= m -> A m.
 Proof NZle_ind.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 7afa1e442e..9b55c771c9 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -29,31 +29,11 @@ Definition NZsub := Zminus.
 Definition NZmul := Zmult.
 
 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 NZpred_succ : forall n : Z, NZpred (NZsucc n) = n.
 Proof.
@@ -61,7 +41,7 @@ exact Zpred'_succ'.
 Qed.
 
 Theorem NZinduction :
-  forall A : Z -> Prop, predicate_wd NZeq A ->
+  forall A : Z -> Prop, Proper (NZeq ==> iff) A ->
     A 0 -> (forall n : Z, A n <-> A (NZsucc n)) -> forall n : Z, A n.
 Proof.
 intros A A_wd A0 AS n; apply Zind; clear n.
@@ -108,25 +88,10 @@ Definition NZle := Zle.
 Definition NZmin := Zmin.
 Definition NZmax := Zmax.
 
-Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
-Proof.
-unfold NZeq. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2.
-Qed.
-
-Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
-Proof.
-unfold NZeq. intros n1 n2 H1 m1 m2 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 : Z, n <= m <-> n < m \/ n = m.
 Proof.
@@ -182,10 +147,7 @@ match x with
 | Zneg x => Zpos x
 end.
 
-Add Morphism Zopp with signature NZeq ==> NZeq as Zopp_wd.
-Proof.
-congruence.
-Qed.
+Program Instance Zopp_wd : Proper (eq==>eq) Zopp.
 
 Theorem Zsucc_pred : forall n : Z, NZsucc (NZpred n) = n.
 Proof.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 3eb5238d98..dcda3f1e59 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -44,7 +44,7 @@ Qed.
 
 Add Ring NSR : Nsemi_ring.
 
-(* The definitios of functions (NZadd, NZmul, etc.) will be unfolded by
+(* The definitions of functions (NZadd, NZmul, etc.) will be unfolded by
 the properties functor. Since we don't want Zadd_comm to refer to unfolded
 definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1),
 we will provide an extra layer of definitions. *)
@@ -130,24 +130,24 @@ Proof.
 split; [apply ZE_refl | apply ZE_sym | apply ZE_trans].
 Qed.
 
-Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd.
+Instance Zpair_wd : Proper (NE==>NE==>Zeq) (@pair N N).
 Proof.
 intros n1 n2 H1 m1 m2 H2; unfold Zeq; simpl; rewrite H1; now rewrite H2.
 Qed.
 
-Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd.
+Instance NZsucc_wd : Proper (Zeq ==> Zeq) NZsucc.
 Proof.
 unfold NZsucc, Zeq; intros n m H; simpl.
 do 2 rewrite add_succ_l; now rewrite H.
 Qed.
 
-Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd.
+Instance NZpred_wd : Proper (Zeq ==> Zeq) NZpred.
 Proof.
 unfold NZpred, Zeq; intros n m H; simpl.
 do 2 rewrite add_succ_r; now rewrite H.
 Qed.
 
-Add Morphism NZadd with signature Zeq ==> Zeq ==> Zeq as NZadd_wd.
+Instance NZadd_wd : Proper (Zeq ==> Zeq ==> Zeq) NZadd.
 Proof.
 unfold Zeq, NZadd; intros n1 m1 H1 n2 m2 H2; simpl.
 assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2))
@@ -156,7 +156,7 @@ stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring.
 now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring.
 Qed.
 
-Add Morphism NZsub with signature Zeq ==> Zeq ==> Zeq as NZsub_wd.
+Instance NZsub_wd : Proper (Zeq ==> Zeq ==> Zeq) NZsub.
 Proof.
 unfold Zeq, NZsub; intros n1 m1 H1 n2 m2 H2; simpl.
 symmetry in H2.
@@ -166,7 +166,7 @@ stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring.
 now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring.
 Qed.
 
-Add Morphism NZmul with signature Zeq ==> Zeq ==> Zeq as NZmul_wd.
+Instance NZmul_wd : Proper (Zeq ==> Zeq ==> Zeq) NZmul.
 Proof.
 unfold NZmul, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
 stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring.
@@ -189,17 +189,13 @@ Qed.
 Section Induction.
 Open Scope NatScope. (* automatically closes at the end of the section *)
 Variable A : Z -> Prop.
-Hypothesis A_wd : predicate_wd Zeq A.
-
-Add Morphism A with signature Zeq ==> iff as A_morph.
-Proof.
-exact A_wd.
-Qed.
+Hypothesis A_wd : Proper (Zeq==>iff) A.
 
 Theorem NZinduction :
-  A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *)
+  A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n.
+  (* 0 is interpreted as in Z due to "Bind" directive *)
 Proof.
-intros A0 AS n; unfold NZ0, Zsucc, predicate_wd, fun_wd, Zeq in *.
+intros A0 AS n; unfold NZ0, Zsucc, Zeq in *.
 destruct n as [n m].
 cut (forall p : N, A (p, 0)); [intro H1 |].
 cut (forall p : N, A (0, p)); [intro H2 |].
@@ -266,7 +262,7 @@ Definition NZle := Zle.
 Definition NZmin := Zmin.
 Definition NZmax := Zmax.
 
-Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd.
+Instance NZlt_wd : Proper (Zeq ==> Zeq ==> iff) NZlt.
 Proof.
 unfold NZlt, Zlt, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H.
 stepr (snd m1 + fst m2) by apply add_comm.
@@ -285,7 +281,7 @@ now stepl (fst m1 + snd m2) by apply add_comm.
 stepl (fst n2 + snd m2) by apply add_comm. now stepr (fst m2 + snd n2) by apply add_comm.
 Qed.
 
-Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd.
+Instance NZle_wd : Proper (Zeq ==> Zeq ==> iff) NZle.
 Proof.
 unfold NZle, Zle, Zeq; intros n1 m1 H1 n2 m2 H2; simpl.
 do 2 rewrite lt_eq_cases. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2)%Int.
@@ -293,7 +289,7 @@ fold (n1 == n2)%Int (m1 == m2)%Int; fold (n1 == m1)%Int in H1; fold (n2 == m2)%I
 now rewrite H1, H2.
 Qed.
 
-Add Morphism NZmin with signature Zeq ==> Zeq ==> Zeq as NZmin_wd.
+Instance NZmin_wd : Proper (Zeq ==> Zeq ==> Zeq) NZmin.
 Proof.
 intros n1 m1 H1 n2 m2 H2; unfold NZmin, Zeq; simpl.
 destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
@@ -309,7 +305,7 @@ stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring.
 unfold Zeq in H2. rewrite H2. ring.
 Qed.
 
-Add Morphism NZmax with signature Zeq ==> Zeq ==> Zeq as NZmax_wd.
+Instance NZmax_wd : Proper (Zeq ==> Zeq ==> Zeq) NZmax.
 Proof.
 intros n1 m1 H1 n2 m2 H2; unfold NZmax, Zeq; simpl.
 destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
@@ -372,7 +368,7 @@ Definition Zopp (n : Z) : Z := (snd n, fst n).
 
 Notation "- x" := (Zopp x) : IntScope.
 
-Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
+Instance Zopp_wd : Proper (Zeq ==> Zeq) Zopp.
 Proof.
 unfold Zeq; intros n m H; simpl. symmetry.
 stepl (fst n + snd m) by apply add_comm.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 3e029d81b6..823ef149c2 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -32,6 +32,7 @@ Hint Rewrite
  Z.spec_mul Z.spec_opp Z.spec_of_Z : Zspec.
 
 Ltac zsimpl := unfold Z.eq in *; autorewrite with Zspec.
+Ltac zcongruence := repeat red; intros; zsimpl; congruence.
 
 Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
 Module Export NZAxiomsMod <: NZAxiomsSig.
@@ -47,30 +48,13 @@ Definition NZmul := Z.mul.
 
 Instance NZeq_equiv : Equivalence Z.eq.
 
-Add Morphism NZsucc with signature Z.eq ==> Z.eq as NZsucc_wd.
-Proof.
-intros; zsimpl; f_equal; assumption.
-Qed.
+Obligation Tactic := zcongruence.
 
-Add Morphism NZpred with signature Z.eq ==> Z.eq as NZpred_wd.
-Proof.
-intros; zsimpl; f_equal; assumption.
-Qed.
-
-Add Morphism NZadd with signature Z.eq ==> Z.eq ==> Z.eq as NZadd_wd.
-Proof.
-intros; zsimpl; f_equal; assumption.
-Qed.
-
-Add Morphism NZsub with signature Z.eq ==> Z.eq ==> Z.eq as NZsub_wd.
-Proof.
-intros; zsimpl; f_equal; assumption.
-Qed.
-
-Add Morphism NZmul with signature Z.eq ==> Z.eq ==> Z.eq as NZmul_wd.
-Proof.
-intros; zsimpl; f_equal; assumption.
-Qed.
+Program Instance NZsucc_wd : Proper (Z.eq ==> Z.eq) NZsucc.
+Program Instance NZpred_wd : Proper (Z.eq ==> Z.eq) NZpred.
+Program Instance NZadd_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) NZadd.
+Program Instance NZsub_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) NZsub.
+Program Instance NZmul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) NZmul.
 
 Theorem NZpred_succ : forall n, Z.pred (Z.succ n) == n.
 Proof.
@@ -80,13 +64,10 @@ Qed.
 Section Induction.
 
 Variable A : Z.t -> Prop.
-Hypothesis A_wd : predicate_wd Z.eq A.
+Hypothesis A_wd : Proper (Z.eq==>iff) A.
 Hypothesis A0 : A 0.
 Hypothesis AS : forall n, A n <-> A (Z.succ n).
 
-Add Morphism A with signature Z.eq ==> iff as A_morph.
-Proof. apply A_wd. Qed.
-
 Let B (z : Z) := A (Z.of_Z z).
 
 Lemma B0 : B 0.
@@ -204,30 +185,30 @@ Proof.
  rewrite spec_compare_alt; destruct Zcompare; auto.
 Qed.
 
-Add Morphism Z.compare with signature Z.eq ==> Z.eq ==> (@eq comparison) as compare_wd.
+Instance compare_wd : Proper (Z.eq ==> Z.eq ==> eq) Z.compare.
 Proof.
 intros x x' Hx y y' Hy.
 rewrite 2 spec_compare_alt; unfold Z.eq in *; rewrite Hx, Hy; intuition.
 Qed.
 
-Add Morphism Z.lt with signature Z.eq ==> Z.eq ==> iff as NZlt_wd.
+Instance NZlt_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.lt.
 Proof.
 intros x x' Hx y y' Hy; unfold Z.lt; rewrite Hx, Hy; intuition.
 Qed.
 
-Add Morphism Z.le with signature Z.eq ==> Z.eq ==> iff as NZle_wd.
+Instance NZle_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.le.
 Proof.
 intros x x' Hx y y' Hy; unfold Z.le; rewrite Hx, Hy; intuition.
 Qed.
 
-Add Morphism Z.min with signature Z.eq ==> Z.eq ==> Z.eq as NZmin_wd.
+Instance NZmin_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.min.
 Proof.
-intros; red; rewrite 2 spec_min; congruence.
+repeat red; intros; rewrite 2 spec_min; congruence.
 Qed.
 
-Add Morphism Z.max with signature Z.eq ==> Z.eq ==> Z.eq as NZmax_wd.
+Instance NZmax_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.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.
@@ -274,10 +255,7 @@ End NZOrdAxiomsMod.
 
 Definition Zopp := Z.opp.
 
-Add Morphism Z.opp with signature Z.eq ==> Z.eq as Zopp_wd.
-Proof.
-intros; zsimpl; auto with zarith.
-Qed.
+Program Instance Zopp_wd : Proper (Z.eq ==> Z.eq) Z.opp.
 
 Theorem Zsucc_pred : forall n, Z.succ (Z.pred n) == n.
 Proof.