An update on axiomatization of number classes.

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

1 files changed, 44 insertions, 13 deletions

diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 2ca4bc5d86..fb4b137d63 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -1,18 +1,28 @@
-Require Export NTimesLt.
+Require Export NMinus.
+Require Export NTimesOrder.
 Require Export ZTimesOrder.
 
-Module NatPairsDomain (Export NPlusModule : NPlus.PlusSignature) :
-  ZDomain.DomainSignature
-  with Definition Z := (N * N)%type.
-  with Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1))%Nat.
-  with Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1))%Nat.
+Module NatPairsDomain (Import NPlusModule : NPlusSignature) <: ZDomainSignature.
+(*  with Definition Z :=
+    (NPM.NatModule.DomainModule.N * NPM.NatModule.DomainModule.N)%type
+  with Definition E :=
+    fun p1 p2  =>
+      NPM.NatModule.DomainModule.E (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1))
+  with Definition e :=
+    fun p1 p2  =>
+      NPM.NatModule.DomainModule.e (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)).*)
 
-Module Export NPlusPropertiesModule := NPlus.PlusProperties NPlusModule.
+Module Export NPlusPropertiesModule := NPlusProperties NPlusModule.
+Open Local Scope NatScope.
 
 Definition Z : Set := (N * N)%type.
+Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)).
+Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1)).
 
-Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1))%Nat.
-Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1))%Nat.
+Delimit Scope IntScope with Int.
+Bind Scope IntScope with Z.
+Notation "x == y" := (E x y) (at level 70) : IntScope.
+Notation "x # y" := (~ E x y) (at level 70) : IntScope.
 
 Theorem E_equiv_e : forall x y : Z, E x y <-> e x y.
 Proof.
@@ -43,12 +53,12 @@ as E_rel.
 
 End NatPairsDomain.
 
-
-Module NatPairsInt (Export NPlusModule : NPlus.PlusSignature) <: IntSignature.
-
+Module NatPairsInt (Import NPlusModule : NPlusSignature) <: IntSignature.
 Module Export ZDomainModule := NatPairsDomain NPlusModule.
+Module Export ZDomainModuleProperties := ZDomainProperties ZDomainModule.
+Open Local Scope IntScope.
 
-Definition O := (0, 0).
+Definition O : Z := (0, 0)%Nat.
 Definition S (n : Z) := (NatModule.S (fst n), snd n).
 Definition P (n : Z) := (fst n, NatModule.S (snd n)).
 (* Unfortunately, we do not have P (S n) = n but only P (S n) == n.
@@ -57,6 +67,8 @@ the elements is 0, and make all operations convert canonical values into
 other canonical values. We do not do this because this is more complex
 and because we do not have the predecessor function on N at this point. *)
 
+Notation "0" := O : IntScope.
+
 Add Morphism S with signature E ==> E as S_wd.
 Proof.
 unfold S, E; intros n m H; simpl.
@@ -70,6 +82,25 @@ do 2 rewrite plus_n_Sm; now rewrite H.
 Qed.
 
 Theorem S_inj : forall x y : Z, S x == S y -> x == y.
+Proof.
+unfold S, E; simpl; intros x y H.
+do 2 rewrite plus_Sn_m in H. now apply S_inj in H.
+Qed.
+
+Theorem S_P : forall x : Z, S (P x) == x.
+Proof.
+intro x; unfold S, P, E; simpl.
+rewrite plus_Sn_m; now rewrite plus_n_Sm.
+Qed.
+
+Theorem induction :
+  forall Q : Z -> Prop,
+    NumPrelude.pred_wd E Q -> Q 0 ->
+    (forall x, Q x -> Q (S x)) ->
+    (forall x, Q x -> Q (P x)) -> forall x, Q x.
+Proof.
+intros Q Q_wd Q0 QS QP x; unfold O, S, P in *.
+