Split ConstructiveRealsLUB and improve comments

7 files changed, 344 insertions, 293 deletions

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 35bcfacd48..cc91776a4d 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -518,6 +518,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Reals/ConstructiveCauchyReals.v
     theories/Reals/Raxioms.v
     theories/Reals/ConstructiveRIneq.v
+    theories/Reals/ConstructiveRealsLUB.v
     theories/Reals/RIneq.v
     theories/Reals/DiscrR.v
     theories/Reals/ROrderedType.v
diff --git a/theories/Reals/ConstructiveRIneq.v b/theories/Reals/ConstructiveRIneq.v
index 95fb991ffe..b53436be55 100644
--- a/theories/Reals/ConstructiveRIneq.v
+++ b/theories/Reals/ConstructiveRIneq.v
@@ -16,10 +16,15 @@
 (* Implement interface ConstructiveReals opaquely with
    Cauchy reals and prove basic results.
    Those are therefore true for any implementation of
-   ConstructiveReals (for example with Dedekind reals). *)
+   ConstructiveReals (for example with Dedekind reals).
+
+   This file is the recommended import for working with
+   constructive reals, do not use ConstructiveCauchyReals
+   directly. *)
 
 Require Import ConstructiveCauchyReals.
 Require Import ConstructiveRcomplete.
+Require Import ConstructiveRealsLUB.
 Require Export ConstructiveReals.
 Require Import Zpower.
 Require Export ZArithRing.
@@ -2529,11 +2534,10 @@ Qed.
    sequence of rational numbers (n maps to the q between
    a and a+1/n). This is how real numbers compute,
    and they are measured by exact rational numbers. *)
-Definition RQ_dense_pos (a b : R)
-  : 0 < b
-    -> a < b -> { q : Q & a < IQR q < b }.
+Definition RQ_dense (a b : R)
+  : a < b -> { q : Q & a < IQR q < b }.
 Proof.
-  intros H H0.
+  intros H0.
   assert (0 < b - a) as epsPos.
   { apply (Rplus_lt_compat_r (-a)) in H0.
     rewrite Rplus_opp_r in H0. apply H0. }
@@ -2580,35 +2584,6 @@ Proof.
       rewrite Rmult_1_r, Rmult_comm. apply maj2.
 Qed.
 
