Numbers: start using Classes stuff, Equivalence, Proper, Instance, etc

TODO: finish removing the "Add Relation", "Add Morphism" fun_* fun2_*
TODO: now that we have Include, flatten the hierarchy...

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

5 files changed, 8 insertions, 32 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index dfffe9a7f..bd6db10d9 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -48,7 +48,7 @@ Parameter Zopp : Z -> Z.
 (*Notation "- 1" := (Zopp 1) : IntScope.
 Check (-1).*)
 
-Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd.
+Instance Zopp_wd : Proper (Zeq==>Zeq) Zopp.
 
 Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope.
 Notation "- 1" := (Zopp (NZsucc NZ0)) : IntScope.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 648cde197..7b3c0ba6e 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -34,13 +34,13 @@ Theorem Zpred_succ : forall n : Z, P (S n) == n.
 Proof NZpred_succ.
 
 Theorem Zeq_refl : forall n : Z, n == n.
-Proof (proj1 NZeq_equiv).
+Proof (@Equivalence_Reflexive _ _ NZeq_equiv).
 
 Theorem Zeq_sym : forall n m : Z, n == m -> m == n.
-Proof (proj2 (proj2 NZeq_equiv)).
+Proof (@Equivalence_Symmetric _ _ NZeq_equiv).
 
 Theorem Zeq_trans : forall n m p : Z, n == m -> m == p -> n == p.
-Proof (proj1 (proj2 NZeq_equiv)).
+Proof (@Equivalence_Transitive _ _ NZeq_equiv).
 
 Theorem Zneq_sym : forall n m : Z, n ~= m -> m ~= n.
 Proof NZneq_sym.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 0ff896367..7afa1e442 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -28,16 +28,7 @@ Definition NZadd := Zplus.
 Definition NZsub := Zminus.
 Definition NZmul := Zmult.
 
-Theorem NZeq_equiv : equiv Z NZeq.
-Proof.
-exact (@eq_equiv Z).
-Qed.
-
-Add Relation Z 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/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 381b9baf6..3eb5238d9 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -125,17 +125,11 @@ stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring.
 now apply -> add_cancel_r in H3.
 Qed.
 
-Theorem NZeq_equiv : equiv Z Zeq.
+Instance NZeq_equiv : Equivalence Zeq.
 Proof.
-unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_sym].
+split; [apply ZE_refl | apply ZE_sym | apply ZE_trans].
 Qed.
 
-Add Relation Z Zeq
- reflexivity proved by (proj1 NZeq_equiv)
- symmetry proved by (proj2 (proj2 NZeq_equiv))
- transitivity proved by (proj1 (proj2 NZeq_equiv))
-as NZeq_rel.
-
 Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd.
 Proof.
 intros n1 n2 H1 m1 m2 H2; unfold Zeq; simpl; rewrite H1; now rewrite H2.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 030c589ff..3e029d81b 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -45,16 +45,7 @@ Definition NZadd := Z.add.
 Definition NZsub := Z.sub.
 Definition NZmul := Z.mul.
 
-Theorem NZeq_equiv : equiv Z.t Z.eq.
-Proof.
-repeat split; repeat red; intros; auto; congruence.
-Qed.
-
-Add Relation Z.t Z.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 Z.eq.
 
 Add Morphism NZsucc with signature Z.eq ==> Z.eq as NZsucc_wd.
 Proof.