diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-22 17:50:26 +0200 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-22 18:07:02 +0200 |
commit | 5a0dd47fc215f2cb077f747eb888377718701d41 (patch) | |
tree | 8ddc006dea193f4c67bc8bdba6cd4ddf92c183ba | |
parent | 923aa7e32c2e388dde1b6ae66c55d74d02bed2ab (diff) |
Remove some uses of excluded middle.
-rw-r--r-- | theories/Reals/RiemannInt.v | 22 | ||||
-rw-r--r-- | theories/Reals/Rtrigo.v | 1 | ||||
-rw-r--r-- | theories/Reals/Rtrigo1.v | 1 |
3 files changed, 11 insertions, 13 deletions
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 87f5c8e26..cdd3b96c0 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -12,8 +12,6 @@ Require Import SeqSeries. Require Import Ranalysis_reg. Require Import Rbase. Require Import RiemannInt_SF. -Require Import Classical_Prop. -Require Import Classical_Pred_Type. Require Import Max. Local Open Scope R_scope. @@ -511,18 +509,20 @@ Proof. intro; elim H4; clear H4; intros; exists (mkposreal _ H4); split. apply H5. unfold is_lub in p; elim p; intros; unfold is_upper_bound in H6; - set (D := Rabs (x0 - y)); elim (classic (exists y : R, D < y /\ E y)); - intro. + set (D := Rabs (x0 - y)). + assert (H11: ((exists y : R, D < y /\ E y) \/ (forall y : R, not (D < y /\ E y)) -> False) -> False). + clear; intros H; apply H. + right; intros y0 H0; apply H. + left; now exists y0. + apply Rnot_le_lt; intros H30. + apply H11; clear H11; intros H11. + revert H30; apply Rlt_not_le. + destruct H11 as [H11|H12]. elim H11; intros; elim H12; clear H12; intros; unfold E in H13; elim H13; intros; apply H15; assumption. - assert (H12 := not_ex_all_not _ (fun y:R => D < y /\ E y) H11); - assert (H13 : is_upper_bound E D). + assert (H13 : is_upper_bound E D). unfold is_upper_bound; intros; assert (H14 := H12 x1); - elim (not_and_or (D < x1) (E x1) H14); intro. - case (Rle_dec x1 D); intro. - assumption. - elim H15; auto with real. - elim H15; assumption. + apply Rnot_lt_le; contradict H14; now split. assert (H14 := H7 _ H13); elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H10)). unfold is_lub in p; unfold is_upper_bound in p; elim p; clear p; intros; split. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 32c4d7d38..f9cbb6e9d 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -16,7 +16,6 @@ Require Export Cos_rel. Require Export Cos_plus. Require Import ZArith_base. Require Import Zcomplements. -Require Import Classical_Prop. Require Import Fourier. Require Import Ranalysis1. Require Import Rsqrt_def. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index 672eae678..0e8beaad3 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -16,7 +16,6 @@ Require Export Cos_rel. Require Export Cos_plus. Require Import ZArith_base. Require Import Zcomplements. -Require Import Classical_Prop. Require Import Fourier. Require Import Ranalysis1. Require Import Rsqrt_def. |