summaryrefslogtreecommitdiff
path: root/theories/Reals/Sqrt_reg.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/Sqrt_reg.v')
-rw-r--r--theories/Reals/Sqrt_reg.v152
1 files changed, 75 insertions, 77 deletions
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v
index 79f39892..89c17821 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -1,18 +1,16 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Sqrt_reg.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Rbase.
Require Import Rfunctions.
Require Import Ranalysis1.
Require Import R_sqrt.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
(**********)
Lemma sqrt_var_maj :
@@ -23,67 +21,67 @@ Proof.
case (total_order_T h 0); intro.
elim s; intro.
repeat rewrite Rabs_left.
- unfold Rminus in |- *; do 2 rewrite <- (Rplus_comm (-1)).
+ unfold Rminus; do 2 rewrite <- (Rplus_comm (-1)).
do 2 rewrite Ropp_plus_distr; rewrite Ropp_involutive;
apply Rplus_le_compat_l.
apply Ropp_le_contravar; apply sqrt_le_1.
apply Rle_0_sqr.
apply H0.
- pattern (1 + h) at 2 in |- *; rewrite <- Rmult_1_r; unfold Rsqr in |- *;
+ pattern (1 + h) at 2; rewrite <- Rmult_1_r; unfold Rsqr;
apply Rmult_le_compat_l.
apply H0.
- pattern 1 at 2 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
+ pattern 1 at 2; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
assumption.
apply Rplus_lt_reg_r with 1; rewrite Rplus_0_r; rewrite Rplus_comm;
- unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_l;
+ unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l;
rewrite Rplus_0_r.
- pattern 1 at 2 in |- *; rewrite <- sqrt_1; apply sqrt_lt_1.
+ pattern 1 at 2; rewrite <- sqrt_1; apply sqrt_lt_1.
apply Rle_0_sqr.
left; apply Rlt_0_1.
- pattern 1 at 2 in |- *; rewrite <- Rsqr_1; apply Rsqr_incrst_1.
- pattern 1 at 2 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
+ pattern 1 at 2; rewrite <- Rsqr_1; apply Rsqr_incrst_1.
+ pattern 1 at 2; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
assumption.
apply H0.
left; apply Rlt_0_1.
apply Rplus_lt_reg_r with 1; rewrite Rplus_0_r; rewrite Rplus_comm;
- unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_l;
+ unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l;
rewrite Rplus_0_r.
- pattern 1 at 2 in |- *; rewrite <- sqrt_1; apply sqrt_lt_1.
+ pattern 1 at 2; rewrite <- sqrt_1; apply sqrt_lt_1.
apply H0.
left; apply Rlt_0_1.
- pattern 1 at 2 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
+ pattern 1 at 2; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
assumption.
rewrite b; rewrite Rplus_0_r; rewrite Rsqr_1; rewrite sqrt_1; right;
reflexivity.
repeat rewrite Rabs_right.
- unfold Rminus in |- *; do 2 rewrite <- (Rplus_comm (-1));
+ unfold Rminus; do 2 rewrite <- (Rplus_comm (-1));
apply Rplus_le_compat_l.
apply sqrt_le_1.
apply H0.
apply Rle_0_sqr.
- pattern (1 + h) at 1 in |- *; rewrite <- Rmult_1_r; unfold Rsqr in |- *;
+ pattern (1 + h) at 1; rewrite <- Rmult_1_r; unfold Rsqr;
apply Rmult_le_compat_l.
apply H0.
- pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
+ pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
assumption.
apply Rle_ge; apply Rplus_le_reg_l with 1.
- rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus in |- *;
+ rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus;
rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r.
- pattern 1 at 1 in |- *; rewrite <- sqrt_1; apply sqrt_le_1.
+ pattern 1 at 1; rewrite <- sqrt_1; apply sqrt_le_1.
left; apply Rlt_0_1.
apply Rle_0_sqr.
- pattern 1 at 1 in |- *; rewrite <- Rsqr_1; apply Rsqr_incr_1.
- pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
+ pattern 1 at 1; rewrite <- Rsqr_1; apply Rsqr_incr_1.
+ pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
assumption.
left; apply Rlt_0_1.
apply H0.
apply Rle_ge; left; apply Rplus_lt_reg_r with 1.
- rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus in |- *;
+ rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus;
rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r.
- pattern 1 at 1 in |- *; rewrite <- sqrt_1; apply sqrt_lt_1.
+ pattern 1 at 1; rewrite <- sqrt_1; apply sqrt_lt_1.
left; apply Rlt_0_1.
apply H0.
- pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
+ pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
assumption.
rewrite sqrt_Rsqr.
replace (1 + h - 1) with h; [ right; reflexivity | ring ].
@@ -103,14 +101,14 @@ Qed.
(** sqrt is continuous in 1 *)
Lemma sqrt_continuity_pt_R1 : continuity_pt sqrt 1.
Proof.
- unfold continuity_pt in |- *; unfold continue_in in |- *;
- unfold limit1_in in |- *; unfold limit_in in |- *;
- unfold dist in |- *; simpl in |- *; unfold R_dist in |- *;
+ unfold continuity_pt; unfold continue_in;
+ unfold limit1_in; unfold limit_in;
+ unfold dist; simpl; unfold R_dist;
intros.
set (alpha := Rmin eps 1).
exists alpha; intros.
split.
- unfold alpha in |- *; unfold Rmin in |- *; case (Rle_dec eps 1); intro.
+ unfold alpha; unfold Rmin; case (Rle_dec eps 1); intro.
assumption.
apply Rlt_0_1.
intros; elim H0; intros.
@@ -119,18 +117,18 @@ Proof.
apply sqrt_var_maj.
apply Rle_trans with alpha.
left; apply H2.
- unfold alpha in |- *; apply Rmin_r.
+ unfold alpha; apply Rmin_r.
apply Rlt_le_trans with alpha;
- [ apply H2 | unfold alpha in |- *; apply Rmin_l ].
+ [ apply H2 | unfold alpha; apply Rmin_l ].
Qed.
(** sqrt is continuous forall x>0 *)
Lemma sqrt_continuity_pt : forall x:R, 0 < x -> continuity_pt sqrt x.
Proof.
intros; generalize sqrt_continuity_pt_R1.
- unfold continuity_pt in |- *; unfold continue_in in |- *;
- unfold limit1_in in |- *; unfold limit_in in |- *;
- unfold dist in |- *; simpl in |- *; unfold R_dist in |- *;
+ unfold continuity_pt; unfold continue_in;
+ unfold limit1_in; unfold limit_in;
+ unfold dist; simpl; unfold R_dist;
intros.
cut (0 < eps / sqrt x).
intro; elim (H0 _ H2); intros alp_1 H3.
@@ -138,9 +136,9 @@ Proof.
set (alpha := alp_1 * x).
exists (Rmin alpha x); intros.
split.
- change (0 < Rmin alpha x) in |- *; unfold Rmin in |- *;
+ change (0 < Rmin alpha x); unfold Rmin;
case (Rle_dec alpha x); intro.
- unfold alpha in |- *; apply Rmult_lt_0_compat; assumption.
+ unfold alpha; apply Rmult_lt_0_compat; assumption.
apply H.
intros; replace x0 with (x + (x0 - x)); [ idtac | ring ];
replace (sqrt (x + (x0 - x)) - sqrt x) with
@@ -152,7 +150,7 @@ Proof.
rewrite Rmult_1_l; rewrite Rmult_comm.
unfold Rdiv in H5.
case (Req_dec x x0); intro.
- rewrite H7; unfold Rminus, Rdiv in |- *; rewrite Rplus_opp_r;
+ rewrite H7; unfold Rminus, Rdiv; rewrite Rplus_opp_r;
rewrite Rmult_0_l; rewrite Rplus_0_r; rewrite Rplus_opp_r;
rewrite Rabs_R0.
apply Rmult_lt_0_compat.
@@ -160,10 +158,10 @@ Proof.
apply Rinv_0_lt_compat; rewrite <- H7; apply sqrt_lt_R0; assumption.
apply H5.
split.
- unfold D_x, no_cond in |- *.
+ unfold D_x, no_cond.
split.
trivial.
- red in |- *; intro.
+ red; intro.
cut ((x0 - x) * / x = 0).
intro.
elim (Rmult_integral _ _ H9); intro.
@@ -172,35 +170,35 @@ Proof.
assert (H11 := Rmult_eq_0_compat_r _ x H10).
rewrite <- Rinv_l_sym in H11.
elim R1_neq_R0; exact H11.
- red in |- *; intro; rewrite H12 in H; elim (Rlt_irrefl _ H).
- symmetry in |- *; apply Rplus_eq_reg_l with 1; rewrite Rplus_0_r;
+ red; intro; rewrite H12 in H; elim (Rlt_irrefl _ H).
+ symmetry ; apply Rplus_eq_reg_l with 1; rewrite Rplus_0_r;
unfold Rdiv in H8; exact H8.
- unfold Rminus in |- *; rewrite Rplus_comm; rewrite <- Rplus_assoc;
+ unfold Rminus; rewrite Rplus_comm; rewrite <- Rplus_assoc;
rewrite Rplus_opp_l; rewrite Rplus_0_l; elim H6; intros.
- unfold Rdiv in |- *; rewrite Rabs_mult.
+ unfold Rdiv; rewrite Rabs_mult.
rewrite Rabs_Rinv.
rewrite (Rabs_right x).
rewrite Rmult_comm; apply Rmult_lt_reg_l with x.
apply H.
rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
- rewrite Rmult_1_l; rewrite Rmult_comm; fold alpha in |- *.
+ rewrite Rmult_1_l; rewrite Rmult_comm; fold alpha.
apply Rlt_le_trans with (Rmin alpha x).
apply H9.
apply Rmin_l.
- red in |- *; intro; rewrite H10 in H; elim (Rlt_irrefl _ H).
+ red; intro; rewrite H10 in H; elim (Rlt_irrefl _ H).
apply Rle_ge; left; apply H.
- red in |- *; intro; rewrite H10 in H; elim (Rlt_irrefl _ H).
+ red; intro; rewrite H10 in H; elim (Rlt_irrefl _ H).
assert (H7 := sqrt_lt_R0 x H).
- red in |- *; intro; rewrite H8 in H7; elim (Rlt_irrefl _ H7).
+ red; intro; rewrite H8 in H7; elim (Rlt_irrefl _ H7).
apply Rle_ge; apply sqrt_positivity.
left; apply H.
- unfold Rminus in |- *; rewrite Rmult_plus_distr_l;
+ unfold Rminus; rewrite Rmult_plus_distr_l;
rewrite Ropp_mult_distr_r_reverse; repeat rewrite <- sqrt_mult.
rewrite Rmult_1_r; rewrite Rmult_plus_distr_l; rewrite Rmult_1_r;
- unfold Rdiv in |- *; rewrite Rmult_comm; rewrite Rmult_assoc;
+ unfold Rdiv; rewrite Rmult_comm; rewrite Rmult_assoc;
rewrite <- Rinv_l_sym.
rewrite Rmult_1_r; reflexivity.
- red in |- *; intro; rewrite H7 in H; elim (Rlt_irrefl _ H).
+ red; intro; rewrite H7 in H; elim (Rlt_irrefl _ H).
left; apply H.
left; apply Rlt_0_1.
left; apply H.
@@ -210,7 +208,7 @@ Proof.
rewrite Rplus_comm.
apply Rplus_le_reg_l with (- ((x0 - x) / x)).
rewrite Rplus_0_r; rewrite <- Rplus_assoc; rewrite Rplus_opp_l;
- rewrite Rplus_0_l; unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse.
+ rewrite Rplus_0_l; unfold Rdiv; rewrite <- Ropp_mult_distr_l_reverse.
apply Rmult_le_reg_l with x.
apply H.
rewrite Rmult_1_r; rewrite Rmult_comm; rewrite Rmult_assoc;
@@ -218,13 +216,13 @@ Proof.
rewrite Rmult_1_r; left; apply Rlt_le_trans with (Rmin alpha x).
apply H8.
apply Rmin_r.
- red in |- *; intro; rewrite H9 in H; elim (Rlt_irrefl _ H).
+ red; intro; rewrite H9 in H; elim (Rlt_irrefl _ H).
apply Rplus_le_le_0_compat.
left; apply Rlt_0_1.
- unfold Rdiv in |- *; apply Rmult_le_pos.
+ unfold Rdiv; apply Rmult_le_pos.
apply Rge_le; exact r.
left; apply Rinv_0_lt_compat; apply H.
- unfold Rdiv in |- *; apply Rmult_lt_0_compat.
+ unfold Rdiv; apply Rmult_lt_0_compat.
apply H1.
apply Rinv_0_lt_compat; apply sqrt_lt_R0; apply H.
Qed.
@@ -237,7 +235,7 @@ Proof.
cut (continuity_pt g 0).
intro; cut (g 0 <> 0).
intro; assert (H2 := continuity_pt_inv g 0 H0 H1).
- unfold derivable_pt_lim in |- *; intros; unfold continuity_pt in H2;
+ unfold derivable_pt_lim; intros; unfold continuity_pt in H2;
unfold continue_in in H2; unfold limit1_in in H2;
unfold limit_in in H2; simpl in H2; unfold R_dist in H2.
elim (H2 eps H3); intros alpha H4.
@@ -249,29 +247,29 @@ Proof.
unfold inv_fct, g in H6; replace (2 * sqrt x) with (sqrt x + sqrt (x + 0)).
apply H6.
split.
- unfold D_x, no_cond in |- *.
+ unfold D_x, no_cond.
split.
trivial.
- apply (sym_not_eq (A:=R)); exact H8.
- unfold Rminus in |- *; rewrite Ropp_0; rewrite Rplus_0_r;
+ apply (not_eq_sym (A:=R)); exact H8.
+ unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r;
apply Rlt_le_trans with alpha1.
exact H9.
- unfold alpha1 in |- *; apply Rmin_l.
+ unfold alpha1; apply Rmin_l.
rewrite Rplus_0_r; ring.
cut (0 <= x + h).
intro; cut (0 < sqrt x + sqrt (x + h)).
intro; apply Rmult_eq_reg_l with (sqrt x + sqrt (x + h)).
rewrite <- Rinv_r_sym.
- rewrite Rplus_comm; unfold Rdiv in |- *; rewrite <- Rmult_assoc;
+ rewrite Rplus_comm; unfold Rdiv; rewrite <- Rmult_assoc;
rewrite Rsqr_plus_minus; repeat rewrite Rsqr_sqrt.
- rewrite Rplus_comm; unfold Rminus in |- *; rewrite Rplus_assoc;
+ rewrite Rplus_comm; unfold Rminus; rewrite Rplus_assoc;
rewrite Rplus_opp_r; rewrite Rplus_0_r; rewrite <- Rinv_r_sym.
reflexivity.
apply H8.
left; apply H.
assumption.
- red in |- *; intro; rewrite H12 in H11; elim (Rlt_irrefl _ H11).
- red in |- *; intro; rewrite H12 in H11; elim (Rlt_irrefl _ H11).
+ red; intro; rewrite H12 in H11; elim (Rlt_irrefl _ H11).
+ red; intro; rewrite H12 in H11; elim (Rlt_irrefl _ H11).
apply Rplus_lt_le_0_compat.
apply sqrt_lt_R0; apply H.
apply sqrt_positivity; apply H10.
@@ -281,35 +279,35 @@ Proof.
rewrite Rplus_0_r; rewrite Rplus_comm; rewrite Rplus_assoc;
rewrite Rplus_opp_r; rewrite Rplus_0_r; left; apply Rlt_le_trans with alpha1.
apply H9.
- unfold alpha1 in |- *; apply Rmin_r.
+ unfold alpha1; apply Rmin_r.
apply Rplus_le_le_0_compat.
left; assumption.
apply Rge_le; apply r.
- unfold alpha1 in |- *; unfold Rmin in |- *; case (Rle_dec alpha x); intro.
+ unfold alpha1; unfold Rmin; case (Rle_dec alpha x); intro.
apply H5.
apply H.
- unfold g in |- *; rewrite Rplus_0_r.
+ unfold g; rewrite Rplus_0_r.
cut (0 < sqrt x + sqrt x).
- intro; red in |- *; intro; rewrite H2 in H1; elim (Rlt_irrefl _ H1).
+ intro; red; intro; rewrite H2 in H1; elim (Rlt_irrefl _ H1).
apply Rplus_lt_0_compat; apply sqrt_lt_R0; apply H.
replace g with (fct_cte (sqrt x) + comp sqrt (fct_cte x + id))%F;
[ idtac | reflexivity ].
apply continuity_pt_plus.
- apply continuity_pt_const; unfold constant, fct_cte in |- *; intro;
+ apply continuity_pt_const; unfold constant, fct_cte; intro;
reflexivity.
apply continuity_pt_comp.
apply continuity_pt_plus.
- apply continuity_pt_const; unfold constant, fct_cte in |- *; intro;
+ apply continuity_pt_const; unfold constant, fct_cte; intro;
reflexivity.
apply derivable_continuous_pt; apply derivable_pt_id.
apply sqrt_continuity_pt.
- unfold plus_fct, fct_cte, id in |- *; rewrite Rplus_0_r; apply H.
+ unfold plus_fct, fct_cte, id; rewrite Rplus_0_r; apply H.
Qed.
(**********)
Lemma derivable_pt_sqrt : forall x:R, 0 < x -> derivable_pt sqrt x.
Proof.
- unfold derivable_pt in |- *; intros.
+ unfold derivable_pt; intros.
exists (/ (2 * sqrt x)).
apply derivable_pt_lim_sqrt; assumption.
Qed.
@@ -332,19 +330,19 @@ Proof.
intros; case (Rtotal_order 0 x); intro.
apply (sqrt_continuity_pt x H0).
elim H0; intro.
- unfold continuity_pt in |- *; unfold continue_in in |- *;
- unfold limit1_in in |- *; unfold limit_in in |- *;
- simpl in |- *; unfold R_dist in |- *; intros.
+ unfold continuity_pt; unfold continue_in;
+ unfold limit1_in; unfold limit_in;
+ simpl; unfold R_dist; intros.
exists (Rsqr eps); intros.
split.
- change (0 < Rsqr eps) in |- *; apply Rsqr_pos_lt.
- red in |- *; intro; rewrite H3 in H2; elim (Rlt_irrefl _ H2).
+ change (0 < Rsqr eps); apply Rsqr_pos_lt.
+ red; intro; rewrite H3 in H2; elim (Rlt_irrefl _ H2).
intros; elim H3; intros.
- rewrite <- H1; rewrite sqrt_0; unfold Rminus in |- *; rewrite Ropp_0;
+ rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0;
rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5;
rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5.
case (Rcase_abs x0); intro.
- unfold sqrt in |- *; case (Rcase_abs x0); intro.
+ unfold sqrt; case (Rcase_abs x0); intro.
rewrite Rabs_R0; apply H2.
assert (H6 := Rge_le _ _ r0); elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 r)).
rewrite Rabs_right.