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.
-