Update of theories/Numbers directory.

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

21 files changed, 74 insertions, 161 deletions

diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v
index b73410256..05b8ede94 100644
--- a/theories/Numbers/Integer/Axioms/ZAxioms.v
+++ b/theories/Numbers/Integer/Axioms/ZAxioms.v
@@ -1,5 +1,4 @@
-Require Import NumPrelude.
-Require Import ZDomain.
+Require Export ZDomain.
 
 Module Type IntSignature.
 Declare Module Export DomainModule : DomainSignature.
@@ -25,7 +24,6 @@ Axiom induction :
 
 End IntSignature.
 
-
 Module IntProperties (Export IntModule : IntSignature).
 Module Export DomainPropertiesModule := DomainProperties DomainModule.
 Open Local Scope ZScope.
diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Axioms/ZDomain.v
index b48684ba8..1a29eddf2 100644
--- a/theories/Numbers/Integer/Axioms/ZDomain.v
+++ b/theories/Numbers/Integer/Axioms/ZDomain.v
@@ -1,4 +1,4 @@
-Require Import NumPrelude.
+Require Export NumPrelude.
 
 Module Type DomainSignature.
 
diff --git a/theories/Numbers/Integer/Axioms/ZOrder.v b/theories/Numbers/Integer/Axioms/ZOrder.v
index 3bf4d61f5..803bfe43b 100644
--- a/theories/Numbers/Integer/Axioms/ZOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZOrder.v
@@ -1,6 +1,4 @@
-Require Import NumPrelude.
-Require Import ZDomain.
-Require Import ZAxioms.
+Require Export ZAxioms.
 
 Module Type OrderSignature.
 Declare Module Export IntModule : IntSignature.
diff --git a/theories/Numbers/Integer/Axioms/ZPlus.v b/theories/Numbers/Integer/Axioms/ZPlus.v
index f455400b7..484607094 100644
--- a/theories/Numbers/Integer/Axioms/ZPlus.v
+++ b/theories/Numbers/Integer/Axioms/ZPlus.v
@@ -1,6 +1,4 @@
-Require Import NumPrelude.
-Require Import ZDomain.
-Require Import ZAxioms.
+Require Export ZAxioms.
 
 Module Type PlusSignature.
 Declare Module Export IntModule : IntSignature.
diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Axioms/ZPlusOrder.v
index 4f677355b..dd311b49a 100644
--- a/theories/Numbers/Integer/Axioms/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZPlusOrder.v
@@ -1,8 +1,8 @@
-Require Import ZOrder.
-Require Import ZPlus.
+Require Export ZOrder.
+Require Export ZPlus.
 
