]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/demo/power_derivative.ma
use named types to force some constraints asap
[helm.git] / helm / software / matita / library / demo / power_derivative.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/plus.ma".
16 include "nat/orders.ma".
17 include "nat/compare.ma".
18
19 axiom R: Type.
20 axiom R0: R.
21 axiom R1: R.
22 axiom Rplus: R→R→R.
23 axiom Rmult: R→R→R.
24
25 notation "0" with precedence 89
26 for @{ 'zero }.
27 interpretation "Rzero" 'zero =
28  (cic:/matita/demo/power_derivative/R0.con).
29 interpretation "Nzero" 'zero =
30  (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)).
31
32 notation "1" with precedence 89
33 for @{ 'one }.
34 interpretation "Rone" 'one =
35  (cic:/matita/demo/power_derivative/R1.con).
36 interpretation "None" 'one =
37  (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
38    cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)).
39
40 interpretation "Rplus" 'plus x y =
41  (cic:/matita/demo/power_derivative/Rplus.con x y).
42
43 interpretation "Rmult" 'middot x y =
44  (cic:/matita/demo/power_derivative/Rmult.con x y).
45
46 definition Fplus ≝
47  λf,g:R→R.λx:R.f x + g x.
48  
49 definition Fmult ≝
50  λf,g:R→R.λx:R.f x · g x.
51
52 interpretation "Fplus" 'plus x y =
53  (cic:/matita/demo/power_derivative/Fplus.con x y).
54 interpretation "Fmult" 'middot x y =
55  (cic:/matita/demo/power_derivative/Fmult.con x y).
56
57 notation "2" with precedence 89
58 for @{ 'two }.
59 interpretation "Rtwo" 'two =
60  (cic:/matita/demo/power_derivative/Rplus.con
61    cic:/matita/demo/power_derivative/R1.con
62    cic:/matita/demo/power_derivative/R1.con).
63 interpretation "Ntwo" 'two =
64  (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
65    (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2)
66      (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))).
67
68 let rec Rpower (x:R) (n:nat) on n ≝
69  match n with
70   [ O ⇒ 1
71   | S n ⇒ x · (Rpower x n)
72   ].
73
74 interpretation "Rpower" 'exp x n =
75  (cic:/matita/demo/power_derivative/Rpower.con x n).
76
77 let rec inj (n:nat) on n : R ≝
78  match n with
79   [ O ⇒ 0
80   | S n ⇒
81      match n with
82       [ O ⇒ 1
83       | S m ⇒ 1 + inj n
84       ]
85   ].
86
87 coercion inj.
88
89 axiom Rplus_Rzero_x: ∀x:R.0+x=x.
90 axiom Rplus_comm: symmetric ? Rplus.
91 axiom Rplus_assoc: associative ? Rplus.
92 axiom Rmult_Rone_x: ∀x:R.1 · x=x.
93 axiom Rmult_Rzero_x: ∀x:R.0 · x=0.
94 axiom Rmult_assoc: associative ? Rmult.
95 axiom Rmult_comm: symmetric ? Rmult.
96 axiom Rmult_Rplus_distr: distributive ? Rmult Rplus.
97
98 alias symbol "middot" = "Rmult".
99 alias symbol "plus" = "natural plus".
100
101 definition monomio ≝
102  λn.λx:R.x\sup n.
103
104 definition costante : nat → R → R ≝
105  λa:nat.λx:R.inj a.
106
107 coercion costante with 1.
108
109 axiom f_eq_extensional:
110  ∀f,g:R→R.(∀x:R.f x = g x) → f=g.
111
112 lemma Fmult_one_f: ∀f:R→R.1·f=f.
113  intro;
114  unfold Fmult;
115  simplify;
116  apply f_eq_extensional;
117  intro;
118  autobatch.
119 qed.
120
121 lemma Fmult_zero_f: ∀f:R→R.0·f=0.
122  intro;
123  unfold Fmult;
124  simplify;
125  apply f_eq_extensional;
126  intro;
127  autobatch.
128 qed.
129
130 lemma Fmult_commutative: symmetric ? Fmult.
131  unfold;
132  intros;
133  unfold Fmult;
134  apply f_eq_extensional;
135  intros;
136  autobatch.
137 qed.
138
139 lemma Fmult_associative: associative ? Fmult.
140  unfold;
141  intros;
142  unfold Fmult;
143  unfold Fmult;
144  apply f_eq_extensional;
145  intros;
146  autobatch.
147 qed.
148
149 lemma Fmult_Fplus_distr: distributive ? Fmult Fplus.
150  unfold;
151  intros;
152  unfold Fmult;
153  unfold Fplus;
154  apply f_eq_extensional;
155  intros;
156  simplify;
157  autobatch.
158 qed.
159
160 lemma monomio_product:
161  ∀n,m.monomio (n+m) = monomio n · monomio m.
162  intros;
163  unfold monomio;
164  unfold Fmult;
165  simplify;
166  elim n;
167   [ simplify;
168     apply f_eq_extensional;
169     intro;
170     autobatch
171   | simplify;
172     apply f_eq_extensional;
173     intro;
174     cut (x\sup (n1+m) = x \sup n1 · x \sup m);
175      [ rewrite > Hcut;
176        autobatch
177      | change in ⊢ (? ? % ?) with ((λx:R.x\sup(n1+m)) x);
178        rewrite > H;
179        reflexivity
180      ]
181   ].
182 qed.
183
184 lemma costante_sum:
185  ∀n,m.costante n + costante m = costante (n+m).
186  intros;
187  unfold Fplus;
188  unfold costante;
189  apply f_eq_extensional;
190  intros;
191  elim n;
192   [ simplify;
193     autobatch
194   | simplify;
195     clear x;
196     clear H;
197     clear n;
198     elim n1;
199      [ simplify;
200        elim m;
201         [ simplify;
202           autobatch
203         | simplify;
204           rewrite < H;
205           autobatch
206         ]
207      | simplify;
208        rewrite < H;
209        clear H;
210        elim n;
211         [ simplify;
212           autobatch
213         | simplify;
214           autobatch
215         ]
216      ]
217    ].
218 qed.
219
220 axiom derivative: (R→R) → R → R.
221
222 notation "hvbox('D'[f])"
223   non associative with precedence 90
224 for @{ 'derivative $f }.
225
226 interpretation "Rderivative" 'derivative f =
227  (cic:/matita/demo/power_derivative/derivative.con f).
228
229 notation "hvbox('x' \sup n)"
230   non associative with precedence 60
231 for @{ 'monomio $n }.
232
233 notation "hvbox('x')"
234   non associative with precedence 60
235 for @{ 'monomio 1 }.
236
237 interpretation "Rmonomio" 'monomio n =
238  (cic:/matita/demo/power_derivative/monomio.con n).
239
240 axiom derivative_x0: D[x \sup 0] = 0.
241 axiom derivative_x1: D[x] = 1.
242 axiom derivative_mult: ∀f,g:R→R. D[f·g] = D[f]·g + f·D[g].
243
244 alias symbol "middot" = "Fmult".
245
246 theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n).
247  assume n:nat.
248  (*we proceed by induction on n to prove
249  (D[x \sup n] = n · x \sup (pred n)).*)
250  elim n 0.
251  case O.
252    the thesis becomes (D[x \sup 0] = 0·x \sup (pred 0)).
253   done.
254  case S (m:nat).
255   by induction hypothesis we know
256    (D[x \sup m] = m·x \sup (pred m)) (H).
257   the thesis becomes
258    (D[x \sup (1+m)] = (1+m) · x \sup m).
259   we need to prove
260    (m · (x \sup (1+ pred m)) = m · x \sup m) (Ppred).
261    we proved (0 < m ∨ 0=m) (cases).
262    we proceed by induction on cases
263    to prove (m · (x \sup (1+ pred m)) = m · x \sup m).
264     case left.
265       suppose (0 < m) (m_pos).
266       using (S_pred ? m_pos) we proved (m = 1 + pred m) (H1).
267      by H1 done.
268     case right.
269       suppose (0=m) (m_zero). 
270     by m_zero, Fmult_zero_f done.
271   conclude
272      (D[x \sup (1+m)])
273    = (D[x · x \sup m]).
274    = (D[x] · x \sup m + x · D[x \sup m]).
275    = (x \sup m + x · (m · x \sup (pred m))) timeout=30.
276    = (x \sup m + m · (x \sup (1 + pred m))).
277    = (x \sup m + m · x \sup m).
278    = ((1+m) · x \sup m) timeout=30 by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum
279   done.
280 qed.
281
282 (*
283 notation "hvbox(\frac 'd' ('d' ident i) break p)"
284   right associative with precedence 90
285 for @{ 'derivative ${default
286   @{\lambda ${ident i} : $ty. $p)}
287   @{\lambda ${ident i} . $p}}}.
288
289 interpretation "Rderivative" 'derivative \eta.f =
290  (cic:/matita/demo/power_derivative/derivative.con f).
291 *)
292
293 notation "hvbox(\frac 'd' ('d' 'x') break p)" with precedence 90
294 for @{ 'derivative $p}.
295
296 interpretation "Rderivative" 'derivative f =
297  (cic:/matita/demo/power_derivative/derivative.con f).
298
299 theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n) · x \sup n.
300  assume n:nat.
301  (*we proceed by induction on n to prove
302  (D[x \sup (1+n)] = (1+n) · x \sup n).*) elim n 0.
303  case O.
304    the thesis becomes (D[x \sup 1] = 1 · x \sup 0).
305   done.
306  case S (m:nat).
307   by induction hypothesis we know
308    (D[x \sup (1+m)] = (1+m) · x \sup m) (H).
309   the thesis becomes
310    (D[x \sup (2+m)] = (2+m) · x \sup (1+m)).
311   conclude
312      (D[x \sup (2+m)])
313    = (D[x · x \sup (1+m)]).
314    = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]).
315    = (x \sup (1+m) + x · (costante (1+m) · x \sup m)).
316    = (x \sup (1+m) + costante (1+m) · x \sup (1+m)).
317    = ((2+m) · x \sup (1+m)) timeout=30 by Fmult_one_f, Fmult_commutative,
318        Fmult_Fplus_distr, assoc_plus, plus_n_SO, costante_sum
319   done.
320 qed.