An update on axiomatic number classes.

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

6 files changed, 197 insertions, 62 deletions

diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Axioms/ZDomain.v
index 87c99066d0..579f8facef 100644
--- a/theories/Numbers/Integer/Axioms/ZDomain.v
+++ b/theories/Numbers/Integer/Axioms/ZDomain.v
@@ -2,9 +2,9 @@ Require Export NumPrelude.
 
 Module Type ZDomainSignature.
 
-Parameter Z : Set.
-Parameter E : relation Z.
-Parameter e : Z -> Z -> bool.
+Parameter Inline Z : Set.
+Parameter Inline E : Z -> Z -> Prop.
+Parameter Inline e : Z -> Z -> bool.
 
 Axiom E_equiv_e : forall x y : Z, E x y <-> e x y.
 Axiom E_equiv : equiv Z E.
@@ -42,4 +42,14 @@ Proof.
 intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
 Qed.
 
+Theorem ZE_stepl : forall x y z : Z, x == y -> x == z -> z == y.
+Proof.
+intros x y z H1 H2; now rewrite <- H1.
+Qed.
+
+Declare Left Step ZE_stepl.
+
+(* The right step lemma is just transitivity of E *)
+Declare Right Step (proj1 (proj2 E_equiv)).
+
 End ZDomainProperties.
diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v
index 7d4329a963..5dc0b7505a 100644
--- a/theories/Numbers/Integer/Axioms/ZTimes.v
+++ b/theories/Numbers/Integer/Axioms/ZTimes.v
@@ -13,19 +13,6 @@ Add Morphism times with signature E ==> E ==> E as times_wd.
 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.
 
 Module ZTimesProperties (Import ZTimesModule : ZTimesSignature).
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
index 5f592dbcb9..683b86ec6e 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v
@@ -1,5 +1,5 @@
-Require Export NTimesOrder.
-Require Export ZTimesOrder.
+Require Import NPlus.
+Require Export ZAxioms.
 
 Module NatPairsDomain (Import NPlusModule : NPlusSignature) <: ZDomainSignature.
 (*  with Definition Z :=
@@ -11,7 +11,7 @@ Module NatPairsDomain (Import NPlusModule : NPlusSignature) <: ZDomainSignature.
     fun p1 p2  =>
       NPM.NatModule.DomainModule.e (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)).*)
 
-Module Export NPlusPropertiesModule := NPlusProperties NPlusModule.
+Module Export NPlusPropertiesModule := NPlusProperties NatModule NPlusModule.
 Open Local Scope NatScope.
 
 Definition Z : Set := (N * N)%type.
@@ -28,26 +28,35 @@ Proof.
 intros x y; unfold E, e; apply E_equiv_e.
 Qed.
 
-Theorem E_equiv : equiv Z E.
+Theorem ZE_refl : reflexive Z E.
+Proof.
+unfold reflexive, E; reflexivity.
+Qed.
+
+Theorem ZE_symm : symmetric Z E.
 Proof.
-split; [| split]; unfold reflexive, symmetric, transitive, E.
-(* reflexivity *)
-now intro.
-(* transitivity *)
-intros x y z H1 H2.
+unfold symmetric, E; now symmetry.
+Qed.
+
+Theorem ZE_trans : transitive Z E.
+Proof.
+unfold transitive, E. intros x y z H1 H2.
 apply plus_cancel_l with (p := fst y + snd y).
 rewrite (plus_shuffle2 (fst y) (snd y) (fst x) (snd z)).
 rewrite (plus_shuffle2 (fst y) (snd y) (fst z) (snd x)).
 rewrite plus_comm. rewrite (plus_comm (snd y) (fst x)).
 rewrite (plus_comm (snd y) (fst z)). now apply plus_wd.
-(* symmetry *)
-now intros.
 Qed.
 
-Add Relation Z E                                                                                 
- reflexivity proved by (proj1 E_equiv)                                                           
- symmetry proved by (proj2 (proj2 E_equiv))                                                      
- transitivity proved by (proj1 (proj2 E_equiv))                                                  
+Theorem E_equiv : equiv Z E.
+Proof.
+unfold equiv; split; [apply ZE_refl | split; [apply ZE_trans | apply ZE_symm]].
+Qed.
+
+Add Relation Z E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
 as E_rel.
 
 Add Morphism (@pair N N)