-Definition RQ_dense (a b : R)
-  : a < b
-    -> { q : Q & a < IQR q < b }.
-Proof.
-  intros H. destruct (linear_order_T a 0 b). apply H.
-  - destruct (RQ_dense_pos (-b) (-a)) as [q maj].
-    apply (Rplus_lt_compat_l (-a)) in r. rewrite Rplus_opp_l in r.
-    rewrite Rplus_0_r in r. apply r.
-    apply (Rplus_lt_compat_l (-a)) in H.
-    rewrite Rplus_opp_l, Rplus_comm in H.
-    apply (Rplus_lt_compat_l (-b)) in H. rewrite <- Rplus_assoc in H.
-    rewrite Rplus_opp_l in H. rewrite Rplus_0_l in H.
-    rewrite Rplus_0_r in H. apply H.
-    exists (-q)%Q. split.
-    + destruct maj as [_ maj].
-      apply (Rplus_lt_compat_l (-IQR q)) in maj.
-      rewrite Rplus_opp_l, <- opp_IQR, Rplus_comm in maj.
-      apply (Rplus_lt_compat_l a) in maj. rewrite <- Rplus_assoc in maj.
-      rewrite Rplus_opp_r, Rplus_0_l in maj.
-      rewrite Rplus_0_r in maj. apply maj.
-    + destruct maj as [maj _].
-      apply (Rplus_lt_compat_l (-IQR q)) in maj.
-      rewrite Rplus_opp_l, <- opp_IQR, Rplus_comm in maj.
-      apply (Rplus_lt_compat_l b) in maj. rewrite <- Rplus_assoc in maj.
-      rewrite Rplus_opp_r in maj. rewrite Rplus_0_l in maj.
-      rewrite Rplus_0_r in maj. apply maj.
-  - apply RQ_dense_pos. apply r. apply H.
-Qed.
-
 Definition RQ_limit : forall (x : R) (n:nat),
     { q:Q & x < IQR q < x + IQR (1 # Pos.of_nat n) }.
 Proof.
@@ -2623,7 +2598,7 @@ Qed.
 Lemma Rlt_lpo_dec : forall x y : R,
     (forall (P : nat -> Prop), (forall n, {P n} + {~P n})
                     -> {n | ~P n} + {forall n, P n})
-    -> (x < y) + (x < y -> False).
+    -> (x < y) + (y <= x).
 Proof.
   intros x y lpo.
   pose (fun n => let (l,_) := RQ_limit x n in l) as xn.
@@ -2681,6 +2656,18 @@ Proof.
       unfold IZR, IPR, IPR_2. ring.
 Qed.
 
+Lemma Rlt_lpo_floor : forall x : R,
+    (forall (P : nat -> Prop), (forall n, {P n} + {~P n})
+                    -> {n | ~P n} + {forall n, P n})
+    -> { p : Z & IZR p <= x < IZR p + 1 }.
+Proof.
+  intros x lpo. destruct (Rfloor x) as [n [H H0]].
+  destruct (Rlt_lpo_dec x (IZR n + 1) lpo).
+  - exists n. split. unfold Rle. apply Rlt_asym. exact H. exact r.
+  - exists (n+1)%Z. split. rewrite plus_IZR. exact r.
+    rewrite plus_IZR, Rplus_assoc. exact H0.
+Qed.
+
 
 (*********)
 Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2.
diff --git a/theories/Reals/ConstructiveRcomplete.v b/theories/Reals/ConstructiveRcomplete.v
index 929fa03051..ce45bcd567 100644
--- a/theories/Reals/ConstructiveRcomplete.v
+++ b/theories/Reals/ConstructiveRcomplete.v
@@ -430,257 +430,3 @@ Proof.
       apply Qplus_lt_r. reflexivity.
       rewrite Qinv_plus_distr. reflexivity.
 Qed.
-
-Definition sig_forall_dec_T : Type
-  := forall (P : nat -> Prop), (forall n, {P n} + {~P n})
-                   -> {n | ~P n} + {forall n, P n}.
-
-Definition sig_not_dec_T : Type := forall P : Prop, { ~~P } + { ~P }.
-
-Definition is_upper_bound (E:CReal -> Prop) (m:CReal)
-  := forall x:CReal, E x -> x <= m.
-
-Definition is_lub (E:CReal -> Prop) (m:CReal) :=
-  is_upper_bound E m /\ (forall b:CReal, is_upper_bound E b -> m <= b).
-
-Lemma is_upper_bound_dec :
-  forall (E:CReal -> Prop) (x:CReal),
-    sig_forall_dec_T
-    -> sig_not_dec_T
-    -> { is_upper_bound E x } + { ~is_upper_bound E x }.
-Proof.
-  intros E x lpo sig_not_dec.
-  destruct (sig_not_dec (~exists y:CReal, E y /\ CRealLtProp x y)).
-  - left. intros y H.
-    destruct (CRealLt_lpo_dec x y lpo). 2: exact f.
-    exfalso. apply n. intro abs. apply abs.
-    exists y. split. exact H. destruct c. exists x0. exact q.
-  - right. intro abs. apply n. intros [y [H H0]].
-    specialize (abs y H). apply CRealLtEpsilon in H0. contradiction.
-Qed.
-
-Lemma is_upper_bound_epsilon :
-  forall (E:CReal -> Prop),
-    sig_forall_dec_T
-    -> sig_not_dec_T
-    -> (exists x:CReal, is_upper_bound E x)
-    -> { n:nat | is_upper_bound E (INR n) }.
-Proof.
-  intros E lpo sig_not_dec Ebound.
-  apply constructive_indefinite_ground_description_nat.
-  - intro n. apply is_upper_bound_dec. exact lpo. exact sig_not_dec.
-  - destruct Ebound as [x H]. destruct (Rup_nat x). exists x0.
-    intros y ey. specialize (H y ey).
-    apply CRealLt_asym. apply (CRealLe_Lt_trans _ x); assumption.
-Qed.
-
-Lemma is_upper_bound_not_epsilon :
-  forall E:CReal -> Prop,
-    sig_forall_dec_T
-    -> sig_not_dec_T
-    -> (exists x : CReal, E x)
-    -> { m:nat | ~is_upper_bound E (-INR m) }.
-Proof.
-  intros E lpo sig_not_dec H.
-  apply constructive_indefinite_ground_description_nat.
-  - intro n. destruct (is_upper_bound_dec E (-INR n) lpo sig_not_dec).
-    right. intro abs. contradiction. left. exact n0.
-  - destruct H as [x H]. destruct (Rup_nat (-x)) as [n H0].
-    exists n. intro abs. specialize (abs x H).
-    apply abs. apply (CReal_plus_lt_reg_l (INR n-x)).
-    ring_simplify. exact H0.
-Qed.
-
-(* Decidable Dedekind cuts are Cauchy reals. *)
-Record DedekindDecCut : Type :=
-  {
-    DDupcut : Q -> Prop;
-    DDproper : forall q r : Q, (q == r -> DDupcut q -> DDupcut r)%Q;
-    DDlow : Q;
-    DDhigh : Q;
-    DDdec : forall q:Q, { DDupcut q } + { ~DDupcut q };
-    DDinterval : forall q r : Q, Qle q r -> DDupcut q -> DDupcut r;
-    DDhighProp : DDupcut DDhigh;
-    DDlowProp : ~DDupcut DDlow;
-  }.
-
-Lemma DDlow_below_up : forall (upcut : DedekindDecCut) (a b : Q),
-    DDupcut upcut a -> ~DDupcut upcut b -> Qlt b a.
-Proof.
-  intros. destruct (Qlt_le_dec b a). exact q.
-  exfalso. apply H0. apply (DDinterval upcut a).
-  exact q. exact H.
-Qed.
-
-Fixpoint DDcut_limit_fix (upcut : DedekindDecCut) (r : Q) (n : nat) :
-  Qlt 0 r
-  -> (DDupcut upcut (DDlow upcut + (Z.of_nat n#1) * r))
-  -> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }.
-Proof.
-  destruct n.
-  - intros. exfalso. simpl in H0.
-    apply (DDproper upcut _ (DDlow upcut)) in H0. 2: ring.
-    exact (DDlowProp upcut H0).
-  - intros. destruct (DDdec upcut (DDlow upcut + (Z.of_nat n # 1) * r)).
-    + exact (DDcut_limit_fix upcut r n H d).
-    + exists (DDlow upcut + (Z.of_nat (S n) # 1) * r)%Q. split.
-      exact H0. intro abs.
-      apply (DDproper upcut _ (DDlow upcut + (Z.of_nat n # 1) * r)) in abs.
-      contradiction.
-      rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite <- Qinv_plus_distr.
-      ring.
-Qed.
-
-Lemma DDcut_limit : forall (upcut : DedekindDecCut) (r : Q),
-  Qlt 0 r
-  -> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }.
-Proof.
-  intros.
-  destruct (Qarchimedean ((DDhigh upcut - DDlow upcut)/r)) as [n nmaj].
-  apply (DDcut_limit_fix upcut r (Pos.to_nat n) H).
-  apply (Qmult_lt_r _ _ r) in nmaj. 2: exact H.
-  unfold Qdiv in nmaj.
-  rewrite <- Qmult_assoc, (Qmult_comm (/r)), Qmult_inv_r, Qmult_1_r in nmaj.
-  apply (DDinterval upcut (DDhigh upcut)). 2: exact (DDhighProp upcut).
-  apply Qlt_le_weak. apply (Qplus_lt_r _ _ (-DDlow upcut)).
-  rewrite Qplus_assoc, <- (Qplus_comm (DDlow upcut)), Qplus_opp_r,
-  Qplus_0_l, Qplus_comm.
-  rewrite positive_nat_Z. exact nmaj.
-  intros abs. rewrite abs in H. exact (Qlt_irrefl 0 H).
-Qed.
-
-Lemma glb_dec_Q : forall upcut : DedekindDecCut,
-    { x : CReal | forall r:Q, (x < IQR r -> DDupcut upcut r)
-                         /\ (IQR r < x -> ~DDupcut upcut r) }.
-Proof.
-  intros.
-  assert (forall a b : Q, Qle a b -> Qle (-b) (-a)).
-  { intros. apply (Qplus_le_l _ _ (a+b)). ring_simplify. exact H. }
-  assert (QCauchySeq (fun n:nat => proj1_sig (DDcut_limit
-                                           upcut (1#Pos.of_nat n) (eq_refl _)))
-                     Pos.to_nat).
-  { intros p i j pi pj.
-    destruct (DDcut_limit upcut (1 # Pos.of_nat i) eq_refl),
-    (DDcut_limit upcut (1 # Pos.of_nat j) eq_refl); unfold proj1_sig.
-    apply Qabs_case. intros.
-    apply (Qplus_lt_l _ _ (x0- (1#p))). ring_simplify.
-    setoid_replace (x + -1 * (1 # p))%Q with (x - (1 # p))%Q.
-    2: ring. apply (Qle_lt_trans _ (x- (1#Pos.of_nat i))).
-    apply Qplus_le_r. apply H.
-    apply Z2Nat.inj_le. discriminate. discriminate. simpl.
-    rewrite Nat2Pos.id. exact pi. intro abs.
-    subst i. inversion pi. pose proof (Pos2Nat.is_pos p).
-    rewrite H2 in H1. inversion H1.
-    apply (DDlow_below_up upcut). apply a0. apply a.
-    intros.
-    apply (Qplus_lt_l _ _ (x- (1#p))). ring_simplify.
-    setoid_replace (x0 + -1 * (1 # p))%Q with (x0 - (1 # p))%Q.
-    2: ring. apply (Qle_lt_trans _ (x0- (1#Pos.of_nat j))).
-    apply Qplus_le_r. apply H.
-    apply Z2Nat.inj_le. discriminate. discriminate. simpl.
-    rewrite Nat2Pos.id. exact pj. intro abs.
-    subst j. inversion pj. pose proof (Pos2Nat.is_pos p).
-    rewrite H2 in H1. inversion H1.
-    apply (DDlow_below_up upcut). apply a. apply a0. }
-  pose (exist (fun qn => QSeqEquiv qn qn Pos.to_nat) _ H0) as l.
-  exists l. split.
-  - intros. (* find an upper point between the limit and r *)
-    rewrite FinjectQ_CReal in H1. destruct H1 as [p pmaj].
-    unfold l,proj1_sig in pmaj.
-    destruct (DDcut_limit upcut (1 # Pos.of_nat (Pos.to_nat p)) eq_refl) as [q qmaj]
-    ; simpl in pmaj.
-    apply (DDinterval upcut q). 2: apply qmaj.
-    apply (Qplus_lt_l _ _ q) in pmaj. ring_simplify in pmaj.
-    apply (Qle_trans _ ((2#p) + q)).
-    apply (Qplus_le_l _ _ (-q)). ring_simplify. discriminate.
-    apply Qlt_le_weak. exact pmaj.
-  - intros H1 abs.
-    rewrite FinjectQ_CReal in H1. destruct H1 as [p pmaj].
-    unfold l,proj1_sig in pmaj.
-    destruct (DDcut_limit upcut (1 # Pos.of_nat (Pos.to_nat p)) eq_refl) as [q qmaj]
-    ; simpl in pmaj.
-    rewrite Pos2Nat.id in qmaj.
-    apply (Qplus_lt_r _ _ (r - (2#p))) in pmaj. ring_simplify in pmaj.
-    destruct qmaj. apply H2.
-    apply (DDinterval upcut r). 2: exact abs.
-    apply Qlt_le_weak, (Qlt_trans _ (-1*(2#p) + q) _ pmaj).
-    apply (Qplus_lt_l _ _ ((2#p) -q)). ring_simplify.
-    setoid_replace (-1 * (1 # p))%Q with (-(1#p))%Q.
-    2: ring. rewrite Qinv_minus_distr. reflexivity.
-Qed.
-
-Lemma is_upper_bound_glb :
-  forall (E:CReal -> Prop),
-    sig_not_dec_T
-    -> sig_forall_dec_T
-    -> (exists x : CReal, E x)
-    -> (exists x : CReal, is_upper_bound E x)
-    -> { x : CReal | forall r:Q, (x < IQR r -> is_upper_bound E (IQR r))
-                           /\ (IQR r < x -> ~is_upper_bound E (IQR r)) }.
-Proof.
-  intros E sig_not_dec lpo Einhab Ebound.
-  destruct (is_upper_bound_epsilon E lpo sig_not_dec Ebound) as [a luba].
-  destruct (is_upper_bound_not_epsilon E lpo sig_not_dec Einhab) as [b glbb].
-  pose (fun q => is_upper_bound E (IQR q)) as upcut.
-  assert (forall q:Q, { upcut q } + { ~upcut q } ).
-  { intro q. apply is_upper_bound_dec. exact lpo. exact sig_not_dec. }
-  assert (forall q r : Q, (q <= r)%Q -> upcut q -> upcut r).
-  { intros. intros x Ex. specialize (H1 x Ex). intro abs.
-    apply H1. apply (CRealLe_Lt_trans _ (IQR r)). 2: exact abs.
-    apply IQR_le. exact H0. }
-  assert (upcut (Z.of_nat a # 1)%Q).
-  { intros x Ex. unfold IQR. rewrite CReal_inv_1, CReal_mult_1_r.
-    specialize (luba x Ex). rewrite <- INR_IZR_INZ. exact luba. }
-  assert (~upcut (- Z.of_nat b # 1)%Q).
-  { intros abs. apply glbb. intros x Ex.
-    specialize (abs x Ex). unfold IQR in abs.
-    rewrite CReal_inv_1, CReal_mult_1_r, opp_IZR, <- INR_IZR_INZ in abs.
-    exact abs. }
-  assert (forall q r : Q, (q == r)%Q -> upcut q -> upcut r).
-  { intros. intros x Ex. specialize (H4 x Ex). rewrite <- H3. exact H4. }
-  destruct (glb_dec_Q (Build_DedekindDecCut
-                         upcut H3 (-Z.of_nat b # 1)%Q (Z.of_nat a # 1)
-                         H H0 H1 H2)).
-  simpl in a0. exists x. intro r. split.
-  - intros. apply a0. exact H4.
-  - intros H6 abs. specialize (a0 r) as [_ a0]. apply a0.
-    exact H6. exact abs.
-Qed.
-
-Lemma is_upper_bound_closed :
-  forall (E:CReal -> Prop) (sig_forall_dec : sig_forall_dec_T)
-    (sig_not_dec : sig_not_dec_T)
-    (Einhab : exists x : CReal, E x)
-    (Ebound : exists x : CReal, is_upper_bound E x),
-    is_lub
-      E (proj1_sig (is_upper_bound_glb
-                      E sig_not_dec sig_forall_dec Einhab Ebound)).
-Proof.
-  intros. split.
-  - intros x Ex.
-    destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl.
-    intro abs. destruct (FQ_dense x0 x abs) as [q [qmaj H]].
-    specialize (a q) as [a _]. specialize (a qmaj x Ex).
-    contradiction.
-  - intros.
-    destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl.
-    intro abs. destruct (FQ_dense b x abs) as [q [qmaj H0]].
-    specialize (a q) as [_ a]. apply a. exact H0.
-    intros y Ey. specialize (H y Ey). intro abs2.
-    apply H. exact (CRealLt_trans _ (IQR q) _ qmaj abs2).
-Qed.
-
-Lemma sig_lub :
-  forall (E:CReal -> Prop),
-    sig_forall_dec_T
-    -> sig_not_dec_T
-    -> (exists x : CReal, E x)
-    -> (exists x : CReal, is_upper_bound E x)
-    -> { u : CReal | is_lub E u }.
-Proof.
-  intros E sig_forall_dec sig_not_dec Einhab Ebound.
-  pose proof (is_upper_bound_closed E sig_forall_dec sig_not_dec Einhab Ebound).
-  destruct (is_upper_bound_glb
-              E sig_not_dec sig_forall_dec Einhab Ebound); simpl in H.
-  exists x. exact H.
-Qed.
diff --git a/theories/Reals/ConstructiveReals.v b/theories/Reals/ConstructiveReals.v
index 97876d129a..fc3d6afe15 100644
--- a/theories/Reals/ConstructiveReals.v
+++ b/theories/Reals/ConstructiveReals.v
@@ -10,8 +10,38 @@
 (************************************************************************)
 
 (* An interface for constructive and computable real numbers.
-   All of its elements are isomorphic, for example it contains
-   the Cauchy reals and the Dedekind reals. *)
+   All of its instances are isomorphic, for example it contains
+   the Cauchy reals implemented in file ConstructivecauchyReals
+   and the sumbool-based Dedekind reals defined by
+
+Structure R := {
+  (* The cuts are represented as propositional functions, rather than subsets,
+     as there are no subsets in type theory. *)
+  lower : Q -> Prop;
+  upper : Q -> Prop;
+  (* The cuts respect equality on Q. *)
+  lower_proper : Proper (Qeq ==> iff) lower;
+  upper_proper : Proper (Qeq ==> iff) upper;
+  (* The cuts are inhabited. *)
+  lower_bound : { q : Q | lower q };
+  upper_bound : { r : Q | upper r };
+  (* The lower cut is a lower set. *)
+  lower_lower : forall q r, q < r -> lower r -> lower q;
+  (* The lower cut is open. *)
+  lower_open : forall q, lower q -> exists r, q < r /\ lower r;
+  (* The upper cut is an upper set. *)
+  upper_upper : forall q r, q < r -> upper q -> upper r;
+  (* The upper cut is open. *)
+  upper_open : forall r, upper r -> exists q,  q < r /\ upper q;
+  (* The cuts are disjoint. *)
+  disjoint : forall q, ~ (lower q /\ upper q);
+  (* There is no gap between the cuts. *)
+  located : forall q r, q < r -> { lower q } + { upper r }
+}.
+
+  see github.com/andrejbauer/dedekind-reals for the Prop-based
+  version of those Dedekind reals (although Prop fails to make
+  them an instance of ConstructiveReals). *)
 
 Require Import QArith.
 
diff --git a/theories/Reals/ConstructiveRealsLUB.v b/theories/Reals/ConstructiveRealsLUB.v
new file mode 100644
index 0000000000..f5c447f7db
--- /dev/null
+++ b/theories/Reals/ConstructiveRealsLUB.v
@@ -0,0 +1,276 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+(************************************************************************)
+
+(* Proof that LPO and the excluded middle for negations imply
+   the existence of least upper bounds for all non-empty and bounded
+   subsets of the real numbers. *)
+
+Require Import QArith_base.
+Require Import Qabs.
+Require Import ConstructiveCauchyReals.
+Require Import ConstructiveRcomplete.
+Require Import Logic.ConstructiveEpsilon.
+
+Local Open Scope CReal_scope.
+
+Definition sig_forall_dec_T : Type
+  := forall (P : nat -> Prop), (forall n, {P n} + {~P n})
+                   -> {n | ~P n} + {forall n, P n}.
+
+Definition sig_not_dec_T : Type := forall P : Prop, { ~~P } + { ~P }.
+
+Definition is_upper_bound (E:CReal -> Prop) (m:CReal)
+  := forall x:CReal, E x -> x <= m.
+
+Definition is_lub (E:CReal -> Prop) (m:CReal) :=
+  is_upper_bound E m /\ (forall b:CReal, is_upper_bound E b -> m <= b).
+
+Lemma is_upper_bound_dec :
+  forall (E:CReal -> Prop) (x:CReal),
+    sig_forall_dec_T
+    -> sig_not_dec_T
+    -> { is_upper_bound E x } + { ~is_upper_bound E x }.
+Proof.
+  intros E x lpo sig_not_dec.
+  destruct (sig_not_dec (~exists y:CReal, E y /\ CRealLtProp x y)).
+  - left. intros y H.
+    destruct (CRealLt_lpo_dec x y lpo). 2: exact f.
+    exfalso. apply n. intro abs. apply abs.
+    exists y. split. exact H. destruct c. exists x0. exact q.
+  - right. intro abs. apply n. intros [y [H H0]].
+    specialize (abs y H). apply CRealLtEpsilon in H0. contradiction.
+Qed.
+
+Lemma is_upper_bound_epsilon :
+  forall (E:CReal -> Prop),
+    sig_forall_dec_T
+    -> sig_not_dec_T
+    -> (exists x:CReal, is_upper_bound E x)
+    -> { n:nat | is_upper_bound E (INR n) }.
+Proof.
+  intros E lpo sig_not_dec Ebound.
+  apply constructive_indefinite_ground_description_nat.
+  - intro n. apply is_upper_bound_dec. exact lpo. exact sig_not_dec.
+  - destruct Ebound as [x H]. destruct (Rup_nat x). exists x0.
+    intros y ey. specialize (H y ey).
+    apply CRealLt_asym. apply (CRealLe_Lt_trans _ x); assumption.
+Qed.
+
+Lemma is_upper_bound_not_epsilon :
+  forall E:CReal -> Prop,
+    sig_forall_dec_T
+    -> sig_not_dec_T
+    -> (exists x : CReal, E x)
+    -> { m:nat | ~is_upper_bound E (-INR m) }.
+Proof.
+  intros E lpo sig_not_dec H.
+  apply constructive_indefinite_ground_description_nat.
+  - intro n. destruct (is_upper_bound_dec E (-INR n) lpo sig_not_dec).
+    right. intro abs. contradiction. left. exact n0.
+  - destruct H as [x H]. destruct (Rup_nat (-x)) as [n H0].
+    exists n. intro abs. specialize (abs x H).
+    apply abs. apply (CReal_plus_lt_reg_l (INR n-x)).
+    ring_simplify. exact H0.
+Qed.
+
+(* Decidable Dedekind cuts are Cauchy reals. *)
+Record DedekindDecCut : Type :=
+  {
+    DDupcut : Q -> Prop;
+    DDproper : forall q r : Q, (q == r -> DDupcut q -> DDupcut r)%Q;
+    DDlow : Q;
+    DDhigh : Q;
+    DDdec : forall q:Q, { DDupcut q } + { ~DDupcut q };
+    DDinterval : forall q r : Q, Qle q r -> DDupcut q -> DDupcut r;
+    DDhighProp : DDupcut DDhigh;
+    DDlowProp : ~DDupcut DDlow;
+  }.
+
+Lemma DDlow_below_up : forall (upcut : DedekindDecCut) (a b : Q),
+    DDupcut upcut a -> ~DDupcut upcut b -> Qlt b a.
+Proof.
+  intros. destruct (Qlt_le_dec b a). exact q.
+  exfalso. apply H0. apply (DDinterval upcut a).
+  exact q. exact H.
+Qed.
+
+Fixpoint DDcut_limit_fix (upcut : DedekindDecCut) (r : Q) (n : nat) :
+  Qlt 0 r
+  -> (DDupcut upcut (DDlow upcut + (Z.of_nat n#1) * r))
+  -> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }.
+Proof.
+  destruct n.
+  - intros. exfalso. simpl in H0.
+    apply (DDproper upcut _ (DDlow upcut)) in H0. 2: ring.
+    exact (DDlowProp upcut H0).
+  - intros. destruct (DDdec upcut (DDlow upcut + (Z.of_nat n # 1) * r)).
+    + exact (DDcut_limit_fix upcut r n H d).
+    + exists (DDlow upcut + (Z.of_nat (S n) # 1) * r)%Q. split.
+      exact H0. intro abs.
+      apply (DDproper upcut _ (DDlow upcut + (Z.of_nat n # 1) * r)) in abs.
+      contradiction.
+      rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite <- Qinv_plus_distr.
+      ring.
+Qed.
+
+Lemma DDcut_limit : forall (upcut : DedekindDecCut) (r : Q),
+  Qlt 0 r
+  -> { q : Q | DDupcut upcut q /\ ~DDupcut upcut (q - r) }.
+Proof.
+  intros.
+  destruct (Qarchimedean ((DDhigh upcut - DDlow upcut)/r)) as [n nmaj].
+  apply (DDcut_limit_fix upcut r (Pos.to_nat n) H).
+  apply (Qmult_lt_r _ _ r) in nmaj. 2: exact H.
+  unfold Qdiv in nmaj.
+  rewrite <- Qmult_assoc, (Qmult_comm (/r)), Qmult_inv_r, Qmult_1_r in nmaj.
+  apply (DDinterval upcut (DDhigh upcut)). 2: exact (DDhighProp upcut).
+  apply Qlt_le_weak. apply (Qplus_lt_r _ _ (-DDlow upcut)).
+  rewrite Qplus_assoc, <- (Qplus_comm (DDlow upcut)), Qplus_opp_r,
+  Qplus_0_l, Qplus_comm.
+  rewrite positive_nat_Z. exact nmaj.
+  intros abs. rewrite abs in H. exact (Qlt_irrefl 0 H).
+Qed.
+
+Lemma glb_dec_Q : forall upcut : DedekindDecCut,
+    { x : CReal | forall r:Q, (x < IQR r -> DDupcut upcut r)
+                         /\ (IQR r < x -> ~DDupcut upcut r) }.
+Proof.
+  intros.
+  assert (forall a b : Q, Qle a b -> Qle (-b) (-a)).
+  { intros. apply (Qplus_le_l _ _ (a+b)). ring_simplify. exact H. }
+  assert (QCauchySeq (fun n:nat => proj1_sig (DDcut_limit
+                                           upcut (1#Pos.of_nat n) (eq_refl _)))
+                     Pos.to_nat).
+  { intros p i j pi pj.
+    destruct (DDcut_limit upcut (1 # Pos.of_nat i) eq_refl),
+    (DDcut_limit upcut (1 # Pos.of_nat j) eq_refl); unfold proj1_sig.
+    apply Qabs_case. intros.
+    apply (Qplus_lt_l _ _ (x0- (1#p))). ring_simplify.
+    setoid_replace (x + -1 * (1 # p))%Q with (x - (1 # p))%Q.
+    2: ring. apply (Qle_lt_trans _ (x- (1#Pos.of_nat i))).
+    apply Qplus_le_r. apply H.
+    apply Z2Nat.inj_le. discriminate. discriminate. simpl.
+    rewrite Nat2Pos.id. exact pi. intro abs.
+    subst i. inversion pi. pose proof (Pos2Nat.is_pos p).
+    rewrite H2 in H1. inversion H1.
+    apply (DDlow_below_up upcut). apply a0. apply a.
+    intros.
+    apply (Qplus_lt_l _ _ (x- (1#p))). ring_simplify.
+    setoid_replace (x0 + -1 * (1 # p))%Q with (x0 - (1 # p))%Q.
+    2: ring. apply (Qle_lt_trans _ (x0- (1#Pos.of_nat j))).
+    apply Qplus_le_r. apply H.
+    apply Z2Nat.inj_le. discriminate. discriminate. simpl.
+    rewrite Nat2Pos.id. exact pj. intro abs.
+    subst j. inversion pj. pose proof (Pos2Nat.is_pos p).
+    rewrite H2 in H1. inversion H1.
+    apply (DDlow_below_up upcut). apply a. apply a0. }
+  pose (exist (fun qn => QSeqEquiv qn qn Pos.to_nat) _ H0) as l.
+  exists l. split.
+  - intros. (* find an upper point between the limit and r *)
+    rewrite FinjectQ_CReal in H1. destruct H1 as [p pmaj].
+    unfold l,proj1_sig in pmaj.
+    destruct (DDcut_limit upcut (1 # Pos.of_nat (Pos.to_nat p)) eq_refl) as [q qmaj]
+    ; simpl in pmaj.
+    apply (DDinterval upcut q). 2: apply qmaj.
+    apply (Qplus_lt_l _ _ q) in pmaj. ring_simplify in pmaj.
+    apply (Qle_trans _ ((2#p) + q)).
+    apply (Qplus_le_l _ _ (-q)). ring_simplify. discriminate.
+    apply Qlt_le_weak. exact pmaj.
+  - intros H1 abs.
+    rewrite FinjectQ_CReal in H1. destruct H1 as [p pmaj].
+    unfold l,proj1_sig in pmaj.
+    destruct (DDcut_limit upcut (1 # Pos.of_nat (Pos.to_nat p)) eq_refl) as [q qmaj]
+    ; simpl in pmaj.
+    rewrite Pos2Nat.id in qmaj.
+    apply (Qplus_lt_r _ _ (r - (2#p))) in pmaj. ring_simplify in pmaj.
+    destruct qmaj. apply H2.
+    apply (DDinterval upcut r). 2: exact abs.
+    apply Qlt_le_weak, (Qlt_trans _ (-1*(2#p) + q) _ pmaj).
+    apply (Qplus_lt_l _ _ ((2#p) -q)). ring_simplify.
+    setoid_replace (-1 * (1 # p))%Q with (-(1#p))%Q.
+    2: ring. rewrite Qinv_minus_distr. reflexivity.
+Qed.
+
+Lemma is_upper_bound_glb :
+  forall (E:CReal -> Prop),
+    sig_not_dec_T
+    -> sig_forall_dec_T
+    -> (exists x : CReal, E x)
+    -> (exists x : CReal, is_upper_bound E x)
+    -> { x : CReal | forall r:Q, (x < IQR r -> is_upper_bound E (IQR r))
+                           /\ (IQR r < x -> ~is_upper_bound E (IQR r)) }.
+Proof.
+  intros E sig_not_dec lpo Einhab Ebound.
+  destruct (is_upper_bound_epsilon E lpo sig_not_dec Ebound) as [a luba].
+  destruct (is_upper_bound_not_epsilon E lpo sig_not_dec Einhab) as [b glbb].
+  pose (fun q => is_upper_bound E (IQR q)) as upcut.
+  assert (forall q:Q, { upcut q } + { ~upcut q } ).
+  { intro q. apply is_upper_bound_dec. exact lpo. exact sig_not_dec. }
+  assert (forall q r : Q, (q <= r)%Q -> upcut q -> upcut r).
+  { intros. intros x Ex. specialize (H1 x Ex). intro abs.
+    apply H1. apply (CRealLe_Lt_trans _ (IQR r)). 2: exact abs.
+    apply IQR_le. exact H0. }
+  assert (upcut (Z.of_nat a # 1)%Q).
+  { intros x Ex. unfold IQR. rewrite CReal_inv_1, CReal_mult_1_r.
+    specialize (luba x Ex). rewrite <- INR_IZR_INZ. exact luba. }
+  assert (~upcut (- Z.of_nat b # 1)%Q).
+  { intros abs. apply glbb. intros x Ex.
+    specialize (abs x Ex). unfold IQR in abs.
+    rewrite CReal_inv_1, CReal_mult_1_r, opp_IZR, <- INR_IZR_INZ in abs.
+    exact abs. }
+  assert (forall q r : Q, (q == r)%Q -> upcut q -> upcut r).
+  { intros. intros x Ex. specialize (H4 x Ex). rewrite <- H3. exact H4. }
+  destruct (glb_dec_Q (Build_DedekindDecCut
+                         upcut H3 (-Z.of_nat b # 1)%Q (Z.of_nat a # 1)
+                         H H0 H1 H2)).
+  simpl in a0. exists x. intro r. split.
+  - intros. apply a0. exact H4.
+  - intros H6 abs. specialize (a0 r) as [_ a0]. apply a0.
+    exact H6. exact abs.
+Qed.
+
+Lemma is_upper_bound_closed :
+  forall (E:CReal -> Prop) (sig_forall_dec : sig_forall_dec_T)
+    (sig_not_dec : sig_not_dec_T)
+    (Einhab : exists x : CReal, E x)
+    (Ebound : exists x : CReal, is_upper_bound E x),
+    is_lub
+      E (proj1_sig (is_upper_bound_glb
+                      E sig_not_dec sig_forall_dec Einhab Ebound)).
+Proof.
+  intros. split.
+  - intros x Ex.
+    destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl.
+    intro abs. destruct (FQ_dense x0 x abs) as [q [qmaj H]].
+    specialize (a q) as [a _]. specialize (a qmaj x Ex).
+    contradiction.
+  - intros.
+    destruct (is_upper_bound_glb E sig_not_dec sig_forall_dec Einhab Ebound); simpl.
+    intro abs. destruct (FQ_dense b x abs) as [q [qmaj H0]].
+    specialize (a q) as [_ a]. apply a. exact H0.
+    intros y Ey. specialize (H y Ey). intro abs2.
+    apply H. exact (CRealLt_trans _ (IQR q) _ qmaj abs2).
+Qed.
+
+Lemma sig_lub :
+  forall (E:CReal -> Prop),
+    sig_forall_dec_T
+    -> sig_not_dec_T
+    -> (exists x : CReal, E x)
+    -> (exists x : CReal, is_upper_bound E x)
+    -> { u : CReal | is_lub E u }.
+Proof.
+  intros E sig_forall_dec sig_not_dec Einhab Ebound.
+  pose proof (is_upper_bound_closed E sig_forall_dec sig_not_dec Einhab Ebound).
+  destruct (is_upper_bound_glb
+              E sig_not_dec sig_forall_dec Einhab Ebound); simpl in H.
+  exists x. exact H.
+Qed.
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index f734b47fb5..f03b0ccea3 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -8,6 +8,13 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(* This file continues Rdefinitions, with more properties of the
+   classical reals, including the existence of least upper bounds
+   for non-empty and bounded subsets.
+   The name "Raxioms" and its contents are kept for backward compatibility,
+   when the classical reals were axiomatized. Otherwise we would
+   have merged this file into RIneq. *)
+
 (*********************************************************)
 (**    Lifts of basic operations for classical reals     *)
 (*********************************************************)
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index c71baf42f5..b1ce8109ca 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -8,7 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(* Classical quotient of the constructive Cauchy real numbers. *)
+(* Classical quotient of the constructive Cauchy real numbers.
+   This file contains the definition of the classical real numbers
+   type R, its algebraic operations, its order and the proof that
+   it is total, and the proof that R is archimedean (up).
+   It also defines IZR, the ring morphism from Z to R. *)
 
 Require Export ZArith_base.
 Require Import QArith_base.
@@ -160,7 +164,7 @@ Proof.
   - left. left. rewrite RbaseSymbolsImpl.Rlt_def.
     apply Rlt_forget. exact r.
   - destruct (Rlt_lpo_dec (Rrepr r2) (Rrepr r1) sig_forall_dec).
-    + right. rewrite RbaseSymbolsImpl.Rlt_def. apply Rlt_forget. exact r.
+    + right. rewrite RbaseSymbolsImpl.Rlt_def. apply Rlt_forget. exact r0.
     + left. right. apply Rquot1. split; assumption.
 Qed.