7 files changed, 27 insertions, 59 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 60f2aae7d..6a34d0f7b 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -50,18 +50,15 @@ Implicit Arguments recursion [A].
 
 Axiom pred_0 : P 0 == 0.
 
-Axiom recursion_wd : forall (A : Type) (Aeq : relation A),
-  forall a a' : A, Aeq a a' ->
-    forall f f' : N -> A -> A, fun2_eq Neq Aeq Aeq f f' ->
-      forall x x' : N, x == x' ->
-        Aeq (recursion a f x) (recursion a' f' x').
+Instance recursion_wd (A : Type) (Aeq : relation A) :
+ Proper (Aeq ==> (Neq==>Aeq==>Aeq) ==> Neq ==> Aeq) (@recursion A).
 
 Axiom recursion_0 :
   forall (A : Type) (a : A) (f : N -> A -> A), recursion a f 0 = a.
 
 Axiom recursion_succ :
   forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A),
-    Aeq a a -> fun2_wd Neq Aeq Aeq f ->
+    Aeq a a -> Proper (Neq==>Aeq==>Aeq) f ->
       forall n : N, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 
 (*Axiom dep_rec :
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index a0111a082..60b43f0d2 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -46,13 +46,13 @@ Theorem pred_0 : P 0 == 0.
 Proof pred_0.
 
 Theorem Neq_refl : forall n : N, n == n.
-Proof (proj1 NZeq_equiv).
+Proof (@Equivalence_Reflexive _ _ NZeq_equiv).
 
 Theorem Neq_sym : forall n m : N, n == m -> m == n.
-Proof (proj2 (proj2 NZeq_equiv)).
+Proof (@Equivalence_Symmetric _ _ NZeq_equiv).
 
 Theorem Neq_trans : forall n m p : N, n == m -> m == p -> n == p.
-Proof (proj1 (proj2 NZeq_equiv)).
+Proof (@Equivalence_Transitive _ _ NZeq_equiv).
 
 Theorem neq_sym : forall n m : N, n ~= m -> m ~= n.
 Proof NZneq_sym.
@@ -81,10 +81,10 @@ function (by recursion) that maps 0 to false and the successor to true *)
 Definition if_zero (A : Set) (a b : A) (n : N) : A :=
   recursion a (fun _ _ => b) n.
 
-Add Parametric Morphism (A : Set) : (if_zero A) with signature (eq ==> eq ==> Neq ==> eq) as if_zero_wd.
+Instance if_zero_wd (A : Set) : Proper (eq ==> eq ==> Neq ==> eq) (if_zero A).
 Proof.
-intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)).
-reflexivity. unfold fun2_eq; now intros. assumption.
+intros; unfold if_zero.
+repeat red; intros. apply recursion_wd; auto. repeat red; auto.
 Qed.
 
 Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a.
@@ -95,7 +95,7 @@ Qed.
 Theorem if_zero_succ : forall (A : Set) (a b : A) (n : N), if_zero A a b (S n) = b.
 Proof.
 intros; unfold if_zero.
-now rewrite (@recursion_succ A (@eq A)); [| | unfold fun2_wd; now intros].
+now rewrite (@recursion_succ A (@eq A)).
 Qed.
 
 Implicit Arguments if_zero [A].
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index e18e3b67f..e2a6df1cc 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -109,12 +109,12 @@ recursion
 
 Infix Local "<<" := def_ltb (at level 70, no associativity).
 
-Lemma lt_base_wd : fun_wd Neq (@eq bool) (if_zero false true).
+Lemma lt_base_wd : Proper (Neq==>eq) (if_zero false true).
 unfold fun_wd; intros; now apply if_zero_wd.
 Qed.
 
 Lemma lt_step_wd :
-fun2_wd Neq (fun_eq Neq (@eq bool)) (fun_eq Neq (@eq bool))
+ fun2_wd Neq (fun_eq Neq (@eq bool)) (fun_eq Neq (@eq bool))
   (fun _ f => fun n => recursion false (fun n' _ => f n') n).
 Proof.
 unfold fun2_wd, fun_eq.
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 5ad343fe0..da48d2fe0 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -51,8 +51,8 @@ Theorem natural_isomorphism_succ :
   forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n).
 Proof.
 unfold natural_isomorphism.
-intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq) ;
-[ | | unfold fun2_wd; intros; apply NBasePropMod2.succ_wd].
+intro n. rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq); auto with *.
+repeat red; intros. apply NBasePropMod2.succ_wd; auto.
 Qed.
 
 Theorem hom_nat_iso : homomorphism natural_isomorphism.
diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v
index c2c7767d5..c5122ac08 100644
--- a/theories/Numbers/Natural/Binary/NBinDefs.v
+++ b/theories/Numbers/Natural/Binary/NBinDefs.v
@@ -31,14 +31,7 @@ Definition NZadd := Nplus.
 Definition NZsub := Nminus.
 Definition NZmul := Nmult.
 
-Theorem NZeq_equiv : equiv N NZeq.
-Proof (eq_equiv N).
-
-Add Relation N NZeq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
-as NZeq_rel.
+Instance NZeq_equiv : Equivalence NZeq.
 
 Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
 Proof.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 8d9e17fb0..38951218d 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -28,14 +28,7 @@ Definition NZadd := plus.
 Definition NZsub := minus.
 Definition NZmul := mult.
 
-Theorem NZeq_equiv : equiv nat NZeq.
-Proof (eq_equiv nat).
-
-Add Relation nat NZeq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
-as NZeq_rel.
+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,
@@ -189,13 +182,11 @@ Proof.
 reflexivity.
 Qed.
 
-Theorem recursion_wd : forall (A : Type) (Aeq : relation A),
-  forall a a' : A, Aeq a a' ->
-    forall f f' : nat -> A -> A, fun2_eq (@eq nat) Aeq Aeq f f' ->
-      forall n n' : nat, n = n' ->
-        Aeq (recursion a f n) (recursion a' f' n').
+Instance recursion_wd (A : Type) (Aeq : relation A) :
+ Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
 Proof.
-unfold fun2_eq; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto.
+intros A Aeq a a' Ha f f' Hf n n' Hn. subst n'.
+induction n; simpl; auto. apply Hf; auto.
 Qed.
 
 Theorem recursion_0 :
@@ -206,10 +197,10 @@ Qed.
 
 Theorem recursion_succ :
   forall (A : Type) (Aeq : relation A) (a : A) (f : nat -> A -> A),
-    Aeq a a -> fun2_wd (@eq nat) Aeq Aeq f ->
+    Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
       forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 Proof.
-induction n; simpl; auto.
+unfold Proper, respectful in *; induction n; simpl; auto.
 Qed.
 
 End NPeanoAxiomsMod.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 578cb6256..596603b6f 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -39,16 +39,7 @@ Definition NZadd := N.add.
 Definition NZsub := N.sub.
 Definition NZmul := N.mul.
 
-Theorem NZeq_equiv : equiv N.t N.eq.
-Proof.
-repeat split; repeat red; intros; auto; congruence.
-Qed.
-
-Add Relation N.t N.eq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
- as NZeq_rel.
+Instance NZeq_equiv : Equivalence N.eq.
 
 Add Morphism NZsucc with signature N.eq ==> N.eq as NZsucc_wd.
 Proof.
@@ -297,14 +288,10 @@ Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) :=
   Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n).
 Implicit Arguments recursion [A].
 
-Theorem recursion_wd :
-forall (A : Type) (Aeq : relation A),
-  forall a a' : A, Aeq a a' ->
-    forall f f' : N.t -> A -> A, fun2_eq N.eq Aeq Aeq f f' ->
-      forall x x' : N.t, x == x' ->
-        Aeq (recursion a f x) (recursion a' f' x').
+Instance recursion_wd (A : Type) (Aeq : relation A) :
+ Proper (Aeq ==> (N.eq==>Aeq==>Aeq) ==> N.eq ==> Aeq) (@recursion A).
 Proof.
-unfold fun2_wd, N.eq, fun2_eq.
+unfold N.eq.
 intros A Aeq a a' Eaa' f f' Eff' x x' Exx'.
 unfold recursion.
 unfold N.to_N.
@@ -312,7 +299,7 @@ rewrite <- Exx'; clear x' Exx'.
 replace (Zabs_N [x]) with (N_of_nat (Zabs_nat [x])).
 induction (Zabs_nat [x]).
 simpl; auto.
-rewrite N_of_S, 2 Nrect_step; auto.
+rewrite N_of_S, 2 Nrect_step; auto. apply Eff'; auto.
 destruct [x]; simpl; auto.
 change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N.
 change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N.