@@ -78,25 +87,25 @@ Notation "0" := O : IntScope.
 Add Morphism S with signature E ==> E as S_wd.
 Proof.
 unfold S, E; intros n m H; simpl.
-do 2 rewrite plus_Sn_m; now rewrite H.
+do 2 rewrite plus_S_l; now rewrite H.
 Qed.
 
 Add Morphism P with signature E ==> E as P_wd.
 Proof.
 unfold P, E; intros n m H; simpl.
-do 2 rewrite plus_n_Sm; now rewrite H.
+do 2 rewrite plus_S_r; 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.
+do 2 rewrite plus_S_l 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.
+rewrite plus_S_l; now rewrite plus_S_r.
 Qed.
 
 Section Induction.
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
new file mode 100644
index 0000000000..29181e0c69
--- /dev/null
+++ b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
@@ -0,0 +1,111 @@
+Require Import NPlusOrder.
+Require Export ZPlusOrder.
+Require Export ZPairsPlus.
+
+Module NatPairsOrder (Import NPlusModule : NPlusSignature)
+                     (Import NOrderModule : NOrderSignature
+                        with Module NatModule := NPlusModule.NatModule) <: ZOrderSignature.
+Module Import NPlusOrderPropertiesModule :=
+  NPlusOrderProperties NPlusModule NOrderModule.
+Module Export IntModule := NatPairsInt NPlusModule.
+Open Local Scope NatScope.
+
+Definition lt (p1 p2 : Z) := (fst p1) + (snd p2) < (fst p2) + (snd p1).
+Definition le (p1 p2 : Z) := (fst p1) + (snd p2) <= (fst p2) + (snd p1).
+
+Notation "x < y" := (lt x y) : IntScope.
+Notation "x <= y" := (le x y) : IntScope.
+
+Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd.
+Proof.
+unfold lt, E; intros x1 y1 H1 x2 y2 H2; simpl.
+rewrite eq_true_iff; split; intro H.
+stepr (snd y1 + fst y2) by apply plus_comm.
+apply (plus_lt_repl_pair (fst x1) (snd x1)); [| assumption].
+stepl (snd y2 + fst x1) by apply plus_comm.
+stepr (fst y2 + snd x1) by apply plus_comm.
+apply (plus_lt_repl_pair (snd x2) (fst x2)).
+now stepl (fst x1 + snd x2) by apply plus_comm.
+stepl (fst y2 + snd x2) by apply plus_comm. now stepr (fst x2 + snd y2) by apply plus_comm.
+stepr (snd x1 + fst x2) by apply plus_comm.
+apply (plus_lt_repl_pair (fst y1) (snd y1)); [| now symmetry].
+stepl (snd x2 + fst y1) by apply plus_comm.
+stepr (fst x2 + snd y1) by apply plus_comm.
+apply (plus_lt_repl_pair (snd y2) (fst y2)).
+now stepl (fst y1 + snd y2) by apply plus_comm.
+stepl (fst x2 + snd y2) by apply plus_comm. now stepr (fst y2 + snd x2) by apply plus_comm.
+Qed.
+
+(* Below is a very long explanation why it would be useful to be
+able to use the fold tactic in hypotheses.
+We will prove the following statement not from scratch, like lt_wd,
+but expanding <= to < and == and then using lt_wd. The theorem we need
+to prove is (x1 <= x2) = (y1 <= y2) for all x1 == y1 and x2 == y2 : Z.
+To be able to express <= through < and ==, we need to expand <=%Int to
+<=%Nat, since we have not proved yet the properties of <=%Int. But
+then it would be convenient to fold back equalities from
+(fst x1 + snd x2 == fst x2 + snd x1)%Nat to (x1 == x2)%Int.
+The reason is that we will need to show that (x1 == x2)%Int <->
+(y1 == y2)%Int from (x1 == x2)%Int and (y1 == y2)%Int. If we fold
+equalities back to Int, then we could do simple rewriting, since we have
+already showed that ==%Int is an equivalence relation. On the other hand,
+if we leave equalities expanded to Nat, we will have to apply the
+transitivity of ==%Int by hand. *)
+
+Add Morphism le with signature E ==> E ==> eq_bool as le_wd.
+Proof.
+unfold le, E; intros x1 y1 H1 x2 y2 H2; simpl.
+rewrite eq_true_iff. do 2 rewrite le_lt.
+pose proof (lt_wd x1 y1 H1 x2 y2 H2) as H; unfold lt in H; rewrite H; clear H.
+(* This is a remark about an extra level of definitions created by
+"with Module NatModule := NPlusModule.NatModule" constraint in the beginning
+of this functor. We cannot just say "fold (x1 == x2)%Int" because it turns out
+that it expand to (NPlusModule.NatModule.NDomainModule.E ... ...), since
+NPlusModule was imported first. On the other hand, the goal uses
+NOrderModule.NatModule.NDomainModule.E, or just NDomainModule.E, since le_lt
+theorem was proved in NOrderDomain module. (E without qualifiers refers to
+ZDomainModule.E.) Therefore, we issue the "replace" command. It would be nicer,
+though, if the constraint "with Module NatModule := NPlusModule.NatModule" in the
+declaration of this functor would not create an extra level of definitions
+and there would be only one NDomainModule.E. *)
+replace NDomainModule.E with NPlusModule.NatModule.NDomainModule.E by reflexivity.
+fold (x1 == x2)%Int. fold (y1 == y2)%Int.
+assert (H1' : (x1 == y1)%Int); [exact H1 |].
+(* We do this instead of "fold (x1 == y1)%Int in H1" *)
+assert (H2' : (x2 == y2)%Int); [exact H2 |].
+rewrite H1'; rewrite H2'. reflexivity.
+Qed.
+
+Open Local Scope IntScope.
+
+Theorem le_lt : forall n m : Z, n <= m <-> n < m \/ n == m.
+Proof.
+intros n m; unfold lt, le, E; simpl. apply le_lt. (* refers to NOrderModule.le_lt *)
+Qed.
+
+Theorem lt_irr : forall n : Z, ~ (n < n).
+Proof.
+intros n; unfold lt, E; simpl. apply lt_irr.
+(* refers to NPlusOrderPropertiesModule.NOrderPropertiesModule.lt_irr *)
+Qed.
+
+Theorem lt_S : forall n m, n < (S m) <-> n <= m.
+Proof.
+intros n m; unfold lt, le, E; simpl. rewrite plus_S_l; apply lt_S.
+Qed.
+
+End NatPairsOrder.
+
+(* Since to define the order on integers we need both plus and order
+on natural numbers, we can export the properties of plus and order together *)
+(*Module NatPairsPlusOrderProperties (NPlusModule : NPlusSignature)
+                                   (NOrderModule : NOrderSignature
+                                     with Module NatModule := NPlusModule.NatModule).
+Module Export NatPairsPlusModule := NatPairsPlus NPlusModule.
+Module Export NatPairsOrderModule := NatPairsOrder NPlusModule NOrderModule.
+Module Export NatPairsPlusOrderPropertiesModule :=
+  ZPlusOrderProperties NatPairsPlusModule NatPairsOrderModule.
+End NatPairsPlusOrderProperties.*)
+(* We cannot prove to Coq that NatPairsPlusModule.IntModule and
+NatPairsOrderModule.IntModule are the same *)
+
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
index b69e4ce7d2..d180762659 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
@@ -1,6 +1,6 @@
-Require Export NTimesOrder.
-Require Export ZTimesOrder.
-Require Import ZPairsAxioms.
+Require Import NPlus.
+Require Export ZPlus.
+Require Export ZPairsAxioms.
 
 Module NatPairsPlus (Import NPlusModule : NPlusSignature) <: ZPlusSignature.
 Module Export IntModule := NatPairsInt NPlusModule.
@@ -46,12 +46,12 @@ 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.
+intro n; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_0_l.
 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.
+intros n m; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_S_l.
 Qed.
 
 Theorem minus_0 : forall n, n - 0 == n.
@@ -61,12 +61,12 @@ 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.
+intros n m; unfold minus, E; simpl. symmetry; now rewrite plus_S_r.
 Qed.
 
 Theorem uminus_0 : - 0 == 0.
 Proof.
-unfold uminus, E; simpl. now rewrite plus_0_n.
+unfold uminus, E; simpl. now rewrite plus_0_l.
 Qed.
 
 Theorem uminus_S : forall n, - (S n) == P (- n).
@@ -77,6 +77,6 @@ Qed.
 End NatPairsPlus.
 
 Module NatPairsPlusProperties (NPlusModule : NPlusSignature).
-Module NatPairsPlusModule := NatPairsPlus NPlusModule.
+Module Export 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
index f5706276c9..b72847c089 100644
--- a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
+++ b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
@@ -1,12 +1,14 @@
+Require Import Ring.
+Require Import NTimes.
+Require Export ZTimes.
 Require Export ZPairsPlus.
 
 Module NatPairsTimes (Import NTimesModule : NTimesSignature) <: ZTimesSignature.
-Module Import ZPlusModule := NatPairsPlus NTimesModule.NPlusModule. (* "NTimesModule." is optional *)
+Module Export ZPlusModule := NatPairsPlus NTimesModule.NPlusModule. (* "NTimesModule." is optional *)
+Module Import NTimesPropertiesModule := NTimesProperties NTimesModule.
 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.
@@ -14,24 +16,40 @@ 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)).
+stepl_ring (fst x1 * fst x2 + (snd x1 * snd x2 + fst y1 * snd y2 + snd y1 * fst y2)).
+stepr_ring (fst x1 * snd x2 + (fst y1 * fst y2 + snd y1 * snd y2 + snd x1 * fst x2)).
+apply plus_times_repl_pair with (n := fst y2) (m := snd y2); [| now idtac].
+stepl_ring (snd x1 * snd x2 + (fst x1 * fst y2 + fst y1 * snd y2 + snd y1 * fst y2)).
+stepr_ring (snd x1 * fst x2 + (fst x1 * snd y2 + fst y1 * fst y2 + snd y1 * snd y2)).
+apply plus_times_repl_pair with (n := snd y2) (m := fst y2);
+  [| rewrite plus_comm; symmetry; now rewrite plus_comm].
+stepl_ring (snd y2 * snd x1 + (fst x1 * fst y2 + fst y1 * snd y2 + snd y1 * fst y2)).
+stepr_ring (snd y2 * fst x1 + (snd x1 * fst y2 + fst y1 * fst y2 + snd y1 * snd y2)).
+apply plus_times_repl_pair with (n := snd y1) (m := fst y1);
+  [| rewrite plus_comm; symmetry; now rewrite plus_comm].
+stepl_ring (fst y2 * fst x1 + (snd y2 * snd y1 + fst y1 * snd y2 + snd y1 * fst y2)).
+stepr_ring (fst y2 * snd x1 + (snd y2 * fst y1 + fst y1 * fst y2 + snd y1 * snd y2)).
+apply plus_times_repl_pair with (n := fst y1) (m := snd y1); [| now idtac].
 ring.
+Qed.
 
+Open Local Scope IntScope.
 
-Axiom times_0 : forall n, n * 0 == 0.
-Axiom times_S : forall n m, n * (S m) == n * m + n.
+Theorem times_0 : forall n, n * 0 == 0.
+Proof.
+intro n; unfold times, E; simpl.
+repeat rewrite times_0_r. now rewrite plus_assoc.
+Qed.
+
+Theorem times_S : forall n m, n * (S m) == n * m + n.
+Proof.
+intros n m; unfold times, S, E; simpl.
+do 2 rewrite times_S_r. ring.
+Qed.
 
-(* 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 NatPairsTimes.
 
-End ZTimesSignature.
+Module NatPairsTimesProperties (NTimesModule : NTimesSignature).
+Module Export NatPairsTimesModule := NatPairsTimes NTimesModule.
+Module Export NatPairsTimesPropertiesModule := ZTimesProperties NatPairsTimesModule.
+End NatPairsTimesProperties.