blob: 1284be48ad962eac81c17b651f76db7e8fe16fb5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
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.
|
