]> matita.cs.unibo.it Git - helm.git/blob - Q/ratio/rtimes.ma
made executable again
[helm.git] / Q / ratio / rtimes.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "Q/ratio/rinv.ma".
16 include "Q/fraction/ftimes.ma".
17
18 definition rtimes : ratio → ratio → ratio ≝
19 λr,s:ratio.
20   match r with
21   [one ⇒ s
22   | (frac f) ⇒ 
23       match s with 
24       [one ⇒ frac f
25       | (frac g) ⇒ ftimes f g]].
26
27 theorem symmetric_rtimes : symmetric ratio rtimes.
28 change with (∀r,s:ratio. rtimes r s = rtimes s r).
29 intros.
30 elim r. elim s.
31 reflexivity.
32 reflexivity.
33 elim s.
34 reflexivity.
35 simplify.apply symmetric2_ftimes.
36 qed.
37
38 variant sym_rtimes : ∀x,y:ratio. rtimes x y = rtimes y x ≝ symmetric_rtimes.
39
40 theorem rtimes_r_one: ∀r.rtimes r one = r.
41  intro; cases r;reflexivity.
42 qed.
43
44 theorem rtimes_one_r: ∀r.rtimes one r = r.
45 intro; cases r;reflexivity.
46 qed.
47
48 theorem rtimes_Zplus: \forall x,y.
49 rtimes (nat_frac_item_to_ratio x) (nat_frac_item_to_ratio y) =
50 nat_frac_item_to_ratio (x + y).
51 intro.
52 elim x
53   [reflexivity
54   |*:elim y;reflexivity
55   ]
56 qed.
57
58 theorem rtimes_Zplus1: \forall x,y,f.
59 rtimes (nat_frac_item_to_ratio x) (frac (cons y f)) =
60 frac (cons ((x + y)) f).
61 intro.
62 elim x
63   [reflexivity
64   |*:elim y;reflexivity
65   ]
66 qed.
67
68 theorem rtimes_Zplus2: \forall x,y,f.
69 rtimes (frac (cons y f)) (nat_frac_item_to_ratio x) =
70 frac (cons ((y + x)) f).
71 intros.
72 elim x
73   [elim y;reflexivity
74   |*:elim y;reflexivity
75   ]
76 qed.
77
78 theorem or_one_frac: \forall f,g.
79 rtimes (frac f) (frac g) = one \lor
80 \exists h.rtimes (frac f) (frac g) = frac h.
81 intros.
82 elim (rtimes (frac f) (frac g))
83   [left.reflexivity
84   |right.apply (ex_intro ? ? f1).reflexivity
85   ]
86 qed.
87
88 theorem one_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
89 rtimes (frac f) (frac g) = one \to
90 rtimes (frac (cons x f)) (frac (cons y g)) = nat_frac_item_to_ratio (x + y).
91 intros.simplify.simplify in H.rewrite > H.simplify.
92 reflexivity.
93 qed.
94
95 theorem frac_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
96 \forall h.rtimes (frac f) (frac g) = frac h \to
97 rtimes (frac (cons x f)) (frac (cons y g)) = frac (cons (x + y) h).
98 intros.simplify.simplify in H.rewrite > H.simplify.
99 reflexivity.
100 qed.
101
102
103 theorem nat_frac_item_to_ratio_frac_frac: \forall z,f1,f2.
104 rtimes (rtimes (nat_frac_item_to_ratio z) (frac f1)) (frac f2)
105 =rtimes (nat_frac_item_to_ratio z) (rtimes (frac f1) (frac f2)).
106 intros 2.elim f1
107   [elim f2
108     [change with
109      (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (pos n1))
110       =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (pos n1)))).
111      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
112      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
113      rewrite > assoc_Zplus.reflexivity
114     |change with
115      (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (neg n1))
116       =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (neg n1)))).
117      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
118      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
119      rewrite > assoc_Zplus.reflexivity
120     |change with
121       (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (pos n))) (frac (cons z1 f))
122        = rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (pos n)) (frac (cons z1 f)))).
123      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
124      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
125      rewrite > assoc_Zplus.reflexivity
126     ]
127   |elim f2
128     [change with
129      (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (pos n1))
130       =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (pos n1)))).
131      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
132      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
133      rewrite > assoc_Zplus.reflexivity
134     |change with
135      (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (neg n1))
136       =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (neg n1)))).
137      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
138      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
139      rewrite > assoc_Zplus.reflexivity
140     |change with
141       (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (neg n))) (frac (cons z1 f))
142        = rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (neg n)) (frac (cons z1 f)))).
143      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
144      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
145      rewrite > assoc_Zplus.reflexivity
146     ]
147   |elim f2
148     [change with
149      (rtimes (rtimes (nat_frac_item_to_ratio z) (frac (cons z1 f))) (nat_frac_item_to_ratio (pos n))
150       =rtimes (nat_frac_item_to_ratio z) (rtimes (frac (cons z1 f)) (nat_frac_item_to_ratio (pos n)))).
151      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
152      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
153      rewrite > assoc_Zplus.reflexivity
154     |change with
155      (rtimes (rtimes (nat_frac_item_to_ratio z) (frac (cons z1 f))) (nat_frac_item_to_ratio (neg n))
156       =rtimes (nat_frac_item_to_ratio z) (rtimes (frac (cons z1 f)) (nat_frac_item_to_ratio (neg n)))).  
157      rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
158      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
159      rewrite > assoc_Zplus.reflexivity
160     |elim (or_one_frac f f3)
161       [rewrite > rtimes_Zplus1.
162        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
163        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
164        rewrite > rtimes_Zplus.
165        rewrite > assoc_Zplus.reflexivity
166       |elim H2.clear H2.
167        rewrite > rtimes_Zplus1.
168        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
169        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
170        rewrite > rtimes_Zplus1.
171        rewrite > assoc_Zplus.reflexivity
172       ]
173     ]
174   ]
175 qed.
176
177 theorem cons_frac_frac: \forall f1,z,f,f2.
178 rtimes (rtimes (frac (cons z f)) (frac f1)) (frac f2)
179 =rtimes (frac (cons z f)) (rtimes (frac f1) (frac f2)).
180 intro.elim f1
181   [elim f2
182     [change with
183      (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (pos n1))
184       =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (pos n1)))).
185      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
186      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
187      rewrite > assoc_Zplus.reflexivity
188     |change with
189      (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (neg n1))
190       =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (neg n1)))).
191      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
192      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
193      rewrite > assoc_Zplus.reflexivity
194     |change with
195       (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (pos n))) (frac (cons z1 f3))
196        = rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (pos n)) (frac (cons z1 f3)))).
197      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
198      elim (or_one_frac f f3)
199       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
200        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
201        rewrite > assoc_Zplus.reflexivity
202       |elim H1.clear H1.
203        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
204        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
205        rewrite > assoc_Zplus.reflexivity
206       ]
207     ]
208   |elim f2
209     [change with
210      (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (pos n1))
211       =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (pos n1)))).
212      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
213      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
214      rewrite > assoc_Zplus.reflexivity
215     |change with
216      (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (neg n1))
217       =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (neg n1)))).
218      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
219      rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
220      rewrite > assoc_Zplus.reflexivity
221     |change with
222       (rtimes (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (neg n))) (frac (cons z1 f3))
223        = rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (neg n)) (frac (cons z1 f3)))).
224      rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
225      elim (or_one_frac f f3)
226       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
227        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
228        rewrite > assoc_Zplus.reflexivity
229       |elim H1.clear H1.
230        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
231        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
232        rewrite > assoc_Zplus.reflexivity
233       ]
234     ]
235   |elim f3
236     [change with
237      (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (nat_frac_item_to_ratio (pos n))
238       =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (pos n)))).
239      rewrite > rtimes_Zplus2.
240      elim (or_one_frac f2 f)
241       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
242        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
243        rewrite > rtimes_Zplus.
244        rewrite > assoc_Zplus.reflexivity
245       |elim H1.clear H1.
246        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
247        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
248        rewrite > rtimes_Zplus2.
249        rewrite > assoc_Zplus.reflexivity
250       ]
251     |change with
252      (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (nat_frac_item_to_ratio (neg n))
253       =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (nat_frac_item_to_ratio (neg n)))).
254      rewrite > rtimes_Zplus2.
255      elim (or_one_frac f2 f)
256       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
257        rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
258        rewrite > rtimes_Zplus.
259        rewrite > assoc_Zplus.reflexivity
260       |elim H1.clear H1.
261        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
262        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
263        rewrite > rtimes_Zplus2.
264        rewrite > assoc_Zplus.reflexivity
265       ]
266     |elim (or_one_frac f2 f)
267       [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
268        rewrite > rtimes_Zplus1.
269        elim (or_one_frac f f4)
270         [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H3).
271          rewrite > rtimes_Zplus2.
272          cut (f4 = f2)
273           [rewrite > Hcut.
274            rewrite > assoc_Zplus.reflexivity
275           |apply injective_frac.
276            rewrite < rtimes_one_r.
277            rewrite < H2.
278            (* problema inaspettato: mi serve l'unicita' dell'inversa,
279               che richiede (?) l'associativita. Per fortuna basta 
280               l'ipotesi induttiva. *)
281            cases f2
282             [change with 
283              (rtimes (rtimes (nat_frac_item_to_ratio (pos n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (pos n)).
284              rewrite > nat_frac_item_to_ratio_frac_frac.
285              rewrite > H3.
286              rewrite > rtimes_r_one.
287              reflexivity
288             |change with 
289              (rtimes (rtimes (nat_frac_item_to_ratio (neg n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (neg n)).
290              rewrite > nat_frac_item_to_ratio_frac_frac.
291              rewrite > H3.
292              rewrite > rtimes_r_one.
293              reflexivity
294             |rewrite > H.
295              rewrite > H3.
296              rewrite > rtimes_r_one.
297              reflexivity
298             ]
299           ]
300         |elim H3.clear H3.
301          rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H4).
302          cut (rtimes (frac f2) (frac a) = frac f4)
303           [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f4 Hcut).
304            rewrite > assoc_Zplus.reflexivity
305           |rewrite < H4.
306            generalize in match H2.
307            cases f2;intro
308             [change with 
309              (rtimes (nat_frac_item_to_ratio (pos n)) (rtimes (frac f)(frac f4)) =frac f4).
310              rewrite < nat_frac_item_to_ratio_frac_frac.
311              rewrite > H3.
312              rewrite > rtimes_one_r.
313              reflexivity
314             |change with 
315              (rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f)(frac f4)) =frac f4).
316              rewrite < nat_frac_item_to_ratio_frac_frac.
317              rewrite > H3.
318              rewrite > rtimes_one_r.
319              reflexivity
320             |rewrite < H.
321              rewrite > H3.
322              rewrite > rtimes_one_r.
323              reflexivity
324             ]
325           ]
326         ]
327       |elim H2.clear H2.
328        rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
329        elim (or_one_frac f f4)
330         [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
331          rewrite > rtimes_Zplus2.
332          cut (rtimes (frac a) (frac f4) = frac f2)
333           [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f2 Hcut).
334            rewrite > assoc_Zplus.reflexivity
335           |rewrite < H3.
336            generalize in match H2.
337            cases f2;intro
338             [change with 
339              (rtimes (rtimes (nat_frac_item_to_ratio (pos n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (pos n)).
340              rewrite > nat_frac_item_to_ratio_frac_frac.
341              rewrite > H4.
342              rewrite > rtimes_r_one.
343              reflexivity
344             |change with 
345              (rtimes (rtimes (nat_frac_item_to_ratio (neg n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (neg n)).
346              rewrite > nat_frac_item_to_ratio_frac_frac.
347              rewrite > H4.
348              rewrite > rtimes_r_one.
349              reflexivity
350             |rewrite > H.
351              rewrite > H4.
352              rewrite > rtimes_r_one.
353              reflexivity
354             ]
355           ]
356         |elim H2.clear H2.
357          rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a1 H4).
358          elim (or_one_frac a f4)
359           [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
360            cut (rtimes (frac f2) (frac a1) = one)
361             [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? Hcut).
362              rewrite > assoc_Zplus.reflexivity
363             |rewrite < H4.
364              generalize in match H3.
365              cases f2;intro
366               [change with 
367                (rtimes (nat_frac_item_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = one).
368                rewrite < nat_frac_item_to_ratio_frac_frac.
369                rewrite > H5.
370                assumption
371               |change with 
372                (rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = one).
373                rewrite < nat_frac_item_to_ratio_frac_frac.
374                rewrite > H5.
375                assumption
376               |rewrite < H.
377                rewrite > H5.
378                assumption
379               ]
380             ]
381           |elim H2.clear H2.
382            rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 H5).
383            cut (rtimes (frac f2) (frac a1) = frac a2)
384             [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 Hcut).
385              rewrite > assoc_Zplus.reflexivity
386             |rewrite < H4.
387              generalize in match H3.
388              cases f2;intro
389               [change with 
390                (rtimes (nat_frac_item_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = frac a2).
391                rewrite < nat_frac_item_to_ratio_frac_frac.
392                rewrite > H2.
393                assumption
394               |change with 
395                (rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = frac a2).
396                rewrite < nat_frac_item_to_ratio_frac_frac.
397                rewrite > H2.
398                assumption
399               |rewrite < H.
400                rewrite > H2.
401                assumption
402               ]
403             ]
404           ]
405         ]
406       ]
407     ]
408   ]
409 qed.
410        
411 theorem frac_frac_fracaux: ∀f,f1,f2.
412 rtimes (rtimes (frac f) (frac f1)) (frac f2)
413 =rtimes (frac f) (rtimes (frac f1) (frac f2)).
414 intros.
415 cases f
416   [change with
417    (rtimes (rtimes (nat_frac_item_to_ratio (pos n)) (frac f1)) (frac f2)
418     =rtimes (nat_frac_item_to_ratio (pos n)) (rtimes (frac f1) (frac f2))).
419    apply nat_frac_item_to_ratio_frac_frac
420   |change with
421    (rtimes (rtimes (nat_frac_item_to_ratio (neg n)) (frac f1)) (frac f2)
422     =rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f1) (frac f2))).
423    apply nat_frac_item_to_ratio_frac_frac
424   |apply cons_frac_frac]
425 qed.
426
427
428 theorem associative_rtimes:associative ? rtimes.
429 unfold.intros.
430 cases x
431   [reflexivity
432   |cases y
433     [reflexivity.
434     |cases z
435       [rewrite > rtimes_r_one.rewrite > rtimes_r_one.reflexivity
436       |apply frac_frac_fracaux
437       ]]]
438 qed.
439
440
441 theorem rtimes_rinv: ∀r:ratio. rtimes r (rinv r) = one.
442 intro.elim r.
443 reflexivity.
444 simplify.apply ftimes_finv.
445 qed.
446
447 theorem rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
448 (rtimes (frac f) (frac g) = one \land
449  rtimes (frac (cons x f)) (frac (cons y g)) = nat_frac_item_to_ratio (x + y))
450 \lor (\exists h.rtimes (frac f) (frac g) = frac h \land
451 rtimes (frac (cons x f)) (frac (cons y g)) =
452 frac (cons (x + y) h)).
453 intros.
454 simplify.
455 elim (rtimes (frac f) (frac g));simplify
456   [left.split;reflexivity
457   |right.
458    apply (ex_intro ? ? f1).
459    split;reflexivity]
460 qed.