Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natural numbers are isomorphic. Added NatScope and IntScope for abstract developments.

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

3 files changed, 22 insertions, 22 deletions

diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 1509b5f7d..89f44fcd4 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -3,7 +3,7 @@ Require Export NumPrelude.
 Module Type NZAxiomsSig.
 
 Parameter Inline NZ : Set.
-Parameter Inline NZE : NZ -> NZ -> Prop.
+Parameter Inline NZeq : NZ -> NZ -> Prop.
 Parameter Inline NZ0 : NZ.
 Parameter Inline NZsucc : NZ -> NZ.
 Parameter Inline NZpred : NZ -> NZ.
@@ -11,26 +11,26 @@ Parameter Inline NZplus : NZ -> NZ -> NZ.
 Parameter Inline NZminus : NZ -> NZ -> NZ.
 Parameter Inline NZtimes : NZ -> NZ -> NZ.
 
-Axiom NZE_equiv : equiv NZ NZE.
-Add Relation NZ NZE
+Axiom NZE_equiv : equiv NZ NZeq.
+Add Relation NZ NZeq
  reflexivity proved by (proj1 NZE_equiv)
  symmetry proved by (proj2 (proj2 NZE_equiv))
  transitivity proved by (proj1 (proj2 NZE_equiv))
 as NZE_rel.
 
-Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd.
-Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd.
-Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd.
-Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd.
-Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd.
+Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
+Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
+Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd.
+Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd.
+Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd.
 
 Delimit Scope NatIntScope with NatInt.
 Open Local Scope NatIntScope.
-Notation "x == y"  := (NZE x y) (at level 70) : NatIntScope.
-Notation "x ~= y" := (~ NZE x y) (at level 70) : NatIntScope.
+Notation "x == y"  := (NZeq x y) (at level 70) : NatIntScope.
+Notation "x ~= y" := (~ NZeq x y) (at level 70) : NatIntScope.
 Notation "0" := NZ0 : NatIntScope.
-Notation "'S'" := NZsucc : NatIntScope.
-Notation "'P'" := NZpred : NatIntScope.
+Notation S := NZsucc.
+Notation P := NZpred.
 Notation "1" := (S 0) : NatIntScope.
 Notation "x + y" := (NZplus x y) : NatIntScope.
 Notation "x - y" := (NZminus x y) : NatIntScope.
@@ -39,7 +39,7 @@ Notation "x * y" := (NZtimes x y) : NatIntScope.
 Axiom NZpred_succ : forall n : NZ, P (S n) == n.
 
 Axiom NZinduction :
-  forall A : NZ -> Prop, predicate_wd NZE A ->
+  forall A : NZ -> Prop, predicate_wd NZeq A ->
     A 0 -> (forall n : NZ, A n <-> A (S n)) -> forall n : NZ, A n.
 
 Axiom NZplus_0_l : forall n : NZ, 0 + n == n.
@@ -60,8 +60,8 @@ Open Local Scope NatIntScope.
 Parameter Inline NZlt : NZ -> NZ -> Prop.
 Parameter Inline NZle : NZ -> NZ -> Prop.
 
-Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd.
-Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd.
+Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.
+Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.
 
 Notation "x < y" := (NZlt x y) : NatIntScope.
 Notation "x <= y" := (NZle x y) : NatIntScope.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 121f78813..c467816d7 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -14,7 +14,7 @@ intros x y z H1 H2; now rewrite <- H1.
 Qed.
 
 Declare Left Step NZE_stepl.
-(* The right step lemma is just the transitivity of NZE *)
+(* The right step lemma is just the transitivity of NZeq *)
 Declare Right Step (proj1 (proj2 NZE_equiv)).
 
 Theorem NZsucc_inj : forall n1 n2 : NZ, S n1 == S n2 -> n1 == n2.
@@ -48,9 +48,9 @@ declaration of the morphism below because the "predicate NZ" is not
 recognized as a type of function. Maybe it should do "eval hnf" or
 something like this. The same goes for "relation". *)
 
-Hypothesis A_wd : predicate_wd NZE A.
+Hypothesis A_wd : predicate_wd NZeq A.
 
-Add Morphism A with signature NZE ==> iff as A_morph.
+Add Morphism A with signature NZeq ==> iff as A_morph.
 Proof A_wd.
 
 Theorem NZcentral_induction :
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index cb3dd3093..f4c39934f 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -347,9 +347,9 @@ in the induction step *)
 Section Induction.
 
 Variable A : NZ -> Prop.
-Hypothesis A_wd : predicate_wd NZE A.
+Hypothesis A_wd : predicate_wd NZeq A.
 
-Add Morphism A with signature NZE ==> iff as A_morph.
+Add Morphism A with signature NZeq ==> iff as A_morph.
 Proof A_wd.
 
 Section Center.
@@ -532,12 +532,12 @@ Variable z : NZ.
 
 Let R (n m : NZ) := z <= n /\ n < m.
 
-Add Morphism R with signature NZE ==> NZE ==> iff as R_wd.
+Add Morphism R with signature NZeq ==> NZeq ==> iff as R_wd.
 Proof.
 intros x1 x2 H1 x3 x4 H2; unfold R; rewrite H1; now rewrite H2.
 Qed.
 
-Lemma NZAcc_lt_wd : predicate_wd NZE (Acc R).
+Lemma NZAcc_lt_wd : predicate_wd NZeq (Acc R).
 Proof.
 unfold predicate_wd, fun_wd.
 intros x1 x2 H; split; intro H1; destruct H1 as [H2];