1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/demo/power_derivative".
17 include "nat/plus.ma".
18 include "nat/orders.ma".
19 include "nat/compare.ma".
27 notation "0" with precedence 89
29 interpretation "Rzero" 'zero =
30 (cic:/matita/demo/power_derivative/R0.con).
31 interpretation "Nzero" 'zero =
32 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)).
34 notation "1" with precedence 89
36 interpretation "Rone" 'one =
37 (cic:/matita/demo/power_derivative/R1.con).
38 interpretation "None" 'one =
39 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
40 cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)).
42 interpretation "Rplus" 'plus x y =
43 (cic:/matita/demo/power_derivative/Rplus.con x y).
44 interpretation "Rmult" 'times x y =
45 (cic:/matita/demo/power_derivative/Rmult.con x y).
48 λf,g:R→R.λx:R.f x + g x.
51 λf,g:R→R.λx:R.f x * g x.
53 interpretation "Fplus" 'plus x y =
54 (cic:/matita/demo/power_derivative/Fplus.con x y).
55 interpretation "Fmult" 'times x y =
56 (cic:/matita/demo/power_derivative/Fmult.con x y).
58 notation "2" with precedence 89
60 interpretation "Rtwo" 'two =
61 (cic:/matita/demo/power_derivative/Rplus.con
62 cic:/matita/demo/power_derivative/R1.con
63 cic:/matita/demo/power_derivative/R1.con).
64 interpretation "Ntwo" 'two =
65 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
66 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
67 (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))).
69 let rec Rpower (x:R) (n:nat) on n ≝
72 | S n ⇒ x * (Rpower x n)
75 interpretation "Rpower" 'exp x n =
76 (cic:/matita/demo/power_derivative/Rpower.con x n).
78 let rec inj (n:nat) on n : R ≝
88 coercion cic:/matita/demo/power_derivative/inj.con.
90 axiom Rplus_Rzero_x: ∀x:R.0+x=x.
91 axiom Rplus_comm: symmetric ? Rplus.
92 axiom Rplus_assoc: associative ? Rplus.
93 axiom Rmult_Rone_x: ∀x:R.1*x=x.
94 axiom Rmult_Rzero_x: ∀x:R.0*x=0.
95 axiom Rmult_assoc: associative ? Rmult.
96 axiom Rmult_comm: symmetric ? Rmult.
97 axiom Rmult_Rplus_distr: distributive ? Rmult Rplus.
99 alias symbol "times" = "Rmult".
100 alias symbol "plus" = "natural plus".
105 definition costante : nat → R → R ≝
108 coercion cic:/matita/demo/power_derivative/costante.con 1.
110 axiom f_eq_extensional:
111 ∀f,g:R→R.(∀x:R.f x = g x) → f=g.
113 lemma Fmult_one_f: ∀f:R→R.1*f=f.
117 apply f_eq_extensional;
122 lemma Fmult_zero_f: ∀f:R→R.0*f=0.
126 apply f_eq_extensional;
131 lemma Fmult_commutative: symmetric ? Fmult.
135 apply f_eq_extensional;
140 lemma Fmult_associative: associative ? Fmult.
145 apply f_eq_extensional;
150 lemma Fmult_Fplus_distr: distributive ? Fmult Fplus.
155 apply f_eq_extensional;
161 lemma monomio_product:
162 ∀n,m.monomio (n+m) = monomio n * monomio m.
169 apply f_eq_extensional;
173 apply f_eq_extensional;
175 cut (x\sup (n1+m) = x \sup n1 * x \sup m);
178 | change in ⊢ (? ? % ?) with ((λx:R.(x)\sup(n1+m)) x);
186 ∀n,m.costante n + costante m = costante (n+m).
190 apply f_eq_extensional;
221 axiom derivative: (R→R) → R → R.
223 notation "hvbox('D'[f])"
224 non associative with precedence 90
225 for @{ 'derivative $f }.
227 interpretation "Rderivative" 'derivative f =
228 (cic:/matita/demo/power_derivative/derivative.con f).
230 notation "hvbox('x' \sup n)"
231 non associative with precedence 60
232 for @{ 'monomio $n }.
234 notation "hvbox('x')"
235 non associative with precedence 60
238 interpretation "Rmonomio" 'monomio n =
239 (cic:/matita/demo/power_derivative/monomio.con n).
241 axiom derivative_x0: D[x \sup 0] = 0.
242 axiom derivative_x1: D[x] = 1.
243 axiom derivative_mult: ∀f,g:R→R. D[f*g] = D[f]*g + f*D[g].
245 alias symbol "times" = "Fmult".
247 theorem derivative_power: ∀n:nat. D[x \sup n] = n*x \sup (pred n).
249 we proceed by induction on n to prove
250 (D[x \sup n] = n*x \sup (pred n)).
252 the thesis becomes (D[x \sup 0] = 0*x \sup (pred 0)).
256 by induction hypothesis we know
257 (D[x \sup m] = m*x \sup (pred m)) (H).
259 (D[x \sup (1+m)] = (1+m)*x \sup m).
261 (m * (x \sup (1+ pred m)) = m * x \sup m) (Ppred).
262 by _ we proved (0 < m ∨ 0=m) (cases).
263 we proceed by induction on cases
264 to prove (m * (x \sup (1+ pred m)) = m * x \sup m).
266 suppose (0 < m) (m_pos).
267 by (S_pred m m_pos) we proved (m = 1 + pred m) (H1).
271 suppose (0=m) (m_zero). by _ done.
274 = (D[x * x \sup m]) by _.
275 = (D[x] * x \sup m + x * D[x \sup m]) by _.
276 = (x \sup m + x * (m * x \sup (pred m))) by _.
278 = (x \sup m + m * (x \sup (1 + pred m))) by _.
279 = (x \sup m + m * x \sup m) by _.
280 = ((1+m)*x \sup m) by _ (timeout=30)
284 notation "hvbox(\frac 'd' ('d' ident i) break p)"
285 right associative with precedence 90
286 for @{ 'derivative ${default
287 @{\lambda ${ident i} : $ty. $p)}
288 @{\lambda ${ident i} . $p}}}.
290 interpretation "Rderivative" 'derivative \eta.f =
291 (cic:/matita/demo/power_derivative/derivative.con f).
293 theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n)*x \sup n.
295 we proceed by induction on n to prove
296 (D[x \sup (1+n)] = (1+n)*x \sup n).
298 the thesis becomes (D[x \sup 1] = 1*x \sup 0).
302 by induction hypothesis we know
303 (D[x \sup (1+m)] = (1+m)*x \sup m) (H).
305 (D[x \sup (2+m)] = (2+m)*x \sup (1+m)).
308 = (D[x \sup 1 * x \sup (1+m)]) by _.
309 = (D[x \sup 1] * x \sup (1+m) + x * D[x \sup (1+m)]) by _.
310 = (x \sup (1+m) + x * (costante (1+m) * x \sup m)) by _.
312 = (x \sup (1+m) + costante (1+m) * x \sup (1+m)) by _.
313 = (x \sup (1+m) * (costante (2 + m))) by _