An update on axiomatization of numbers.

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

3 files changed, 153 insertions, 10 deletions

diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
index fb4b137d6..5f592dbcb 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
@@ -1,4 +1,3 @@
-Require Export NMinus.
 Require Export NTimesOrder.
 Require Export ZTimesOrder.
 
@@ -51,6 +50,13 @@ Add Relation Z E
  transitivity proved by (proj1 (proj2 E_equiv))                                                  
 as E_rel.
 
+Add Morphism (@pair N N)
+  with signature NDomainModule.E ==> NDomainModule.E ==> E
+  as pair_wd.
+Proof.
+intros x1 x2 H1 y1 y2 H2; unfold E; simpl; rewrite H1; now rewrite H2.
+Qed.
+
 End NatPairsDomain.
 
 Module NatPairsInt (Import NPlusModule : NPlusSignature) <: IntSignature.
@@ -93,16 +99,34 @@ 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 *.
-
+Section Induction.
+Open Scope NatScope. (* automatically closes at the end of the section *)
+Variable Q : Z -> Prop.
+Hypothesis Q_wd : pred_wd E Q.
 
+Add Morphism Q with signature E ==> iff as Q_morph.
+Proof.
+exact Q_wd.
+Qed.
 
+Theorem induction :
+  Q 0 -> (forall x, Q x -> Q (S x)) -> (forall x, Q x -> Q (P x)) -> forall x, Q x.
+Proof.
+intros Q0 QS QP x; unfold O, S, P, pred_wd, E in *.
+destruct x as [n m].
+cut (forall p : N, Q (p, 0)); [intro H1 |].
+cut (forall p : N, Q (0, p)); [intro H2 |].
+destruct (plus_dichotomy n m) as [[p H] | [p H]].
+rewrite (Q_wd (n, m) (0, p)); simpl. rewrite plus_0_l; now rewrite plus_comm. apply H2.
+rewrite (Q_wd (n, m) (p, 0)); simpl. now rewrite plus_0_r. apply H1.
+induct p. assumption. intros p IH.
+replace 0 with (fst (0, p)); [| reflexivity].
+replace p with (snd (0, p)); [| reflexivity]. now apply QP.
+induct p. assumption. intros p IH.
+replace 0 with (snd (p, 0)); [| reflexivity].
+replace p with (fst (p, 0)); [| reflexivity]. now apply QS.
+Qed.
 
-Definition N_Z (n : nat) := nat_rec (fun _ : nat => Z) 0 (fun _ p => S p).
+End Induction.
 
