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/didactic/ex_deriv".
19 theorem p_plus_p_p: ∀f:F. ∀g:F. (fpari f ∧ fpari g) → fpari (f ⊕ g).
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) ∘ ρ).
29 = ((f ∘ ρ) ⊕ (g ∘ ρ)) by _.
34 theorem p_mult_p_p: ∀f:F. ∀g:F. (fpari f ∧ fpari g) → fpari (f · g).
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) ∘ ρ).
44 = ((f ∘ ρ) · (g ∘ ρ)) by _.
49 theorem d_plus_d_d: ∀f:F. ∀g:F. (fdispari f ∧ fdispari g) → fdispari (f ⊕ g).
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) ∘ ρ))).
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 _
69 theorem d_mult_d_p: ∀f:F. ∀g:F. (fdispari f ∧ fdispari g) → fpari (f · g).
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) ∘ ρ).
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 _.
91 theorem p_mult_d_p: ∀f:F. ∀g:F. (fpari f ∧ fdispari g) → fdispari (f · g).
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) ∘ ρ)).
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 _
109 theorem p_plus_c_p: ∀f:F. ∀x:R. fpari f → fpari (f ⊕ (i x)).
112 suppose (fpari f) (h).
113 we need to prove (fpari (f ⊕ (i x)))
114 or equivalently (f ⊕ (i x) = (f ⊕ (i x)) ∘ ρ).
118 theorem p_mult_c_p: ∀f:F. ∀x:R. fpari f → fpari (f · (i x)).
121 suppose (fpari f) (h).
122 we need to prove (fpari (f · (i x)))
123 or equivalently ((f · (i x)) = (f · (i x)) ∘ ρ).
127 theorem d_mult_c_d: ∀f:F. ∀x:R. fdispari f → fdispari (f · (i x)).
130 suppose (fdispari f) (h).
131 rewrite < fmult_commutative.
135 theorem d_comp_d_d: ∀f,g:F. fdispari f → fdispari g → fdispari (f ∘ g).
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) ∘ ρ)).
144 = (ρ ∘ (f ∘ ρ) ∘ g) by _.
145 = (ρ ∘ (f ∘ ρ) ∘ ρ ∘ (g ∘ ρ)) by _.
146 = (ρ ∘ f ∘ (ρ ∘ ρ) ∘ (g ∘ ρ)) by _.
147 = (ρ ∘ f ∘ id ∘ (g ∘ ρ)) by _.
148 = (ρ ∘ ((f ∘ g) ∘ ρ)) by _
152 theorem pari_in_dispari: ∀ f:F. fpari f → fdispari f '.
154 suppose (fpari f) (h1).
155 we need to prove (fdispari f ')
156 or equivalently (f ' = ρ ∘ (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 _
167 theorem dispari_in_pari: ∀ f:F. fdispari f → fpari f '.
169 suppose (fdispari f) (h1).
170 we need to prove (fpari f ')
171 or equivalently (f ' = 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 _.
187 alias id "plus" = "cic:/matita/nat/plus/plus.con".
188 theorem de_prodotto_funzioni:
189 ∀ n:nat. (id ^ (plus n (S O))) ' = (i (n + (S O))) · (id ^ n).
191 we proceed by induction on n to prove
192 ((id ^ (plus n (S O))) ' = (i (n + (S O))) · (id ^ n)).
194 we need to prove ((id ^ (plus O (S O))) ' = (i (S O)) · (id ^ O)).
196 ((id ^ (plus O (S O))) ')
197 = ((id ^ (S O)) ') by _.
198 = ((id · (id ^ O)) ') by _.
199 = ((id · (i R1)) ') by _.
202 = (i R1 · i R1) by _.
203 = (i (R0 + R1) · R1) by _.
204 = ((i (S O)) · (id ^ O)) by _
207 by induction hypothesis we know
208 ((id ^ (plus n (S O))) ' = (i (n + (S O))) · (id ^ n)) (H).
210 ((id ^ (plus (plus n (S O)) (S O))) '
211 = (i (plus (plus n (S O)) (S O))) · (id ^ (plus n (S O)))).
213 ((id ^ ((n + (S O)) + (S O))) ')
214 = ((id ^ ((n + (S (S O))))) ') by _.
215 = ((id ^ (S (n + S O))) ') by _.
216 = ((id · (id ^ (n + (S O)))) ') by _.
217 = ((id ' · (id ^ (n + (S O)))) ⊕ (id · (id ^ (n + (S O))) ')) by _.
218 alias symbol "plus" (instance 4) = "natural plus".
219 = ((R1 · (id ^ (n + (S O)))) ⊕ (id · ((i (n + S O)) · (id ^ n)))) by _.
220 = ((R1 · (id ^ (n + (S O)))) ⊕ (((i (n + S O)) · id · (id ^ n)))) by _.
221 alias symbol "plus" (instance 8) = "natural plus".
222 = ((R1 · (id ^ (n + (S O)))) ⊕ ((i (n + S O)) · (id ^ (n + (S O))))) by _.
223 = ((i R1 · (id ^ (n + (S O)))) ⊕ ((i (n + S O)) · (id ^ (n + (S O))))) by _.
224 alias symbol "plus" = "natural plus".
225 cut (((i R1 · (id ^ (n + (S O)))) ⊕ ((i (n + S O)) · (id ^ (n + (S O))))) =
226 (((i R1 ⊕ (i (plus n (S O)))) · (id ^ (n + (S O))))));[| by _ done;]
227 unfold F_OF_nat in Hcut;
229 = (((i R1 ⊕ (i (plus n (S O)))) · (id ^ (n + (S O))))) by _.
230 = ((i (n + S O + S O)) · (id ^ (n + S O))) by _
235 let rec times (n:nat) (x:R) on n: R ≝
238 | S n ⇒ Rplus x (times n x)
242 axiom invS1: ∀n:nat. Rmult (invS n) (real_of_nat (n + S O)) = R1.
243 axiom invS2: invS (S O) + invS (S O) = R1. (*forse*)
246 axiom deriv_e: e ' = e.
247 axiom e1: e · (e ∘ ρ) = R1.
251 (invS (S O) · (e ⊕ (e ∘ ρ)))' = (invS (S O) · (e ⊕ (ρ ∘ (e ∘ ρ)))).