1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
16 let rec nat_fact_to_fraction_inv l \def
18 [nf_last a \Rightarrow nn a
19 |nf_cons a p \Rightarrow
20 cons (neg_Z_of_nat a) (nat_fact_to_fraction_inv p)
24 definition nat_fact_all_to_Q_inv \def
27 [nfa_zero \Rightarrow OQ
28 |nfa_one \Rightarrow Qpos one
29 |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction_inv l))
33 definition nat_to_Q_inv \def
34 \lambda n. nat_fact_all_to_Q_inv (factorize n).
37 definition frac:nat \to nat \to Q \def
38 \lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
40 theorem rtimes_oner: \forall r.rtimes r one = r.
41 intro.cases r;reflexivity.
44 theorem rtimes_onel: \forall r.rtimes one r = r.
45 intro.cases r;reflexivity.
48 let rec times_f h g \def
50 [nf_last a \Rightarrow
52 [nf_last b \Rightarrow nf_last (S (a+b))
53 |nf_cons b g1 \Rightarrow nf_cons (S (a+b)) g1
55 |nf_cons a h1 \Rightarrow
57 [nf_last b \Rightarrow nf_cons (S (a+b)) h1
58 |nf_cons b g1 \Rightarrow nf_cons (a+b) (times_f h1 g1)
63 definition times_fa \def
66 [nfa_zero \Rightarrow nfa_zero
67 |nfa_one \Rightarrow g
68 |nfa_proper f1 \Rightarrow match g with
69 [nfa_zero \Rightarrow nfa_zero
70 |nfa_one \Rightarrow nfa_proper f1
71 |nfa_proper g1 \Rightarrow nfa_proper (times_f f1 g1)
76 theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
77 =defactorize_aux g m*defactorize_aux h m.
79 [elim h;simplify;autobatch
82 |simplify.rewrite > (H n3 (S m)).autobatch
87 theorem eq_times_fa_times: \forall f,g.
88 defactorize (times_fa f g) = defactorize f*defactorize g.
92 |simplify.apply plus_n_O
96 |apply eq_times_f_times1
101 theorem eq_times_times_fa: \forall n,m.
102 factorize (n*m) = times_fa (factorize n) (factorize m).
104 rewrite <(factorize_defactorize (times_fa (factorize n) (factorize m))).
105 rewrite > eq_times_fa_times.
106 rewrite > defactorize_factorize.
107 rewrite > defactorize_factorize.
112 theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
113 Z_of_nat n + Z_of_nat m.
117 [simplify.rewrite < plus_n_O.reflexivity
118 |simplify.reflexivity.
123 definition unfrac \def \lambda f.
125 [one \Rightarrow pp O
126 |frac f \Rightarrow f
130 lemma injective_frac: injective fraction ratio frac.
132 change with ((unfrac (frac x)) = (unfrac (frac y))).
133 rewrite < H.reflexivity.
136 theorem times_f_ftimes: \forall n,m.
137 frac (nat_fact_to_fraction (times_f n m))
138 = ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m).
143 rewrite < plus_n_Sm.reflexivity
145 [simplify.rewrite < plus_n_O.reflexivity
146 |simplify.reflexivity.
151 [simplify.reflexivity
152 |simplify.rewrite < plus_n_Sm.reflexivity
155 cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h)
161 |apply injective_frac.
165 |generalize in match n4.
167 [cases n6;simplify;autobatch
181 theorem times_fa_Qtimes: \forall f,g. nat_fact_all_to_Q (times_fa f g) =
182 Qtimes (nat_fact_all_to_Q f) (nat_fact_all_to_Q g).
190 |rewrite > times_f_ftimes.reflexivity
195 theorem times_Qtimes: \forall p,q.
196 (nat_to_Q (p*q)) = Qtimes (nat_to_Q p) (nat_to_Q q).
197 intros.unfold nat_to_Q.
198 rewrite < times_fa_Qtimes.
199 rewrite < eq_times_times_fa.
203 theorem rtimes_Zplus: \forall x,y.
204 rtimes (Z_to_ratio x) (Z_to_ratio y) =
214 theorem rtimes_Zplus1: \forall x,y,f.
215 rtimes (Z_to_ratio x) (frac (cons y f)) =
216 frac (cons ((x + y)) f).
225 theorem rtimes_Zplus2: \forall x,y,f.
226 rtimes (frac (cons y f)) (Z_to_ratio x) =
227 frac (cons ((y + x)) f).
236 theorem or_one_frac: \forall f,g.
237 rtimes (frac f) (frac g) = one \lor
238 \exists h.rtimes (frac f) (frac g) = frac h.
240 elim (rtimes (frac f) (frac g))
242 |right.apply (ex_intro ? ? f1).reflexivity
246 theorem one_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
247 rtimes (frac f) (frac g) = one \to
248 rtimes (frac (cons x f)) (frac (cons y g)) = Z_to_ratio (x + y).
249 intros.simplify.simplify in H.rewrite > H.simplify.
253 theorem frac_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
254 \forall h.rtimes (frac f) (frac g) = frac h \to
255 rtimes (frac (cons x f)) (frac (cons y g)) = frac (cons (x + y) h).
256 intros.simplify.simplify in H.rewrite > H.simplify.
260 theorem rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
261 (rtimes (frac f) (frac g) = one \land
262 rtimes (frac (cons x f)) (frac (cons y g)) = Z_to_ratio (x + y))
263 \lor (\exists h.rtimes (frac f) (frac g) = frac h \land
264 rtimes (frac (cons x f)) (frac (cons y g)) =
265 frac (cons (x + y) h)).
268 elim (rtimes (frac f) (frac g));simplify
269 [left.split;reflexivity
271 apply (ex_intro ? ? f1).
276 theorem Z_to_ratio_frac_frac: \forall z,f1,f2.
277 rtimes (rtimes (Z_to_ratio z) (frac f1)) (frac f2)
278 =rtimes (Z_to_ratio z) (rtimes (frac f1) (frac f2)).
282 (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1))
283 =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))).
284 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
285 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
286 rewrite > assoc_Zplus.reflexivity
288 (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (neg n1))
289 =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (neg n1)))).
290 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
291 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
292 rewrite > assoc_Zplus.reflexivity
294 (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (frac (cons z1 f))
295 = rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (frac (cons z1 f)))).
296 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
297 rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
298 rewrite > assoc_Zplus.reflexivity
302 (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (Z_to_ratio (pos n1))
303 =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (pos n1)))).
304 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
305 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
306 rewrite > assoc_Zplus.reflexivity
308 (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (Z_to_ratio (neg n1))
309 =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (neg n1)))).
310 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
311 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
312 rewrite > assoc_Zplus.reflexivity
314 (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (frac (cons z1 f))
315 = rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (frac (cons z1 f)))).
316 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
317 rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
318 rewrite > assoc_Zplus.reflexivity
322 (rtimes (rtimes (Z_to_ratio z) (frac (cons z1 f))) (Z_to_ratio (pos n))
323 =rtimes (Z_to_ratio z) (rtimes (frac (cons z1 f)) (Z_to_ratio (pos n)))).
324 rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
325 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
326 rewrite > assoc_Zplus.reflexivity
328 (rtimes (rtimes (Z_to_ratio z) (frac (cons z1 f))) (Z_to_ratio (neg n))
329 =rtimes (Z_to_ratio z) (rtimes (frac (cons z1 f)) (Z_to_ratio (neg n)))).
330 rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
331 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
332 rewrite > assoc_Zplus.reflexivity
333 |elim (or_one_frac f f3)
334 [rewrite > rtimes_Zplus1.
335 rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
336 rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
337 rewrite > rtimes_Zplus.
338 rewrite > assoc_Zplus.reflexivity
340 rewrite > rtimes_Zplus1.
341 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
342 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
343 rewrite > rtimes_Zplus1.
344 rewrite > assoc_Zplus.reflexivity
350 theorem cons_frac_frac: \forall f1,z,f,f2.
351 rtimes (rtimes (frac (cons z f)) (frac f1)) (frac f2)
352 =rtimes (frac (cons z f)) (rtimes (frac f1) (frac f2)).
356 (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1))
357 =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))).
358 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
359 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
360 rewrite > assoc_Zplus.reflexivity
362 (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (Z_to_ratio (neg n1))
363 =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (neg n1)))).
364 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
365 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
366 rewrite > assoc_Zplus.reflexivity
368 (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (frac (cons z1 f3))
369 = rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (frac (cons z1 f3)))).
370 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
371 elim (or_one_frac f f3)
372 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
373 rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
374 rewrite > assoc_Zplus.reflexivity
376 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
377 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
378 rewrite > assoc_Zplus.reflexivity
383 (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (Z_to_ratio (pos n1))
384 =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (pos n1)))).
385 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
386 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
387 rewrite > assoc_Zplus.reflexivity
389 (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (Z_to_ratio (neg n1))
390 =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (neg n1)))).
391 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
392 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
393 rewrite > assoc_Zplus.reflexivity
395 (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (frac (cons z1 f3))
396 = rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (frac (cons z1 f3)))).
397 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
398 elim (or_one_frac f f3)
399 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
400 rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
401 rewrite > assoc_Zplus.reflexivity
403 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
404 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
405 rewrite > assoc_Zplus.reflexivity
410 (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (Z_to_ratio (pos n))
411 =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (Z_to_ratio (pos n)))).
412 rewrite > rtimes_Zplus2.
413 elim (or_one_frac f2 f)
414 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
415 rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
416 rewrite > rtimes_Zplus.
417 rewrite > assoc_Zplus.reflexivity
419 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
420 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
421 rewrite > rtimes_Zplus2.
422 rewrite > assoc_Zplus.reflexivity
425 (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (Z_to_ratio (neg n))
426 =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (Z_to_ratio (neg n)))).
427 rewrite > rtimes_Zplus2.
428 elim (or_one_frac f2 f)
429 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
430 rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
431 rewrite > rtimes_Zplus.
432 rewrite > assoc_Zplus.reflexivity
434 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
435 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
436 rewrite > rtimes_Zplus2.
437 rewrite > assoc_Zplus.reflexivity
439 |elim (or_one_frac f2 f)
440 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
441 rewrite > rtimes_Zplus1.
442 elim (or_one_frac f f4)
443 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H3).
444 rewrite > rtimes_Zplus2.
447 rewrite > assoc_Zplus.reflexivity
448 |apply injective_frac.
449 rewrite < rtimes_onel.
451 (* problema inaspettato: mi serve l'unicita' dell'inversa,
452 che richiede (?) l'associativita. Per fortuna basta
453 l'ipotesi induttiva. *)
456 (rtimes (rtimes (Z_to_ratio (pos n)) (frac f)) (frac f4)=Z_to_ratio (pos n)).
457 rewrite > Z_to_ratio_frac_frac.
459 rewrite > rtimes_oner.
462 (rtimes (rtimes (Z_to_ratio (neg n)) (frac f)) (frac f4)=Z_to_ratio (neg n)).
463 rewrite > Z_to_ratio_frac_frac.
465 rewrite > rtimes_oner.
469 rewrite > rtimes_oner.
474 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H4).
475 cut (rtimes (frac f2) (frac a) = frac f4)
476 [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f4 Hcut).
477 rewrite > assoc_Zplus.reflexivity
479 generalize in match H2.
482 (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) =frac f4).
483 rewrite < Z_to_ratio_frac_frac.
485 rewrite > rtimes_onel.
488 (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) =frac f4).
489 rewrite < Z_to_ratio_frac_frac.
491 rewrite > rtimes_onel.
495 rewrite > rtimes_onel.
501 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
502 elim (or_one_frac f f4)
503 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
504 rewrite > rtimes_Zplus2.
505 cut (rtimes (frac a) (frac f4) = frac f2)
506 [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f2 Hcut).
507 rewrite > assoc_Zplus.reflexivity
509 generalize in match H2.
512 (rtimes (rtimes (Z_to_ratio (pos n)) (frac f)) (frac f4)=Z_to_ratio (pos n)).
513 rewrite > Z_to_ratio_frac_frac.
515 rewrite > rtimes_oner.
518 (rtimes (rtimes (Z_to_ratio (neg n)) (frac f)) (frac f4)=Z_to_ratio (neg n)).
519 rewrite > Z_to_ratio_frac_frac.
521 rewrite > rtimes_oner.
525 rewrite > rtimes_oner.
530 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a1 H4).
531 elim (or_one_frac a f4)
532 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
533 cut (rtimes (frac f2) (frac a1) = one)
534 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? Hcut).
535 rewrite > assoc_Zplus.reflexivity
537 generalize in match H3.
540 (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = one).
541 rewrite < Z_to_ratio_frac_frac.
545 (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = one).
546 rewrite < Z_to_ratio_frac_frac.
555 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 H5).
556 cut (rtimes (frac f2) (frac a1) = frac a2)
557 [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 Hcut).
558 rewrite > assoc_Zplus.reflexivity
560 generalize in match H3.
563 (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = frac a2).
564 rewrite < Z_to_ratio_frac_frac.
568 (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = frac a2).
569 rewrite < Z_to_ratio_frac_frac.
584 theorem frac_frac_fracaux: \forall f,f1,f2.
585 rtimes (rtimes (frac f) (frac f1)) (frac f2)
586 =rtimes (frac f) (rtimes (frac f1) (frac f2)).
590 (rtimes (rtimes (Z_to_ratio (pos n)) (frac f1)) (frac f2)
591 =rtimes (Z_to_ratio (pos n)) (rtimes (frac f1) (frac f2))).
592 apply Z_to_ratio_frac_frac
594 (rtimes (rtimes (Z_to_ratio (neg n)) (frac f1)) (frac f2)
595 =rtimes (Z_to_ratio (neg n)) (rtimes (frac f1) (frac f2))).
596 apply Z_to_ratio_frac_frac
597 |apply cons_frac_frac
601 theorem associative_rtimes:associative ? rtimes.
608 [rewrite > rtimes_oner.rewrite > rtimes_oner.reflexivity
609 |apply frac_frac_fracaux
615 theorem associative_Qtimes:associative ? Qtimes.
619 (* non posso scrivere 2,3: ... ?? *)
624 |simplify.rewrite > associative_rtimes.
626 |simplify.rewrite > associative_rtimes.
631 |simplify.rewrite > associative_rtimes.
633 |simplify.rewrite > associative_rtimes.
641 |simplify.rewrite > associative_rtimes.
643 |simplify.rewrite > associative_rtimes.
648 |simplify.rewrite > associative_rtimes.
650 |simplify.rewrite > associative_rtimes.
657 theorem Qtimes_OQ: \forall q.Qtimes q OQ = OQ.
658 intro.cases q;reflexivity.
661 theorem symmetric_Qtimes: symmetric ? Qtimes.
664 [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity
667 |simplify.rewrite > symmetric_rtimes.reflexivity
668 |simplify.rewrite > symmetric_rtimes.reflexivity
672 |simplify.rewrite > symmetric_rtimes.reflexivity
673 |simplify.rewrite > symmetric_rtimes.reflexivity
678 theorem Qtimes_Qinv: \forall q. q \neq OQ \to Qtimes q (Qinv q) = Qone.
682 |simplify.rewrite > rtimes_rinv.reflexivity
683 |simplify.rewrite > rtimes_rinv.reflexivity
687 theorem eq_Qtimes_OQ_to_eq_OQ: \forall p,q.
688 Qtimes p q = OQ \to p = OQ \lor q = OQ.
691 [intro.left.reflexivity
693 [intro.right.reflexivity
694 |simplify.intro.destruct H
695 |simplify.intro.destruct H
698 [intro.right.reflexivity
699 |simplify.intro.destruct H
700 |simplify.intro.destruct H
705 theorem Qinv_Qtimes: \forall p,q.
706 p \neq OQ \to q \neq OQ \to
708 Qtimes (Qinv p) (Qinv q).
710 rewrite < Qtimes_Qone_q in ⊢ (? ? ? %).
711 rewrite < (Qtimes_Qinv (Qtimes p q))
712 [lapply (Qtimes_Qinv ? H).
713 lapply (Qtimes_Qinv ? H1).
714 rewrite > symmetric_Qtimes in ⊢ (? ? ? (? % ?)).
715 rewrite > associative_Qtimes.
716 rewrite > associative_Qtimes.
717 rewrite < associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
718 rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
719 rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
721 rewrite > Qtimes_q_Qone.
723 rewrite > Qtimes_q_Qone.
726 elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
727 [apply (H H3)|apply (H1 H3)]
731 (* a stronger version, taking advantage of inv(O) = O *)
732 theorem Qinv_Qtimes': \forall p,q.
734 Qtimes (Qinv p) (Qinv q).
740 |apply Qinv_Qtimes;intro;destruct H
741 |apply Qinv_Qtimes;intro;destruct H
745 |apply Qinv_Qtimes;intro;destruct H
746 |apply Qinv_Qtimes;intro;destruct H
751 theorem Qtimes_frac_frac: \forall p,q,r,s.
752 Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)).
755 rewrite > associative_Qtimes.
756 rewrite < associative_Qtimes in ⊢ (? ? (? ? %) ?).
757 rewrite > symmetric_Qtimes in ⊢ (? ? (? ? (? % ?)) ?).
758 rewrite > associative_Qtimes in ⊢ (? ? (? ? %) ?).
759 rewrite < associative_Qtimes.
760 rewrite < times_Qtimes.
761 rewrite < Qinv_Qtimes'.
762 rewrite < times_Qtimes.
767 (* la prova seguente e' tutta una ripetizione. Sistemare. *)
769 theorem Qtimes1: \forall f:fraction.
770 Qtimes (nat_fact_all_to_Q (numerator f))
771 (Qinv (nat_fact_all_to_Q (numerator (finv f))))
777 |elim (or_numerator_nfa_one_nfa_proper f1)
780 cut (finv (nat_fact_to_fraction a) = f1)
783 rewrite > H2.rewrite > H1.simplify.
784 rewrite > Hcut.reflexivity
786 rewrite > H2.rewrite > H1.simplify.
787 rewrite > Hcut.reflexivity
789 rewrite > H2.rewrite > H1.simplify.
790 rewrite > Hcut.reflexivity
792 |generalize in match H.
793 rewrite > H2.rewrite > H1.simplify.
794 intro.destruct H3.assumption
799 rewrite > H2.rewrite > H2.simplify.
800 elim (or_numerator_nfa_one_nfa_proper (finv f1))
802 rewrite > H3.simplify.
803 cut (nat_fact_to_fraction a = f1)
804 [rewrite > Hcut.reflexivity
805 |generalize in match H.
808 rewrite > Qtimes_q_Qone.
814 generalize in match H.
816 rewrite > H3.simplify.
822 |simplify.rewrite > H2.simplify.
823 elim (or_numerator_nfa_one_nfa_proper (finv f1))
825 rewrite > H3.simplify.
826 cut (nat_fact_to_fraction a = f1)
827 [rewrite > Hcut.reflexivity
828 |generalize in match H.
831 rewrite > Qtimes_q_Qone.
837 generalize in match H.
839 rewrite > H3.simplify.
845 |simplify.rewrite > H2.simplify.
846 elim (or_numerator_nfa_one_nfa_proper (finv f1))
848 rewrite > H3.simplify.
849 cut (nat_fact_to_fraction a = f1)
850 [rewrite > Hcut.reflexivity
851 |generalize in match H.
854 rewrite > Qtimes_q_Qone.
860 generalize in match H.
862 rewrite > H3.simplify.
874 definition numQ:Q \to Z \def
878 |Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r)))
879 |Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r)))
883 definition numQ:Q \to nat \def
884 \lambda q. defactorize (numeratorQ q).
886 definition denomQ:Q \to nat \def
887 \lambda q. defactorize (numeratorQ (Qinv q)).
889 definition Qopp:Q \to Q \def \lambda q.
892 |Qpos q \Rightarrow Qneg q
893 |Qneg q \Rightarrow Qpos q
896 theorem frac_numQ_denomQ1: \forall r:ratio.
897 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
899 unfold frac.unfold denomQ.unfold numQ.
901 rewrite > factorize_defactorize.
902 rewrite > factorize_defactorize.
914 theorem frac_numQ_denomQ2: \forall r:ratio.
915 frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
917 unfold frac.unfold denomQ.unfold numQ.
919 rewrite > factorize_defactorize.
920 rewrite > factorize_defactorize.
931 definition Qabs:Q \to Q \def \lambda q.
934 |Qpos q \Rightarrow Qpos q
935 |Qneg q \Rightarrow Qpos q
938 theorem frac_numQ_denomQ: \forall q.
939 frac (numQ q) (denomQ q) = (Qabs q).
943 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
944 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
948 definition Qfrac: Z \to nat \to Q \def
949 \lambda z,n.match z with
951 |Zpos m \Rightarrow (frac (S m) n)
952 |Zneg m \Rightarrow Qopp (frac (S m) n)
955 definition QnumZ \def \lambda q.
958 |Qpos r \Rightarrow Z_of_nat (numQ (Qpos r))
959 |Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r))
962 theorem Qfrac_Z_of_nat: \forall n,m.
963 Qfrac (Z_of_nat n) m = frac n m.
964 intros.cases n;reflexivity.
967 theorem Qfrac_neg_Z_of_nat: \forall n,m.
968 Qfrac (neg_Z_of_nat n) m = Qopp (frac n m).
969 intros.cases n;reflexivity.
972 theorem Qfrac_QnumZ_denomQ: \forall q.
973 Qfrac (QnumZ q) (denomQ q) = q.
978 (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r).
979 rewrite > Qfrac_Z_of_nat.
980 apply frac_numQ_denomQ1.
981 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2