summaryrefslogtreecommitdiff
path: root/theories/Reals/Rsqrt_def.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /theories/Reals/Rsqrt_def.v
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/Reals/Rsqrt_def.v')
-rw-r--r--theories/Reals/Rsqrt_def.v30
1 files changed, 14 insertions, 16 deletions
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 0a9f7754..0a3af6ca 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rsqrt_def.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: Rsqrt_def.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
Require Import Sumbool.
Require Import Rbase.
@@ -192,7 +192,7 @@ Qed.
Lemma dicho_lb_cv :
forall (x y:R) (P:R -> bool),
- x <= y -> sigT (fun l:R => Un_cv (dicho_lb x y P) l).
+ x <= y -> { l:R | Un_cv (dicho_lb x y P) l }.
Proof.
intros.
apply growing_cv.
@@ -202,7 +202,7 @@ Qed.
Lemma dicho_up_cv :
forall (x y:R) (P:R -> bool),
- x <= y -> sigT (fun l:R => Un_cv (dicho_up x y P) l).
+ x <= y -> { l:R | Un_cv (dicho_up x y P) l }.
Proof.
intros.
apply decreasing_cv.
@@ -466,7 +466,7 @@ Qed.
Lemma IVT :
forall (f:R -> R) (x y:R),
continuity f ->
- x < y -> f x < 0 -> 0 < f y -> sigT (fun z:R => x <= z <= y /\ f z = 0).
+ x < y -> f x < 0 -> 0 < f y -> { z:R | x <= z <= y /\ f z = 0 }.
Proof.
intros.
cut (x <= y).
@@ -478,7 +478,7 @@ Proof.
elim X0; intros.
assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p).
rewrite H4 in p0.
- apply existT with x0.
+ exists x0.
split.
split.
apply Rle_trans with (dicho_lb x y (fun z:R => cond_positivity (f z)) 0).
@@ -602,7 +602,7 @@ Qed.
Lemma IVT_cor :
forall (f:R -> R) (x y:R),
continuity f ->
- x <= y -> f x * f y <= 0 -> sigT (fun z:R => x <= z <= y /\ f z = 0).
+ x <= y -> f x * f y <= 0 -> { z:R | x <= z <= y /\ f z = 0 }.
Proof.
intros.
case (total_order_T 0 (f x)); intro.
@@ -628,7 +628,7 @@ Proof.
cut (0 < (- f)%F y).
intros.
elim (H3 H5 H4); intros.
- apply existT with x0.
+ exists x0.
elim p; intros.
split.
assumption.
@@ -643,7 +643,7 @@ Proof.
assumption.
rewrite H2 in a.
elim (Rlt_irrefl _ (Rlt_trans _ _ _ r a)).
- apply existT with x.
+ exists x.
split.
split; [ right; reflexivity | assumption ].
symmetry in |- *; assumption.
@@ -656,7 +656,7 @@ Proof.
assumption.
rewrite H2 in r.
elim (Rlt_irrefl _ (Rlt_trans _ _ _ r a)).
- apply existT with y.
+ exists y.
split.
split; [ assumption | right; reflexivity ].
symmetry in |- *; assumption.
@@ -670,7 +670,7 @@ Qed.
(** We can now define the square root function as the reciprocal
transformation of the square root function *)
Lemma Rsqrt_exists :
- forall y:R, 0 <= y -> sigT (fun z:R => 0 <= z /\ y = Rsqr z).
+ forall y:R, 0 <= y -> { z:R | 0 <= z /\ y = Rsqr z }.
Proof.
intros.
set (f := fun x:R => Rsqr x - y).
@@ -686,7 +686,7 @@ Proof.
intro.
assert (X := IVT_cor f 0 1 H1 (Rlt_le _ _ Rlt_0_1) H3).
elim X; intros t H4.
- apply existT with t.
+ exists t.
elim H4; intros.
split.
elim H5; intros; assumption.
@@ -700,7 +700,7 @@ Proof.
rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus in |- *;
rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
left; assumption.
- apply existT with 1.
+ exists 1.
split.
left; apply Rlt_0_1.
rewrite b; symmetry in |- *; apply Rsqr_1.
@@ -710,7 +710,7 @@ Proof.
intro.
assert (X := IVT_cor f 0 y H1 H H3).
elim X; intros t H4.
- apply existT with t.
+ exists t.
elim H4; intros.
split.
elim H5; intros; assumption.
@@ -739,9 +739,7 @@ Qed.
(* Definition of the square root: R+->R *)
Definition Rsqrt (y:nonnegreal) : R :=
- match Rsqrt_exists (nonneg y) (cond_nonneg y) with
- | existT a b => a
- end.
+ let (a,_) := Rsqrt_exists (nonneg y) (cond_nonneg y) in a.
(**********)
Lemma Rsqrt_positivity : forall x:nonnegreal, 0 <= Rsqrt x.