1 files changed, 136 insertions, 0 deletions
diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v
new file mode 100644
index 00000000..eaa0690c
--- /dev/null
+++ b/test-suite/success/Reg.v
@@ -0,0 +1,136 @@
+Require 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.
+
+Lemma essai0 : (continuity_pt [x:R]``(x+2)/(y x)+x/(y x)`` R0).
+Assert H := d_y.
+Assert H0 := n_y.
+Reg.
+Qed.
+
+Lemma essai1 : (derivable_pt [x:R]``/2*(sin x)`` ``1``).
+Reg.
+Qed.
+
+Lemma essai2 : (continuity [x:R]``(Rsqr x)*(cos (x*x))+x``).
+Reg.
+Qed.
+
+Lemma essai3 : (derivable_pt [x:R]``x*((Rsqr x)+3)`` R0).
+Reg.
+Qed.
+
+Lemma essai4 : (derivable [x:R]``(x+x)*(sin x)``).
+Reg.
+Qed.
+
+Lemma essai5 : (derivable [x:R]``1+(sin (2*x+3))*(cos (cos x))``).
+Reg.
+Qed.
+
+Lemma essai6 : (derivable [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.
+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].
+Qed.
+
+Lemma essai9 : (derivable_pt (plus_fct id sin) R1).
+Reg.
+Qed.
+
+Lemma essai10 : (derivable_pt [x:R]``x+2`` R0).
+Reg.
+Qed.
+
+Lemma essai11 : (derive_pt [x:R]``x+2`` R0 essai10)==R1.
+Reg.
+Qed.
+
+Lemma essai12 : (derivable [x:R]``x+(Rsqr (x+2))``).
+Reg.
+Qed.
+
+Lemma essai13 : (derive_pt [x:R]``x+(Rsqr (x+2))`` R0 (essai12 R0)) == ``5``.
+Reg.
+Qed.
+
+Lemma essai14 : (derivable_pt [x:R]``2*x+x`` ``2``).
+Reg.
+Qed.
+
+Lemma essai15 : (derive_pt [x:R]``2*x+x`` ``2`` essai14) == ``3``.
+Reg.
+Qed.
+
+Lemma essai16 : (derivable_pt [x:R]``x+(sin x)`` R0).
+Reg.
+Qed.
+
+Lemma essai17 : (derive_pt [x:R]``x+(sin x)`` R0 essai16)==``2``.
+Reg.
+Rewrite cos_0.
+Reflexivity.
+Qed.
+
+Lemma essai18 : (derivable_pt [x:R]``x+(y x)`` ``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.
+Qed.
+
+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.
+Qed.
+
+Lemma essai21 : (derive_pt [x:R]``(z (y x))`` R0 essai20) == R1.
+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.
+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].
+Qed.