-Module PlusOrderProperties (Export PlusModule : PlusSignature)
-                           (Export OrderModule : OrderSignature with
+Module PlusOrderProperties (PlusModule : PlusSignature)
+                           (OrderModule : OrderSignature with
                              Module IntModule := PlusModule.IntModule).
 (* Warning: Notation _ == _ was already used in scope ZScope !!! *)
 Module Export PlusPropertiesModule := PlusProperties PlusModule.
diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v
index ff0de6196..052dcf66f 100644
--- a/theories/Numbers/Integer/Axioms/ZTimes.v
+++ b/theories/Numbers/Integer/Axioms/ZTimes.v
@@ -1,7 +1,4 @@
-Require Import NumPrelude.
-Require Import ZDomain.
-Require Import ZAxioms.
-Require Import ZPlus.
+Require Export ZPlus.
 
 Module Type TimesSignature.
 Declare Module Export PlusModule : PlusSignature.
diff --git a/theories/Numbers/Integer/Axioms/ZTimesOrder.v b/theories/Numbers/Integer/Axioms/ZTimesOrder.v
index 460a13bf4..a72636a42 100644
--- a/theories/Numbers/Integer/Axioms/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Axioms/ZTimesOrder.v
@@ -1,12 +1,9 @@
-Require Import ZPlus.
-Require Import ZTimes.
-Require Import ZOrder.
-Require Import ZPlusOrder.
+Require Export ZTimes.
+Require Export ZPlusOrder.
 
-Module TimesOrderProperties (Export TimesModule : TimesSignature)
-                            (Export OrderModule : OrderSignature with
+Module TimesOrderProperties (TimesModule : TimesSignature)
+                            (OrderModule : OrderSignature with
                               Module IntModule := TimesModule.PlusModule.IntModule).
-
 Module Export TimesPropertiesModule := TimesProperties TimesModule.
 Module Export PlusOrderPropertiesModule :=
   PlusOrderProperties TimesModule.PlusModule OrderModule.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 02f73f4d1..2ca4bc5d8 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -1,21 +1,12 @@
-Require Import NDomain.
-Require Import NAxioms.
-Require Import NPlus.
-Require Import NTimes.
-Require Import NLt.
-Require Import NPlusLt.
-Require Import NTimesLt.
-
-Require Import ZDomain.
-Require Import ZAxioms.
-Require Import ZPlus.
-Require Import ZTimes.
-Require Import ZOrder.
-Require Import ZPlusOrder.
-Require Import ZTimesOrder.
-
-Module NatPairsDomain (NPlusModule : NPlus.PlusSignature) <:
-  ZDomain.DomainSignature.
+Require Export NTimesLt.
+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 Export NPlusPropertiesModule := NPlus.PlusProperties NPlusModule.
 
 Definition Z : Set := (N * N)%type.
diff --git a/theories/Numbers/Natural/Axioms/NAxioms.v b/theories/Numbers/Natural/Axioms/NAxioms.v
index 7d8fb573a..ad17e5255 100644
--- a/theories/Numbers/Natural/Axioms/NAxioms.v
+++ b/theories/Numbers/Natural/Axioms/NAxioms.v
@@ -174,7 +174,7 @@ Implicit Arguments recursion_S [A].
 
 End NatSignature.
 
-Module NatProperties (Import NatModule : NatSignature).
+Module NatProperties (Export NatModule : NatSignature).
 Module Export DomainPropertiesModule := DomainProperties DomainModule.
 Open Local Scope NScope.
 
diff --git a/theories/Numbers/Natural/Axioms/NDepRec.v b/theories/Numbers/Natural/Axioms/NDepRec.v
index 1d35bfbc4..85ff0eb72 100644
--- a/theories/Numbers/Natural/Axioms/NDepRec.v
+++ b/theories/Numbers/Natural/Axioms/NDepRec.v
@@ -1,6 +1,4 @@
-Require Import NAxioms.
-Require Import NPlus.
-Require Import NTimes.
+Require Export NTimes.
 
 (* Here we allow dependent recursion only for domains with Libniz
 equality. The reason is that, if the domain is A : nat -> Set, then (A
@@ -28,9 +26,10 @@ Axiom dep_recursion_S :
 
 End DepRecSignature.
 
-Module DepRecTimesProperties (Import DepRecModule : DepRecSignature)
-                             (Import TimesModule : TimesSignature
-                                with Module PlusModule.NatModule := DepRecModule.NatModule).
+Module DepRecTimesProperties
+  (Export DepRecModule : DepRecSignature)
+  (TimesModule : TimesSignature
+    with Module PlusModule.NatModule := DepRecModule.NatModule).
 Module Export TimesPropertiesModule := TimesProperties TimesModule.
 Open Local Scope NScope.
 
diff --git a/theories/Numbers/Natural/Axioms/NDomain.v b/theories/Numbers/Natural/Axioms/NDomain.v
index 9dc8e4078..de2ddf116 100644
--- a/theories/Numbers/Natural/Axioms/NDomain.v
+++ b/theories/Numbers/Natural/Axioms/NDomain.v
@@ -61,7 +61,7 @@ Notation "x # y" := ((E x y) -> False) (at level 70) : NScope.
 
 End DomainEqSignature.
 
-Module DomainProperties (Import DomainModule : DomainSignature).
+Module DomainProperties (Export DomainModule : DomainSignature).
 (* It also accepts module of type NatDomainEq *)
 Open Local Scope NScope.
 
diff --git a/theories/Numbers/Natural/Axioms/NIso.v b/theories/Numbers/Natural/Axioms/NIso.v
index fdf3418ed..83bcf8ebe 100644
--- a/theories/Numbers/Natural/Axioms/NIso.v
+++ b/theories/Numbers/Natural/Axioms/NIso.v
@@ -1,4 +1,4 @@
-Require Import NAxioms.
+Require Export NAxioms.
 
 Module Homomorphism (Nat1 Nat2 : NatSignature).
 
diff --git a/theories/Numbers/Natural/Axioms/NLt.v b/theories/Numbers/Natural/Axioms/NLt.v
index a70b3f95b..254db11d6 100644
--- a/theories/Numbers/Natural/Axioms/NLt.v
+++ b/theories/Numbers/Natural/Axioms/NLt.v
@@ -14,8 +14,8 @@ Axiom lt_0 : forall x, ~ (x < 0).
 Axiom lt_S : forall x y, x < S y <-> x < y \/ x == y.
 End LtSignature.
 
-Module LtProperties (Import LtModule : LtSignature).
-Module Import NatPropertiesModule := NatProperties NatModule.
+Module LtProperties (Export LtModule : LtSignature).
+Module Export NatPropertiesModule := NatProperties NatModule.
 Open Local Scope NScope.
 
 Theorem lt_n_Sn : forall n, n < S n.
diff --git a/theories/Numbers/Natural/Axioms/NMiscFunct.v b/theories/Numbers/Natural/Axioms/NMiscFunct.v
index 03f3cd86e..38af96b1d 100644
--- a/theories/Numbers/Natural/Axioms/NMiscFunct.v
+++ b/theories/Numbers/Natural/Axioms/NMiscFunct.v
@@ -1,11 +1,6 @@
-Require Import Bool. (* To get the negb function *)
-Require Import NAxioms.
-Require Import NStrongRec.
-Require Import NPlus.
-Require Import NTimes.
-Require Import NLt.
-Require Import NPlusLt.
-Require Import NTimesLt.
+Require Export Bool. (* To get the negb function *)
+Require Export NStrongRec.
+Require Export NTimesLt.
 
 Module MiscFunctFunctor (NatMod : NatSignature).
 Module Export NatPropertiesModule := NatProperties NatMod.
@@ -318,7 +313,7 @@ Qed.
 End DefaultPlusModule.
 
 Module DefaultTimesModule <: TimesSignature.
-Module Import PlusModule := DefaultPlusModule.
+Module PlusModule := DefaultPlusModule.
 
 Definition times := times.
 
@@ -361,11 +356,11 @@ Qed.
 
 End DefaultLtModule.
 
-Module Import DefaultPlusProperties := PlusProperties DefaultPlusModule.
-Module Import DefaultTimesProperties := TimesProperties DefaultTimesModule.
-Module Import DefaultLtProperties := LtProperties DefaultLtModule.
-Module Import DefaultPlusLtProperties := PlusLtProperties DefaultPlusModule DefaultLtModule.
-Module Import DefaultTimesLtProperties := TimesLtProperties DefaultTimesModule DefaultLtModule.
+Module Export DefaultPlusProperties := PlusProperties DefaultPlusModule.
+Module Export DefaultTimesProperties := TimesProperties DefaultTimesModule.
+Module Export DefaultLtProperties := LtProperties DefaultLtModule.
+Module Export DefaultPlusLtProperties := PlusLtProperties DefaultPlusModule DefaultLtModule.
+Module Export DefaultTimesLtProperties := TimesLtProperties DefaultTimesModule DefaultLtModule.
 
 (*Opaque MiscFunctFunctor.plus.
 Check plus_comm. (* This produces the following *)
diff --git a/theories/Numbers/Natural/Axioms/NPlus.v b/theories/Numbers/Natural/Axioms/NPlus.v
index d2ef81018..63cc8a40f 100644
--- a/theories/Numbers/Natural/Axioms/NPlus.v
+++ b/theories/Numbers/Natural/Axioms/NPlus.v
@@ -17,7 +17,7 @@ Axiom plus_Sn_m : forall n m, (S n) + m == S (n + m).
 
 End PlusSignature.
 
-Module PlusProperties (Import PlusModule : PlusSignature).
+Module PlusProperties (Export PlusModule : PlusSignature).
 Module Export NatPropertiesModule := NatProperties NatModule.
 Open Local Scope NScope.
 
diff --git a/theories/Numbers/Natural/Axioms/NPlusLt.v b/theories/Numbers/Natural/Axioms/NPlusLt.v
index 77bd80012..3724f9ec5 100644
--- a/theories/Numbers/Natural/Axioms/NPlusLt.v
+++ b/theories/Numbers/Natural/Axioms/NPlusLt.v
@@ -1,8 +1,8 @@
 Require Export NPlus.
 Require Export NLt.
 
-Module PlusLtProperties (Import PlusModule : PlusSignature)
-                        (Import LtModule : LtSignature with
+Module PlusLtProperties (PlusModule : PlusSignature)
+                        (LtModule : LtSignature with
                            Module NatModule := PlusModule.NatModule).
 Module Export PlusPropertiesModule := PlusProperties PlusModule.
 Module Export LtPropertiesModule := LtProperties LtModule.
diff --git a/theories/Numbers/Natural/Axioms/NStrongRec.v b/theories/Numbers/Natural/Axioms/NStrongRec.v
index 5e8223108..a2e73f99a 100644
--- a/theories/Numbers/Natural/Axioms/NStrongRec.v
+++ b/theories/Numbers/Natural/Axioms/NStrongRec.v
@@ -1,7 +1,7 @@
-Require Import NAxioms.
+Require Export NAxioms.
 
-Module StrongRecProperties (Import NatModule : NatSignature).
-Module Export DomainPropertiesModule := DomainProperties NatModule.DomainModule.
+Module StrongRecProperties (NatModule : NatSignature).
+Module Export NatPropertiesModule := NatProperties NatModule.
 Open Local Scope NScope.
 
 Section StrongRecursion.
diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v
index 6a7e9ba39..4d1d2b0ca 100644
--- a/theories/Numbers/Natural/Axioms/NTimes.v
+++ b/theories/Numbers/Natural/Axioms/NTimes.v
@@ -15,7 +15,7 @@ Axiom times_Sn_m : forall n m, (S n) * m == m + n * m.
 
 End TimesSignature.
 
-Module TimesProperties (Import TimesModule : TimesSignature).
+Module TimesProperties (Export TimesModule : TimesSignature).
 Module Export PlusPropertiesModule := PlusProperties PlusModule.
 Open Local Scope NScope.
 
diff --git a/theories/Numbers/Natural/Axioms/NTimesLt.v b/theories/Numbers/Natural/Axioms/NTimesLt.v
index c728f05a8..36989f1b3 100644
--- a/theories/Numbers/Natural/Axioms/NTimesLt.v
+++ b/theories/Numbers/Natural/Axioms/NTimesLt.v
@@ -1,13 +1,13 @@
-Require Export NLt.
 Require Export NTimes.
 Require Export NPlusLt.
 
-Module TimesLtProperties (Import TimesModule : TimesSignature)
-                         (Import LtModule : LtSignature with
+Module TimesLtProperties (TimesModule : TimesSignature)
+                         (LtModule : LtSignature with
                             Module NatModule := TimesModule.PlusModule.NatModule).
-Module Export TimesPropertiesModule := TimesProperties TimesModule.
-Module Export LtPropertiesModule := LtProperties LtModule.
-Module Export PlusLtPropertiesModule := PlusLtProperties TimesModule.PlusModule LtModule.
+Module Export TimesPropertiesModule :=
+  TimesProperties TimesModule.
+Module Export PlusLtPropertiesModule :=
+  PlusLtProperties TimesModule.PlusModule LtModule.
 Open Local Scope NScope.
 
 Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 47b39bfeb..77fbdcaf7 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -1,18 +1,16 @@
 Require Import NArith.
 Require Import Ndec.
 
-Require Import NDepRec.
-Require Import NAxioms.
-Require Import NPlus.
-Require Import NTimes.
-Require Import NLt.
-Require Import NPlusLt.
-Require Import NTimesLt.
-Require Import NMiscFunct.
+Require Export NDepRec.
+Require Export NTimesLt.
+Require Export NMiscFunct.
 
-Open Scope N_scope.
+Open Local Scope N_scope.
 
-Module BinaryDomain <: DomainEqSignature.
+Module BinaryDomain : DomainEqSignature
+  with Definition N := N
+  with Definition E := (@eq N)
+  with Definition e := Neqb.
 
 Definition N := N.
 Definition E := (@eq N).
@@ -188,17 +186,16 @@ Qed.
 
 End BinaryLt.
 
-Module Export BinaryPlusProperties := PlusProperties BinaryPlus.
-Module Export BinaryTimesProperties := TimesProperties BinaryTimes.
-Module Export BinaryDepRecTimesProperties :=
-  DepRecTimesProperties BinaryDepRec BinaryTimes.
-Module Export BinaryLtProperties := LtProperties BinaryLt.
-Module Export BinaryPlusLtProperties := PlusLtProperties BinaryPlus BinaryLt.
 Module Export BinaryTimesLtProperties := TimesLtProperties BinaryTimes BinaryLt.
 
-Module Export BinaryRecEx := MiscFunctFunctor BinaryNat.
+(*Module Export BinaryRecEx := MiscFunctFunctor BinaryNat.*)
+
+(* Just some fun comparing the efficiency of the generic log defined
+by strong (course-of-value) recursion and the log defined by recursion
+on notation *)
 (* Time Eval compute in (log 100000). *) (* 98 sec *)
 
+(*
 Fixpoint binposlog (p : positive) : N :=
 match p with
 | xH => 0
@@ -211,11 +208,5 @@ match n with
 | 0 => 0
 | Npos p => binposlog p
 end.
-
+*)
 (* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *)
-
-
-(*Check nat_total_order : forall n m : N, (n = m -> False) -> lt n m \/ lt m n.
-Check mult_positive : forall n m : N, lt 0 n -> lt 0 m -> lt 0 (n * m).*)
-
-Close Scope N_scope.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 057a0e5ac..00248a53c 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -1,10 +1,6 @@
-Require Import NDepRec.
-Require Import NPlus.
-Require Import NTimes.
-Require Import NLt.
-Require Import NPlusLt.
-Require Import NTimesLt.
-Require Import NMiscFunct.
+Require Export NDepRec.
+Require Export NTimesLt.
+Require Export NMiscFunct.
 
 Module PeanoDomain : DomainEqSignature
   with Definition N := nat
@@ -31,8 +27,6 @@ Add Relation N E
 as E_rel.
 
 End PeanoDomain.
-Open Scope NScope.
-Import PeanoDomain.
 
 Module PeanoNat <: NatSignature.
 Module Export DomainModule := PeanoDomain.
@@ -40,13 +34,6 @@ Module Export DomainModule := PeanoDomain.
 Definition O := 0.
 Definition S := S.
 
-(* For the following line, it is important that we declared
-PeanoDomain module above to be transparent, i.e., we used "<:"
-operator intead of ":". If we used ":", then the value of N, i.e.,
-nat, would not be visible here. Therefore, the type of E, which is
-N -> N -> Prop, would not be coercible to nat -> nat -> Prop.
-So we would not be able to claim that S is a morphism with respect
-to E. The same goes for defining * in terms of +, etc. *)
 Add Morphism S with signature E ==> E as S_wd.
 Proof.
 congruence.
@@ -161,11 +148,6 @@ Qed.
 
 End PeanoTimes.
 
-(* Some checks:
-Check times_eq_1 : forall n m, n * m = 1 -> n = 1 /\ m = 1.
-Eval compute in times_eq_0_dec 0 5.
-Eval compute in times_eq_0_dec 5 0. *)
-
 Module PeanoLt <: LtSignature.
 Module Export NatModule := PeanoNat.
 
@@ -190,43 +172,10 @@ End PeanoLt.
 
 (* Obtaining properties for +, *, <, and their combinations *)
 
-Module Export PeanoPlusProperties := PlusProperties PeanoPlus.
-Module Export PeanoTimesProperties := TimesProperties PeanoTimes.
-Module Export PeanoLtProperties := LtProperties PeanoLt.
-Module Export PeanoPlusLtProperties := PlusLtProperties PeanoPlus PeanoLt.
 Module Export PeanoTimesLtProperties := TimesLtProperties PeanoTimes PeanoLt.
 Module Export PeanoDepRecTimesProperties :=
   DepRecTimesProperties PeanoDepRec PeanoTimes.
 
-Module MiscFunctModule := MiscFunctFunctor PeanoNat.
-
-(*Eval compute in MiscFunctModule.lt 6 5.*)
-
-(*Set Printing All.*)
-(*Check plus_comm.
-Goal forall x y : nat, x + y = y + x.
-intros x y.
-rewrite plus_comm. reflexivity. (* does now work -- but the next line does *)
-apply plus_comm.*)
-
-(*Opaque plus.
-Eval compute in (forall n m : N, E m (PeanoPlus.Nat.S (PeanoPlus.plus n m)) -> False).
-
-Eval compute in (plus_eq_1_dec 1 1).
-Opaque plus_eq_1_dec.
-Check plus_eq_1.
-Eval compute in (forall m n : N,
-       E (PeanoPlus.plus m n) (PeanoPlus.Nat.S PeanoPlus.Nat.O) ->
-       (plus_eq_1_dec m n = true ->
-        E m PeanoPlus.Nat.O /\ E n (PeanoPlus.Nat.S PeanoPlus.Nat.O)) /\
-       (plus_eq_1_dec m n = false ->
-        E m (PeanoPlus.Nat.S PeanoPlus.Nat.O) /\ E n PeanoPlus.Nat.O)).*)
-
-(*Require Import rec_ex.
-
-Module Import PeanoRecursionExamples := RecursionExamples PeanoNat.
+(*Module MiscFunctModule := MiscFunctFunctor PeanoNat.*)
+(* The instruction above adds about 1M to the size of the .vo file !!! *)
 
-Eval compute in mult 3 15.
-Eval compute in e 100 100.
-Eval compute in log 8.
-Eval compute in half 0.*)