diff options
Diffstat (limited to 'theories7/Reals/Rsqrt_def.v')
| -rw-r--r-- | theories7/Reals/Rsqrt_def.v | 688 |
1 files changed, 688 insertions, 0 deletions
diff --git a/theories7/Reals/Rsqrt_def.v b/theories7/Reals/Rsqrt_def.v new file mode 100644 index 00000000..17367dce --- /dev/null +++ b/theories7/Reals/Rsqrt_def.v @@ -0,0 +1,688 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Rsqrt_def.v,v 1.1.2.1 2004/07/16 19:31:35 herbelin Exp $ i*) + +Require Sumbool. +Require Rbase. +Require Rfunctions. +Require SeqSeries. +Require Ranalysis1. +V7only [ Import nat_scope. Import Z_scope. Import R_scope. ]. +Open Local Scope R_scope. + +Fixpoint Dichotomy_lb [x,y:R;P:R->bool;N:nat] : R := +Cases N of + O => x +| (S n) => let down = (Dichotomy_lb x y P n) in let up = (Dichotomy_ub x y P n) in let z = ``(down+up)/2`` in if (P z) then down else z +end +with Dichotomy_ub [x,y:R;P:R->bool;N:nat] : R := +Cases N of + O => y +| (S n) => let down = (Dichotomy_lb x y P n) in let up = (Dichotomy_ub x y P n) in let z = ``(down+up)/2`` in if (P z) then z else up +end. + +Definition dicho_lb [x,y:R;P:R->bool] : nat->R := [N:nat](Dichotomy_lb x y P N). +Definition dicho_up [x,y:R;P:R->bool] : nat->R := [N:nat](Dichotomy_ub x y P N). + +(**********) +Lemma dicho_comp : (x,y:R;P:R->bool;n:nat) ``x<=y`` -> ``(dicho_lb x y P n)<=(dicho_up x y P n)``. +Intros. +Induction n. +Simpl; Assumption. +Simpl. +Case (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``). +Unfold Rdiv; Apply Rle_monotony_contra with ``2``. +Sup0. +Pattern 1 ``2``; Rewrite Rmult_sym. +Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR]. +Rewrite Rmult_1r. +Rewrite double. +Apply Rle_compatibility. +Assumption. +Unfold Rdiv; Apply Rle_monotony_contra with ``2``. +Sup0. +Pattern 3 ``2``; Rewrite Rmult_sym. +Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR]. +Rewrite Rmult_1r. +Rewrite double. +Rewrite <- (Rplus_sym (Dichotomy_ub x y P n)). +Apply Rle_compatibility. +Assumption. +Qed. + +Lemma dicho_lb_growing : (x,y:R;P:R->bool) ``x<=y`` -> (Un_growing (dicho_lb x y P)). +Intros. +Unfold Un_growing. +Intro. +Simpl. +Case (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``). +Right; Reflexivity. +Unfold Rdiv; Apply Rle_monotony_contra with ``2``. +Sup0. +Pattern 1 ``2``; Rewrite Rmult_sym. +Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR]. +Rewrite Rmult_1r. +Rewrite double. +Apply Rle_compatibility. +Replace (Dichotomy_ub x y P n) with (dicho_up x y P n); [Apply dicho_comp; Assumption | Reflexivity]. +Qed. + +Lemma dicho_up_decreasing : (x,y:R;P:R->bool) ``x<=y`` -> (Un_decreasing (dicho_up x y P)). +Intros. +Unfold Un_decreasing. +Intro. +Simpl. +Case (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``). +Unfold Rdiv; Apply Rle_monotony_contra with ``2``. +Sup0. +Pattern 3 ``2``; Rewrite Rmult_sym. +Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR]. +Rewrite Rmult_1r. +Rewrite double. +Replace (Dichotomy_ub x y P n) with (dicho_up x y P n); [Idtac | Reflexivity]. +Replace (Dichotomy_lb x y P n) with (dicho_lb x y P n); [Idtac | Reflexivity]. +Rewrite <- (Rplus_sym ``(dicho_up x y P n)``). +Apply Rle_compatibility. +Apply dicho_comp; Assumption. +Right; Reflexivity. +Qed. + +Lemma dicho_lb_maj_y : (x,y:R;P:R->bool) ``x<=y`` -> (n:nat)``(dicho_lb x y P n)<=y``. +Intros. +Induction n. +Simpl; Assumption. +Simpl. +Case (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``). +Assumption. +Unfold Rdiv; Apply Rle_monotony_contra with ``2``. +Sup0. +Pattern 3 ``2``; Rewrite Rmult_sym. +Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Rewrite Rmult_1r | DiscrR]. +Rewrite double; Apply Rplus_le. +Assumption. +Pattern 2 y; Replace y with (Dichotomy_ub x y P O); [Idtac | Reflexivity]. +Apply decreasing_prop. +Assert H0 := (dicho_up_decreasing x y P H). +Assumption. +Apply le_O_n. +Qed. + +Lemma dicho_lb_maj : (x,y:R;P:R->bool) ``x<=y`` -> (has_ub (dicho_lb x y P)). +Intros. +Cut (n:nat)``(dicho_lb x y P n)<=y``. +Intro. +Unfold has_ub. +Unfold bound. +Exists y. +Unfold is_upper_bound. +Intros. +Elim H1; Intros. +Rewrite H2; Apply H0. +Apply dicho_lb_maj_y; Assumption. +Qed. + +Lemma dicho_up_min_x : (x,y:R;P:R->bool) ``x<=y`` -> (n:nat)``x<=(dicho_up x y P n)``. +Intros. +Induction n. +Simpl; Assumption. +Simpl. +Case (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``). +Unfold Rdiv; Apply Rle_monotony_contra with ``2``. +Sup0. +Pattern 1 ``2``; Rewrite Rmult_sym. +Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Rewrite Rmult_1r | DiscrR]. +Rewrite double; Apply Rplus_le. +Pattern 1 x; Replace x with (Dichotomy_lb x y P O); [Idtac | Reflexivity]. +Apply tech9. +Assert H0 := (dicho_lb_growing x y P H). +Assumption. +Apply le_O_n. +Assumption. +Assumption. +Qed. + +Lemma dicho_up_min : (x,y:R;P:R->bool) ``x<=y`` -> (has_lb (dicho_up x y P)). +Intros. +Cut (n:nat)``x<=(dicho_up x y P n)``. +Intro. +Unfold has_lb. +Unfold bound. +Exists ``-x``. +Unfold is_upper_bound. +Intros. +Elim H1; Intros. +Rewrite H2. +Unfold opp_seq. +Apply Rle_Ropp1. +Apply H0. +Apply dicho_up_min_x; Assumption. +Qed. + +Lemma dicho_lb_cv : (x,y:R;P:R->bool) ``x<=y`` -> (sigTT R [l:R](Un_cv (dicho_lb x y P) l)). +Intros. +Apply growing_cv. +Apply dicho_lb_growing; Assumption. +Apply dicho_lb_maj; Assumption. +Qed. + +Lemma dicho_up_cv : (x,y:R;P:R->bool) ``x<=y`` -> (sigTT R [l:R](Un_cv (dicho_up x y P) l)). +Intros. +Apply decreasing_cv. +Apply dicho_up_decreasing; Assumption. +Apply dicho_up_min; Assumption. +Qed. + +Lemma dicho_lb_dicho_up : (x,y:R;P:R->bool;n:nat) ``x<=y`` -> ``(dicho_up x y P n)-(dicho_lb x y P n)==(y-x)/(pow 2 n)``. +Intros. +Induction n. +Simpl. +Unfold Rdiv; Rewrite Rinv_R1; Ring. +Simpl. +Case (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``). +Unfold Rdiv. +Replace ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))*/2- + (Dichotomy_lb x y P n)`` with ``((dicho_up x y P n)-(dicho_lb x y P n))/2``. +Unfold Rdiv; Rewrite Hrecn. +Unfold Rdiv. +Rewrite Rinv_Rmult. +Ring. +DiscrR. +Apply pow_nonzero; DiscrR. +Pattern 2 (Dichotomy_lb x y P n); Rewrite (double_var (Dichotomy_lb x y P n)); Unfold dicho_up dicho_lb Rminus Rdiv; Ring. +Replace ``(Dichotomy_ub x y P n)-((Dichotomy_lb x y P n)+ + (Dichotomy_ub x y P n))/2`` with ``((dicho_up x y P n)-(dicho_lb x y P n))/2``. +Unfold Rdiv; Rewrite Hrecn. +Unfold Rdiv. +Rewrite Rinv_Rmult. +Ring. +DiscrR. +Apply pow_nonzero; DiscrR. +Pattern 1 (Dichotomy_ub x y P n); Rewrite (double_var (Dichotomy_ub x y P n)); Unfold dicho_up dicho_lb Rminus Rdiv; Ring. +Qed. + +Definition pow_2_n := [n:nat](pow ``2`` n). + +Lemma pow_2_n_neq_R0 : (n:nat) ``(pow_2_n n)<>0``. +Intro. +Unfold pow_2_n. +Apply pow_nonzero. +DiscrR. +Qed. + +Lemma pow_2_n_growing : (Un_growing pow_2_n). +Unfold Un_growing. +Intro. +Replace (S n) with (plus n (1)); [Unfold pow_2_n; Rewrite pow_add | Ring]. +Pattern 1 (pow ``2`` n); Rewrite <- Rmult_1r. +Apply Rle_monotony. +Left; Apply pow_lt; Sup0. +Simpl. +Rewrite Rmult_1r. +Pattern 1 R1; Rewrite <- Rplus_Or; Apply Rle_compatibility; Left; Apply Rlt_R0_R1. +Qed. + +Lemma pow_2_n_infty : (cv_infty pow_2_n). +Cut (N:nat)``(INR N)<=(pow 2 N)``. +Intros. +Unfold cv_infty. +Intro. +Case (total_order_T R0 M); Intro. +Elim s; Intro. +Pose N := (up M). +Cut `0<=N`. +Intro. +Elim (IZN N H0); Intros N0 H1. +Exists N0. +Intros. +Apply Rlt_le_trans with (INR N0). +Rewrite INR_IZR_INZ. +Rewrite <- H1. +Unfold N. +Assert H3 := (archimed M). +Elim H3; Intros; Assumption. +Apply Rle_trans with (pow_2_n N0). +Unfold pow_2_n; Apply H. +Apply Rle_sym2. +Apply growing_prop. +Apply pow_2_n_growing. +Assumption. +Apply le_IZR. +Unfold N. +Simpl. +Assert H0 := (archimed M); Elim H0; Intros. +Left; Apply Rlt_trans with M; Assumption. +Exists O; Intros. +Rewrite <- b. +Unfold pow_2_n; Apply pow_lt; Sup0. +Exists O; Intros. +Apply Rlt_trans with R0. +Assumption. +Unfold pow_2_n; Apply pow_lt; Sup0. +Induction N. +Simpl. +Left; Apply Rlt_R0_R1. +Intros. +Pattern 2 (S n); Replace (S n) with (plus n (1)); [Idtac | Ring]. +Rewrite S_INR; Rewrite pow_add. +Simpl. +Rewrite Rmult_1r. +Apply Rle_trans with ``(pow 2 n)``. +Rewrite <- (Rplus_sym R1). +Rewrite <- (Rmult_1r (INR n)). +Apply (poly n R1). +Apply Rlt_R0_R1. +Pattern 1 (pow ``2`` n); Rewrite <- Rplus_Or. +Rewrite <- (Rmult_sym ``2``). +Rewrite double. +Apply Rle_compatibility. +Left; Apply pow_lt; Sup0. +Qed. + +Lemma cv_dicho : (x,y,l1,l2:R;P:R->bool) ``x<=y`` -> (Un_cv (dicho_lb x y P) l1) -> (Un_cv (dicho_up x y P) l2) -> l1==l2. +Intros. +Assert H2 := (CV_minus ? ? ? ? H0 H1). +Cut (Un_cv [i:nat]``(dicho_lb x y P i)-(dicho_up x y P i)`` R0). +Intro. +Assert H4 := (UL_sequence ? ? ? H2 H3). +Symmetry; Apply Rminus_eq_right; Assumption. +Unfold Un_cv; Unfold R_dist. +Intros. +Assert H4 := (cv_infty_cv_R0 pow_2_n pow_2_n_neq_R0 pow_2_n_infty). +Case (total_order_T x y); Intro. +Elim s; Intro. +Unfold Un_cv in H4; Unfold R_dist in H4. +Cut ``0<y-x``. +Intro Hyp. +Cut ``0<eps/(y-x)``. +Intro. +Elim (H4 ``eps/(y-x)`` H5); Intros N H6. +Exists N; Intros. +Replace ``(dicho_lb x y P n)-(dicho_up x y P n)-0`` with ``(dicho_lb x y P n)-(dicho_up x y P n)``; [Idtac | Ring]. +Rewrite <- Rabsolu_Ropp. +Rewrite Ropp_distr3. +Rewrite dicho_lb_dicho_up. +Unfold Rdiv; Rewrite Rabsolu_mult. +Rewrite (Rabsolu_right ``y-x``). +Apply Rlt_monotony_contra with ``/(y-x)``. +Apply Rlt_Rinv; Assumption. +Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Replace ``/(pow 2 n)`` with ``/(pow 2 n)-0``; [Unfold pow_2_n Rdiv in H6; Rewrite <- (Rmult_sym eps); Apply H6; Assumption | Ring]. +Red; Intro; Rewrite H8 in Hyp; Elim (Rlt_antirefl ? Hyp). +Apply Rle_sym1. +Apply Rle_anti_compatibility with x; Rewrite Rplus_Or. +Replace ``x+(y-x)`` with y; [Assumption | Ring]. +Assumption. +Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Assumption]. +Apply Rlt_anti_compatibility with x; Rewrite Rplus_Or. +Replace ``x+(y-x)`` with y; [Assumption | Ring]. +Exists O; Intros. +Replace ``(dicho_lb x y P n)-(dicho_up x y P n)-0`` with ``(dicho_lb x y P n)-(dicho_up x y P n)``; [Idtac | Ring]. +Rewrite <- Rabsolu_Ropp. +Rewrite Ropp_distr3. +Rewrite dicho_lb_dicho_up. +Rewrite b. +Unfold Rminus Rdiv; Rewrite Rplus_Ropp_r; Rewrite Rmult_Ol; Rewrite Rabsolu_R0; Assumption. +Assumption. +Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H r)). +Qed. + +Definition cond_positivity [x:R] : bool := Cases (total_order_Rle R0 x) of + (leftT _) => true +| (rightT _) => false end. + +(* Sequential caracterisation of continuity *) +Lemma continuity_seq : (f:R->R;Un:nat->R;l:R) (continuity_pt f l) -> (Un_cv Un l) -> (Un_cv [i:nat](f (Un i)) (f l)). +Unfold continuity_pt Un_cv; Unfold continue_in. +Unfold limit1_in. +Unfold limit_in. +Unfold dist. +Simpl. +Unfold R_dist. +Intros. +Elim (H eps H1); Intros alp H2. +Elim H2; Intros. +Elim (H0 alp H3); Intros N H5. +Exists N; Intros. +Case (Req_EM (Un n) l); Intro. +Rewrite H7; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption. +Apply H4. +Split. +Unfold D_x no_cond. +Split. +Trivial. +Apply not_sym; Assumption. +Apply H5; Assumption. +Qed. + +Lemma dicho_lb_car : (x,y:R;P:R->bool;n:nat) (P x)=false -> (P (dicho_lb x y P n))=false. +Intros. +Induction n. +Simpl. +Assumption. +Simpl. +Assert X := (sumbool_of_bool (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``)). +Elim X; Intro. +Rewrite a. +Unfold dicho_lb in Hrecn; Assumption. +Rewrite b. +Assumption. +Qed. + +Lemma dicho_up_car : (x,y:R;P:R->bool;n:nat) (P y)=true -> (P (dicho_up x y P n))=true. +Intros. +Induction n. +Simpl. +Assumption. +Simpl. +Assert X := (sumbool_of_bool (P ``((Dichotomy_lb x y P n)+(Dichotomy_ub x y P n))/2``)). +Elim X; Intro. +Rewrite a. +Unfold dicho_lb in Hrecn; Assumption. +Rewrite b. +Assumption. +Qed. + +(* Intermediate Value Theorem *) +Lemma IVT : (f:R->R;x,y:R) (continuity f) -> ``x<y`` -> ``(f x)<0`` -> ``0<(f y)`` -> (sigTT R [z:R]``x<=z<=y``/\``(f z)==0``). +Intros. +Cut ``x<=y``. +Intro. +Generalize (dicho_lb_cv x y [z:R](cond_positivity (f z)) H3). +Generalize (dicho_up_cv x y [z:R](cond_positivity (f z)) H3). +Intros. +Elim X; Intros. +Elim X0; Intros. +Assert H4 := (cv_dicho ? ? ? ? ? H3 p0 p). +Rewrite H4 in p0. +Apply existTT with x0. +Split. +Split. +Apply Rle_trans with (dicho_lb x y [z:R](cond_positivity (f z)) O). +Simpl. +Right; Reflexivity. +Apply growing_ineq. +Apply dicho_lb_growing; Assumption. +Assumption. +Apply Rle_trans with (dicho_up x y [z:R](cond_positivity (f z)) O). +Apply decreasing_ineq. +Apply dicho_up_decreasing; Assumption. +Assumption. +Right; Reflexivity. +2:Left; Assumption. +Pose Vn := [n:nat](dicho_lb x y [z:R](cond_positivity (f z)) n). +Pose Wn := [n:nat](dicho_up x y [z:R](cond_positivity (f z)) n). +Cut ((n:nat)``(f (Vn n))<=0``)->``(f x0)<=0``. +Cut ((n:nat)``0<=(f (Wn n))``)->``0<=(f x0)``. +Intros. +Cut (n:nat)``(f (Vn n))<=0``. +Cut (n:nat)``0<=(f (Wn n))``. +Intros. +Assert H9 := (H6 H8). +Assert H10 := (H5 H7). +Apply Rle_antisym; Assumption. +Intro. +Unfold Wn. +Cut (z:R) (cond_positivity z)=true <-> ``0<=z``. +Intro. +Assert H8 := (dicho_up_car x y [z:R](cond_positivity (f z)) n). +Elim (H7 (f (dicho_up x y [z:R](cond_positivity (f z)) n))); Intros. +Apply H9. +Apply H8. +Elim (H7 (f y)); Intros. +Apply H12. +Left; Assumption. +Intro. +Unfold cond_positivity. +Case (total_order_Rle R0 z); Intro. +Split. +Intro; Assumption. +Intro; Reflexivity. +Split. +Intro; Elim diff_false_true; Assumption. +Intro. +Elim n0; Assumption. +Unfold Vn. +Cut (z:R) (cond_positivity z)=false <-> ``z<0``. +Intros. +Assert H8 := (dicho_lb_car x y [z:R](cond_positivity (f z)) n). +Left. +Elim (H7 (f (dicho_lb x y [z:R](cond_positivity (f z)) n))); Intros. +Apply H9. +Apply H8. +Elim (H7 (f x)); Intros. +Apply H12. +Assumption. +Intro. +Unfold cond_positivity. +Case (total_order_Rle R0 z); Intro. +Split. +Intro; Elim diff_true_false; Assumption. +Intro; Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r H7)). +Split. +Intro; Auto with real. +Intro; Reflexivity. +Cut (Un_cv Wn x0). +Intros. +Assert H7 := (continuity_seq f Wn x0 (H x0) H5). +Case (total_order_T R0 (f x0)); Intro. +Elim s; Intro. +Left; Assumption. +Rewrite <- b; Right; Reflexivity. +Unfold Un_cv in H7; Unfold R_dist in H7. +Cut ``0< -(f x0)``. +Intro. +Elim (H7 ``-(f x0)`` H8); Intros. +Cut (ge x2 x2); [Intro | Unfold ge; Apply le_n]. +Assert H11 := (H9 x2 H10). +Rewrite Rabsolu_right in H11. +Pattern 1 ``-(f x0)`` in H11; Rewrite <- Rplus_Or in H11. +Unfold Rminus in H11; Rewrite (Rplus_sym (f (Wn x2))) in H11. +Assert H12 := (Rlt_anti_compatibility ? ? ? H11). +Assert H13 := (H6 x2). +Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H13 H12)). +Apply Rle_sym1; Left; Unfold Rminus; Apply ge0_plus_gt0_is_gt0. +Apply H6. +Exact H8. +Apply Rgt_RO_Ropp; Assumption. +Unfold Wn; Assumption. +Cut (Un_cv Vn x0). +Intros. +Assert H7 := (continuity_seq f Vn x0 (H x0) H5). +Case (total_order_T R0 (f x0)); Intro. +Elim s; Intro. +Unfold Un_cv in H7; Unfold R_dist in H7. +Elim (H7 ``(f x0)`` a); Intros. +Cut (ge x2 x2); [Intro | Unfold ge; Apply le_n]. +Assert H10 := (H8 x2 H9). +Rewrite Rabsolu_left in H10. +Pattern 2 ``(f x0)`` in H10; Rewrite <- Rplus_Or in H10. +Rewrite Ropp_distr3 in H10. +Unfold Rminus in H10. +Assert H11 := (Rlt_anti_compatibility ? ? ? H10). +Assert H12 := (H6 x2). +Cut ``0<(f (Vn x2))``. +Intro. +Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H13 H12)). +Rewrite <- (Ropp_Ropp (f (Vn x2))). +Apply Rgt_RO_Ropp; Assumption. +Apply Rlt_anti_compatibility with ``(f x0)-(f (Vn x2))``. +Rewrite Rplus_Or; Replace ``(f x0)-(f (Vn x2))+((f (Vn x2))-(f x0))`` with R0; [Unfold Rminus; Apply gt0_plus_ge0_is_gt0 | Ring]. +Assumption. +Apply Rge_RO_Ropp; Apply Rle_sym1; Apply H6. +Right; Rewrite <- b; Reflexivity. +Left; Assumption. +Unfold Vn; Assumption. +Qed. + +Lemma IVT_cor : (f:R->R;x,y:R) (continuity f) -> ``x<=y`` -> ``(f x)*(f y)<=0`` -> (sigTT R [z:R]``x<=z<=y``/\``(f z)==0``). +Intros. +Case (total_order_T R0 (f x)); Intro. +Case (total_order_T R0 (f y)); Intro. +Elim s; Intro. +Elim s0; Intro. +Cut ``0<(f x)*(f y)``; [Intro; Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H1 H2)) | Apply Rmult_lt_pos; Assumption]. +Exists y. +Split. +Split; [Assumption | Right; Reflexivity]. +Symmetry; Exact b. +Exists x. +Split. +Split; [Right; Reflexivity | Assumption]. +Symmetry; Exact b. +Elim s; Intro. +Cut ``x<y``. +Intro. +Assert H3 := (IVT (opp_fct f) x y (continuity_opp f H) H2). +Cut ``(opp_fct f x)<0``. +Cut ``0<(opp_fct f y)``. +Intros. +Elim (H3 H5 H4); Intros. +Apply existTT with x0. +Elim p; Intros. +Split. +Assumption. +Unfold opp_fct in H7. +Rewrite <- (Ropp_Ropp (f x0)). +Apply eq_RoppO; Assumption. +Unfold opp_fct; Apply Rgt_RO_Ropp; Assumption. +Unfold opp_fct. +Apply Rlt_anti_compatibility with (f x); Rewrite Rplus_Ropp_r; Rewrite Rplus_Or; Assumption. +Inversion H0. +Assumption. +Rewrite H2 in a. +Elim (Rlt_antirefl ? (Rlt_trans ? ? ? r a)). +Apply existTT with x. +Split. +Split; [Right; Reflexivity | Assumption]. +Symmetry; Assumption. +Case (total_order_T R0 (f y)); Intro. +Elim s; Intro. +Cut ``x<y``. +Intro. +Apply IVT; Assumption. +Inversion H0. +Assumption. +Rewrite H2 in r. +Elim (Rlt_antirefl ? (Rlt_trans ? ? ? r a)). +Apply existTT with y. +Split. +Split; [Assumption | Right; Reflexivity]. +Symmetry; Assumption. +Cut ``0<(f x)*(f y)``. +Intro. +Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H2 H1)). +Rewrite <- Ropp_mul2; Apply Rmult_lt_pos; Apply Rgt_RO_Ropp; Assumption. +Qed. + +(* We can now define the square root function as the reciprocal transformation of the square root function *) +Lemma Rsqrt_exists : (y:R) ``0<=y`` -> (sigTT R [z:R]``0<=z``/\``y==(Rsqr z)``). +Intros. +Pose f := [x:R]``(Rsqr x)-y``. +Cut ``(f 0)<=0``. +Intro. +Cut (continuity f). +Intro. +Case (total_order_T y R1); Intro. +Elim s; Intro. +Cut ``0<=(f 1)``. +Intro. +Cut ``(f 0)*(f 1)<=0``. +Intro. +Assert X := (IVT_cor f R0 R1 H1 (Rlt_le ? ? Rlt_R0_R1) H3). +Elim X; Intros t H4. +Apply existTT with t. +Elim H4; Intros. +Split. +Elim H5; Intros; Assumption. +Unfold f in H6. +Apply Rminus_eq_right; Exact H6. +Rewrite Rmult_sym; Pattern 2 R0; Rewrite <- (Rmult_Or (f R1)). +Apply Rle_monotony; Assumption. +Unfold f. +Rewrite Rsqr_1. +Apply Rle_anti_compatibility with y. +Rewrite Rplus_Or; Rewrite Rplus_sym; Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Left; Assumption. +Apply existTT with R1. +Split. +Left; Apply Rlt_R0_R1. +Rewrite b; Symmetry; Apply Rsqr_1. +Cut ``0<=(f y)``. +Intro. +Cut ``(f 0)*(f y)<=0``. +Intro. +Assert X := (IVT_cor f R0 y H1 H H3). +Elim X; Intros t H4. +Apply existTT with t. +Elim H4; Intros. +Split. +Elim H5; Intros; Assumption. +Unfold f in H6. +Apply Rminus_eq_right; Exact H6. +Rewrite Rmult_sym; Pattern 2 R0; Rewrite <- (Rmult_Or (f y)). +Apply Rle_monotony; Assumption. +Unfold f. +Apply Rle_anti_compatibility with y. +Rewrite Rplus_Or; Rewrite Rplus_sym; Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or. +Pattern 1 y; Rewrite <- Rmult_1r. +Unfold Rsqr; Apply Rle_monotony. +Assumption. +Left; Exact r. +Replace f with (minus_fct Rsqr (fct_cte y)). +Apply continuity_minus. +Apply derivable_continuous; Apply derivable_Rsqr. +Apply derivable_continuous; Apply derivable_const. +Reflexivity. +Unfold f; Rewrite Rsqr_O. +Unfold Rminus; Rewrite Rplus_Ol. +Apply Rle_sym2. +Apply Rle_RO_Ropp; Assumption. +Qed. + +(* Definition of the square root: R+->R *) +Definition Rsqrt [y:nonnegreal] : R := Cases (Rsqrt_exists (nonneg y) (cond_nonneg y)) of (existTT a b) => a end. + +(**********) +Lemma Rsqrt_positivity : (x:nonnegreal) ``0<=(Rsqrt x)``. +Intro. +Assert X := (Rsqrt_exists (nonneg x) (cond_nonneg x)). +Elim X; Intros. +Cut x0==(Rsqrt x). +Intros. +Elim p; Intros. +Rewrite H in H0; Assumption. +Unfold Rsqrt. +Case (Rsqrt_exists x (cond_nonneg x)). +Intros. +Elim p; Elim a; Intros. +Apply Rsqr_inj. +Assumption. +Assumption. +Rewrite <- H0; Rewrite <- H2; Reflexivity. +Qed. + +(**********) +Lemma Rsqrt_Rsqrt : (x:nonnegreal) ``(Rsqrt x)*(Rsqrt x)==x``. +Intros. +Assert X := (Rsqrt_exists (nonneg x) (cond_nonneg x)). +Elim X; Intros. +Cut x0==(Rsqrt x). +Intros. +Rewrite <- H. +Elim p; Intros. +Rewrite H1; Reflexivity. +Unfold Rsqrt. +Case (Rsqrt_exists x (cond_nonneg x)). +Intros. +Elim p; Elim a; Intros. +Apply Rsqr_inj. +Assumption. +Assumption. +Rewrite <- H0; Rewrite <- H2; Reflexivity. +Qed. |