From 425f5dc5df05a85ddd35dd54136a94eb7baeb1f2 Mon Sep 17 00:00:00 2001 From: desmettr Date: Fri, 29 Mar 2002 15:09:06 +0000 Subject: sans utiliser Field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2578 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/Ranalysis.v | 173 ++++++++++++++++++++++++++++++++++----------- 1 file changed, 131 insertions(+), 42 deletions(-) diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index dcf4e6406f..a771d2b98d 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -236,8 +236,14 @@ Generalize (H5 h H6 (Rlt_le_trans (Rabsolu h) (Rmin delta1 delta2) delta2 H7 (Rm Generalize (Rplus_lt ``(Rabsolu (((f1 (x+h))-(f1 x))/h-l1))`` ``eps/2`` ``(Rabsolu (((f2 (x+h))-(f2 x))/h-l2))`` ``eps/2`` H9 H8). Replace ``eps/2+eps/2`` with ``eps``. Intro H10; Assumption. -Field; DiscrR. -Field; Assumption. +Apply double_var. +Unfold Rdiv. +Repeat Rewrite <- (Rmult_sym ``/h``). +Repeat Rewrite Rminus_distr. +Repeat Rewrite Rmult_Rplus_distr. +Unfold Rminus. +Repeat Rewrite Ropp_distr1. +Ring. Discriminate. Save. @@ -259,11 +265,15 @@ Save. (* Opposite *) Lemma deriv_opposite : (f:R->R;x:R) (derivable_pt f x) -> ``(derive_pt (opp_fct f) x)==-(derive_pt f x)``. -Intros; Generalize (derivable_derive f x H); Intro H0; Elim H0; Intros l H1; Rewrite H1; Unfold opp_fct; Apply derive_pt_def_0; Intros; Generalize (derive_pt_def_1 f x l H1); Intro H3; Elim (H3 eps H2); Intros delta H4; Exists delta; Intros; Replace ``( -(f (x+h))- -(f x))/h- -l`` with ``- (((f (x+h))-(f x))/h-l)``; [Rewrite Rabsolu_Ropp; Apply (H4 h H5 H6) | Field; Assumption]. +Intros; Generalize (derivable_derive f x H); Intro H0; Elim H0; Intros l H1; Rewrite H1; Unfold opp_fct; Apply derive_pt_def_0; Intros; Generalize (derive_pt_def_1 f x l H1); Intro H3; Elim (H3 eps H2); Intros delta H4; Exists delta; Intros; Replace ``( -(f (x+h))- -(f x))/h- -l`` with ``- (((f (x+h))-(f x))/h-l)``. +Rewrite Rabsolu_Ropp; Apply (H4 h H5 H6). +Unfold Rminus Rdiv; Rewrite Ropp_distr1; Repeat Rewrite Ropp_Ropp; Rewrite <- Ropp_mul1; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Reflexivity. Save. Lemma opposite_derivable_pt : (f:R->R;x:R) (derivable_pt f x) -> (derivable_pt (opp_fct f) x). -Unfold opp_fct derivable_pt; Intros; Elim H; Intros; Exists ``-x0``; Intros; Elim (H0 eps H1); Intros; Exists x1; Intros; Generalize (H2 h H3 H4); Intro H5; Replace ``( -(f (x+h))- -(f x))/h- -x0`` with ``- (((f (x+h))-(f x))/h-x0)``; [Rewrite Rabsolu_Ropp; Assumption | Field; Assumption]. +Unfold opp_fct derivable_pt; Intros; Elim H; Intros; Exists ``-x0``; Intros; Elim (H0 eps H1); Intros; Exists x1; Intros; Generalize (H2 h H3 H4); Intro H5; Replace ``( -(f (x+h))- -(f x))/h- -x0`` with ``- (((f (x+h))-(f x))/h-x0)``. +Rewrite Rabsolu_Ropp; Assumption. +Unfold Rminus Rdiv; Rewrite Ropp_distr1; Repeat Rewrite Ropp_Ropp; Rewrite <- Ropp_mul1; Rewrite Ropp_distr1; Rewrite Ropp_Ropp; Reflexivity. Save. Lemma opposite_derivable : (f:R->R) (derivable f) -> (derivable (opp_fct f)). @@ -303,7 +313,11 @@ Apply Rlt_monotony. Apply (Rabsolu_pos_lt a H1). Apply (H3 h H4 H5). Rewrite <- Rmult_sym; Unfold Rdiv; Rewrite Rmult_assoc; Rewrite <- (Rinv_l_sym (Rabsolu a)); [Apply Rmult_1r | Apply (Rabsolu_no_R0 a H1)]. -Field; Assumption. +Rewrite Rminus_distr. +Unfold Rdiv. +Rewrite <- Rmult_assoc. +Rewrite Rminus_distr. +Reflexivity. Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply (Rabsolu_pos_lt a H1)]. Save. @@ -318,7 +332,11 @@ Apply Rlt_monotony. Apply (Rabsolu_pos_lt a H1). Apply (H4 h H5 H6). Rewrite <- Rmult_sym; Unfold Rdiv; Rewrite Rmult_assoc; Rewrite <- (Rinv_l_sym (Rabsolu a)); [Apply Rmult_1r | Apply (Rabsolu_no_R0 a H1)]. -Field; Assumption. +Rewrite Rminus_distr. +Unfold Rdiv. +Rewrite <- Rmult_assoc. +Rewrite Rminus_distr. +Reflexivity. Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply (Rabsolu_pos_lt a H1)]. Save. @@ -327,8 +345,7 @@ Intros; Generalize (scal_derivable_pt f a x H); Unfold mult_real_fct; Intro; Ass Save. Lemma scal_derivable : (f:R->R;a:R) (derivable f) -> (derivable (mult_real_fct a f)). -Unfold derivable; Intros f a H1 x; Apply scal_derivable_pt; Exact -(H1 x). +Unfold derivable; Intros f a H1 x; Apply scal_derivable_pt; Exact (H1 x). Save. Lemma derive_scal : (f:R->R;a,x:R) (derivable_pt f x) -> (derive_pt ([x:R]``a*(f x)``) x)==``a*(derive_pt f x)``. @@ -372,11 +389,21 @@ Save. Lemma deriv_id : (x:R) (derive_pt ([y:R] y) x)==``1``. Intro x; Apply derive_pt_def_0; Intros; Exists (mkposreal ``1`` Rlt_R0_R1); Intros; Replace ``(x+h-x)/h-1`` with ``0``. Rewrite Rabsolu_R0; Assumption. -Field; Assumption. +Unfold Rminus; Rewrite Rplus_assoc; Rewrite (Rplus_sym x); Rewrite Rplus_assoc. +Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Unfold Rdiv; Rewrite <- Rinv_r_sym. +Symmetry; Apply Rplus_Ropp_r. +Assumption. Save. Lemma diff_id : (derivable ([x:R] x)). -Unfold derivable; Intro x; Unfold derivable_pt; Exists ``1``; Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Replace ``(x+h-x)/h-1`` with ``0``; [Rewrite Rabsolu_R0; Apply Rle_lt_trans with ``(Rabsolu h)``; [Apply Rabsolu_pos | Assumption] | Field; Assumption]. +Unfold derivable; Intro x; Unfold derivable_pt; Exists ``1``; Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Replace ``(x+h-x)/h-1`` with ``0``. +Rewrite Rabsolu_R0; Apply Rle_lt_trans with ``(Rabsolu h)``. +Apply Rabsolu_pos. +Assumption. +Unfold Rminus; Rewrite Rplus_assoc; Rewrite (Rplus_sym x); Rewrite Rplus_assoc. +Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Unfold Rdiv; Rewrite <- Rinv_r_sym. +Symmetry; Apply Rplus_Ropp_r. +Assumption. Save. (**********) @@ -394,11 +421,27 @@ Save. (**********) Lemma deriv_Rsqr : (x:R) (derive Rsqr x)==``2*x``. -Intro x; Unfold Rsqr; Unfold derive; Apply (derive_pt_def_0 ([x0:R]``x0*x0``) x); Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Replace ``((x+h)*(x+h)-x*x)/h-2*x`` with ``h``; [Assumption | Field; Assumption]. +Intro x; Unfold Rsqr; Unfold derive; Apply (derive_pt_def_0 ([x0:R]``x0*x0``) x); Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Replace ``((x+h)*(x+h)-x*x)/h-2*x`` with ``h``. +Assumption. +Replace ``(x+h)*(x+h)`` with ``(Rsqr (x+h))``. +Rewrite Rsqr_plus; Unfold Rminus; Repeat Rewrite Rplus_assoc; Rewrite (Rplus_sym (Rsqr x)); Repeat Rewrite Rplus_assoc; Unfold Rsqr; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Unfold Rdiv; Rewrite Rmult_Rplus_distrl. +Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. +Repeat Rewrite Rmult_1r; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r. +Rewrite Rplus_Or; Reflexivity. +Assumption. +Unfold Rsqr; Reflexivity. Save. Lemma diff_Rsqr : (derivable Rsqr). -Unfold derivable; Intro x; Unfold Rsqr; Unfold derivable_pt; Exists ``2*x``; Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Replace ``((x+h)*(x+h)-x*x)/h-2*x`` with ``h``; [Assumption | Field; Assumption]. +Unfold derivable; Intro x; Unfold Rsqr; Unfold derivable_pt; Exists ``2*x``; Intros eps Heps; Exists (mkposreal eps Heps); Intros h H1 H2; Replace ``((x+h)*(x+h)-x*x)/h-2*x`` with ``h``. +Assumption. +Replace ``(x+h)*(x+h)`` with ``(Rsqr (x+h))``. +Rewrite Rsqr_plus; Unfold Rminus; Repeat Rewrite Rplus_assoc; Rewrite (Rplus_sym (Rsqr x)); Repeat Rewrite Rplus_assoc; Unfold Rsqr; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Unfold Rdiv; Rewrite Rmult_Rplus_distrl. +Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. +Repeat Rewrite Rmult_1r; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r. +Rewrite Rplus_Or; Reflexivity. +Assumption. +Unfold Rsqr; Reflexivity. Save. Lemma Rsqr_derivable_pt : (f:R->R;t:R) (derivable_pt f t) -> (derivable_pt ([x:R](Rsqr (f x))) t). @@ -531,7 +574,10 @@ Unfold Rabsolu; Case (case_Rabsolu ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f Replace `` -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l)`` with ``l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2)))``. Intro; Generalize (Rlt_compatibility ``-l`` ``l+ -(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2)))`` ``l/2`` H20); Repeat Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Replace ``-l+l/2`` with ``-(l/2)``. Intro; Generalize (Rlt_Ropp ``-(((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2)))`` ``-(l/2)`` H21); Repeat Rewrite Ropp_Ropp; Intro; Generalize (Rlt_trans ``0`` ``l/2`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))`` H7 H22); Intro; Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))`` ``0`` H23 H17)). -Field; DiscrR. +Pattern 2 l; Rewrite double_var. +Rewrite Ropp_distr1. +Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l. +Symmetry; Apply Rplus_Or. Ring. Intro; Generalize (Rle_sym2 ``0`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l`` r); Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` ``((f (c+(Rmin (delta/2) ((b+ -c)/2))))+ -(f c))/(Rmin (delta/2) ((b+ -c)/2))+ -l`` ``0`` H21 H19)). Assumption. @@ -541,7 +587,18 @@ Ring. Rewrite <- Ropp_O; Apply Rlt_Ropp; Assumption. Replace ``((f (c+(Rmin (delta/2) ((b-c)/2))))-(f c))/(Rmin (delta/2) ((b-c)/2))`` with ``- (((f c)-(f (c+(Rmin (delta/2) ((b-c)/2)))))/(Rmin (delta/2) ((b-c)/2)))``. Rewrite <- Ropp_O; Apply Rge_Ropp; Apply Rle_sym1; Unfold Rdiv; Apply Rmult_le_pos; [Generalize (Rle_compatibility_r ``-(f (c+(Rmin (delta*/2) ((b-c)*/2))))`` ``(f (c+(Rmin (delta*/2) ((b-c)*/2))))`` (f c) H16); Rewrite Rplus_Ropp_r; Intro; Assumption | Left; Apply Rlt_Rinv; Assumption]. -Field; Assumption. +Unfold Rdiv. +Rewrite <- Ropp_mul1. +Repeat Rewrite <- (Rmult_sym ``/(Rmin (delta*/2) ((b-c)*/2))``). +Apply r_Rmult_mult with ``(Rmin (delta*/2) ((b-c)*/2))``. +Repeat Rewrite <- Rmult_assoc. +Rewrite <- Rinv_r_sym. +Repeat Rewrite Rmult_1l. +Ring. +Red; Intro. +Unfold Rdiv in H13; Rewrite H17 in H13; Elim (Rlt_antirefl ``0`` H13). +Red; Intro. +Unfold Rdiv in H13; Rewrite H17 in H13; Elim (Rlt_antirefl ``0`` H13). Generalize (Rmin_r ``(delta/2)`` ``((b-c)/2)``); Intro; Generalize (Rle_compatibility ``c`` ``(Rmin (delta/2) ((b-c)/2))`` ``(b-c)/2`` H14); Intro; Apply Rle_lt_trans with ``c+(b-c)/2``. Assumption. Apply Rlt_monotony_contra with ``2``. @@ -550,7 +607,12 @@ Replace ``2*(c+(b-c)/2)`` with ``c+b``. Replace ``2*b`` with ``b+b``. Apply Rlt_compatibility_r; Assumption. Ring. -Field; DiscrR. +Unfold Rdiv; Rewrite Rmult_Rplus_distr. +Repeat Rewrite (Rmult_sym ``2``). +Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r. +Ring. +Apply aze. Apply Rlt_trans with c. Assumption. Pattern 1 c; Rewrite <- (Rplus_Or c); Apply Rlt_compatibility; Assumption. @@ -572,8 +634,8 @@ Rewrite Rmult_1l. Replace ``2*delta`` with ``delta+delta``. Pattern 2 delta; Rewrite <- (Rplus_Or delta); Apply Rlt_compatibility. Rewrite Rplus_Or; Apply (cond_pos delta). -Ring. -DiscrR. +Symmetry; Apply double. +Apply aze. Cut ``0R;a,b,c:R) ``a``c(derivable_pt f c)->((x:R) ``a``x``(f c)<=(f x)``)->``(derive_pt f c)==0``. @@ -672,7 +754,8 @@ Intros; Generalize (Rlt_compatibility_r l ``((f (x+delta/2))-(f x))/(delta/2)-l` Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Intro; Generalize (Rle_lt_trans ``0`` ``((f (x+delta/2))-(f x))/(delta/2)`` ``l/2`` H10 H15); Intro; Cut ``l/2<0``. Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``l/2`` ``0`` H16 H17)). Rewrite <- Ropp_O in H6; Generalize (Rlt_Ropp ``-0`` ``-(l/2)`` H6); Repeat Rewrite Ropp_Ropp; Intro; Assumption. -Field; DiscrR. +Pattern 3 l ; Rewrite double_var. +Ring. Unfold Rminus; Apply ge0_plus_ge0_is_ge0. Unfold Rdiv; Apply Rmult_le_pos. Cut ``x<=(x+(delta*/2))``. @@ -702,7 +785,9 @@ Apply Rlt_compatibility. Rewrite Rplus_Or. Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. Ring. -Field; DiscrR. +Rewrite <- Rmult_assoc. +Apply Rinv_r_simpl_m. +Apply aze. Rewrite <- Ropp_O; Apply Rlt_Ropp; Unfold Rdiv; Generalize (Rlt_monotony_r ``/2`` l ``0`` (Rlt_Rinv ``2`` Rgt_2_0) H4); Rewrite Rmult_Ol; Intro; Assumption. Save. @@ -731,7 +816,8 @@ Intro. Generalize (Rlt_trans ``0`` ``l/2`` ``((f (x+delta/2))-(f x))/(delta/2)`` H6 H16); Intro. Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``((f (x+delta/2))-(f x))/(delta/2)`` ``0`` H17 H10)). Ring. -Field; DiscrR. +Pattern 3 l; Rewrite double_var. +Ring. Intros. Generalize (Rge_Ropp ``((f (x+delta/2))-(f x))/(delta/2)-l`` ``0`` r). Rewrite Ropp_O. @@ -746,12 +832,15 @@ Intro; Generalize (H0 x ``x+(delta*/2)`` H13); Intro; Generalize (Rle_compatibil Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption. Left; Apply Rlt_Rinv; Assumption. Assumption. -Field. -DiscrR. -Case delta; Intros. -Apply prod_neq_R0. -Compute; Intro H13; Rewrite H13 in cond_pos; Elim (Rlt_antirefl ``0`` cond_pos). -Apply Rinv_neq_R0; DiscrR. +Rewrite Ropp_distr2. +Unfold Rminus. +Rewrite (Rplus_sym l). +Unfold Rdiv. +Rewrite <- Ropp_mul1. +Rewrite Ropp_distr1. +Rewrite Ropp_Ropp. +Rewrite (Rplus_sym (f x)). +Reflexivity. Replace ``((f (x+delta/2))-(f x))/(delta/2)`` with ``-(((f x)-(f (x+delta/2)))/(delta/2))``. Rewrite <- Ropp_O. Apply Rge_Ropp. @@ -762,11 +851,9 @@ Intro; Generalize (H0 x ``x+(delta*/2)`` H10); Intro. Generalize (Rle_compatibility ``-(f (x+delta/2))`` ``(f (x+delta/2))`` ``(f x)`` H13); Rewrite Rplus_Ropp_l; Rewrite Rplus_sym; Intro; Assumption. Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Left; Assumption. Left; Apply Rlt_Rinv; Assumption. -Field. -Case delta; Intros. -Apply prod_neq_R0. -Compute; Intro H13; Rewrite H13 in cond_pos; Elim (Rlt_antirefl ``0`` cond_pos). -Apply Rinv_neq_R0; DiscrR. +Unfold Rdiv; Rewrite <- Ropp_mul1. +Rewrite Ropp_distr2. +Reflexivity. Split. Unfold Rdiv; Apply prod_neq_R0. Generalize (cond_pos delta); Intro; Red; Intro H9; Rewrite H9 in H8; Elim (Rlt_antirefl ``0`` H8). @@ -784,7 +871,9 @@ Apply Rlt_compatibility. Rewrite Rplus_Or. Apply Rmult_lt_pos; [Apply (cond_pos delta) | Apply Rlt_Rinv; Apply Rgt_2_0]. Ring. -Field; DiscrR. +Rewrite <- Rmult_assoc. +Apply Rinv_r_simpl_m. +Apply aze. Unfold Rdiv; Apply Rmult_lt_pos. Assumption. Apply Rlt_Rinv; Apply Rgt_2_0. -- cgit v1.2.3