diff options
-rw-r--r-- | test-suite/success/Reg.v | 52 | ||||
-rw-r--r-- | theories/Reals/NewtonInt.v | 20 | ||||
-rw-r--r-- | theories/Reals/Ranalysis.v | 7 |
3 files changed, 38 insertions, 41 deletions
diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v index b088321d3..eaa0690cb 100644 --- a/test-suite/success/Reg.v +++ b/test-suite/success/Reg.v @@ -8,129 +8,129 @@ Axiom dy_0 : (derive_pt y R0 (d_y R0)) == R1. Lemma essai0 : (continuity_pt [x:R]``(x+2)/(y x)+x/(y x)`` R0). Assert H := d_y. Assert H0 := n_y. -Reg(). +Reg. Qed. Lemma essai1 : (derivable_pt [x:R]``/2*(sin x)`` ``1``). -Reg (). +Reg. Qed. Lemma essai2 : (continuity [x:R]``(Rsqr x)*(cos (x*x))+x``). -Reg (). +Reg. Qed. Lemma essai3 : (derivable_pt [x:R]``x*((Rsqr x)+3)`` R0). -Reg (). +Reg. Qed. Lemma essai4 : (derivable [x:R]``(x+x)*(sin x)``). -Reg (). +Reg. Qed. Lemma essai5 : (derivable [x:R]``1+(sin (2*x+3))*(cos (cos x))``). -Reg (). +Reg. Qed. Lemma essai6 : (derivable [x:R]``(cos (x+3))``). -Reg (). +Reg. Qed. Lemma essai7 : (derivable_pt [x:R]``(cos (/(sqrt x)))*(Rsqr ((sin x)+1))`` R1). -Reg (). +Reg. Apply Rlt_R0_R1. Red; Intro; Rewrite sqrt_1 in H; Assert H0 := R1_neq_R0; Elim H0; Assumption. Qed. Lemma essai8 : (derivable_pt [x:R]``(sqrt ((Rsqr x)+(sin x)+1))`` R0). -Reg (). +Reg. Rewrite sin_0. Rewrite Rsqr_O. Replace ``0+0+1`` with ``1``; [Apply Rlt_R0_R1 | Ring]. Qed. Lemma essai9 : (derivable_pt (plus_fct id sin) R1). -Reg (). +Reg. Qed. Lemma essai10 : (derivable_pt [x:R]``x+2`` R0). -Reg(). +Reg. Qed. Lemma essai11 : (derive_pt [x:R]``x+2`` R0 essai10)==R1. -Reg(). +Reg. Qed. Lemma essai12 : (derivable [x:R]``x+(Rsqr (x+2))``). -Reg(). +Reg. Qed. Lemma essai13 : (derive_pt [x:R]``x+(Rsqr (x+2))`` R0 (essai12 R0)) == ``5``. -Reg(). +Reg. Qed. Lemma essai14 : (derivable_pt [x:R]``2*x+x`` ``2``). -Reg (). +Reg. Qed. Lemma essai15 : (derive_pt [x:R]``2*x+x`` ``2`` essai14) == ``3``. -Reg(). +Reg. Qed. Lemma essai16 : (derivable_pt [x:R]``x+(sin x)`` R0). -Reg(). +Reg. Qed. Lemma essai17 : (derive_pt [x:R]``x+(sin x)`` R0 essai16)==``2``. -Reg (). +Reg. Rewrite cos_0. Reflexivity. Qed. Lemma essai18 : (derivable_pt [x:R]``x+(y x)`` ``0``). Assert H := d_y. -Reg (). +Reg. Qed. Lemma essai19 : (derive_pt [x:R]``x+(y x)`` ``0`` essai18) == ``2``. Assert H := dy_0. Assert H0 := d_y. -Reg (). +Reg. Qed. Axiom z:R->R. Axiom d_z: (derivable z). Lemma essai20 : (derivable_pt [x:R]``(z (y x))`` R0). -Reg (). +Reg. Apply d_y. Apply d_z. Qed. Lemma essai21 : (derive_pt [x:R]``(z (y x))`` R0 essai20) == R1. Assert H := dy_0. -Reg(). +Reg. Abort. Lemma essai22 : (derivable [x:R]``(sin (z x))+(Rsqr (z x))/(y x)``). Assert H := d_y. -Reg(). +Reg. Apply n_y. Apply d_z. Qed. (* Pour tester la continuite de sqrt en 0 *) Lemma essai23 : (continuity_pt [x:R]``(sin (sqrt (x-1)))+(exp (Rsqr ((sqrt x)+3)))`` R1). -Reg(). +Reg. Left; Apply Rlt_R0_R1. Right; Unfold Rminus; Rewrite Rplus_Ropp_r; Reflexivity. Qed. Lemma essai24 : (derivable [x:R]``(sqrt (x*x+2*x+2))+(Rabsolu (x*x+1))``). -Reg (). +Reg. Replace ``x*x+2*x+2`` with ``(Rsqr (x+1))+1``. Apply ge0_plus_gt0_is_gt0; [Apply pos_Rsqr | Apply Rlt_R0_R1]. Unfold Rsqr; Ring. Red; Intro; Cut ``0<x*x+1``. Intro; Rewrite H in H0; Elim (Rlt_antirefl ? H0). Apply ge0_plus_gt0_is_gt0; [Replace ``x*x`` with (Rsqr x); [Apply pos_Rsqr | Reflexivity] | Apply Rlt_R0_R1]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 6346fc2ee..4010f1d44 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -90,8 +90,8 @@ Left; Unfold antiderivative; Unfold antiderivative in H H0; Elim H; Clear H; Int Split. Intros; Elim (H ? H2); Elim (H0 ? H2); Intros. Assert H5 : (derivable_pt [y:R]``l*(x y)+(x0 y)`` x1). -Reg (). -Exists H5; Symmetry; Reg (); Rewrite <- H3; Rewrite <- H4; Reflexivity. +Reg. +Exists H5; Symmetry; Reg; Rewrite <- H3; Rewrite <- H4; Reflexivity. Assumption. Unfold antiderivative in H H0; Elim H; Elim H0; Intros; Elim H4; Intro. Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H5 H2)). @@ -107,8 +107,8 @@ Unfold derivable_pt; Exists (f x1); Elim (H3 ? H10); Intros; EApply derive_pt_eq Assert H13 : (derivable_pt x0 x1). Unfold derivable_pt; Exists (g x1); Elim (H1 ? H11); Intros; EApply derive_pt_eq_1; Symmetry; Apply H13. Assert H14 : (derivable_pt [y:R]``l*(x y)+(x0 y)`` x1). -Reg (). -Exists H14; Symmetry; Reg (). +Reg. +Exists H14; Symmetry; Reg. Assert H15 : ``(derive_pt x0 x1 H13)==(g x1)``. Elim (H1 ? H11); Intros; Rewrite H15; Apply pr_nu. Assert H16 : ``(derive_pt x x1 H12)==(f x1)``. @@ -130,8 +130,8 @@ Unfold derivable_pt; Exists (f x1); Elim (H3 ? H11); Intros; EApply derive_pt_eq Assert H13 : (derivable_pt x0 x1). Unfold derivable_pt; Exists (g x1); Elim (H1 ? H10); Intros; EApply derive_pt_eq_1; Symmetry; Apply H13. Assert H14 : (derivable_pt [y:R]``l*(x y)+(x0 y)`` x1). -Reg (). -Exists H14; Symmetry; Reg (). +Reg. +Exists H14; Symmetry; Reg. Assert H15 : ``(derive_pt x0 x1 H13)==(g x1)``. Elim (H1 ? H10); Intros; Rewrite H15; Apply pr_nu. Assert H16 : ``(derive_pt x x1 H12)==(f x1)``. @@ -141,8 +141,8 @@ Right; Reflexivity. Right; Unfold antiderivative; Unfold antiderivative in H H0; Elim H; Clear H; Intros; Elim H0; Clear H0; Intros H0 _; Split. Intros; Elim (H ? H2); Elim (H0 ? H2); Intros. Assert H5 : (derivable_pt [y:R]``l*(x y)+(x0 y)`` x1). -Reg (). -Exists H5; Symmetry; Reg (); Rewrite <- H3; Rewrite <- H4; Reflexivity. +Reg. +Exists H5; Symmetry; Reg; Rewrite <- H3; Rewrite <- H4; Reflexivity. Assumption. Defined. @@ -151,8 +151,8 @@ Lemma antiderivative_P1 : (f,g,F,G:R->R;l,a,b:R) (antiderivative f F a b) -> (an Unfold antiderivative; Intros; Elim H; Elim H0; Clear H H0; Intros; Split. Intros; Elim (H ? H3); Elim (H1 ? H3); Intros. Assert H6 : (derivable_pt [x:R]``l*(F x)+(G x)`` x). -Reg (). -Exists H6; Symmetry; Reg (); Rewrite <- H4; Rewrite <- H5; Ring. +Reg. +Exists H6; Symmetry; Reg; Rewrite <- H4; Rewrite <- H5; Ring. Assumption. Qed. diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 17d9ea08f..2575b8508 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -456,7 +456,7 @@ Match trm With | _ -> Idtac. (**********) -Tactic Definition Regularity () := +Tactic Definition Reg := Match Context With | [|-(derivable_pt ?1 ?2)] -> Let trm = Eval Cbv Beta in (?1 AppVar) In @@ -473,7 +473,4 @@ Let aux = (RewTerm trm) In IntroHypL aux ?2; Try (Change (continuity_pt aux ?2); | [|-(eqT ? (derive_pt ?1 ?2 ?3) ?4)] -> Let trm = Eval Cbv Beta in (?1 AppVar) In Let aux = (RewTerm trm) In -IntroHypL aux ?2; Let aux2 = (ConsProof aux ?2) In Try (Replace (derive_pt ?1 ?2 ?3) with (derive_pt aux ?2 aux2); [SimplifyDerive aux ?2; Try Unfold plus_fct minus_fct mult_fct div_fct id fct_cte inv_fct opp_fct; Try Ring | Try Apply pr_nu]) Orelse IsDiff_pt. - -(**********) -Tactic Definition Reg () := Regularity (). +IntroHypL aux ?2; Let aux2 = (ConsProof aux ?2) In Try (Replace (derive_pt ?1 ?2 ?3) with (derive_pt aux ?2 aux2); [SimplifyDerive aux ?2; Try Unfold plus_fct minus_fct mult_fct div_fct id fct_cte inv_fct opp_fct; Try Ring | Try Apply pr_nu]) Orelse IsDiff_pt.
\ No newline at end of file |