Merge PR #13872: Make lemmas from Reals opaque whenever possible.

Reviewed-by: thery

9 files changed, 49 insertions, 77 deletions

diff --git a/theories/Reals/Abstract/ConstructiveReals.v b/theories/Reals/Abstract/ConstructiveReals.v
index 60fad8795a..5a599587d0 100644
--- a/theories/Reals/Abstract/ConstructiveReals.v
+++ b/theories/Reals/Abstract/ConstructiveReals.v
@@ -285,14 +285,14 @@ Lemma CRlt_trans : forall {R : ConstructiveReals} (x y z : CRcarrier R),
 Proof.
   intros. apply (CRlt_le_trans _ y _ H).
   apply CRlt_asym. exact H0.
-Defined.
+Qed.
 
 Lemma CRlt_trans_flip : forall {R : ConstructiveReals} (x y z : CRcarrier R),
     y < z -> x < y -> x < z.
 Proof.
   intros. apply (CRlt_le_trans _ y). exact H0.
   apply CRlt_asym. exact H.
-Defined.
+Qed.
 
 Lemma CReq_refl : forall {R : ConstructiveReals} (x : CRcarrier R),
     x == x.
diff --git a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
index 53b5aca38c..6ed5845440 100644
--- a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
+++ b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v
@@ -232,7 +232,7 @@ Proof.
   apply CRplus_lt_compat_l.
   apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CRle_refl.
   apply CR_of_Q_lt. exact H.
-Defined.
+Qed.
 
 Lemma CRplus_neg_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Q),
     Qlt q 0 -> CRlt R (CRplus R x (CR_of_Q R q)) x.
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index 069a1292cd..9a00408de3 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -112,7 +112,7 @@ Proof.
       pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r;
 	apply Rplus_le_compat_l; left; apply H
       | apply H1 ].
-Defined.
+Qed.
 
 Lemma Alembert_C2 :
   forall An:nat -> R,
@@ -330,7 +330,7 @@ Proof.
   rewrite <- Rabs_Ropp; apply RRle_abs.
   rewrite double; pattern (Rabs (An n)) at 1; rewrite <- Rplus_0_r;
     apply Rplus_lt_compat_l; apply Rabs_pos_lt; apply H.
-Defined.
+Qed.
 
 Lemma AlembertC3_step1 :
   forall (An:nat -> R) (x:R),
@@ -374,7 +374,7 @@ Proof.
     [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ].
   intro; unfold Bn; apply prod_neq_R0;
     [ apply H0 | apply pow_nonzero; assumption ].
-Defined.
+Qed.
 
 Lemma AlembertC3_step2 :
   forall (An:nat -> R) (x:R), x = 0 -> { l:R | Pser An x l }.
@@ -405,7 +405,7 @@ Proof.
   cut (x <> 0).
   intro; apply AlembertC3_step1; assumption.
   red; intro; rewrite H1 in Hgt; elim (Rlt_irrefl _ Hgt).
-Defined.
+Qed.
 
 Lemma Alembert_C4 :
   forall (An:nat -> R) (k:R),
diff --git a/theories/Reals/Cauchy/ConstructiveCauchyReals.v b/theories/Reals/Cauchy/ConstructiveCauchyReals.v
index 8a11c155ce..4fb3846abc 100644
--- a/theories/Reals/Cauchy/ConstructiveCauchyReals.v
+++ b/theories/Reals/Cauchy/ConstructiveCauchyReals.v
@@ -320,7 +320,6 @@ Proof.
   - contradiction.
   - exact Hxltz.
 Qed.
-(* Todo: this was Defined. Why *)
 
 Lemma CReal_lt_le_trans : forall x y z : CReal,
     x < y -> y <= z -> x < z.
@@ -330,7 +329,6 @@ Proof.
   - exact Hxltz.
   - contradiction.
 Qed.
-(* Todo: this was Defined. Why *)
 
 Lemma CReal_le_trans : forall x y z : CReal,
     x <= y -> y <= z -> x <= z.
@@ -347,7 +345,6 @@ Proof.
   apply (CReal_lt_le_trans _ y _ Hxlty).
   apply CRealLt_asym; exact Hyltz.
 Qed.
-(* Todo: this was Defined. Why *)
 
 Lemma CRealEq_trans : forall x y z : CReal,
     CRealEq x y -> CRealEq y z -> CRealEq x z.
