Added the proof (in Numbers/Integers/TreeMod) that tree-like representation of integers due to Gregoire and Théry satisfies the axioms of integers without order. This refers to integers modulo n, i.e., those that fit trees of certain size, not to BigZ.

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

4 files changed, 0 insertions, 252 deletions

diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 41fc7e75ee..5c8b5890d5 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -25,7 +25,6 @@ In that case, we could get rid of setoids as well as arrive at integers as
 signed natural numbers. *)
 Definition NZplus (n m : Z) := ((fst n) + (fst m), (snd n) + (snd m)).
 Definition NZminus (n m : Z) := ((fst n) + (snd m), (snd n) + (fst m)).
-Definition NZuminus (n : Z) := (snd n, fst n).
 (* Unfortunately, the elements of the pair keep increasing, even during
 subtraction *)
 Definition NZtimes (n m : Z) :=
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
deleted file mode 100644
index dc258f873f..0000000000
--- a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v
+++ /dev/null
@@ -1,112 +0,0 @@
-Require Import NPlusOrder.
-Require Export ZPlusOrder.
-Require Export ZPairsPlus.
-
-Module NatPairsOrder (Import NPlusMod : NPlusSig)
-                     (Import NOrderModule : NOrderSig
-                        with Module NBaseMod := NPlusMod.NBaseMod) <: ZOrderSignature.
-Module Import NPlusOrderPropertiesModule :=
-  NPlusOrderProperties NPlusMod NOrderModule.
-Module Export ZBaseMod := NatPairsInt NPlusMod.
-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 NBaseMod := NPlusMod.NBaseMod" constraint in the beginning
-of this functor. We cannot just say "fold (x1 == x2)%Int" because it turns out
-that it expand to (NPlusMod.NBaseMod.NDomainModule.E ... ...), since
-NPlusMod was imported first. On the other hand, the goal uses
-NOrderModule.NBaseMod.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 NBaseMod := NPlusMod.NBaseMod" 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 NPlusMod.NBaseMod.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.NOrderPropFunctModule.lt_irr *)
-Qed.
-
-Theorem lt_succ : forall n m, n < (S m) <-> n <= m.
-Proof.
-intros n m; unfold lt, le, E; simpl. rewrite plus_succ_l; apply lt_succ.
-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 (NPlusMod : NPlusSig)
-                                   (NOrderModule : NOrderSig
-                                     with Module NBaseMod := NPlusMod.NBaseMod).
-Module Export NatPairsPlusModule := NatPairsPlus NPlusMod.
-Module Export NatPairsOrderModule := NatPairsOrder NPlusMod NOrderModule.
-Module Export NatPairsPlusOrderPropertiesModule :=
-  ZPlusOrderProperties NatPairsPlusModule NatPairsOrderModule.
-End NatPairsPlusOrderProperties.*)
-(* We cannot prove to Coq that NatPairsPlusModule.ZBaseMod and
-NatPairsOrderModule.ZBaseMod are the same *)
-
-
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
deleted file mode 100644
index 2e658c181f..0000000000
--- a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v
+++ /dev/null
@@ -1,83 +0,0 @@
-Require Import NPlus.
-Require Export ZPlus.
-Require Export ZPairsAxioms.
-
-Module NatPairsPlus (Import NPlusMod : NPlusSig) <: ZPlusSignature.
-Module Export ZBaseMod := NatPairsInt NPlusMod.
-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 (NPlusMod.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 NPlusMod.plus_0_l.
-Qed.
-
-Theorem plus_succ : forall n m, (S n) + m == S (n + m).
-Proof.
-intros n m; unfold plus, E; simpl. now do 2 rewrite NPlusMod.plus_succ_l.
-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_succ : forall n m, n - (S m) == P (n - m).
-Proof.
-intros n m; unfold minus, E; simpl. symmetry; now rewrite plus_succ_r.
-Qed.
-
-Theorem uminus_0 : - 0 == 0.
-Proof.
-unfold uminus, E; simpl. now rewrite plus_0_l.
-Qed.
-
-Theorem uminus_succ : forall n, - (S n) == P (- n).
-Proof.
-reflexivity.
-Qed.
-
-End NatPairsPlus.
-
-Module NatPairsPlusProperties (NPlusMod : NPlusSig).
-Module Export NatPairsPlusModule := NatPairsPlus NPlusMod.
-Module Export NatPairsPlusPropertiesModule := ZPlusProperties NatPairsPlusModule.
-End NatPairsPlusProperties.
-
diff --git a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
deleted file mode 100644
index 553c6df22f..0000000000
--- a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v
+++ /dev/null
@@ -1,56 +0,0 @@
-Require Import Ring.
-Require Import NTimes.
-Require Export ZTimes.
-Require Export ZPairsPlus.
-
-Module NatPairsTimes (Import NTimesMod : NTimesSig) <: ZTimesSignature.
-Module Export ZPlusModule := NatPairsPlus NTimesMod.NPlusMod. (* "NTimesMod." is optional *)
-Module Import NTimesPropertiesModule := NTimesPropFunct NTimesMod.
-Open Local Scope NatScope.
-
-Definition times (n m : Z) :=
-  ((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.
-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.
-
-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_succ : forall n m, n * (S m) == n * m + n.
-Proof.
-intros n m; unfold times, S, E; simpl.
-do 2 rewrite times_succ_r. ring.
-Qed.
-
-End NatPairsTimes.
-
-Module NatPairsTimesProperties (NTimesMod : NTimesSig).
-Module Export NatPairsTimesModule := NatPairsTimes NTimesMod.
-Module Export NatPairsTimesPropertiesModule := ZTimesProperties NatPairsTimesModule.
-End NatPairsTimesProperties.
-