Separate theories directory, explicit require-import

_CoqProject

@@ -1,14 +1,14 @@
--R . DedekindReals
+-Q theories DedekindReals
 
 -arg -w -arg -deprecated-instance-without-locality
 
-Additive.v
-Archimedean.v
-Cauchy.v
-Completeness.v
-Cut.v
-DecOrder.v
-MinMax.v
-MiscLemmas.v
-Multiplication.v
-Order.v
+theories/Additive.v
+theories/Archimedean.v
+theories/Cauchy.v
+theories/Completeness.v
+theories/Cut.v
+theories/DecOrder.v
+theories/MinMax.v
+theories/MiscLemmas.v
+theories/Multiplication.v
+theories/Order.v

Additive.v → theories/Additive.v

@@ -1,10 +1,10 @@
 (** The additive structure of reals. *)
 
-Require Import Setoid Morphisms SetoidClass.
-Require Import MiscLemmas.
-Require Import QArith QOrderedType Qminmax Qabs.
-Require Import Cut.
-Require Import Archimedean.
+From Coq Require Import Setoid Morphisms SetoidClass.
+From DedekindReals Require Import MiscLemmas.
+From Coq Require Import QArith QOrderedType Qminmax Qabs.
+From DedekindReals Require Import Cut.
+From DedekindReals Require Import Archimedean.
 
 Local Open Scope Q_scope.
 

Archimedean.v → theories/Archimedean.v

@@ -7,9 +7,9 @@
    can find a straddling pair (u, l). In other words, this means we cna find arbitrarily
    good lower and upper rational approximations to x. *)
 
-Require Import QArith.
-Require Import MiscLemmas.
-Require Import Cut.
+From Coq Require Import QArith.
+From DedekindReals Require Import MiscLemmas.
+From DedekindReals Require Import Cut.
 
 Local Open Scope Q_scope.
 

Cauchy.v → theories/Cauchy.v

@@ -1,11 +1,11 @@
 (** The inclusion of Cauchy reals into Dedekind reals,
     and the proof that Dedekind reals are Cauchy-complete. *)
 
-Require Import QArith.
-Require Import Qabs.
-Require Import Qpower.
-Require Import Cut.
-Require Import MiscLemmas.
+From Coq Require Import QArith.
+From Coq Require Import Qabs.
+From Coq Require Import Qpower.
+From DedekindReals Require Import Cut.
+From DedekindReals Require Import MiscLemmas.
 
 Definition CauchyQ (un : nat -> Q) : Set
   := forall eps:Q,

Completeness.v → theories/Completeness.v

@@ -3,9 +3,9 @@
    get R back. 
 *)
 
-Require Import Morphisms.
-Require Import QArith.
-Require Import Cut Order.
+From Coq Require Import Morphisms.
+From Coq Require Import QArith.
+From DedekindReals Require Import Cut Order.
 
 Local Open Scope R_scope.
 

Cut.v → theories/Cut.v

@@ -1,8 +1,8 @@
 (** The definition of Dedekind cuts. *)
 
-Require Import QArith QOrderedType.
-Require Import Morphisms SetoidClass.
-Require Import MiscLemmas.
+From Coq Require Import QArith QOrderedType.
+From Coq Require Import Morphisms SetoidClass.
+From DedekindReals Require Import MiscLemmas.
 
 (** In the definition below we use disjunction and existence where one might
     expect sums and disjoint sums, in particular in [lower_open], [upper_open],

DecOrder.v → theories/DecOrder.v

@@ -12,15 +12,15 @@
     The series vn is convergent, because bounded by the convergent
     series 2^{-n}. *)
 
-Require Import Logic.ConstructiveEpsilon.
-Require Import QArith.
-Require Import Qabs.
-Require Import Qpower.
-Require Import Cut.
-Require Import Cauchy.
-Require Import Additive.
-Require Import MiscLemmas.
-Require Import Qminmax.
+From Coq Require Import ConstructiveEpsilon.
+From Coq Require Import QArith.
+From Coq Require Import Qabs.
+From Coq Require Import Qpower.
+From DedekindReals Require Import Cut.
+From DedekindReals Require Import Cauchy.
+From DedekindReals Require Import Additive.
+From DedekindReals Require Import MiscLemmas.
+From Coq Require Import Qminmax.
 
 Local Open Scope R_scope.
 
@@ -200,7 +200,7 @@
       apply Pos2Z.is_nonneg. unfold Z.le. rewrite <- Pos2Z.inj_compare.
       apply Pos2Nat.inj_le. destruct (Pos.to_nat b) eqn:des.
       exfalso. pose proof (Pos2Nat.is_pos b). rewrite des in H0.
       inversion H0. apply le_n_S. apply le_0_n.
     + apply xIsNegative. apply (upper_upper x (Z.neg p # b)).
       reflexivity. exact qmaj.
   - exact X. 

MinMax.v → theories/MinMax.v

@@ -1,10 +1,10 @@
 (* The lattice structure of the reals. *)
 
-Require Import Setoid Morphisms.
-Require Import QArith.
-Require Import Qminmax.
+From Coq Require Import Setoid Morphisms.
+From Coq Require Import QArith.
+From Coq Require Import Qminmax.
 
-Require Import Cut MiscLemmas Additive Multiplication Order.
+From DedekindReals Require Import Cut MiscLemmas Additive Multiplication Order.
 
 Local Open Scope R_scope.
 

Multiplication.v → theories/Multiplication.v

@@ -1,10 +1,10 @@
 (** The multiplicative structure of reals. *)
 
-Require Import Setoid Morphisms SetoidClass.
-Require Import MiscLemmas.
-Require Import QArith QOrderedType Qminmax Qabs.
-Require Import Psatz.
-Require Import Cut Additive Archimedean.
+From Coq Require Import Setoid Morphisms SetoidClass.
+From DedekindReals Require Import MiscLemmas.
+From Coq Require Import QArith QOrderedType Qminmax Qabs.
+From Coq Require Import Psatz.
+From DedekindReals Require Import Cut Additive Archimedean.
 
 Local Open Scope Q_scope.
 

Order.v → theories/Order.v

@@ -1,10 +1,10 @@
 (* The order relations < and <=. *)
 
-Require Import Morphisms Setoid.
-Require Import QArith.
-Require Import Cut.
-Require Import Additive Multiplication.
-Require Import Archimedean.
+From Coq Require Import Morphisms Setoid.
+From Coq Require Import QArith.
+From DedekindReals Require Import Cut.
+From DedekindReals Require Import Additive Multiplication.
+From DedekindReals Require Import Archimedean.
 
 Local Open Scope R_scope.