Removed SeqProp's dependency on Classical.

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

2 files changed, 103 insertions, 159 deletions

diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 15f02c69b..1ed6b03c5 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -100,12 +100,9 @@ Section sequence.
   Qed.
 
 (*********)
-  Lemma Un_cv_crit : Un_growing -> bound EUn ->  exists l : R, Un_cv l.
+  Lemma Un_cv_crit_lub : Un_growing -> forall l, is_lub EUn l -> Un_cv l.
   Proof.
-    intros Hug Heub.
-    destruct (completeness EUn Heub EUn_noempty) as (l, H).
-    exists l.
-    intros eps Heps.
+    intros Hug l H eps Heps.
 
     cut (exists N, Un N > l - eps).
     intros (N, H3).
@@ -263,6 +260,15 @@ Section sequence.
   Qed.
 
 (*********)
+  Lemma Un_cv_crit : Un_growing -> bound EUn ->  exists l : R, Un_cv l.
+  Proof.
+    intros Hug Heub.
+    exists (projT1 (completeness EUn Heub EUn_noempty)).
+    destruct (completeness EUn Heub EUn_noempty) as (l, H).
+    now apply Un_cv_crit_lub.
+  Qed.
+
+(*********)
   Lemma finite_greater :
     forall N:nat,  exists M : R, (forall n:nat, (n <= N)%nat -> Un n <= M).
   Proof.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index a84a1cc97..e53e9cc6d 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -11,7 +11,6 @@
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
-Require Import Classical.
 Require Import Max.
 Open Local Scope R_scope.
 
@@ -29,31 +28,10 @@ Definition has_lb (Un:nat -> R) : Prop := bound (EUn (opp_seq Un)).
 Lemma growing_cv :
   forall Un:nat -> R, Un_growing Un -> has_ub Un -> { l:R | Un_cv Un l }.
 Proof.
-  unfold Un_growing, Un_cv in |- *; intros;
-    destruct (completeness (EUn Un) H0 (EUn_noempty Un)) as [x [H2 H3]].
-  exists x; intros eps H1.
-  unfold is_upper_bound in H2, H3.
-  assert (H5 : forall n:nat, Un n <= x).
-  intro n; apply (H2 (Un n) (Un_in_EUn Un n)).
-  cut (exists N : nat, x - eps < Un N).
-  intro H6; destruct H6 as [N H6]; exists N.
-  intros n H7; unfold R_dist in |- *; apply (Rabs_def1 (Un n - x) eps).
-  unfold Rgt in H1.
-  apply (Rle_lt_trans (Un n - x) 0 eps (Rle_minus (Un n) x (H5 n)) H1).
-  fold Un_growing in H; generalize (growing_prop Un n N H H7); intro H8.
-  generalize
-    (Rlt_le_trans (x - eps) (Un N) (Un n) H6 (Rge_le (Un n) (Un N) H8));
-    intro H9; generalize (Rplus_lt_compat_l (- x) (x - eps) (Un n) H9);
-      unfold Rminus in |- *; rewrite <- (Rplus_assoc (- x) x (- eps));
-        rewrite (Rplus_comm (- x) (Un n)); fold (Un n - x) in |- *;
-          rewrite Rplus_opp_l; rewrite (let (H1, H2) := Rplus_ne (- eps) in H2);
-            trivial.
-  cut (~ (forall N:nat, Un N <= x - eps)).
-  intro H6; apply (not_all_not_ex nat (fun N:nat => x - eps < Un N)).
-  intro H7; apply H6; intro N; apply Rnot_lt_le; apply H7.
-  intro H7; generalize (Un_bound_imp Un (x - eps) H7); intro H8;
-    unfold is_upper_bound in H8; generalize (H3 (x - eps) H8);
-      apply Rlt_not_le; apply tech_Rgt_minus; exact H1.
+  intros Un Hug Heub.
+  exists (projT1 (completeness (EUn Un) Heub (EUn_noempty Un))).
+  destruct (completeness _ Heub (EUn_noempty Un)) as (l, H).
+  now apply Un_cv_crit_lub.
 Qed.
 
 Lemma decreasing_growing :
@@ -518,68 +496,77 @@ Lemma approx_maj :
   forall (Un:nat -> R) (pr:has_ub Un) (eps:R),
     0 < eps ->  exists k : nat, Rabs (lub Un pr - Un k) < eps.
 Proof.