+End NatPairsInt.
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
new file mode 100644
index 000000000..b69e4ce7d
--- /dev/null
+++ b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
@@ -0,0 +1,82 @@
+Require Export NTimesOrder.
+Require Export ZTimesOrder.
+Require Import ZPairsAxioms.
+
+Module NatPairsPlus (Import NPlusModule : NPlusSignature) <: ZPlusSignature.
+Module Export IntModule := NatPairsInt NPlusModule.
+Open Local Scope NatScope.
+
+Definition plus (x y : Z) := ((fst x) + (fst y), (snd x) + (snd y)).
+Definition minus (x y : Z) := ((fst x) + (snd y), (snd x) + (fst y)).
+Definition uminus (x : Z) := (snd x, fst x).
+(* Unfortunately, the elements of pair keep increasing, even during subtraction *)
+
+Notation "x + y" := (plus x y) : IntScope.
+Notation "x - y" := (minus x y) : IntScope.
+Notation "- x" := (uminus x) : IntScope.
+
+(* Below, we need to rewrite subtems that have several occurrences.
+Since with the currect setoid_rewrite we cannot point an accurrence
+using pattern, we use symmetry tactic to make a particular occurrence
+the leftmost, since that is what rewrite will use. *)
+Add Morphism plus with signature E ==> E ==> E as plus_wd.
+Proof.
+unfold E, plus; intros x1 y1 H1 x2 y2 H2; simpl.
+pose proof (plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1
+                    (fst x2 + snd y2) (fst y2 + snd x2) H2) as H.
+rewrite plus_shuffle1. symmetry. now rewrite plus_shuffle1.
+Qed.
+
+Add Morphism minus with signature E ==> E ==> E as minus_wd.
+Proof.
+unfold E, plus; intros x1 y1 H1 x2 y2 H2; simpl.
+rewrite plus_comm in H2. symmetry in H2; rewrite plus_comm in H2.
+pose proof (NPlusModule.plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1
+                                (snd x2 + fst y2) (snd y2 + fst x2) H2) as H.
+rewrite plus_shuffle1. symmetry. now rewrite plus_shuffle1.
+Qed.
+
+Add Morphism uminus with signature E ==> E as uminus_wd.
+Proof.
+unfold E, plus; intros x y H; simpl.
+rewrite plus_comm. symmetry. now rewrite plus_comm.
+Qed.
+
+Open Local Scope IntScope.
+
+Theorem plus_0 : forall n, 0 + n == n.
+Proof.
+intro n; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_0_n.
+Qed.
+
+Theorem plus_S : forall n m, (S n) + m == S (n + m).
+Proof.
+intros n m; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_Sn_m.
+Qed.
+
+Theorem minus_0 : forall n, n - 0 == n.
+Proof.
+intro n; unfold minus, E; simpl. now do 2 rewrite plus_0_r.
+Qed.
+
+Theorem minus_S : forall n m, n - (S m) == P (n - m).
+Proof.
+intros n m; unfold minus, E; simpl. symmetry; now rewrite plus_n_Sm.
+Qed.
+
+Theorem uminus_0 : - 0 == 0.
+Proof.
+unfold uminus, E; simpl. now rewrite plus_0_n.
+Qed.
+
+Theorem uminus_S : forall n, - (S n) == P (- n).
+Proof.
+reflexivity.
+Qed.
+
+End NatPairsPlus.
+
+Module NatPairsPlusProperties (NPlusModule : NPlusSignature).
+Module NatPairsPlusModule := NatPairsPlus NPlusModule.
+Module Export NatPairsPlusPropertiesModule := ZPlusProperties NatPairsPlusModule.
+End NatPairsPlusProperties.
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
new file mode 100644
index 000000000..f5706276c
--- /dev/null
+++ b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
@@ -0,0 +1,37 @@
+Require Export ZPairsPlus.
+
+Module NatPairsTimes (Import NTimesModule : NTimesSignature) <: ZTimesSignature.
+Module Import ZPlusModule := NatPairsPlus NTimesModule.NPlusModule. (* "NTimesModule." is optional *)
+Open Local Scope NatScope.
+
+Definition times (n m : Z) :=
+(*  let (n1, n2) := n in
+  let (m1, m2) := m in (n1 * m1 + n2 * m2, n1 * m2 + n2 * m1).*)
+  ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)).
+
+Notation "x * y" := (times x y) : IntScope.
+
+Add Morphism times with signature E ==> E ==> E as times_wd.
+Proof.
+unfold times, E; intros x1 y1 H1 x2 y2 H2; simpl.
+assert ((fst x1) + (fst y1) == (fst y1) + (fst x1)).
+ring.
+
+
+Axiom times_0 : forall n, n * 0 == 0.
+Axiom times_S : forall n m, n * (S m) == n * m + n.
+
+(* Here recursion is done on the second argument to conform to the
+usual definition of ordinal multiplication in set theory, which is not
+commutative. It seems, however, that this definition in set theory is
+unfortunate for two reasons. First, multiplication of two ordinals A
+and B can be defined as (an order type of) the cartesian product B x A
+(not A x B) ordered lexicographically. For example, omega * 2 =
+2 x omega = {(0,0) < (0,1) < (0,2) < ... < (1,0) < (1,1) < (1,2) < ...},
+while 2 * omega = omega x 2 = {(0,0) < (0,1) < (1,0) < (1,1) < (2,0) <
+(2,1) < ...} = omega. Secondly, the way the product 2 * 3 is said in
+French (deux fois trois) and Russian (dvazhdy tri) implies 3 + 3, not
+2 + 2 + 2. So it would possibly be more reasonable to define multiplication
+(here as well as in set theory) by recursion on the first argument. *)
+
+End ZTimesSignature.