diff options
Diffstat (limited to 'theories/Reals/Sqrt_reg.v')
| -rw-r--r-- | theories/Reals/Sqrt_reg.v | 152 |
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. |