summaryrefslogtreecommitdiff
path: root/theories/Reals/R_sqrt.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Reals/R_sqrt.v
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Reals/R_sqrt.v')
-rw-r--r--theories/Reals/R_sqrt.v214
1 files changed, 155 insertions, 59 deletions
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index 63b8940b..2c43ee9b 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: R_sqrt.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
+(*i $Id$ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -20,15 +20,21 @@ Definition sqrt (x:R) : R :=
| right a => Rsqrt (mknonnegreal x (Rge_le _ _ a))
end.
-Lemma sqrt_positivity : forall x:R, 0 <= x -> 0 <= sqrt x.
+Lemma sqrt_pos : forall x : R, 0 <= sqrt x.
Proof.
- intros.
- unfold sqrt in |- *.
- case (Rcase_abs x); intro.
- elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ r H)).
+ intros x.
+ unfold sqrt.
+ destruct (Rcase_abs x) as [H|H].
+ apply Rle_refl.
apply Rsqrt_positivity.
Qed.
+Lemma sqrt_positivity : forall x:R, 0 <= x -> 0 <= sqrt x.
+Proof.
+ intros x _.
+ apply sqrt_pos.
+Qed.
+
Lemma sqrt_sqrt : forall x:R, 0 <= x -> sqrt x * sqrt x = x.
Proof.
intros.
@@ -40,7 +46,7 @@ Qed.
Lemma sqrt_0 : sqrt 0 = 0.
Proof.
- apply Rsqr_eq_0; unfold Rsqr in |- *; apply sqrt_sqrt; right; reflexivity.
+ apply Rsqr_eq_0; unfold Rsqr in |- *; apply sqrt_sqrt; right; reflexivity.
Qed.
Lemma sqrt_1 : sqrt 1 = 1.
@@ -48,7 +54,7 @@ Proof.
apply (Rsqr_inj (sqrt 1) 1);
[ apply sqrt_positivity; left
| left
- | unfold Rsqr in |- *; rewrite sqrt_sqrt; [ ring | left ] ];
+ | unfold Rsqr in |- *; rewrite sqrt_sqrt; [ ring | left ] ];
apply Rlt_0_1.
Qed.
@@ -100,17 +106,41 @@ Proof.
intros x H1; unfold Rsqr in |- *; apply (sqrt_sqrt x H1).
Qed.
+Lemma sqrt_mult_alt :
+ forall x y : R, 0 <= x -> sqrt (x * y) = sqrt x * sqrt y.
+Proof.
+ intros x y Hx.
+ unfold sqrt at 3.
+ destruct (Rcase_abs y) as [Hy|Hy].
+ rewrite Rmult_0_r.
+ destruct Hx as [Hx'|Hx'].
+ unfold sqrt.
+ destruct (Rcase_abs (x * y)) as [Hxy|Hxy].
+ apply eq_refl.
+ elim Rge_not_lt with (1 := Hxy).
+ rewrite <- (Rmult_0_r x).
+ now apply Rmult_lt_compat_l.
+ rewrite <- Hx', Rmult_0_l.
+ exact sqrt_0.
+ apply Rsqr_inj.
+ apply sqrt_pos.
+ apply Rmult_le_pos.
+ apply sqrt_pos.
+ apply Rsqrt_positivity.
+ rewrite Rsqr_mult, 2!Rsqr_sqrt.
+ unfold Rsqr.
+ now rewrite Rsqrt_Rsqrt.
+ exact Hx.
+ apply Rmult_le_pos.
+ exact Hx.
+ now apply Rge_le.
+Qed.
+
Lemma sqrt_mult :
forall x y:R, 0 <= x -> 0 <= y -> sqrt (x * y) = sqrt x * sqrt y.
Proof.
- intros x y H1 H2;
- apply
- (Rsqr_inj (sqrt (x * y)) (sqrt x * sqrt y)
- (sqrt_positivity (x * y) (Rmult_le_pos x y H1 H2))
- (Rmult_le_pos (sqrt x) (sqrt y) (sqrt_positivity x H1)
- (sqrt_positivity y H2))); rewrite Rsqr_mult;
- repeat rewrite Rsqr_sqrt;
- [ ring | assumption | assumption | apply (Rmult_le_pos x y H1 H2) ].
+ intros x y Hx _.
+ now apply sqrt_mult_alt.
Qed.
Lemma sqrt_lt_R0 : forall x:R, 0 < x -> 0 < sqrt x.
@@ -121,46 +151,90 @@ Proof.
| apply (sqrt_positivity x (Rlt_le 0 x H1)) ].
Qed.
+Lemma sqrt_div_alt :
+ forall x y : R, 0 < y -> sqrt (x / y) = sqrt x / sqrt y.
+Proof.
+ intros x y Hy.
+ unfold sqrt at 2.
+ destruct (Rcase_abs x) as [Hx|Hx].
+ unfold Rdiv.
+ rewrite Rmult_0_l.
+ unfold sqrt.
+ destruct (Rcase_abs (x * / y)) as [Hxy|Hxy].
+ apply eq_refl.
+ elim Rge_not_lt with (1 := Hxy).
+ apply Rmult_lt_reg_r with y.
+ exact Hy.
+ rewrite Rmult_assoc, Rinv_l, Rmult_1_r, Rmult_0_l.
+ exact Hx.
+ now apply Rgt_not_eq.
+ set (Hx' := Rge_le x 0 Hx).
+ clearbody Hx'. clear Hx.
+ apply Rsqr_inj.
+ apply sqrt_pos.
+ apply Fourier_util.Rle_mult_inv_pos.
+ apply Rsqrt_positivity.
+ now apply sqrt_lt_R0.
+ rewrite Rsqr_div, 2!Rsqr_sqrt.
+ unfold Rsqr.
+ now rewrite Rsqrt_Rsqrt.
+ now apply Rlt_le.
+ now apply Fourier_util.Rle_mult_inv_pos.
+ apply Rgt_not_eq.
+ now apply sqrt_lt_R0.
+Qed.
+
Lemma sqrt_div :
forall x y:R, 0 <= x -> 0 < y -> sqrt (x / y) = sqrt x / sqrt y.
Proof.
- intros x y H1 H2; apply Rsqr_inj;
- [ apply sqrt_positivity; apply (Rmult_le_pos x (/ y));
- [ assumption
- | generalize (Rinv_0_lt_compat y H2); clear H2; intro H2; left;
- assumption ]
- | apply (Rmult_le_pos (sqrt x) (/ sqrt y));
- [ apply (sqrt_positivity x H1)
- | generalize (sqrt_lt_R0 y H2); clear H2; intro H2;
- generalize (Rinv_0_lt_compat (sqrt y) H2); clear H2;
- intro H2; left; assumption ]
- | rewrite Rsqr_div; repeat rewrite Rsqr_sqrt;
- [ reflexivity
- | left; assumption
- | assumption
- | generalize (Rinv_0_lt_compat y H2); intro H3;
- generalize (Rlt_le 0 (/ y) H3); intro H4;
- apply (Rmult_le_pos x (/ y) H1 H4)
- | red in |- *; intro H3; generalize (Rlt_le 0 y H2); intro H4;
- generalize (sqrt_eq_0 y H4 H3); intro H5; rewrite H5 in H2;
- elim (Rlt_irrefl 0 H2) ] ].
+ intros x y _ H.
+ now apply sqrt_div_alt.
+Qed.
+
+Lemma sqrt_lt_0_alt :
+ forall x y : R, sqrt x < sqrt y -> x < y.
+Proof.
+ intros x y.
+ unfold sqrt at 2.
+ destruct (Rcase_abs y) as [Hy|Hy].
+ intros Hx.
+ elim Rlt_not_le with (1 := Hx).
+ apply sqrt_pos.
+ set (Hy' := Rge_le y 0 Hy).
+ clearbody Hy'. clear Hy.
+ unfold sqrt.
+ destruct (Rcase_abs x) as [Hx|Hx].
+ intros _.
+ now apply Rlt_le_trans with R0.
+ intros Hxy.
+ apply Rsqr_incrst_1 in Hxy ; try apply Rsqrt_positivity.
+ unfold Rsqr in Hxy.
+ now rewrite 2!Rsqrt_Rsqrt in Hxy.
Qed.
Lemma sqrt_lt_0 : forall x y:R, 0 <= x -> 0 <= y -> sqrt x < sqrt y -> x < y.
Proof.
- intros x y H1 H2 H3;
- generalize
- (Rsqr_incrst_1 (sqrt x) (sqrt y) H3 (sqrt_positivity x H1)
- (sqrt_positivity y H2)); intro H4; rewrite (Rsqr_sqrt x H1) in H4;
- rewrite (Rsqr_sqrt y H2) in H4; assumption.
+ intros x y _ _.
+ apply sqrt_lt_0_alt.
+Qed.
+
+Lemma sqrt_lt_1_alt :
+ forall x y : R, 0 <= x < y -> sqrt x < sqrt y.
+Proof.
+ intros x y (Hx, Hxy).
+ apply Rsqr_incrst_0 ; try apply sqrt_pos.
+ rewrite 2!Rsqr_sqrt.
+ exact Hxy.
+ apply Rlt_le.
+ now apply Rle_lt_trans with x.
+ exact Hx.
Qed.
Lemma sqrt_lt_1 : forall x y:R, 0 <= x -> 0 <= y -> x < y -> sqrt x < sqrt y.
Proof.
- intros x y H1 H2 H3; apply Rsqr_incrst_0;
- [ rewrite (Rsqr_sqrt x H1); rewrite (Rsqr_sqrt y H2); assumption
- | apply (sqrt_positivity x H1)
- | apply (sqrt_positivity y H2) ].
+ intros x y Hx _ Hxy.
+ apply sqrt_lt_1_alt.
+ now split.
Qed.
Lemma sqrt_le_0 :
@@ -173,13 +247,27 @@ Proof.
rewrite (Rsqr_sqrt y H2) in H4; assumption.
Qed.
+Lemma sqrt_le_1_alt :
+ forall x y : R, x <= y -> sqrt x <= sqrt y.
+Proof.
+ intros x y [Hxy|Hxy].
+ destruct (Rle_or_lt 0 x) as [Hx|Hx].
+ apply Rlt_le.
+ apply sqrt_lt_1_alt.
+ now split.
+ unfold sqrt at 1.
+ destruct (Rcase_abs x) as [Hx'|Hx'].
+ apply sqrt_pos.
+ now elim Rge_not_lt with (1 := Hx').
+ rewrite Hxy.
+ apply Rle_refl.
+Qed.
+
Lemma sqrt_le_1 :
forall x y:R, 0 <= x -> 0 <= y -> x <= y -> sqrt x <= sqrt y.
Proof.
- intros x y H1 H2 H3; apply Rsqr_incr_0;
- [ rewrite (Rsqr_sqrt x H1); rewrite (Rsqr_sqrt y H2); assumption
- | apply (sqrt_positivity x H1)
- | apply (sqrt_positivity y H2) ].
+ intros x y _ _ Hxy.
+ now apply sqrt_le_1_alt.
Qed.
Lemma sqrt_inj : forall x y:R, 0 <= x -> 0 <= y -> sqrt x = sqrt y -> x = y.
@@ -190,22 +278,30 @@ Proof.
rewrite H1; reflexivity.
Qed.
+Lemma sqrt_less_alt :
+ forall x : R, 1 < x -> sqrt x < x.
+Proof.
+ intros x Hx.
+ assert (Hx1 := Rle_lt_trans _ _ _ Rle_0_1 Hx).
+ assert (Hx2 := Rlt_le _ _ Hx1).
+ apply Rsqr_incrst_0 ; trivial.
+ rewrite Rsqr_sqrt ; trivial.
+ rewrite <- (Rmult_1_l x) at 1.
+ now apply Rmult_lt_compat_r.
+ apply sqrt_pos.
+Qed.
+
Lemma sqrt_less : forall x:R, 0 <= x -> 1 < x -> sqrt x < x.
Proof.
- intros x H1 H2; generalize (sqrt_lt_1 1 x (Rlt_le 0 1 Rlt_0_1) H1 H2);
- intro H3; rewrite sqrt_1 in H3; generalize (Rmult_ne (sqrt x));
- intro H4; elim H4; intros H5 H6; rewrite <- H5; pattern x at 2 in |- *;
- rewrite <- (sqrt_def x H1);
- apply
- (Rmult_lt_compat_l (sqrt x) 1 (sqrt x)
- (sqrt_lt_R0 x (Rlt_trans 0 1 x Rlt_0_1 H2)) H3).
+ intros x _.
+ apply sqrt_less_alt.
Qed.
Lemma sqrt_more : forall x:R, 0 < x -> x < 1 -> x < sqrt x.
Proof.
intros x H1 H2;
- generalize (sqrt_lt_1 x 1 (Rlt_le 0 x H1) (Rlt_le 0 1 Rlt_0_1) H2);
- intro H3; rewrite sqrt_1 in H3; generalize (Rmult_ne (sqrt x));
+ generalize (sqrt_lt_1 x 1 (Rlt_le 0 x H1) (Rlt_le 0 1 Rlt_0_1) H2);
+ intro H3; rewrite sqrt_1 in H3; generalize (Rmult_ne (sqrt x));
intro H4; elim H4; intros H5 H6; rewrite <- H5; pattern x at 1 in |- *;
rewrite <- (sqrt_def x (Rlt_le 0 x H1));
apply (Rmult_lt_compat_l (sqrt x) (sqrt x) 1 (sqrt_lt_R0 x H1) H3).
@@ -338,7 +434,7 @@ Proof.
(b * (- b * (/ 2 * / a)) + c).
repeat rewrite <- Rplus_assoc; replace (b * b + b * b) with (2 * (b * b)).
rewrite Rmult_plus_distr_r; repeat rewrite Rmult_assoc;
- rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc;
+ rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc;
rewrite <- Rinv_l_sym.
rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc.
rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.