diff options
Diffstat (limited to 'test-suite/success/Reg.v')
| -rw-r--r-- | test-suite/success/Reg.v | 178 |
1 files changed, 93 insertions, 85 deletions
diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v index eaa0690c..89b3032c 100644 --- a/test-suite/success/Reg.v +++ b/test-suite/success/Reg.v @@ -1,136 +1,144 @@ -Require Reals. +Require Import Reals. -Axiom y : R->R. -Axiom d_y : (derivable y). -Axiom n_y : (x:R)``(y x)<>0``. -Axiom dy_0 : (derive_pt y R0 (d_y R0)) == R1. +Axiom y : R -> R. +Axiom d_y : derivable y. +Axiom n_y : forall x : R, y x <> 0%R. +Axiom dy_0 : derive_pt y 0 (d_y 0%R) = 1%R. -Lemma essai0 : (continuity_pt [x:R]``(x+2)/(y x)+x/(y x)`` R0). -Assert H := d_y. -Assert H0 := n_y. -Reg. +Lemma essai0 : continuity_pt (fun x : R => ((x + 2) / y x + x / y x)%R) 0. +assert (H := d_y). +assert (H0 := n_y). +reg. Qed. -Lemma essai1 : (derivable_pt [x:R]``/2*(sin x)`` ``1``). -Reg. +Lemma essai1 : derivable_pt (fun x : R => (/ 2 * sin x)%R) 1. +reg. Qed. -Lemma essai2 : (continuity [x:R]``(Rsqr x)*(cos (x*x))+x``). -Reg. +Lemma essai2 : continuity (fun x : R => (Rsqr x * cos (x * x) + x)%R). +reg. Qed. -Lemma essai3 : (derivable_pt [x:R]``x*((Rsqr x)+3)`` R0). -Reg. +Lemma essai3 : derivable_pt (fun x : R => (x * (Rsqr x + 3))%R) 0. +reg. Qed. -Lemma essai4 : (derivable [x:R]``(x+x)*(sin x)``). -Reg. +Lemma essai4 : derivable (fun x : R => ((x + x) * sin x)%R). +reg. Qed. -Lemma essai5 : (derivable [x:R]``1+(sin (2*x+3))*(cos (cos x))``). -Reg. +Lemma essai5 : derivable (fun x : R => (1 + sin (2 * x + 3) * cos (cos x))%R). +reg. Qed. -Lemma essai6 : (derivable [x:R]``(cos (x+3))``). -Reg. +Lemma essai6 : derivable (fun x : R => cos (x + 3)). +reg. Qed. -Lemma essai7 : (derivable_pt [x:R]``(cos (/(sqrt x)))*(Rsqr ((sin x)+1))`` R1). -Reg. -Apply Rlt_R0_R1. -Red; Intro; Rewrite sqrt_1 in H; Assert H0 := R1_neq_R0; Elim H0; Assumption. +Lemma essai7 : + derivable_pt (fun x : R => (cos (/ sqrt x) * Rsqr (sin x + 1))%R) 1. +reg. +apply Rlt_0_1. +red in |- *; 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. -Rewrite sin_0. -Rewrite Rsqr_O. -Replace ``0+0+1`` with ``1``; [Apply Rlt_R0_R1 | Ring]. +Lemma essai8 : derivable_pt (fun x : R => sqrt (Rsqr x + sin x + 1)) 0. +reg. + rewrite sin_0. + rewrite Rsqr_0. + replace (0 + 0 + 1)%R with 1%R; [ apply Rlt_0_1 | ring ]. Qed. -Lemma essai9 : (derivable_pt (plus_fct id sin) R1). -Reg. +Lemma essai9 : derivable_pt (id + sin) 1. +reg. Qed. -Lemma essai10 : (derivable_pt [x:R]``x+2`` R0). -Reg. +Lemma essai10 : derivable_pt (fun x : R => (x + 2)%R) 0. +reg. Qed. -Lemma essai11 : (derive_pt [x:R]``x+2`` R0 essai10)==R1. -Reg. +Lemma essai11 : derive_pt (fun x : R => (x + 2)%R) 0 essai10 = 1%R. +reg. Qed. -Lemma essai12 : (derivable [x:R]``x+(Rsqr (x+2))``). -Reg. +Lemma essai12 : derivable (fun x : R => (x + Rsqr (x + 2))%R). +reg. Qed. -Lemma essai13 : (derive_pt [x:R]``x+(Rsqr (x+2))`` R0 (essai12 R0)) == ``5``. -Reg. +Lemma essai13 : + derive_pt (fun x : R => (x + Rsqr (x + 2))%R) 0 (essai12 0%R) = 5%R. +reg. Qed. -Lemma essai14 : (derivable_pt [x:R]``2*x+x`` ``2``). -Reg. +Lemma essai14 : derivable_pt (fun x : R => (2 * x + x)%R) 2. +reg. Qed. -Lemma essai15 : (derive_pt [x:R]``2*x+x`` ``2`` essai14) == ``3``. -Reg. +Lemma essai15 : derive_pt (fun x : R => (2 * x + x)%R) 2 essai14 = 3%R. +reg. Qed. -Lemma essai16 : (derivable_pt [x:R]``x+(sin x)`` R0). -Reg. +Lemma essai16 : derivable_pt (fun x : R => (x + sin x)%R) 0. +reg. Qed. -Lemma essai17 : (derive_pt [x:R]``x+(sin x)`` R0 essai16)==``2``. -Reg. -Rewrite cos_0. -Reflexivity. +Lemma essai17 : derive_pt (fun x : R => (x + sin x)%R) 0 essai16 = 2%R. +reg. + rewrite cos_0. +reflexivity. Qed. -Lemma essai18 : (derivable_pt [x:R]``x+(y x)`` ``0``). -Assert H := d_y. -Reg. +Lemma essai18 : derivable_pt (fun x : R => (x + y x)%R) 0. +assert (H := d_y). +reg. Qed. -Lemma essai19 : (derive_pt [x:R]``x+(y x)`` ``0`` essai18) == ``2``. -Assert H := dy_0. -Assert H0 := d_y. -Reg. +Lemma essai19 : derive_pt (fun x : R => (x + y x)%R) 0 essai18 = 2%R. +assert (H := dy_0). +assert (H0 := d_y). +reg. Qed. -Axiom z:R->R. -Axiom d_z: (derivable z). +Axiom z : R -> R. +Axiom d_z : derivable z. -Lemma essai20 : (derivable_pt [x:R]``(z (y x))`` R0). -Reg. -Apply d_y. -Apply d_z. +Lemma essai20 : derivable_pt (fun x : R => z (y x)) 0. +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. +Lemma essai21 : derive_pt (fun x : R => z (y x)) 0 essai20 = 1%R. +assert (H := dy_0). +reg. Abort. -Lemma essai22 : (derivable [x:R]``(sin (z x))+(Rsqr (z x))/(y x)``). -Assert H := d_y. -Reg. -Apply n_y. -Apply d_z. +Lemma essai22 : derivable (fun x : R => (sin (z x) + Rsqr (z x) / y x)%R). +assert (H := d_y). +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. -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. -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]. +Lemma essai23 : + continuity_pt + (fun x : R => (sin (sqrt (x - 1)) + exp (Rsqr (sqrt x + 3)))%R) 1. +reg. +left; apply Rlt_0_1. +right; unfold Rminus in |- *; rewrite Rplus_opp_r; reflexivity. +Qed. + +Lemma essai24 : + derivable (fun x : R => (sqrt (x * x + 2 * x + 2) + Rabs (x * x + 1))%R). +reg. + replace (x * x + 2 * x + 2)%R with (Rsqr (x + 1) + 1)%R. +apply Rplus_le_lt_0_compat; [ apply Rle_0_sqr | apply Rlt_0_1 ]. +unfold Rsqr in |- *; ring. +red in |- *; intro; cut (0 < x * x + 1)%R. +intro; rewrite H in H0; elim (Rlt_irrefl _ H0). +apply Rplus_le_lt_0_compat; + [ replace (x * x)%R with (Rsqr x); [ apply Rle_0_sqr | reflexivity ] + | apply Rlt_0_1 ]. Qed. |