diff --git a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
index a180e13444..bc45868244 100644
--- a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
+++ b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
@@ -733,13 +733,11 @@ Definition CReal_inv_pos (x : CReal) (Hxpos : 0 < x) : CReal :=
   bound := CReal_inv_pos_bound x Hxpos
 |}.
 
-(* ToDo: make this more obviously computing *)
-
 Definition CReal_neg_lt_pos : forall x : CReal, x < 0 -> 0 < -x.
 Proof.
   intros x [n nmaj]. exists n.
-  apply (Qlt_le_trans _ _ _ nmaj). destruct x. simpl.
-  unfold Qminus. rewrite Qplus_0_l, Qplus_0_r. apply Qle_refl.
+  simpl in *. unfold CReal_opp_seq, Qminus.
+  abstract now rewrite Qplus_0_r, <- (Qplus_0_l (- seq x n)).
 Defined.
 
 Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal
diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v
index 70d2861d17..c2b60e6478 100644
--- a/theories/Reals/Cauchy/ConstructiveRcomplete.v
+++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v
@@ -75,7 +75,7 @@ Proof.
     rewrite inject_Q_plus, (opp_inject_Q 2).
     ring_simplify. exact H.
     rewrite Qinv_plus_distr. reflexivity.
-Defined.
+Qed.
 
 (* ToDo: Move to ConstructiveCauchyAbs.v *)
 Lemma Qabs_Rabs : forall q : Q,
@@ -688,21 +688,7 @@ Proof.
   exact (a i j H0 H1).
   exists l. intros p. destruct (cv p).
   exists x. exact c.
-Defined.
-
-(* ToDO: Belongs into sumbool.v *)
-Section connectives.
-
-  Variables A B : Prop.
-
-  Hypothesis H1 : {A} + {~A}.
-  Hypothesis H2 : {B} + {~B}.
-
-  Definition sumbool_or_not_or : {A \/ B} + {~(A \/ B)}.
-    case H1; case H2; tauto.
-  Defined.
-
-End connectives.
+Qed.
 
 Lemma Qnot_le_iff_lt: forall x y : Q,
   ~ (x <= y)%Q <-> (y < x)%Q.
@@ -740,13 +726,11 @@ Proof.
       clear maj. right. exists n.
       apply H0.
   - clear H0 H. intro n.
-    apply sumbool_or_not_or.
-    + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq b n - seq a n)%Q).
-      * left; assumption.
-      * right; apply Qle_not_lt; assumption.
-    + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq d n - seq c n)%Q).
-      * left; assumption.
-      * right; apply Qle_not_lt; assumption.
+    destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq b n - seq a n)%Q) as [H1|H1].
+    + now left; left.
+    + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq d n - seq c n)%Q) as [H2|H2].
+      * now left; right.
+      * now right; intros [H3|H3]; apply Qle_not_lt with (2 := H3).
 Qed.
 
 Definition CRealConstructive : ConstructiveReals
diff --git a/theories/Reals/ClassicalDedekindReals.v b/theories/Reals/ClassicalDedekindReals.v
index 500838ed26..0736b09761 100644
--- a/theories/Reals/ClassicalDedekindReals.v
+++ b/theories/Reals/ClassicalDedekindReals.v
@@ -233,17 +233,12 @@ Qed.
 
 (** *** Conversion from CReal to DReal *)
 
-Definition DRealAbstr : CReal -> DReal.
+Lemma DRealAbstr_aux :
+  forall x H,
+  isLowerCut (fun q : Q =>
+    if sig_forall_dec (fun n : nat => seq x (- Z.of_nat n) <= q + 2 ^ (- Z.of_nat n)) (H q)
+    then true else false).
 Proof.
