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 (**************************************************************************)
15 set "baseuri" "cic:/matita/Q/frac".
17 include "nat/factorization.ma".
21 definition numeratorQ \def
22 \lambda q.match q with
23 [OQ \Rightarrow nfa_zero
26 [one \Rightarrow nfa_one
27 |frac x \Rightarrow numerator x
31 [one \Rightarrow nfa_one
32 |frac x \Rightarrow numerator x
37 definition nat_fact_all_to_Q \def
40 [nfa_zero \Rightarrow OQ
41 |nfa_one \Rightarrow Qpos one
42 |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction l))
46 theorem numeratorQ_nat_fact_all_to_Q: \forall g.
47 numeratorQ (nat_fact_all_to_Q g) = g.
51 |apply numerator_nat_fact_to_fraction
55 definition nat_to_Q \def
56 \lambda n. nat_fact_all_to_Q (factorize n).
58 let rec nat_fact_to_fraction_inv l \def
60 [nf_last a \Rightarrow nn a
61 |nf_cons a p \Rightarrow
62 cons (neg_Z_of_nat a) (nat_fact_to_fraction_inv p)
68 definition nat_fact_all_to_Q_inv \def
71 [nfa_zero \Rightarrow OQ
72 |nfa_one \Rightarrow Qpos one
73 |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction_inv l))
77 definition nat_to_Q_inv \def
78 \lambda n. nat_fact_all_to_Q_inv (factorize n).
82 \lambda q.match q with
84 |Qpos r \Rightarrow Qpos (rinv r)
85 |Qneg r \Rightarrow Qneg (rinv r)
88 definition frac:nat \to nat \to Q \def
89 \lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
91 theorem rtimes_oner: \forall r.rtimes r one = r.
92 intro.cases r;reflexivity.
95 theorem rtimes_onel: \forall r.rtimes one r = r.
96 intro.cases r;reflexivity.
99 definition Qone \def Qpos one.
101 theorem Qtimes_Qoner: \forall q.Qtimes q Qone = q.
115 theorem Qtimes_Qonel: \forall q.Qtimes Qone q = q.
129 let rec times_f h g \def
131 [nf_last a \Rightarrow
133 [nf_last b \Rightarrow nf_last (S (a+b))
134 |nf_cons b g1 \Rightarrow nf_cons (S (a+b)) g1
136 |nf_cons a h1 \Rightarrow
138 [nf_last b \Rightarrow nf_cons (S (a+b)) h1
139 |nf_cons b g1 \Rightarrow nf_cons (a+b) (times_f h1 g1)
144 definition times_fa \def
147 [nfa_zero \Rightarrow nfa_zero
148 |nfa_one \Rightarrow g
149 |nfa_proper f1 \Rightarrow match g with
150 [nfa_zero \Rightarrow nfa_zero
151 |nfa_one \Rightarrow nfa_proper f1
152 |nfa_proper g1 \Rightarrow nfa_proper (times_f f1 g1)
157 theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
158 =defactorize_aux g m*defactorize_aux h m.
160 [elim h;simplify;autobatch
163 |simplify.rewrite > (H n3 (S m)).autobatch
168 theorem eq_times_fa_times: \forall f,g.
169 defactorize (times_fa f g) = defactorize f*defactorize g.
173 |simplify.apply plus_n_O
177 |apply eq_times_f_times1
182 theorem eq_times_times_fa: \forall n,m.
183 factorize (n*m) = times_fa (factorize n) (factorize m).
185 rewrite <(factorize_defactorize (times_fa (factorize n) (factorize m))).
186 rewrite > eq_times_fa_times.
187 rewrite > defactorize_factorize.
188 rewrite > defactorize_factorize.
193 theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
194 Z_of_nat n + Z_of_nat m.
198 [simplify.rewrite < plus_n_O.reflexivity
199 |simplify.reflexivity.
204 definition unfrac \def \lambda f.
206 [one \Rightarrow pp O
207 |frac f \Rightarrow f
211 lemma injective_frac: injective fraction ratio frac.
213 change with ((unfrac (frac x)) = (unfrac (frac y))).
214 rewrite < H.reflexivity.
217 theorem times_f_ftimes: \forall n,m.
218 frac (nat_fact_to_fraction (times_f n m))
219 = ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m).
224 rewrite < plus_n_Sm.reflexivity
226 [simplify.rewrite < plus_n_O.reflexivity
227 |simplify.reflexivity.
232 [simplify.reflexivity
233 |simplify.rewrite < plus_n_Sm.reflexivity
236 cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h)
242 |apply injective_frac.
246 |generalize in match n4.
248 [cases n6;simplify;autobatch
262 theorem times_fa_Qtimes: \forall f,g. nat_fact_all_to_Q (times_fa f g) =
263 Qtimes (nat_fact_all_to_Q f) (nat_fact_all_to_Q g).
271 |rewrite > times_f_ftimes.reflexivity
276 theorem times_Qtimes: \forall p,q.
277 (nat_to_Q (p*q)) = Qtimes (nat_to_Q p) (nat_to_Q q).
278 intros.unfold nat_to_Q.
279 rewrite < times_fa_Qtimes.
280 rewrite < eq_times_times_fa.
284 theorem rtimes_Zplus: \forall x,y.
285 rtimes (Z_to_ratio x) (Z_to_ratio y) =
295 theorem rtimes_Zplus1: \forall x,y,f.
296 rtimes (Z_to_ratio x) (frac (cons y f)) =
297 frac (cons ((x + y)) f).
306 theorem rtimes_Zplus2: \forall x,y,f.
307 rtimes (frac (cons y f)) (Z_to_ratio x) =
308 frac (cons ((y + x)) f).
317 theorem or_one_frac: \forall f,g.
318 rtimes (frac f) (frac g) = one \lor
319 \exists h.rtimes (frac f) (frac g) = frac h.
321 elim (rtimes (frac f) (frac g))
323 |right.apply (ex_intro ? ? f1).reflexivity
327 theorem one_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
328 rtimes (frac f) (frac g) = one \to
329 rtimes (frac (cons x f)) (frac (cons y g)) = Z_to_ratio (x + y).
330 intros.simplify.simplify in H.rewrite > H.simplify.
334 theorem frac_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
335 \forall h.rtimes (frac f) (frac g) = frac h \to
336 rtimes (frac (cons x f)) (frac (cons y g)) = frac (cons (x + y) h).
337 intros.simplify.simplify in H.rewrite > H.simplify.
341 theorem rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
342 (rtimes (frac f) (frac g) = one \land
343 rtimes (frac (cons x f)) (frac (cons y g)) = Z_to_ratio (x + y))
344 \lor (\exists h.rtimes (frac f) (frac g) = frac h \land
345 rtimes (frac (cons x f)) (frac (cons y g)) =
346 frac (cons (x + y) h)).
349 elim (rtimes (frac f) (frac g));simplify
350 [left.split;reflexivity
352 apply (ex_intro ? ? f1).
357 theorem Z_to_ratio_frac_frac: \forall z,f1,f2.
358 rtimes (rtimes (Z_to_ratio z) (frac f1)) (frac f2)
359 =rtimes (Z_to_ratio z) (rtimes (frac f1) (frac f2)).
363 (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1))
364 =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))).
365 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
366 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
367 rewrite > assoc_Zplus.reflexivity
369 (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (neg n1))
370 =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (neg n1)))).
371 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
372 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
373 rewrite > assoc_Zplus.reflexivity
375 (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (frac (cons z1 f))
376 = rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (frac (cons z1 f)))).
377 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
378 rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
379 rewrite > assoc_Zplus.reflexivity
383 (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (Z_to_ratio (pos n1))
384 =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (pos n1)))).
385 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
386 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
387 rewrite > assoc_Zplus.reflexivity
389 (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (Z_to_ratio (neg n1))
390 =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (neg n1)))).
391 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
392 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
393 rewrite > assoc_Zplus.reflexivity
395 (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (frac (cons z1 f))
396 = rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (frac (cons z1 f)))).
397 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
398 rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
399 rewrite > assoc_Zplus.reflexivity
403 (rtimes (rtimes (Z_to_ratio z) (frac (cons z1 f))) (Z_to_ratio (pos n))
404 =rtimes (Z_to_ratio z) (rtimes (frac (cons z1 f)) (Z_to_ratio (pos n)))).
405 rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
406 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
407 rewrite > assoc_Zplus.reflexivity
409 (rtimes (rtimes (Z_to_ratio z) (frac (cons z1 f))) (Z_to_ratio (neg n))
410 =rtimes (Z_to_ratio z) (rtimes (frac (cons z1 f)) (Z_to_ratio (neg n)))).
411 rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
412 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
413 rewrite > assoc_Zplus.reflexivity
414 |elim (or_one_frac f f3)
415 [rewrite > rtimes_Zplus1.
416 rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
417 rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
418 rewrite > rtimes_Zplus.
419 rewrite > assoc_Zplus.reflexivity
421 rewrite > rtimes_Zplus1.
422 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
423 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
424 rewrite > rtimes_Zplus1.
425 rewrite > assoc_Zplus.reflexivity
431 theorem cons_frac_frac: \forall f1,z,f,f2.
432 rtimes (rtimes (frac (cons z f)) (frac f1)) (frac f2)
433 =rtimes (frac (cons z f)) (rtimes (frac f1) (frac f2)).
437 (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1))
438 =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))).
439 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
440 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
441 rewrite > assoc_Zplus.reflexivity
443 (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (Z_to_ratio (neg n1))
444 =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (neg n1)))).
445 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
446 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
447 rewrite > assoc_Zplus.reflexivity
449 (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (frac (cons z1 f3))
450 = rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (frac (cons z1 f3)))).
451 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
452 elim (or_one_frac f f3)
453 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
454 rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
455 rewrite > assoc_Zplus.reflexivity
457 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
458 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
459 rewrite > assoc_Zplus.reflexivity
464 (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (Z_to_ratio (pos n1))
465 =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (pos n1)))).
466 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
467 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
468 rewrite > assoc_Zplus.reflexivity
470 (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (Z_to_ratio (neg n1))
471 =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (neg n1)))).
472 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
473 rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
474 rewrite > assoc_Zplus.reflexivity
476 (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (frac (cons z1 f3))
477 = rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (frac (cons z1 f3)))).
478 rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
479 elim (or_one_frac f f3)
480 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
481 rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
482 rewrite > assoc_Zplus.reflexivity
484 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
485 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
486 rewrite > assoc_Zplus.reflexivity
491 (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (Z_to_ratio (pos n))
492 =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (Z_to_ratio (pos n)))).
493 rewrite > rtimes_Zplus2.
494 elim (or_one_frac f2 f)
495 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
496 rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
497 rewrite > rtimes_Zplus.
498 rewrite > assoc_Zplus.reflexivity
500 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
501 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
502 rewrite > rtimes_Zplus2.
503 rewrite > assoc_Zplus.reflexivity
506 (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (Z_to_ratio (neg n))
507 =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (Z_to_ratio (neg n)))).
508 rewrite > rtimes_Zplus2.
509 elim (or_one_frac f2 f)
510 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
511 rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
512 rewrite > rtimes_Zplus.
513 rewrite > assoc_Zplus.reflexivity
515 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
516 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
517 rewrite > rtimes_Zplus2.
518 rewrite > assoc_Zplus.reflexivity
520 |elim (or_one_frac f2 f)
521 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
522 rewrite > rtimes_Zplus1.
523 elim (or_one_frac f f4)
524 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H3).
525 rewrite > rtimes_Zplus2.
528 rewrite > assoc_Zplus.reflexivity
529 |apply injective_frac.
530 rewrite < rtimes_onel.
532 (* problema inaspettato: mi serve l'unicita' dell'inversa,
533 che richiede (?) l'associativita. Per fortuna basta
534 l'ipotesi induttiva. *)
537 (rtimes (rtimes (Z_to_ratio (pos n)) (frac f)) (frac f4)=Z_to_ratio (pos n)).
538 rewrite > Z_to_ratio_frac_frac.
540 rewrite > rtimes_oner.
543 (rtimes (rtimes (Z_to_ratio (neg n)) (frac f)) (frac f4)=Z_to_ratio (neg n)).
544 rewrite > Z_to_ratio_frac_frac.
546 rewrite > rtimes_oner.
550 rewrite > rtimes_oner.
555 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H4).
556 cut (rtimes (frac f2) (frac a) = frac f4)
557 [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f4 Hcut).
558 rewrite > assoc_Zplus.reflexivity
560 generalize in match H2.
563 (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) =frac f4).
564 rewrite < Z_to_ratio_frac_frac.
566 rewrite > rtimes_onel.
569 (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) =frac f4).
570 rewrite < Z_to_ratio_frac_frac.
572 rewrite > rtimes_onel.
576 rewrite > rtimes_onel.
582 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
583 elim (or_one_frac f f4)
584 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
585 rewrite > rtimes_Zplus2.
586 cut (rtimes (frac a) (frac f4) = frac f2)
587 [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f2 Hcut).
588 rewrite > assoc_Zplus.reflexivity
590 generalize in match H2.
593 (rtimes (rtimes (Z_to_ratio (pos n)) (frac f)) (frac f4)=Z_to_ratio (pos n)).
594 rewrite > Z_to_ratio_frac_frac.
596 rewrite > rtimes_oner.
599 (rtimes (rtimes (Z_to_ratio (neg n)) (frac f)) (frac f4)=Z_to_ratio (neg n)).
600 rewrite > Z_to_ratio_frac_frac.
602 rewrite > rtimes_oner.
606 rewrite > rtimes_oner.
611 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a1 H4).
612 elim (or_one_frac a f4)
613 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
614 cut (rtimes (frac f2) (frac a1) = one)
615 [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? Hcut).
616 rewrite > assoc_Zplus.reflexivity
618 generalize in match H3.
621 (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = one).
622 rewrite < Z_to_ratio_frac_frac.
626 (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = one).
627 rewrite < Z_to_ratio_frac_frac.
636 rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 H5).
637 cut (rtimes (frac f2) (frac a1) = frac a2)
638 [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 Hcut).
639 rewrite > assoc_Zplus.reflexivity
641 generalize in match H3.
644 (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = frac a2).
645 rewrite < Z_to_ratio_frac_frac.
649 (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = frac a2).
650 rewrite < Z_to_ratio_frac_frac.
665 theorem frac_frac_fracaux: \forall f,f1,f2.
666 rtimes (rtimes (frac f) (frac f1)) (frac f2)
667 =rtimes (frac f) (rtimes (frac f1) (frac f2)).
671 (rtimes (rtimes (Z_to_ratio (pos n)) (frac f1)) (frac f2)
672 =rtimes (Z_to_ratio (pos n)) (rtimes (frac f1) (frac f2))).
673 apply Z_to_ratio_frac_frac
675 (rtimes (rtimes (Z_to_ratio (neg n)) (frac f1)) (frac f2)
676 =rtimes (Z_to_ratio (neg n)) (rtimes (frac f1) (frac f2))).
677 apply Z_to_ratio_frac_frac
678 |apply cons_frac_frac
682 theorem associative_rtimes:associative ? rtimes.
689 [rewrite > rtimes_oner.rewrite > rtimes_oner.reflexivity
690 |apply frac_frac_fracaux
696 theorem associative_Qtimes:associative ? Qtimes.
700 (* non posso scrivere 2,3: ... ?? *)
705 |simplify.rewrite > associative_rtimes.
707 |simplify.rewrite > associative_rtimes.
712 |simplify.rewrite > associative_rtimes.
714 |simplify.rewrite > associative_rtimes.
722 |simplify.rewrite > associative_rtimes.
724 |simplify.rewrite > associative_rtimes.
729 |simplify.rewrite > associative_rtimes.
731 |simplify.rewrite > associative_rtimes.
738 theorem Qtimes_OQ: \forall q.Qtimes q OQ = OQ.
739 intro.cases q;reflexivity.
742 theorem symmetric_Qtimes: symmetric ? Qtimes.
745 [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity
748 |simplify.alias id "symmetric_rtimes" = "cic:/matita/Q/times/symmetric_rtimes.con".
749 rewrite > symmetric_rtimes.reflexivity
750 |simplify.rewrite > symmetric_rtimes.reflexivity
754 |simplify.rewrite > symmetric_rtimes.reflexivity
755 |simplify.rewrite > symmetric_rtimes.reflexivity
760 theorem Qtimes_Qinv: \forall q. q \neq OQ \to Qtimes q (Qinv q) = Qone.
764 |simplify.alias id "rtimes_rinv" = "cic:/matita/Q/times/rtimes_rinv.con".
765 rewrite > rtimes_rinv.reflexivity
766 |simplify.rewrite > rtimes_rinv.reflexivity
770 theorem eq_Qtimes_OQ_to_eq_OQ: \forall p,q.
771 Qtimes p q = OQ \to p = OQ \lor q = OQ.
774 [intro.left.reflexivity
776 [intro.right.reflexivity
777 |simplify.intro.destruct H
778 |simplify.intro.destruct H
781 [intro.right.reflexivity
782 |simplify.intro.destruct H
783 |simplify.intro.destruct H
788 theorem Qinv_Qtimes: \forall p,q.
789 p \neq OQ \to q \neq OQ \to
791 Qtimes (Qinv p) (Qinv q).
793 rewrite < Qtimes_Qonel in ⊢ (? ? ? %).
794 rewrite < (Qtimes_Qinv (Qtimes p q))
795 [lapply (Qtimes_Qinv ? H).
796 lapply (Qtimes_Qinv ? H1).
797 rewrite > symmetric_Qtimes in ⊢ (? ? ? (? % ?)).
798 rewrite > associative_Qtimes.
799 rewrite > associative_Qtimes.
800 rewrite < associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
801 rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
802 rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
804 rewrite > Qtimes_Qoner.
806 rewrite > Qtimes_Qoner.
809 elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
810 [apply (H H3)|apply (H1 H3)]
814 (* a stronger version, taking advantage of inv(O) = O *)
815 theorem Qinv_Qtimes': \forall p,q.
817 Qtimes (Qinv p) (Qinv q).
823 |apply Qinv_Qtimes;intro;destruct H
824 |apply Qinv_Qtimes;intro;destruct H
828 |apply Qinv_Qtimes;intro;destruct H
829 |apply Qinv_Qtimes;intro;destruct H
834 theorem Qtimes_frac_frac: \forall p,q,r,s.
835 Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)).
838 rewrite > associative_Qtimes.
839 rewrite < associative_Qtimes in ⊢ (? ? (? ? %) ?).
840 rewrite > symmetric_Qtimes in ⊢ (? ? (? ? (? % ?)) ?).
841 rewrite > associative_Qtimes in ⊢ (? ? (? ? %) ?).
842 rewrite < associative_Qtimes.
843 rewrite < times_Qtimes.
844 rewrite < Qinv_Qtimes'.
845 rewrite < times_Qtimes.
850 (* la prova seguente e' tutta una ripetizione. Sistemare. *)
852 theorem Qtimes1: \forall f:fraction.
853 Qtimes (nat_fact_all_to_Q (numerator f))
854 (Qinv (nat_fact_all_to_Q (numerator (finv f))))
860 |elim (or_numerator_nfa_one_nfa_proper f1)
863 cut (finv (nat_fact_to_fraction a) = f1)
866 rewrite > H2.rewrite > H1.simplify.
867 rewrite > Hcut.reflexivity
869 rewrite > H2.rewrite > H1.simplify.
870 rewrite > Hcut.reflexivity
872 rewrite > H2.rewrite > H1.simplify.
873 rewrite > Hcut.reflexivity
875 |generalize in match H.
876 rewrite > H2.rewrite > H1.simplify.
877 intro.destruct H3.assumption
882 rewrite > H2.rewrite > H2.simplify.
883 elim (or_numerator_nfa_one_nfa_proper (finv f1))
885 rewrite > H3.simplify.
886 cut (nat_fact_to_fraction a = f1)
887 [rewrite > Hcut.reflexivity
888 |generalize in match H.
891 rewrite > Qtimes_Qoner.
897 generalize in match H.
899 rewrite > H3.simplify.
905 |simplify.rewrite > H2.simplify.
906 elim (or_numerator_nfa_one_nfa_proper (finv f1))
908 rewrite > H3.simplify.
909 cut (nat_fact_to_fraction a = f1)
910 [rewrite > Hcut.reflexivity
911 |generalize in match H.
914 rewrite > Qtimes_Qoner.
920 generalize in match H.
922 rewrite > H3.simplify.
928 |simplify.rewrite > H2.simplify.
929 elim (or_numerator_nfa_one_nfa_proper (finv f1))
931 rewrite > H3.simplify.
932 cut (nat_fact_to_fraction a = f1)
933 [rewrite > Hcut.reflexivity
934 |generalize in match H.
937 rewrite > Qtimes_Qoner.
943 generalize in match H.
945 rewrite > H3.simplify.
957 definition numQ:Q \to Z \def
961 |Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r)))
962 |Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r)))
966 definition numQ:Q \to nat \def
967 \lambda q. defactorize (numeratorQ q).
969 definition denomQ:Q \to nat \def
970 \lambda q. defactorize (numeratorQ (Qinv q)).
972 definition Qopp:Q \to Q \def \lambda q.
975 |Qpos q \Rightarrow Qneg q
976 |Qneg q \Rightarrow Qpos q
979 theorem frac_numQ_denomQ1: \forall r:ratio.
980 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
982 unfold frac.unfold denomQ.unfold numQ.
984 rewrite > factorize_defactorize.
985 rewrite > factorize_defactorize.
997 theorem frac_numQ_denomQ2: \forall r:ratio.
998 frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
1000 unfold frac.unfold denomQ.unfold numQ.
1002 rewrite > factorize_defactorize.
1003 rewrite > factorize_defactorize.
1014 definition Qabs:Q \to Q \def \lambda q.
1017 |Qpos q \Rightarrow Qpos q
1018 |Qneg q \Rightarrow Qpos q
1021 theorem frac_numQ_denomQ: \forall q.
1022 frac (numQ q) (denomQ q) = (Qabs q).
1026 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
1027 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
1031 definition Qfrac: Z \to nat \to Q \def
1032 \lambda z,n.match z with
1034 |Zpos m \Rightarrow (frac (S m) n)
1035 |Zneg m \Rightarrow Qopp (frac (S m) n)
1038 definition QnumZ \def \lambda q.
1041 |Qpos r \Rightarrow Z_of_nat (numQ (Qpos r))
1042 |Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r))
1045 theorem Qfrac_Z_of_nat: \forall n,m.
1046 Qfrac (Z_of_nat n) m = frac n m.
1047 intros.cases n;reflexivity.
1050 theorem Qfrac_neg_Z_of_nat: \forall n,m.
1051 Qfrac (neg_Z_of_nat n) m = Qopp (frac n m).
1052 intros.cases n;reflexivity.
1055 theorem Qfrac_QnumZ_denomQ: \forall q.
1056 Qfrac (QnumZ q) (denomQ q) = q.
1061 (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r).
1062 rewrite > Qfrac_Z_of_nat.
1063 apply frac_numQ_denomQ1.
1064 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2