diff options
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/DiscrR.v | 29 | ||||
| -rw-r--r-- | theories/Reals/Exp_prop.v | 4 | ||||
| -rw-r--r-- | theories/Reals/R_sqr.v | 31 | ||||
| -rw-r--r-- | theories/Reals/R_sqrt.v | 29 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis2.v | 18 | ||||
| -rw-r--r-- | theories/Reals/Ranalysis3.v | 22 | ||||
| -rw-r--r-- | theories/Reals/Rbase.v | 4 | ||||
| -rw-r--r-- | theories/Reals/Rsyntax.v | 31 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo.v | 14 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo_alt.v | 4 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo_calc.v | 24 |
11 files changed, 118 insertions, 92 deletions
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 828962656..494a7d685 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -39,17 +39,20 @@ Tactic Definition DiscrR := Replace ?1 with (INR nbr); [Apply not_O_INR;Discriminate|Simpl;Ring]). -Tactic Definition Sup0_lt trm:= - Replace ``0`` with (INR O); - [Let nbr=(ToINR trm) In - Replace trm with (INR nbr); - [Apply lt_INR; Apply lt_O_Sn|Simpl;Ring]|Simpl;Reflexivity]. - -Tactic Definition Sup0_gt trm:= - Unfold Rgt; Sup0_lt trm. - -Tactic Definition Sup0 := +Lemma Rlt_R0_R2 : ``0<2``. +Replace ``2`` with (INR (2)); [Apply lt_INR_0; Apply lt_O_Sn | Reflexivity]. +Qed. + +Lemma Rplus_lt_pos : (x,y:R) ``0<x`` -> ``0<y`` -> ``0<x+y``. +Intros. +Apply Rlt_trans with x. +Assumption. +Pattern 1 x; Rewrite <- Rplus_Or. +Apply Rlt_compatibility. +Assumption. +Qed. + +Recursive Tactic Definition Sup0 := Match Context With - | [ |- ``0<?1`` ] -> (Sup0_lt ?1) - | [ |- ``?1>0`` ] -> (Sup0_gt ?1). - + | [ |- ``0<?1`` ] -> Repeat (Apply Rmult_lt_pos Orelse Apply Rplus_lt_pos; Try Apply Rlt_R0_R1 Orelse Apply Rlt_R0_R2) + | [ |- ``?1>0`` ] -> Change ``0<?1``; Sup0.
\ No newline at end of file diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index ae6433466..3c2b16f10 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -381,6 +381,7 @@ Repeat Rewrite <- Rmult_assoc. Rewrite <- Rinv_r_sym. Rewrite Rmult_1l. Replace ``(INR N)*(INR N)`` with (Rsqr (INR N)); [Idtac | Reflexivity]. +Rewrite Rmult_assoc. Rewrite Rmult_sym. Replace ``4`` with (Rsqr ``2``); [Idtac | SqRing]. Rewrite <- Rsqr_times. @@ -576,8 +577,9 @@ Apply RmaxLess1. Left; Apply Rlt_Rinv; Apply INR_fact_lt_0. DiscrR. Apply Rle_sym1. -Unfold Rdiv; Repeat Apply Rmult_le_pos. +Unfold Rdiv; Apply Rmult_le_pos. Left; Sup0. +Apply Rmult_le_pos. Apply pow_le. Apply Rle_trans with R1. Left; Apply Rlt_R0_R1. diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 2cd6e2fb9..8a711809e 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -168,6 +168,7 @@ Intros; Unfold Rsqr. Rewrite Rinv_Rmult; Try Reflexivity Orelse Assumption. Qed. +Import R_scope. Lemma canonical_Rsqr : (a:nonzeroreal;b,c,x:R) ``a*(Rsqr x)+b*x+c == a* (Rsqr (x+b/(2*a))) + (4*a*c - (Rsqr b))/(4*a)``. Intros. Rewrite Rsqr_plus. @@ -175,6 +176,7 @@ Repeat Rewrite Rmult_Rplus_distr. Repeat Rewrite Rplus_assoc. Apply Rplus_plus_r. Unfold Rdiv Rminus. +Replace ``2*1+2*1`` with ``4``; [Idtac | Ring]. Rewrite (Rmult_Rplus_distrl ``4*a*c`` ``-(Rsqr b)`` ``/(4*a)``). Rewrite Rsqr_times. Repeat Rewrite Rinv_Rmult. @@ -186,39 +188,36 @@ Rewrite (Rmult_sym ``2``). Repeat Rewrite Rmult_assoc. Rewrite <- Rinv_l_sym. Rewrite Rmult_1r. -Rewrite (Rmult_sym ``/4``). -Rewrite (Rmult_sym ``4``). +Rewrite (Rmult_sym ``/2``). +Rewrite (Rmult_sym ``2``). Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. Rewrite Rmult_1r. Rewrite (Rmult_sym a). -Rewrite Rmult_assoc. +Repeat Rewrite Rmult_assoc. Rewrite <- Rinv_l_sym. Rewrite Rmult_1r. -Rewrite (Rmult_sym x). +Rewrite (Rmult_sym ``2``). +Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. +Rewrite Rmult_1r. Repeat Rewrite Rplus_assoc. -Rewrite (Rplus_sym ``(Rsqr b)*((Rsqr (/2*/a))*a)``). +Rewrite (Rplus_sym ``(Rsqr b)*((Rsqr (/a*/2))*a)``). Repeat Rewrite Rplus_assoc. +Rewrite (Rmult_sym x). Apply Rplus_plus_r. -Rewrite Ropp_mul1. -Unfold Rsqr. -Repeat Rewrite Rmult_assoc. +Rewrite (Rmult_sym ``/a``). +Unfold Rsqr; Repeat Rewrite Rmult_assoc. Rewrite <- Rinv_l_sym. Rewrite Rmult_1r. -Rewrite <- (Rmult_sym ``(/a*/2)``). -Rewrite Rmult_assoc. -Rewrite <- (Rinv_Rmult ``2`` ``2``). -Replace ``2*2`` with ``4``. -Rewrite Rplus_Ropp_l. -Symmetry; Apply Rplus_Or. Ring. -DiscrR. -DiscrR. Apply (cond_nonzero a). +DiscrR. Apply (cond_nonzero a). DiscrR. DiscrR. Apply (cond_nonzero a). DiscrR. +DiscrR. +DiscrR. Apply (cond_nonzero a). DiscrR. Apply (cond_nonzero a). diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index eb3f967a3..b830f213a 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -141,17 +141,19 @@ Unfold Rsqr; Repeat Rewrite Rinv_Rmult. Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym a). Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. Rewrite Rmult_1r; Rewrite Rmult_Rplus_distrl. -Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``). +Repeat Rewrite Rmult_assoc. +Pattern 2 ``2``; Rewrite (Rmult_sym ``2``). Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Rewrite (Rmult_Rplus_distrl ``-b`` ``(sqrt (b*b-4*(a*c))) `` ``(/2*/a)``). +Rewrite Rmult_1r. +Rewrite (Rmult_Rplus_distrl ``-b`` ``(sqrt (b*b-(2*(2*(a*c)))))`` ``(/2*/a)``). Rewrite Rmult_Rplus_distr; Repeat Rewrite Rplus_assoc. -Replace ``( -b*((sqrt (b*b-4*(a*c)))*(/2*/a))+(b*( -b*(/2*/a))+(b*((sqrt (b*b-4*(a*c)))*(/2*/a))+c)))`` with ``(b*( -b*(/2*/a)))+c``. +Replace ``( -b*((sqrt (b*b-(2*(2*(a*c)))))*(/2*/a))+(b*( -b*(/2*/a))+(b*((sqrt (b*b-(2*(2*(a*c)))))*(/2*/a))+c)))`` with ``(b*( -b*(/2*/a)))+c``. Unfold Rminus; Repeat Rewrite <- Rplus_assoc. Replace ``b*b+b*b`` with ``2*(b*b)``. Rewrite Rmult_Rplus_distrl; Repeat Rewrite Rmult_assoc. Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc. Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Replace ``2+1+1`` with ``2*2``. +Rewrite Rmult_1r. Rewrite Ropp_mul1; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``). Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. Rewrite Rmult_1r; Rewrite (Rmult_sym ``/2``); Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``). @@ -164,13 +166,9 @@ Ring. Apply (cond_nonzero a). DiscrR. DiscrR. -Ring. DiscrR. Ring. -Repeat Rewrite Rplus_assoc; Repeat Rewrite <- (Rplus_sym c); Repeat Rewrite Rplus_assoc. -Rewrite (Rplus_sym ``-b*((sqrt (b*b-4*(a*c)))*(/2*/a))``); Repeat Rewrite Rplus_assoc. -Repeat Rewrite Ropp_mul1; Rewrite Rplus_Ropp_r. -Rewrite Rplus_Or; Apply Rplus_sym. +Ring. DiscrR. Apply (cond_nonzero a). DiscrR. @@ -185,15 +183,14 @@ Unfold Rsqr; Repeat Rewrite Rinv_Rmult; Repeat Rewrite Rmult_assoc. Rewrite (Rmult_sym a); Repeat Rewrite Rmult_assoc. Rewrite <- Rinv_l_sym. Rewrite Rmult_1r; Unfold Rminus; Rewrite Rmult_Rplus_distrl. -Rewrite Ropp_mul1; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``). +Rewrite Ropp_mul1; Repeat Rewrite Rmult_assoc; Pattern 2 ``2``; Rewrite (Rmult_sym ``2``). Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Rewrite (Rmult_Rplus_distrl ``-b`` ``-(sqrt (b*b+ -(4*(a*c)))) `` ``(/2*/a)``). +Rewrite Rmult_1r; Rewrite (Rmult_Rplus_distrl ``-b`` ``-(sqrt (b*b+ -(2*(2*(a*c))))) `` ``(/2*/a)``). Rewrite Rmult_Rplus_distr; Repeat Rewrite Rplus_assoc. Rewrite Ropp_mul1; Rewrite Ropp_Ropp. -Replace ``(b*((sqrt (b*b+ -(4*(a*c))))*(/2*/a))+(b*( -b*(/2*/a))+(b*( -(sqrt (b*b+ -(4*(a*c))))*(/2*/a))+c)))`` with ``(b*( -b*(/2*/a)))+c``. +Replace ``(b*((sqrt (b*b+ -(2*(2*(a*c)))))*(/2*/a))+(b*( -b*(/2*/a))+(b*( -(sqrt (b*b+ -(2*(2*(a*c)))))*(/2*/a))+c)))`` with ``(b*( -b*(/2*/a)))+c``. Repeat Rewrite <- Rplus_assoc; Replace ``b*b+b*b`` with ``2*(b*b)``. Rewrite Rmult_Rplus_distrl; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Replace ``2+1+1`` with ``2*2``. Rewrite Ropp_mul1; Repeat Rewrite Rmult_assoc. Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. Rewrite Rmult_1r; Rewrite (Rmult_sym ``/2``); Repeat Rewrite Rmult_assoc. @@ -203,13 +200,13 @@ Rewrite Rmult_1r; Rewrite <- Ropp_mul2; Ring. Apply (cond_nonzero a). DiscrR. DiscrR. -Ring. DiscrR. Ring. Ring. DiscrR. Apply (cond_nonzero a). DiscrR. +DiscrR. Apply (cond_nonzero a). Apply prod_neq_R0; DiscrR Orelse Apply (cond_nonzero a). Apply prod_neq_R0; DiscrR Orelse Apply (cond_nonzero a). @@ -236,10 +233,10 @@ Repeat Rewrite Rmult_assoc. Rewrite (Rmult_sym ``/a``). Rewrite Rmult_assoc. Rewrite <- Rinv_Rmult. -Replace ``4*a*a`` with ``(Rsqr (2*a))``. +Replace ``(2*(2*a))*a`` with ``(Rsqr (2*a))``. Reflexivity. SqRing. -Apply prod_neq_R0; [DiscrR | Apply (cond_nonzero a)]. +Rewrite <- Rmult_assoc; Apply prod_neq_R0; [DiscrR | Apply (cond_nonzero a)]. Apply (cond_nonzero a). Assumption. Apply prod_neq_R0; [DiscrR | Apply (cond_nonzero a)]. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 85c92176f..5af07f40f 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -34,11 +34,11 @@ Case (total_order_Rle x y); Intro; Assumption. Qed. Lemma Rgt_8_0 : ``0 < 8``. -Cut ~(O=(8)); [Intro H; Generalize (lt_INR_0 (8) (neq_O_lt (8) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H0; Assumption | Discriminate]. +Sup0. Qed. Lemma Rgt_4_0 : ``0 < 4``. -Cut ~(O=(4)); [Intro H; Generalize (lt_INR_0 (4) (neq_O_lt (4) H)); Rewrite INR_eq_INR2; Unfold INR2; Intro H0; Assumption | Discriminate]. +Sup0. Qed. Lemma maj_term1 : (x,h,eps,l1,alp_f2:R;eps_f2,alp_f1d:posreal;f1,f2:R->R) ``0 < eps`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ((h:R)``h <> 0``->``(Rabsolu h) < alp_f1d``->``(Rabsolu (((f1 (x+h))-(f1 x))/h-l1)) < (Rabsolu ((eps*(f2 x))/8))``) -> ((a:R)``(Rabsolu a) < (Rmin eps_f2 alp_f2)``->``/(Rabsolu (f2 (x+a))) < 2/(Rabsolu (f2 x))``) -> ``h<>0`` -> ``(Rabsolu h)<alp_f1d`` -> ``(Rabsolu h) < (Rmin eps_f2 alp_f2)`` -> ``(Rabsolu (/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1))) < eps/4``. @@ -98,7 +98,8 @@ Unfold Rdiv in H8; Exact H8. Symmetry; Apply Rabsolu_right; Left; Sup0. Right. Unfold Rsqr Rdiv. -Repeat Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Do 1 Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Do 1 Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. Repeat Rewrite Rabsolu_mult. Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR. Replace (Rabsolu eps) with eps. @@ -144,7 +145,8 @@ Unfold Rdiv in H9; Exact H9. Symmetry; Apply Rabsolu_right; Left; Sup0. Right. Unfold Rsqr Rdiv. -Repeat Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. Repeat Rewrite Rabsolu_mult. Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR. Replace (Rabsolu eps) with eps. @@ -174,7 +176,8 @@ Apply Rlt_monotony_r. Apply Rabsolu_pos_lt. Unfold Rdiv; Unfold Rsqr; Repeat Apply prod_neq_R0; Assumption Orelse Idtac. Red; Intro H11; Rewrite H11 in H; Elim (Rlt_antirefl ? H). -Apply Rinv_neq_R0; Repeat Apply prod_neq_R0. +Apply Rinv_neq_R0; Apply prod_neq_R0. +Apply prod_neq_R0. DiscrR. Assumption. Assumption. @@ -193,7 +196,10 @@ Rewrite <- (Rmult_sym ``2``). Unfold Rdiv in H10; Exact H10. Symmetry; Apply Rabsolu_right; Left; Sup0. Right; Unfold Rsqr Rdiv. -Repeat Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. +Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. Repeat Rewrite Rabsolu_mult. Repeat Rewrite Rabsolu_Rinv; Try Assumption Orelse DiscrR. Replace (Rabsolu eps) with eps. diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index 5ffa915dc..5ef28ab37 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -91,7 +91,7 @@ Unfold limit_in in H10. Unfold dist in H10. Simpl in H10. Unfold R_dist in H10. -Elim (H10 ``(Rabsolu (eps*(Rsqr (f2 x)))/(8*l1))``); [Idtac | Change ``0<(Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``; Apply Rabsolu_pos_lt; Unfold Rdiv Rsqr; Repeat Rewrite Rmult_assoc; Repeat Apply prod_neq_R0; [Red; Intro; Rewrite H11 in H6; Elim (Rlt_antirefl ? H6) | Assumption | Assumption | Apply Rinv_neq_R0; Apply prod_neq_R0; [DiscrR | Assumption]]]. +Elim (H10 ``(Rabsolu (eps*(Rsqr (f2 x)))/(8*l1))``). Clear H10; Intros alp_f2t2 H10. Cut (a:R) ``(Rabsolu a) < alp_f2t2`` -> ``(Rabsolu ((f2 (x+a)) - (f2 x))) < (Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``. Intro H11. @@ -153,18 +153,24 @@ Apply Rabsolu_pos_lt. Unfold Rdiv Rsqr; Repeat Rewrite Rmult_assoc. Repeat Apply prod_neq_R0; Try Assumption. Red; Intro; Rewrite H15 in H6; Elim (Rlt_antirefl ? H6). -Apply Rinv_neq_R0; Apply prod_neq_R0; [DiscrR | Assumption]. +Apply Rinv_neq_R0; Repeat Apply prod_neq_R0; DiscrR Orelse Assumption. Apply H13. Split. Apply D_x_no_cond; Assumption. Replace ``x+a-x`` with a; [Assumption | Ring]. +Change ``0<(Rabsolu ((eps*(Rsqr (f2 x)))/(8*l1)))``. +Apply Rabsolu_pos_lt; Unfold Rdiv Rsqr; Repeat Rewrite Rmult_assoc; Repeat Apply prod_neq_R0. +Red; Intro; Rewrite H11 in H6; Elim (Rlt_antirefl ? H6). +Assumption. +Assumption. +Apply Rinv_neq_R0; Repeat Apply prod_neq_R0; [DiscrR | DiscrR | DiscrR | Assumption]. (***********************************) (* Cas n° 3 *) (* (f1 x)<>0 l1=0 l2=0 *) (***********************************) Case (Req_EM l1 R0); Intro. Case (Req_EM l2 R0); Intro. -Elim (H0 ``(Rabsolu ((Rsqr (f2 x))*eps)/(8*(f1 x)))``); [Idtac | Apply Rabsolu_pos_lt; Unfold Rdiv Rsqr; Repeat Rewrite Rmult_assoc; Repeat Apply prod_neq_R0; [Assumption | Assumption | Red; Intro; Rewrite H11 in H6; Elim (Rlt_antirefl ? H6) | Apply Rinv_neq_R0; Apply prod_neq_R0; DiscrR Orelse Assumption]]. +Elim (H0 ``(Rabsolu ((Rsqr (f2 x))*eps)/(8*(f1 x)))``); [Idtac | Apply Rabsolu_pos_lt; Unfold Rdiv Rsqr; Repeat Rewrite Rmult_assoc; Repeat Apply prod_neq_R0; [Assumption | Assumption | Red; Intro; Rewrite H11 in H6; Elim (Rlt_antirefl ? H6) | Apply Rinv_neq_R0; Repeat Apply prod_neq_R0; DiscrR Orelse Assumption]]. Intros alp_f2d H12. Cut ``0 < (Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d))``. Intro. @@ -286,9 +292,15 @@ Repeat Rewrite Rinv_Rmult; Try Assumption. Repeat Apply prod_neq_R0; Try Assumption. Red; Intro H18; Rewrite H18 in H6; Elim (Rlt_antirefl ? H6). Apply Rinv_neq_R0; DiscrR. +Apply Rinv_neq_R0; DiscrR. +Apply Rinv_neq_R0; DiscrR. Apply Rinv_neq_R0; Assumption. Apply Rinv_neq_R0; Assumption. DiscrR. +DiscrR. +DiscrR. +DiscrR. +DiscrR. Apply prod_neq_R0; [DiscrR | Assumption]. Elim H13; Intros. Apply H19. @@ -308,11 +320,15 @@ Repeat Rewrite Rinv_Rmult; Try Assumption Orelse DiscrR. Repeat Apply prod_neq_R0; Try Assumption. Red; Intro H13; Rewrite H13 in H6; Elim (Rlt_antirefl ? H6). Apply Rinv_neq_R0; DiscrR. +Apply Rinv_neq_R0; DiscrR. +Apply Rinv_neq_R0; DiscrR. Apply Rinv_neq_R0; Assumption. Apply Rinv_neq_R0; Assumption. Apply prod_neq_R0; [DiscrR | Assumption]. Red; Intro H11; Rewrite H11 in H6; Elim (Rlt_antirefl ? H6). Apply Rinv_neq_R0; DiscrR. +Apply Rinv_neq_R0; DiscrR. +Apply Rinv_neq_R0; DiscrR. Apply Rinv_neq_R0; Assumption. (***********************************) (* Cas n° 5 *) diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index 11203d5ba..09dadee90 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -1508,7 +1508,7 @@ Qed. Lemma double_var : (x:R) ``x == x/2 + x/2``. Intro; Rewrite <- double; Unfold Rdiv; Rewrite <- Rmult_assoc; Symmetry; Apply Rinv_r_simpl_m. -Replace ``2`` with (INR (2)); [Apply not_O_INR; Discriminate | Reflexivity]. +Replace ``2`` with (INR (2)); [Apply not_O_INR; Discriminate | Unfold INR; Ring]. Qed. (**********************************************************) @@ -1597,4 +1597,4 @@ Qed. (**********) Lemma complet_weak : (E:R->Prop) (bound E) -> (ExT [x:R] (E x)) -> (ExT [m:R] (is_lub E m)). Intros; Elim (complet E H H0); Intros; Split with x; Assumption. -Qed. +Qed.
\ No newline at end of file diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v index 96cb568f2..44c2638e8 100644 --- a/theories/Reals/Rsyntax.v +++ b/theories/Reals/Rsyntax.v @@ -9,7 +9,8 @@ Require Export Rdefinitions. -Axiom NRplus : R->R->R. +Axiom NRplus : R->R. +Axiom NRmult : R->R. Grammar rnatural ident := nat_id [ prim:var($id) ] -> [$id] @@ -73,7 +74,6 @@ with rapplication : constr := | pair [ rexpr($p) "," rexpr($c) ] -> [ ($p, $c) ] | appl0 [ rexpr($a) ] -> [ $a ]. - Grammar constr constr0 := r_in_com [ "``" rnatural:rformula($c) "``" ] -> [ $c ]. @@ -81,10 +81,6 @@ Grammar constr atomic_pattern := r_in_pattern [ "``" rnatural:rnumber($c) "``" ] -> [ $c ]. (*i* pp **) -(* pb: on rajoute des () lorsque les constantes commencent par 1 lors de -l'appel avec NRplus i*) - - Syntax constr level 0: @@ -119,7 +115,7 @@ Syntax constr level 7: Rplus [ (Rplus $n1 $n2) ] -> [ [<hov 0> "``"(REXPR $n1):E "+" [0 0] (REXPR $n2):L "``"] ] - | Rconst [(Rplus R1 $r)] -> [$r:"r_printer_outside"] + | Rodd_outside [(Rplus R1 $r)] -> [ $r:"r_printer_odd_outside"] | Rminus [ (Rminus $n1 $n2) ] -> [ [<hov 0> "``"(REXPR $n1):E "-" [0 0] (REXPR $n2):L "``"] ] ; @@ -127,13 +123,14 @@ Syntax constr level 6: Rmult [ (Rmult $n1 $n2) ] -> [ [<hov 0> "``"(REXPR $n1):E "*" [0 0] (REXPR $n2):L "``"] ] - |Rdiv [ (Rdiv $n1 $n2) ] + | Reven_outside [ (Rmult (Rplus R1 R1) $r) ] -> [ $r:"r_printer_even_outside"] + | Rdiv [ (Rdiv $n1 $n2) ] -> [ [<hov 0> "``"(REXPR $n1):E "/" [0 0] (REXPR $n2):L "``"] ] ; level 8: Ropp [(Ropp $n1)] -> [ [<hov 0> "``" "-"(REXPR $n1):E "``"] ] - |Rinv [(Rinv $n1)] -> [ [<hov 0> "``" "/"(REXPR $n1):E "``"] ] + | Rinv [(Rinv $n1)] -> [ [<hov 0> "``" "/"(REXPR $n1):E "``"] ] ; level 0: @@ -172,20 +169,21 @@ Syntax constr [<<(REXPR <<(Rminus $n1 $n2)>>)>>] -> [ (REXPR $n1):E "-" [0 0] (REXPR $n2):L ] | NRplus_inside - [<<(REXPR <<(NRplus $n1 $n2)>>)>>] - -> ["(" (REXPR $n1):E "+" [0 0] (REXPR $n2):L ")"] + [<<(REXPR <<(NRplus $r)>>)>>] -> [ "(" "1" "+" (REXPR $r):L ")"] ; level 6: Rmult_inside [<<(REXPR <<(Rmult $n1 $n2)>>)>>] - -> [ (REXPR $n1):E "*" [0 0] (REXPR $n2):L ] + -> [ (REXPR $n1):E "*" (REXPR $n2):L ] + | NRmult_inside + [<<(REXPR <<(NRmult $r)>>)>>] -> [ "(" "2" "*" (REXPR $r):L ")"] ; level 5: - Ropp_inside [<<(REXPR <<(Ropp $n1)>>)>>] -> [ " -" (REXPR $n1):E ] -|Rinv_inside [<<(REXPR <<(Rinv $n1)>>)>>] -> [ "/" (REXPR $n1):E ] -|Rdiv_inside + Ropp_inside [<<(REXPR <<(Ropp $n1)>>)>>] -> [ " -" (REXPR $n1):E ] + | Rinv_inside [<<(REXPR <<(Rinv $n1)>>)>>] -> [ "/" (REXPR $n1):E ] + | Rdiv_inside [<<(REXPR <<(Rdiv $n1 $n2)>>)>>] -> [ (REXPR $n1):E "/" [0 0] (REXPR $n2):L ] ; @@ -193,7 +191,8 @@ Syntax constr level 0: Rzero_inside [<<(REXPR <<R0>>)>>] -> ["0"] | Rone_inside [<<(REXPR <<R1>>)>>] -> ["1"] - | Rconst_inside [<<(REXPR <<(Rplus R1 $r)>>)>>] -> [$r:"r_printer"] + | Rodd_inside [<<(REXPR <<(Rplus R1 $r)>>)>>] -> [ $r:"r_printer_odd" ] + | Reven_inside [<<(REXPR <<(Rmult (Rplus R1 R1) $r)>>)>>] -> [ $r:"r_printer_even" ] . (* For parsing/printing based on scopes *) diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index ace4d0a95..2219b1b04 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -295,7 +295,10 @@ Apply Rle_trans with ``PI/2``; [Assumption | Unfold Rdiv; Apply Rle_monotony_con Left; Assumption. Left; Sup0. Rewrite H1; Replace (plus (plus (mult (S (S O)) n) (S O)) (S (S O))) with (S (S (plus (mult (S (S O)) n) (S O)))). -Do 2 Rewrite fact_simpl; Do 2 Rewrite mult_INR; Rewrite <- Rmult_assoc; Rewrite <- (Rmult_sym (INR (fact (plus (mult (S (S O)) n) (S O))))). +Do 2 Rewrite fact_simpl; Do 2 Rewrite mult_INR. +Repeat Rewrite <- Rmult_assoc. +Rewrite <- (Rmult_sym (INR (fact (plus (mult (S (S O)) n) (S O))))). +Rewrite Rmult_assoc. Apply Rlt_monotony. Apply lt_INR_0; Apply neq_O_lt. Assert H2 := (fact_neq_0 (plus (mult (2) n) (1))). @@ -305,7 +308,14 @@ Replace ``(2*x+1+1+1)*(2*x+1+1)`` with ``4*x*x+10*x+6``; [Idtac | Ring]. Apply Rlt_anti_compatibility with ``-4``; Rewrite Rplus_Ropp_l; Replace ``-4+(4*x*x+10*x+6)`` with ``(4*x*x+10*x)+2``; [Idtac | Ring]. Apply ge0_plus_gt0_is_gt0. Cut ``0<=x``. -Intro; Apply ge0_plus_ge0_is_ge0; Repeat Apply Rmult_le_pos; Try (Left; Sup0) Orelse Assumption. +Intro; Apply ge0_plus_ge0_is_ge0; Repeat Apply Rmult_le_pos. +Left; Sup0. +Left; Sup0. +Assumption. +Assumption. +Left; Sup0. +Left; Sup0. +Assumption. Unfold x; Replace R0 with (INR O); [Rewrite <- INR_eq_INR2; Apply le_INR; Apply le_O_n | Reflexivity]. Sup0. Apply INR_eq; Do 2 Rewrite S_INR; Do 3 Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Ring. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 1cf745281..13ea21aa7 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -75,11 +75,12 @@ Apply Rsqr_incr_1. Apply Rle_trans with PI; [Assumption | Apply PI_4]. Assumption. Left; Sup0. -Pattern 1 ``16``; Rewrite <- Rplus_Or; Replace ``20`` with ``16+4``; [Apply Rle_compatibility; Left; Sup0 | Ring]. +Rewrite <- (Rplus_Or ``16``); Replace ``20`` with ``16+4``; [Apply Rle_compatibility; Left; Sup0 | Ring]. Rewrite <- (Rplus_sym ``20``); Pattern 1 ``20``; Rewrite <- Rplus_Or; Apply Rle_compatibility. Apply ge0_plus_ge0_is_ge0. Repeat Apply Rmult_le_pos. Left; Sup0. +Left; Sup0. Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. Apply Rmult_le_pos. @@ -214,6 +215,7 @@ Rewrite <- (Rplus_sym ``12``); Pattern 1 ``12``; Rewrite <- Rplus_Or; Apply Rle_ Apply ge0_plus_ge0_is_ge0. Repeat Apply Rmult_le_pos. Left; Sup0. +Left; Sup0. Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. Apply Rmult_le_pos. diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 7054b3749..a0f7e01b2 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -37,11 +37,11 @@ Rewrite neg_sin; Rewrite sin_neg; Ring. Cut ``PI==PI/2+PI/2``; [Intro | Apply double_var]. Pattern 2 3 PI; Rewrite H. Pattern 2 3 PI; Rewrite H. -Unfold Rdiv; Cut ``2*2==4``. -Intro; Rewrite Rmult_Rplus_distrl. -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_Rmult; [Rewrite H0; Ring | DiscrR | DiscrR]. +Unfold Rdiv. +Repeat Rewrite Rinv_Rmult. Ring. +DiscrR. +DiscrR. Qed. @@ -128,7 +128,7 @@ Rewrite sin_PI3_cos_PI6. Unfold Rdiv. Rewrite Rmult_1l. Rewrite Rmult_assoc. -Rewrite (Rmult_sym ``2``). +Pattern 2 ``2``; Rewrite (Rmult_sym ``2``). Rewrite Rmult_assoc. Rewrite <- Rinv_l_sym. Rewrite Rmult_1r; Reflexivity. @@ -200,7 +200,7 @@ Reflexivity. DiscrR. DiscrR. DiscrR. -Ring. +Reflexivity. Unfold Rdiv. Rewrite Rmult_1l. Repeat Rewrite <- Rmult_assoc. @@ -424,11 +424,7 @@ Symmetry; Apply Ropp_mul1. Pattern 2 PI; Rewrite double_var. Pattern 2 3 PI; Rewrite double_var. Unfold Rdiv. -Rewrite Rmult_Rplus_distrl. -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_Rmult. -Replace ``2*2`` with ``4``. -Ring. +Repeat Rewrite Rinv_Rmult. Ring. DiscrR. DiscrR. @@ -441,11 +437,7 @@ Unfold Rdiv; Symmetry; Apply Ropp_mul1. Pattern 2 PI; Rewrite double_var. Pattern 2 3 PI; Rewrite double_var. Unfold Rdiv. -Rewrite Rmult_Rplus_distrl. -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_Rmult. -Replace ``2*2`` with ``4``. -Ring. +Repeat Rewrite Rinv_Rmult. Ring. DiscrR. DiscrR. |