-  intro x.
-  assert (forall (q : Q) (n : nat),
-   {(fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n} +
-   {~ (fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n}).
-  { intros. destruct (Qlt_le_dec (q + (2^-Z.of_nat n)) (seq x (-Z.of_nat n))).
-    right. apply (Qlt_not_le _ _ q0). left. exact q0. }
-
-  exists (fun q:Q => if sig_forall_dec (fun n:nat => Qle (seq x (-Z.of_nat n)) (q + (2^-Z.of_nat n))) (H q)
-             then true else false).
   repeat split.
   - intros.
     destruct (sig_forall_dec (fun n : nat => (seq x (-Z.of_nat n) <= q + (2^-Z.of_nat n))%Q)
@@ -303,6 +298,20 @@ Proof.
       apply (Qmult_le_l _ _ 2) in q0. field_simplify in q0.
       apply (Qplus_le_l _ _ (-seq x (-Z.of_nat n))) in q0. ring_simplify in q0.
       contradiction. reflexivity.
+Qed.
+
+Definition DRealAbstr : CReal -> DReal.
+Proof.
+  intro x.
+  assert (forall (q : Q) (n : nat),
+   {(fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n} +
+   {~ (fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n}).
+  { intros. destruct (Qlt_le_dec (q + (2^-Z.of_nat n)) (seq x (-Z.of_nat n))).
+    right. apply (Qlt_not_le _ _ q0). left. exact q0. }
+
+  exists (fun q:Q => if sig_forall_dec (fun n:nat => Qle (seq x (-Z.of_nat n)) (q + (2^-Z.of_nat n))) (H q)
+             then true else false).
+  apply DRealAbstr_aux.
 Defined.
 
 (** *** Conversion from DReal to CReal *)
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index 6692119738..6107775003 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -170,7 +170,7 @@ Proof.
   reg.
   exists H5; symmetry ; reg; rewrite <- H3; rewrite <- H4; reflexivity.
   assumption.
-Defined.
+Qed.
 
 (**********)
 Lemma antiderivative_P1 :
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index 7f5a859c81..2004f40f00 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -41,9 +41,13 @@ Proof.
   red; intro; rewrite H0 in H; elim (lt_irrefl _ H).
 Qed.
 
-Lemma exist_exp0 : { l:R | exp_in 0 l }.
+(* Value of [exp 0] *)
+Lemma exp_0 : exp 0 = 1.
 Proof.
-  exists 1.
+  cut (exp_in 0 1).
+  cut (exp_in 0 (exp 0)).
+  apply uniqueness_sum.
+  exact (proj2_sig (exist_exp 0)).
   unfold exp_in; unfold infinite_sum; intros.
   exists 0%nat.
   intros; replace (sum_f_R0 (fun i:nat => / INR (fact i) * 0 ^ i) n) with 1.
@@ -56,18 +60,6 @@ Proof.
   simpl.
   ring.
   unfold ge; apply le_O_n.
-Defined.
-
-(* Value of [exp 0] *)
-Lemma exp_0 : exp 0 = 1.
-Proof.
-  cut (exp_in 0 (exp 0)).
-  cut (exp_in 0 1).
-  unfold exp_in; intros; eapply uniqueness_sum.
-  apply H0.
-  apply H.
-  exact (proj2_sig exist_exp0).
-  exact (proj2_sig (exist_exp 0)).
 Qed.
 
 (*****************************************)
@@ -384,9 +376,14 @@ Proof.
   intros; ring.
 Qed.
 
-Lemma exist_cos0 : { l:R | cos_in 0 l }.
+(* Value of [cos 0] *)
+Lemma cos_0 : cos 0 = 1.
 Proof.
-  exists 1.
+  cut (cos_in 0 1).
+  cut (cos_in 0 (cos 0)).
+  apply uniqueness_sum.
+  rewrite <- Rsqr_0 at 1.
+  exact (proj2_sig (exist_cos (Rsqr 0))).
   unfold cos_in; unfold infinite_sum; intros; exists 0%nat.
   intros.
   unfold R_dist.
@@ -400,17 +397,4 @@ Proof.
   rewrite Rplus_0_r.
   apply Hrecn; unfold ge; apply le_O_n.
   simpl; ring.
-Defined.
-
-(* Value of [cos 0] *)
-Lemma cos_0 : cos 0 = 1.
-Proof.
-  cut (cos_in 0 (cos 0)).
-  cut (cos_in 0 1).
-  unfold cos_in; intros; eapply uniqueness_sum.
-  apply H0.
-  apply H.
-  exact (proj2_sig exist_cos0).
-  assert (H := proj2_sig (exist_cos (Rsqr 0))); unfold cos;
-    pattern 0 at 1; replace 0 with (Rsqr 0); [ exact H | apply Rsqr_0 ].
 Qed.