-  intros.
-  set (P := fun k:nat => Rabs (lub Un pr - Un k) < eps).
-  unfold P in |- *.
-  cut
-    ((exists k : nat, P k) ->
-      exists k : nat, Rabs (lub Un pr - Un k) < eps).
-  intros.
-  apply H0.
-  apply not_all_not_ex.
-  red in |- *; intro.
-  2: unfold P in |- *; trivial.
-  unfold P in H1.
-  cut (forall n:nat, Rabs (lub Un pr - Un n) >= eps).
-  intro.
-  cut (is_lub (EUn Un) (lub Un pr)).
-  intro.
-  unfold is_lub in H3.
-  unfold is_upper_bound in H3.
-  elim H3; intros.
-  cut (forall n:nat, eps <= lub Un pr - Un n).
-  intro.
-  cut (forall n:nat, Un n <= lub Un pr - eps).
-  intro.
-  cut (forall x:R, EUn Un x -> x <= lub Un pr - eps).
-  intro.
-  assert (H9 := H5 (lub Un pr - eps) H8).
-  cut (eps <= 0).
-  intro.
-  elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H H10)).
-  apply Rplus_le_reg_l with (lub Un pr - eps).
-  rewrite Rplus_0_r.
-  replace (lub Un pr - eps + eps) with (lub Un pr);
-  [ assumption | ring ].
-  intros.
-  unfold EUn in H8.
-  elim H8; intros.
-  rewrite H9; apply H7.
-  intro.
-  assert (H7 := H6 n).
-  apply Rplus_le_reg_l with (eps - Un n).
-  replace (eps - Un n + Un n) with eps.
-  replace (eps - Un n + (lub Un pr - eps)) with (lub Un pr - Un n).
-  assumption.
-  ring.
-  ring.
-  intro.
-  assert (H6 := H2 n).
-  rewrite Rabs_right in H6.
-  apply Rge_le.
-  assumption.
-  apply Rle_ge.
-  apply Rplus_le_reg_l with (Un n).
-  rewrite Rplus_0_r;
-    replace (Un n + (lub Un pr - Un n)) with (lub Un pr);
-    [ apply H4 | ring ].
-  exists n; reflexivity.
-  unfold lub in |- *.
-  case (ub_to_lub Un pr).
-  trivial.
-  intro.
-  assert (H2 := H1 n).
-  apply not_Rlt; assumption.
+  intros Un pr.
+  pose (Vn := fix aux n := match n with S n' => if Rle_lt_dec (aux n') (Un n) then Un n else aux n' | O => Un O end).
+  pose (In := fix aux n := match n with S n' => if Rle_lt_dec (Vn n) (Un n) then n else aux n' | O => O end).
+
+  assert (VUI: forall n, Vn n = Un (In n)).
+  induction n.
+  easy.
+  simpl.
+  destruct (Rle_lt_dec (Vn n) (Un (S n))) as [H1|H1].
+  destruct (Rle_lt_dec (Un (S n)) (Un (S n))) as [H2|H2].
+  easy.
+  elim (Rlt_irrefl _ H2).
+  destruct (Rle_lt_dec (Vn n) (Un (S n))) as [H2|H2].
+  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 H1)).
+  exact IHn.
+
+  assert (HubV : has_ub Vn).
+  destruct pr as (ub, Hub).
+  exists ub.
+  intros x (n, Hn).
+  rewrite Hn, VUI.
+  apply Hub.
+  now exists (In n).
+
+  assert (HgrV : Un_growing Vn).
+  intros n.
+  induction n.
+  simpl.
+  destruct (Rle_lt_dec (Un O) (Un 1%nat)) as [H|_].
+  exact H.
+  apply Rle_refl.
+  simpl.
+  destruct (Rle_lt_dec (Vn n) (Un (S n))) as [H1|H1].
+  destruct (Rle_lt_dec (Un (S n)) (Un (S (S n)))) as [H2|H2].
+  exact H2.
+  apply Rle_refl.
+  destruct (Rle_lt_dec (Vn n) (Un (S (S n)))) as [H2|H2].
+  exact H2.
+  apply Rle_refl.
+
+  destruct (ub_to_lub Vn HubV) as (l, Hl).
+  unfold lub.
+  destruct (ub_to_lub Un pr) as (l', Hl').
+  replace l' with l.
+  intros eps Heps.
+  destruct (Un_cv_crit_lub Vn HgrV l Hl eps Heps) as (n, Hn).
+  exists (In n).
+  rewrite <- VUI.
+  rewrite Rabs_minus_sym.
+  apply Hn.
+  apply le_refl.
+
+  apply Rle_antisym.
+  apply Hl.
+  intros n (k, Hk).
+  rewrite Hk, VUI.
+  apply Hl'.
+  now exists (In k).
+  apply Hl'.
+  intros n (k, Hk).
+  rewrite Hk.
+  apply Rle_trans with (Vn k).
+  clear.
+  induction k.
+  apply Rle_refl.
+  simpl.
+  destruct (Rle_lt_dec (Vn k) (Un (S k))) as [H|H].
+  apply Rle_refl.
+  now apply Rlt_le.
+  apply Hl.
+  now exists k.
 Qed.
 
 (**********)
