]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/contribs/dama/dama_didactic/ex_deriv.ma
Matitaweb: Fixes a bug which prevented Mozilla from displaying long goals
[helm.git] / matitaB / matita / contribs / dama / dama_didactic / ex_deriv.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
16
17 include "deriv.ma".
18
19 theorem p_plus_p_p: ∀f:F. ∀g:F. (fpari f ∧ fpari g) → fpari (f + g).
20  assume f:F.
21  assume g:F.
22  suppose (fpari f ∧ fpari g) (h).
23  by h we have (fpari f) (H) and (fpari g) (K).
24  we need to prove (fpari (f + g))
25  or equivalently ((f + g) = (f + g) ∘ ρ).
26  conclude
27     (f + g)
28   = (f + (g ∘ ρ)) by _.
29   = ((f ∘ ρ) + (g ∘ ρ)) by _.
30   = ((f + g) ∘ ρ) by _
31  done.
32 qed.
33
34 theorem p_mult_p_p: ∀f:F. ∀g:F. (fpari f ∧ fpari g) → fpari (f · g).
35  assume f:F.
36  assume g:F.
37  suppose (fpari f ∧ fpari g) (h).
38  by h we have (fpari f) (H) and (fpari g) (K).
39  we need to prove (fpari (f · g))
40  or equivalently ((f · g) = (f · g) ∘ ρ).
41  conclude
42     (f · g)
43   = (f · (g ∘ ρ)) by _.
44   = ((f ∘ ρ) · (g ∘ ρ)) by _.
45   = ((f · g) ∘ ρ) by _
46  done.
47 qed.
48
49 theorem d_plus_d_d: ∀f:F. ∀g:F. (fdispari f ∧ fdispari g) → fdispari (f + g).
50  assume f:F.
51  assume g:F.
52  suppose (fdispari f ∧ fdispari g) (h).
53  by h we have (fdispari f) (H) and (fdispari g) (K).
54  we need to prove (fdispari (f + g))
55  or equivalently ((f + g) = (ρ ∘ ((f + g) ∘ ρ))).
56  conclude
57     (f + g)
58   = (f + (ρ ∘ (g ∘ ρ))) by _.
59   = ((ρ ∘ (f ∘ ρ)) + (ρ ∘ (g ∘ ρ))) by _.
60   = (((-R1) · (f ∘ ρ)) + (ρ ∘ (g ∘ ρ))) by _.
61   = (((i (-R1)) · (f ∘ ρ)) + ((i (-R1)) · (g ∘ ρ))) by _.
62   = (((f ∘ ρ) · (i (-R1))) + ((g ∘ ρ) · (i (-R1)))) by _.
63   = (((f ∘ ρ) + (g ∘ ρ)) · (i (-R1))) by _.
64   = ((i (-R1)) · ((f + g) ∘ ρ)) by _.
65   = (ρ ∘ ((f + g) ∘ ρ)) by _
66  done.
67 qed.
68
69 theorem d_mult_d_p: ∀f:F. ∀g:F. (fdispari f ∧ fdispari g) → fpari (f · g).
70  assume f:F.
71  assume g:F.
72  suppose (fdispari f ∧ fdispari g) (h).
73  by h we have (fdispari f) (h1) and (fdispari g) (h2).
74  we need to prove (fpari (f · g))
75  or equivalently ((f · g) = (f · g) ∘ ρ).
76  conclude
77     (f · g)
78   = (f · (ρ ∘ (g ∘ ρ))) by _.
79   = ((ρ ∘ (f ∘ ρ)) · (ρ ∘ (g ∘ ρ))) by _.
80   = (((-R1) · (f ∘ ρ)) · (ρ ∘ (g ∘ ρ))) by _.
81   = (((-R1) · (f ∘ ρ)) · ((-R1) · (g ∘ ρ))) by _.
82   = ((-R1) · (f ∘ ρ) · (-R1) · (g ∘ ρ)) by _.
83   = ((-R1) · ((f ∘ ρ) · (-R1)) · (g ∘ ρ)) by _.
84   = ((-R1) · (-R1) · (f ∘ ρ) · (g ∘ ρ)) by _.
85   = (R1 · ((f ∘ ρ) · (g ∘ ρ))) by _.
86   = (((f ∘ ρ) · (g ∘ ρ))) by _.
87   = ((f · g) ∘ ρ) by _
88  done.
89 qed.
90
91 theorem p_mult_d_p: ∀f:F. ∀g:F. (fpari f ∧ fdispari g) → fdispari (f · g).
92  assume f:F.
93  assume g:F.
94  suppose (fpari f ∧ fdispari g) (h).
95  by h we have (fpari f) (h1) and (fdispari g) (h2).
96  we need to prove (fdispari (f · g))
97  or equivalently ((f · g) = ρ ∘ ((f · g) ∘ ρ)).
98  conclude
99     (f · g)
100   = (f · (ρ ∘ (g ∘ ρ))) by _.
101   = ((f ∘ ρ) · (ρ ∘ (g ∘ ρ))) by _.
102   = ((f ∘ ρ) · ((-R1) · (g ∘ ρ))) by _.
103   = ((-R1) · ((f ∘ ρ) · (g ∘ ρ))) by _.
104   = ((-R1) · ((f · g) ∘ ρ)) by _.
105   = (ρ ∘ ((f · g) ∘ ρ)) by _
106  done.
107 qed.
108
109 theorem p_plus_c_p: ∀f:F. ∀x:R. fpari f → fpari (f + (i x)).
110  assume f:F.
111  assume x:R.
112  suppose (fpari f) (h).
113  we need to prove (fpari (f + (i x)))
114  or equivalently (f + (i x) = (f + (i x)) ∘ ρ).
115  by _ done.
116 qed.
117
118 theorem p_mult_c_p: ∀f:F. ∀x:R. fpari f → fpari (f · (i x)).
119  assume f:F.
120  assume x:R.
121  suppose (fpari f) (h).
122  we need to prove (fpari (f · (i x)))
123  or equivalently ((f · (i x)) = (f · (i x)) ∘ ρ).
124  by _ done.
125 qed.
126
127 theorem d_mult_c_d: ∀f:F. ∀x:R. fdispari f → fdispari (f · (i x)).
128  assume f:F.
129  assume x:R.
130  suppose (fdispari f) (h).
131  rewrite < fmult_commutative.
132  by _ done.
133 qed.
134
135 theorem d_comp_d_d: ∀f,g:F. fdispari f → fdispari g → fdispari (f ∘ g).
136  assume f:F.
137  assume g:F.
138  suppose (fdispari f) (h1).
139  suppose (fdispari g) (h2).
140  we need to prove (fdispari (f ∘ g))
141  or equivalently (f ∘ g = ρ ∘ ((f ∘ g) ∘ ρ)).
142  conclude
143     (f ∘ g)
144   = (ρ ∘ (f ∘ ρ) ∘ g) by _.
145   = (ρ ∘ (f ∘ ρ) ∘ ρ ∘ (g ∘ ρ)) by _.
146   = (ρ ∘ f ∘ (ρ ∘ ρ) ∘ (g ∘ ρ)) by _.
147   = (ρ ∘ f ∘ id ∘ (g ∘ ρ)) by _.
148   = (ρ ∘ ((f ∘ g) ∘ ρ)) by _
149  done.
150 qed.
151
152 theorem pari_in_dispari: ∀ f:F. fpari f → fdispari f '.
153  assume f:F. 
154  suppose (fpari f) (h1).
155  we need to prove (fdispari f ')
156  or equivalently (f ' = ρ ∘ (f ' ∘ ρ)).
157  conclude 
158     (f ')
159   = ((f ∘ ρ) ') by _. (*h1*)
160   = ((f ' ∘ ρ) · ρ ') by _. (*demult*)
161   = ((f ' ∘ ρ) · -R1) by _. (*deinv*)
162   = ((-R1) · (f ' ∘ ρ)) by _. (*fmult_commutative*)
163   = (ρ ∘ (f ' ∘ ρ)) (*reflex_ok*) by _
164  done.
165 qed.
166
167 theorem dispari_in_pari: ∀ f:F. fdispari f → fpari f '.
168  assume f:F. 
169  suppose (fdispari f) (h1).
170  we need to prove (fpari f ')
171  or equivalently (f ' = f ' ∘ ρ).
172  conclude 
173     (f ')
174   = ((ρ ∘ (f ∘ ρ)) ') by _.
175   = ((ρ ' ∘ (f ∘ ρ)) · ((f ∘ ρ) ')) by _.
176   = (((-R1) ∘ (f ∘ ρ)) · ((f ∘ ρ) ')) by _.
177   = (((-R1) ∘ (f ∘ ρ)) · ((f ' ∘ ρ) · (-R1))) by _.
178   = ((-R1) · ((f ' ∘ ρ) · (-R1))) by _.
179   = (((f ' ∘ ρ) · (-R1)) · (-R1)) by _.
180   = ((f ' ∘ ρ) · ((-R1) · (-R1))) by _.
181   = ((f ' ∘ ρ) · R1) by _.
182   = (f ' ∘ ρ) by _
183  done.
184 qed.
185
186 alias symbol "plus" = "natural plus".
187 alias num (instance 0) = "natural number".
188 theorem de_prodotto_funzioni:
189  ∀ n:nat. (id ^ (n + 1)) ' = ((n + 1)) · (id ^ n).
190  assume n:nat.
191  we proceed by induction on n to prove
192    ((id ^ (n + 1)) ' = (i (n + 1)) · (id ^ n)).
193  case O.
194   we need to prove ((id ^ (0 + 1)) ' = (i 1) · (id ^ 0)).
195   conclude
196      ((id ^ (0 + 1)) ')
197    = ((id ^ 1) ') by _.
198    = ((id · (id ^ 0)) ') by _.
199    = ((id · R1) ') by _.
200    = (id ') by _.
201    = (i R1) by _.
202    = (i R1 · R1) by _.
203    = (i (R0 + R1) · R1) by _.
204    = (1 · (id ^ 0)) by _
205  done.
206  case S (n:nat).
207   by induction hypothesis we know
208      ((id ^ (n + 1)) ' = ((n + 1)) · (id ^ n)) (H).
209   we need to prove
210      ((id ^ ((n + 1)+1)) '
211    = (i ((n + 1)+1)) · (id ^ (n+1))).
212   conclude
213      ((id ^ ((n + 1) + 1)) ')
214    = ((id ^ ((n + (S 1)))) ') by _.
215    = ((id ^ (S (n + 1))) ') by _.
216    = ((id · (id ^ (n + 1))) ') by _.
217    = ((id ' · (id ^ (n + 1))) + (id · (id ^ (n + 1)) ')) by _.
218    alias symbol "plus" (instance 1) = "function plus".
219    = ((R1 · (id ^ (n + 1))) + (id · (((n + 1)) · (id ^ n)))) by _.
220    = ((R1 · (id ^ (n + 1))) + (((n + 1) · id · (id ^ n)))) by _.
221    = ((R1 · (id ^ (n + 1))) + ((n + 1) · (id ^ (1 + n)))) by _.
222    = ((R1 · (id ^ (n + 1))) + ((n + 1) · (id ^ (n + 1)))) by _.
223    alias symbol "plus" (instance 2) = "function plus".
224    = (((R1 + (n + 1))) · (id ^ (n + 1))) by _.
225    = ((1 + (n + 1)) · (id ^ (n + 1))) by _;
226    = ((n + 1 + 1) · (id ^ (n + 1))) by _
227   done.
228 qed.
229
230 let rec times (n:nat) (x:R) on n: R ≝
231  match n with
232  [ O ⇒ R0
233  | S n ⇒ Rplus x (times n x)
234  ].
235
236 axiom invS: nat→R.
237 axiom invS1: ∀n:nat. Rmult (invS n) (real_of_nat (n + 1)) = R1.
238 axiom invS2: invS 1 + invS 1 = R1. (*forse*)
239
240 axiom e:F.
241 axiom deriv_e: e ' = e.
242 axiom e1: e · (e ∘ ρ) = R1.
243
244 (*
245 theorem decosh_senh:
246    (invS 1 · (e + (e ∘ ρ)))' = (invS 1 · (e + (ρ ∘ (e ∘ ρ)))).
247 *)