aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals')
-rw-r--r--theories/Reals/RIneq.v16
-rw-r--r--theories/Reals/Rbasic_fun.v46
-rw-r--r--theories/Reals/Rderiv.v2
-rw-r--r--theories/Reals/Rfunctions.v4
-rw-r--r--theories/Reals/Rlimit.v4
-rw-r--r--theories/Reals/Rlogic.v4
-rw-r--r--theories/Reals/Rseries.v4
7 files changed, 40 insertions, 40 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 0fe8bb176..2b6af10ec 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1283,8 +1283,8 @@ Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
Proof.
intros z x y H H0.
case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0.
- rewrite Eq0 in H0; elimtype False; apply (Rlt_irrefl (z * y)); auto.
- generalize (Rmult_lt_compat_l z y x H Eq0); intro; elimtype False;
+ rewrite Eq0 in H0; exfalso; apply (Rlt_irrefl (z * y)); auto.
+ generalize (Rmult_lt_compat_l z y x H Eq0); intro; exfalso;
generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1);
intro; apply (Rlt_irrefl (z * x)); auto.
Qed.
@@ -1619,11 +1619,11 @@ Hint Resolve pos_INR: real.
Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat.
Proof.
double induction n m; intros.
- simpl in |- *; elimtype False; apply (Rlt_irrefl 0); auto.
+ simpl in |- *; exfalso; apply (Rlt_irrefl 0); auto.
auto with arith.
generalize (pos_INR (S n0)); intro; cut (INR 0 = 0);
[ intro H2; rewrite H2 in H0; idtac | simpl in |- *; trivial ].
- generalize (Rle_lt_trans 0 (INR (S n0)) 0 H1 H0); intro; elimtype False;
+ generalize (Rle_lt_trans 0 (INR (S n0)) 0 H1 H0); intro; exfalso;
apply (Rlt_irrefl 0); auto.
do 2 rewrite S_INR in H1; cut (INR n1 < INR n0).
intro H2; generalize (H0 n0 H2); intro; auto with arith.
@@ -1665,7 +1665,7 @@ Proof.
intros n m H; case (le_or_lt n m); intros H1.
case (le_lt_or_eq _ _ H1); intros H2.
apply Rlt_dichotomy_converse; auto with real.
- elimtype False; auto.
+ exfalso; auto.
apply sym_not_eq; apply Rlt_dichotomy_converse; auto with real.
Qed.
Hint Resolve not_INR: real.
@@ -1675,10 +1675,10 @@ Proof.
intros; case (le_or_lt n m); intros H1.
case (le_lt_or_eq _ _ H1); intros H2; auto.
cut (n <> m).
- intro H3; generalize (not_INR n m H3); intro H4; elimtype False; auto.
+ intro H3; generalize (not_INR n m H3); intro H4; exfalso; auto.
omega.
symmetry in |- *; cut (m <> n).
- intro H3; generalize (not_INR m n H3); intro H4; elimtype False; auto.
+ intro H3; generalize (not_INR m n H3); intro H4; exfalso; auto.
omega.
Qed.
Hint Resolve INR_eq: real.
@@ -1884,7 +1884,7 @@ Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m.
Proof.
intros m n H; cut (m <= n)%Z.
intro H0; elim (IZR_le m n H0); intro; auto.
- generalize (eq_IZR m n H1); intro; elimtype False; omega.
+ generalize (eq_IZR m n H1); intro; exfalso; omega.
omega.
Qed.
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index f5570286d..7588020c5 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -294,7 +294,7 @@ Definition Rabs r : R :=
Lemma Rabs_R0 : Rabs 0 = 0.
Proof.
unfold Rabs in |- *; case (Rcase_abs 0); auto; intro.
- generalize (Rlt_irrefl 0); intro; elimtype False; auto.
+ generalize (Rlt_irrefl 0); intro; exfalso; auto.
Qed.
Lemma Rabs_R1 : Rabs 1 = 1.
@@ -356,7 +356,7 @@ Definition RRle_abs := Rle_abs.
Lemma Rabs_pos_eq : forall x:R, 0 <= x -> Rabs x = x.
Proof.
intros; unfold Rabs in |- *; case (Rcase_abs x); intro;
- [ generalize (Rgt_not_le 0 x r); intro; elimtype False; auto | trivial ].
+ [ generalize (Rgt_not_le 0 x r); intro; exfalso; auto | trivial ].
Qed.
(*********)
@@ -370,7 +370,7 @@ Lemma Rabs_pos_lt : forall x:R, x <> 0 -> 0 < Rabs x.
Proof.
intros; generalize (Rabs_pos x); intro; unfold Rle in H0; elim H0; intro;
auto.
- elimtype False; clear H0; elim H; clear H; generalize H1; unfold Rabs in |- *;
+ exfalso; clear H0; elim H; clear H; generalize H1; unfold Rabs in |- *;
case (Rcase_abs x); intros; auto.
clear r H1; generalize (Rplus_eq_compat_l x 0 (- x) H0);
rewrite (let (H1, H2) := Rplus_ne x in H1); rewrite (Rplus_opp_r x);
@@ -383,14 +383,14 @@ Proof.
intros; unfold Rabs in |- *; case (Rcase_abs (x - y));
case (Rcase_abs (y - x)); intros.
generalize (Rminus_lt y x r); generalize (Rminus_lt x y r0); intros;
- generalize (Rlt_asym x y H); intro; elimtype False;
+ generalize (Rlt_asym x y H); intro; exfalso;
auto.
rewrite (Ropp_minus_distr x y); trivial.
rewrite (Ropp_minus_distr y x); trivial.
unfold Rge in r, r0; elim r; elim r0; intros; clear r r0.
generalize (Ropp_lt_gt_0_contravar (x - y) H); rewrite (Ropp_minus_distr x y);
intro; unfold Rgt in H0; generalize (Rlt_asym 0 (y - x) H0);
- intro; elimtype False; auto.
+ intro; exfalso; auto.
rewrite (Rminus_diag_uniq x y H); trivial.
rewrite (Rminus_diag_uniq y x H0); trivial.
rewrite (Rminus_diag_uniq y x H0); trivial.
@@ -403,46 +403,46 @@ Proof.
case (Rcase_abs y); intros; auto.
generalize (Rmult_lt_gt_compat_neg_l y x 0 r r0); intro;
rewrite (Rmult_0_r y) in H; generalize (Rlt_asym (x * y) 0 r1);
- intro; unfold Rgt in H; elimtype False; rewrite (Rmult_comm y x) in H;
+ intro; unfold Rgt in H; exfalso; rewrite (Rmult_comm y x) in H;
auto.
rewrite (Ropp_mult_distr_l_reverse x y); trivial.
rewrite (Rmult_comm x (- y)); rewrite (Ropp_mult_distr_l_reverse y x);
rewrite (Rmult_comm x y); trivial.
unfold Rge in r, r0; elim r; elim r0; clear r r0; intros; unfold Rgt in H, H0.
generalize (Rmult_lt_compat_l x 0 y H H0); intro; rewrite (Rmult_0_r x) in H1;
- generalize (Rlt_asym (x * y) 0 r1); intro; elimtype False;
+ generalize (Rlt_asym (x * y) 0 r1); intro; exfalso;
auto.
rewrite H in r1; rewrite (Rmult_0_l y) in r1; generalize (Rlt_irrefl 0);
- intro; elimtype False; auto.
+ intro; exfalso; auto.
rewrite H0 in r1; rewrite (Rmult_0_r x) in r1; generalize (Rlt_irrefl 0);
- intro; elimtype False; auto.
+ intro; exfalso; auto.
rewrite H0 in r1; rewrite (Rmult_0_r x) in r1; generalize (Rlt_irrefl 0);
- intro; elimtype False; auto.
+ intro; exfalso; auto.
rewrite (Rmult_opp_opp x y); trivial.
unfold Rge in r, r1; elim r; elim r1; clear r r1; intros; unfold Rgt in H0, H.
generalize (Rmult_lt_compat_l y x 0 H0 r0); intro;
rewrite (Rmult_0_r y) in H1; rewrite (Rmult_comm y x) in H1;
- generalize (Rlt_asym (x * y) 0 H1); intro; elimtype False;
+ generalize (Rlt_asym (x * y) 0 H1); intro; exfalso;
auto.
generalize (Rlt_dichotomy_converse x 0 (or_introl (x > 0) r0));
generalize (Rlt_dichotomy_converse y 0 (or_intror (y < 0) H0));
intros; generalize (Rmult_integral x y H); intro;
- elim H3; intro; elimtype False; auto.
+ elim H3; intro; exfalso; auto.
rewrite H0 in H; rewrite (Rmult_0_r x) in H; unfold Rgt in H;
- generalize (Rlt_irrefl 0); intro; elimtype False;
+ generalize (Rlt_irrefl 0); intro; exfalso;
auto.
rewrite H0; rewrite (Rmult_0_r x); rewrite (Rmult_0_r (- x)); trivial.
unfold Rge in r0, r1; elim r0; elim r1; clear r0 r1; intros;
unfold Rgt in H0, H.
generalize (Rmult_lt_compat_l x y 0 H0 r); intro; rewrite (Rmult_0_r x) in H1;
- generalize (Rlt_asym (x * y) 0 H1); intro; elimtype False;
+ generalize (Rlt_asym (x * y) 0 H1); intro; exfalso;
auto.
generalize (Rlt_dichotomy_converse y 0 (or_introl (y > 0) r));
generalize (Rlt_dichotomy_converse 0 x (or_introl (0 > x) H0));
intros; generalize (Rmult_integral x y H); intro;
- elim H3; intro; elimtype False; auto.
+ elim H3; intro; exfalso; auto.
rewrite H0 in H; rewrite (Rmult_0_l y) in H; unfold Rgt in H;
- generalize (Rlt_irrefl 0); intro; elimtype False;
+ generalize (Rlt_irrefl 0); intro; exfalso;
auto.
rewrite H0; rewrite (Rmult_0_l y); rewrite (Rmult_0_l (- y)); trivial.
Qed.
@@ -454,14 +454,14 @@ Proof.
intros.
apply Ropp_inv_permute; auto.
generalize (Rinv_lt_0_compat r r1); intro; unfold Rge in r0; elim r0; intros.
- unfold Rgt in H1; generalize (Rlt_asym 0 (/ r) H1); intro; elimtype False;
+ unfold Rgt in H1; generalize (Rlt_asym 0 (/ r) H1); intro; exfalso;
auto.
generalize (Rlt_dichotomy_converse (/ r) 0 (or_introl (/ r > 0) H0)); intro;
- elimtype False; auto.
+ exfalso; auto.
unfold Rge in r1; elim r1; clear r1; intro.
unfold Rgt in H0; generalize (Rlt_asym 0 (/ r) (Rinv_0_lt_compat r H0));
- intro; elimtype False; auto.
- elimtype False; auto.
+ intro; exfalso; auto.
+ exfalso; auto.
Qed.
Lemma Rabs_Ropp : forall x:R, Rabs (- x) = Rabs x.
@@ -478,7 +478,7 @@ Proof.
generalize (Ropp_le_ge_contravar 0 (-1) H1).
rewrite Ropp_involutive; rewrite Ropp_0.
intro; generalize (Rgt_not_le 1 0 Rlt_0_1); intro; generalize (Rge_le 0 1 H2);
- intro; elimtype False; auto.
+ intro; exfalso; auto.
ring.
Qed.
@@ -505,7 +505,7 @@ Proof.
clear v w; rewrite (Rplus_opp_l a) in H0; apply (Rlt_trans (- a) 0 a H0 H).
right; rewrite H; apply Ropp_0.
(**)
- elimtype False; generalize (Rplus_ge_compat_l a b 0 r); intro;
+ exfalso; generalize (Rplus_ge_compat_l a b 0 r); intro;
elim (Rplus_ne a); intros v w; rewrite v in H; clear v w;
generalize (Rge_trans (a + b) a 0 H r0); intro; clear H;
unfold Rge in H0; elim H0; intro; clear H0.
@@ -513,7 +513,7 @@ Proof.
absurd (a + b = 0); auto.
apply (Rlt_dichotomy_converse (a + b) 0); left; assumption.
(**)
- elimtype False; generalize (Rplus_lt_compat_l a b 0 r); intro;
+ exfalso; generalize (Rplus_lt_compat_l a b 0 r); intro;
elim (Rplus_ne a); intros v w; rewrite v in H; clear v w;
generalize (Rlt_trans (a + b) a 0 H r0); intro; clear H;
unfold Rge in r1; elim r1; clear r1; intro.
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index 3309f7d50..55982aa54 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -168,7 +168,7 @@ Proof.
rewrite eps2 in H10; assumption.
unfold Rabs in |- *; case (Rcase_abs 2); auto.
intro; cut (0 < 2).
- intro; generalize (Rlt_asym 0 2 H7); intro; elimtype False; auto.
+ intro; generalize (Rlt_asym 0 2 H7); intro; exfalso; auto.
fourier.
apply Rabs_no_R0.
discrR.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index a57bb1638..11be9772e 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -113,7 +113,7 @@ Hint Resolve pow_lt: real.
Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n.
Proof.
intros x n; elim n; simpl in |- *; auto with real.
- intros H' H'0; elimtype False; omega.
+ intros H' H'0; exfalso; omega.
intros n0; case n0.
simpl in |- *; rewrite Rmult_1_r; auto.
intros n1 H' H'0 H'1.
@@ -756,7 +756,7 @@ Proof.
unfold R_dist in |- *; intros; split_Rabs; try ring.
generalize (Ropp_gt_lt_0_contravar (y - x) r); intro;
rewrite (Ropp_minus_distr y x) in H; generalize (Rlt_asym (x - y) 0 r0);
- intro; unfold Rgt in H; elimtype False; auto.
+ intro; unfold Rgt in H; exfalso; auto.
generalize (minus_Rge y x r); intro; generalize (minus_Rge x y r0); intro;
generalize (Rge_antisym x y H0 H); intro; rewrite H1;
ring.
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 810a7de03..be7895f5c 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -95,7 +95,7 @@ Proof.
elim H0; intro.
apply Req_le; assumption.
clear H0; generalize (H r H1); intro; generalize (Rlt_irrefl r); intro;
- elimtype False; auto.
+ exfalso; auto.
Qed.
(*********)
@@ -355,7 +355,7 @@ Proof.
intro; generalize (prop_eps (- (l - l')) H1); intro;
generalize (Ropp_gt_lt_0_contravar (l - l') r); intro;
unfold Rgt in H3; generalize (Rgt_not_le (- (l - l')) 0 H3);
- intro; elimtype False; auto.
+ intro; exfalso; auto.
intros; cut (eps * / 2 > 0).
intro; generalize (H0 (eps * / 2) H2); rewrite (Rmult_comm eps (/ 2));
rewrite <- (Rmult_assoc 2 (/ 2) eps); rewrite (Rinv_r 2).
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index d940a1d11..379d3495b 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -179,7 +179,7 @@ assert (Z: Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)).
simpl; unfold g;
destruct (eq_nat_dec 0 n) as [t|f]; try reflexivity.
elim f; auto with *.
- elimtype False; omega.
+ exfalso; omega.
destruct IHa as [IHa0 IHa1].
split;
intros H;
@@ -191,7 +191,7 @@ assert (Z: Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)).
ring_simplify.
apply IHa0.
omega.
- elimtype False; omega.
+ exfalso; omega.
ring_simplify.
apply IHa1.
omega.
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 62f1940bf..33b7c8d1d 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -81,7 +81,7 @@ Section sequence.
Proof.
double induction n m; intros.
unfold Rge in |- *; right; trivial.
- elimtype False; unfold ge in H1; generalize (le_Sn_O n0); intro; auto.
+ exfalso; unfold ge in H1; generalize (le_Sn_O n0); intro; auto.
cut (n0 >= 0)%nat.
generalize H0; intros; unfold Un_growing in H0;
apply
@@ -91,7 +91,7 @@ Section sequence.
elim (lt_eq_lt_dec n1 n0); intro y.
elim y; clear y; intro y.
unfold ge in H2; generalize (le_not_lt n0 n1 (le_S_n n0 n1 H2)); intro;
- elimtype False; auto.
+ exfalso; auto.
rewrite y; unfold Rge in |- *; right; trivial.
unfold ge in H0; generalize (H0 (S n0) H1 (lt_le_S n0 n1 y)); intro;
unfold Un_growing in H1;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 12:23:20 +0000