@@ -587,72 +574,23 @@ Lemma approx_min :
   forall (Un:nat -> R) (pr:has_lb Un) (eps:R),
     0 < eps ->  exists k : nat, Rabs (glb Un pr - Un k) < eps.
 Proof.
-  intros.
-  set (P := fun k:nat => Rabs (glb Un pr - Un k) < eps).
-  unfold P in |- *.
-  cut
-    ((exists k : nat, P k) ->
-      exists k : nat, Rabs (glb Un pr - Un k) < eps).
-  intros.
-  apply H0.
-  apply not_all_not_ex.
-  red in |- *; intro.
-  2: unfold P in |- *; trivial.
-  unfold P in H1.
-  cut (forall n:nat, Rabs (glb Un pr - Un n) >= eps).
-  intro.
-  cut (is_lub (EUn (opp_seq Un)) (- glb Un pr)).
-  intro.
-  unfold is_lub in H3.
-  unfold is_upper_bound in H3.
-  elim H3; intros.
-  cut (forall n:nat, eps <= Un n - glb Un pr).
-  intro.
-  cut (forall n:nat, opp_seq Un n <= - glb Un pr - eps).
-  intro.
-  cut (forall x:R, EUn (opp_seq Un) x -> x <= - glb Un pr - eps).
-  intro.
-  assert (H9 := H5 (- glb Un pr - eps) H8).
-  cut (eps <= 0).
-  intro.
-  elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H H10)).
-  apply Rplus_le_reg_l with (- glb Un pr - eps).
-  rewrite Rplus_0_r.
-  replace (- glb Un pr - eps + eps) with (- glb Un pr);
-  [ assumption | ring ].
-  intros.
-  unfold EUn in H8.
-  elim H8; intros.
-  rewrite H9; apply H7.
-  intro.
-  assert (H7 := H6 n).
-  unfold opp_seq in |- *.
-  apply Rplus_le_reg_l with (eps + Un n).
-  replace (eps + Un n + - Un n) with eps.
-  replace (eps + Un n + (- glb Un pr - eps)) with (Un n - glb Un pr).
-  assumption.
-  ring.
-  ring.
-  intro.
-  assert (H6 := H2 n).
-  rewrite Rabs_left1 in H6.
-  apply Rge_le.
-  replace (Un n - glb Un pr) with (- (glb Un pr - Un n));
-  [ assumption | ring ].
-  apply Rplus_le_reg_l with (- glb Un pr).
-  rewrite Rplus_0_r;
-    replace (- glb Un pr + (glb Un pr - Un n)) with (- Un n).
-  apply H4.
-  exists n; reflexivity.
-  ring.
-  unfold glb in |- *.
-  case (lb_to_glb Un pr); simpl.
-  intro.
-  rewrite Ropp_involutive.
-  trivial.
-  intro.
-  assert (H2 := H1 n).
-  apply not_Rlt; assumption.
+  intros Un pr.
+  unfold glb.
+  destruct lb_to_glb as (lb, Hlb).
+  intros eps Heps.
+  destruct (approx_maj _ pr eps Heps) as (n, Hn).
+  exists n.
+  unfold Rminus.
+  rewrite <- Ropp_plus_distr, Rabs_Ropp.
+  replace lb with (lub (opp_seq Un) pr).
+  now rewrite <- (Ropp_involutive (Un n)).
+  unfold lub.
+  destruct ub_to_lub as (ub, Hub).
+  apply Rle_antisym.
+  apply Hub.
+  apply Hlb.
+  apply Hlb.
+  apply Hub.
 Qed.
 
 (** Unicity of limit for convergent sequences *)