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

4 files changed, 14 insertions, 17 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.