From: Andrea Asperti Date: Fri, 6 Jun 2008 09:20:29 +0000 (+0000) Subject: Added frac.ma X-Git-Tag: make_still_working~5078 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3a43b5be5e112404f79a6b8b5dab07e91f2467f2;p=helm.git Added frac.ma --- diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma new file mode 100644 index 000000000..b5871dc94 --- /dev/null +++ b/helm/software/matita/library/Q/frac.ma @@ -0,0 +1,1193 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/Q/frac". + +include "nat/factorization.ma". +include "Q/q.ma". + +(* transformation from nat_fact to fracion *) +let rec nat_fact_to_fraction l \def + match l with + [nf_last a \Rightarrow pp a + |nf_cons a p \Rightarrow + cons (Z_of_nat a) (nat_fact_to_fraction p) + ] +. + +(* returns the numerator of a fraction in the form of a nat_fact_all *) +let rec numerator f \def + match f with + [pp a \Rightarrow nfa_proper (nf_last a) + |nn a \Rightarrow nfa_one + |cons a l \Rightarrow + let n \def numerator l in + match n with + [nfa_zero \Rightarrow (* this case is vacuous *) nfa_zero + |nfa_one \Rightarrow + match a with + [OZ \Rightarrow nfa_one + |pos x \Rightarrow nfa_proper (nf_last x) + |neg x \Rightarrow nfa_one + ] + |nfa_proper g \Rightarrow + match a with + [OZ \Rightarrow nfa_proper (nf_cons O g) + |pos x \Rightarrow nfa_proper (nf_cons (S x) g) + |neg x \Rightarrow nfa_proper (nf_cons O g) + ] + ] + ] +. + +theorem not_eq_numerator_nfa_zero: +\forall f.numerator f \neq nfa_zero. +intro.elim f + [simplify.intro.destruct H + |simplify.intro.destruct H + |simplify.generalize in match H. + cases (numerator f1) + [intro.elim H1.reflexivity + |simplify.intro. + cases z;simplify;intro;destruct H2 + |simplify.intro. + cases z;simplify;intro;destruct H2 + ] + ] +qed. + +theorem or_numerator_nfa_one_nfa_proper: +\forall f.(numerator f = nfa_one \land \exists g.numerator (finv f) = +nfa_proper g) \lor \exists g.numerator f = nfa_proper g. +intro.elim f + [simplify.right. + apply (ex_intro ? ? (nf_last n)).reflexivity + |simplify.left.split + [reflexivity + |apply (ex_intro ? ? (nf_last n)).reflexivity + ] + |elim H;clear H + [elim H1.clear H1. + elim H2.clear H2. + elim z + [simplify. + rewrite > H.rewrite > H1.simplify. + left.split + [reflexivity + |apply (ex_intro ? ? (nf_cons O a)).reflexivity + ] + |simplify. + rewrite > H.rewrite > H1.simplify. + right.apply (ex_intro ? ? (nf_last n)).reflexivity + |simplify. + rewrite > H.rewrite > H1.simplify. + left.split + [reflexivity + |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity + ] + ] + |elim H1.clear H1. + elim z + [simplify. + rewrite > H.simplify. + right. + apply (ex_intro ? ? (nf_cons O a)).reflexivity + |simplify. + rewrite > H.simplify. + right.apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity + |simplify. + rewrite > H.simplify. + right. + apply (ex_intro ? ? (nf_cons O a)).reflexivity + ] + ] + ] +qed. + +theorem eq_nfa_one_to_eq_finv_nfa_proper: +\forall f.numerator f = nfa_one \to +\exist h.numerator (finv f) = nfa_proper h. +intro.elim f + [simplify in H.destruct H + |simplify.apply (ex_intro ? ? (nf_last n)).reflexivity + |generalize in match H1.clear H1. + generalize in match H.clear H. + simplify. + cases (numerator f1);simplify + [intros;destruct H1 + |intros;elim (H (refl_eq ? ?)). + rewrite > H2.simplify. + elim z;simplify + [apply (ex_intro ? ? (nf_cons O a)).reflexivity + |apply (ex_intro ? ? (nf_cons O a)).reflexivity + |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity + ] + |elim z;destruct H1 + ] + ] +qed. + +theorem numerator_nat_fact_to_fraction: \forall g:nat_fact. +numerator (nat_fact_to_fraction g) = nfa_proper g. +intro. +elim g + [simplify.reflexivity. + |simplify.rewrite > H.simplify. + cases n;reflexivity + ] +qed. + +definition numeratorQ \def +\lambda q.match q with + [OQ \Rightarrow nfa_zero + |pos r \Rightarrow + match r with + [one \Rightarrow nfa_one + |frac x \Rightarrow numerator x + ] + |neg r \Rightarrow + match r with + [one \Rightarrow nfa_one + |frac x \Rightarrow numerator x + ] + ] +. + +definition nat_fact_all_to_Q \def +\lambda n. + match n with + [nfa_zero \Rightarrow OQ + |nfa_one \Rightarrow Qpos one + |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction l)) + ] +. + +theorem numeratorQ_nat_fact_all_to_Q: \forall g. +numeratorQ (nat_fact_all_to_Q g) = g. +intro.cases g + [reflexivity + |reflexivity + |apply numerator_nat_fact_to_fraction + ] +qed. + +definition nat_to_Q \def +\lambda n. nat_fact_all_to_Q (factorize n). + +let rec nat_fact_to_fraction_inv l \def + match l with + [nf_last a \Rightarrow nn a + |nf_cons a p \Rightarrow + cons (neg_Z_of_nat a) (nat_fact_to_fraction_inv p) + ] +. + +(* +definition nat_fact_all_to_Q_inv \def +\lambda n. + match n with + [nfa_zero \Rightarrow OQ + |nfa_one \Rightarrow Qpos one + |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction_inv l)) + ] +. + +definition nat_to_Q_inv \def +\lambda n. nat_fact_all_to_Q_inv (factorize n). +*) + +definition Qinv \def +\lambda q.match q with +[OQ \Rightarrow OQ +|Qpos r \Rightarrow Qpos (rinv r) +|Qneg r \Rightarrow Qneg (rinv r) +]. + +definition frac:nat \to nat \to Q \def +\lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)). + +theorem rtimes_oner: \forall r.rtimes r one = r. +intro.cases r;reflexivity. +qed. + +theorem rtimes_onel: \forall r.rtimes one r = r. +intro.cases r;reflexivity. +qed. + +definition Qone \def Qpos one. + +theorem Qtimes_Qoner: \forall q.Qtimes q Qone = q. +intro.cases q + [reflexivity + |cases r + [reflexivity + |reflexivity + ] + |cases r + [reflexivity + |reflexivity + ] + ] +qed. + +theorem Qtimes_Qonel: \forall q.Qtimes Qone q = q. +intros.cases q + [reflexivity + |cases r + [reflexivity + |reflexivity + ] + |cases r + [reflexivity + |reflexivity + ] + ] +qed. + +let rec times_f h g \def + match h with + [nf_last a \Rightarrow + match g with + [nf_last b \Rightarrow nf_last (S (a+b)) + |nf_cons b g1 \Rightarrow nf_cons (S (a+b)) g1 + ] + |nf_cons a h1 \Rightarrow + match g with + [nf_last b \Rightarrow nf_cons (S (a+b)) h1 + |nf_cons b g1 \Rightarrow nf_cons (a+b) (times_f h1 g1) + ] + ] +. + +definition times_fa \def +\lambda f,g. +match f with +[nfa_zero \Rightarrow nfa_zero +|nfa_one \Rightarrow g +|nfa_proper f1 \Rightarrow match g with + [nfa_zero \Rightarrow nfa_zero + |nfa_one \Rightarrow nfa_proper f1 + |nfa_proper g1 \Rightarrow nfa_proper (times_f f1 g1) + ] +] +. + +theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m +=defactorize_aux g m*defactorize_aux h m. +intro.elim g + [elim h;simplify;autobatch + |elim h + [simplify;autobatch + |simplify.rewrite > (H n3 (S m)).autobatch + ] + ] +qed. + +theorem eq_times_fa_times: \forall f,g. +defactorize (times_fa f g) = defactorize f*defactorize g. +intros. +elim f + [reflexivity + |simplify.apply plus_n_O + |elim g;simplify + [apply times_n_O + |apply times_n_SO + |apply eq_times_f_times1 + ] + ] +qed. + +theorem eq_times_times_fa: \forall n,m. +factorize (n*m) = times_fa (factorize n) (factorize m). +intros. +rewrite <(factorize_defactorize (times_fa (factorize n) (factorize m))). +rewrite > eq_times_fa_times. +rewrite > defactorize_factorize. +rewrite > defactorize_factorize. +reflexivity. +qed. + + +theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) = +Z_of_nat n + Z_of_nat m. +intro.cases n;intro + [reflexivity + |cases m + [simplify.rewrite < plus_n_O.reflexivity + |simplify.reflexivity. + ] + ] +qed. + +definition unfrac \def \lambda f. +match f with + [one \Rightarrow pp O + |frac f \Rightarrow f + ] +. + +lemma injective_frac: injective fraction ratio frac. +unfold.intros. +change with ((unfrac (frac x)) = (unfrac (frac y))). +rewrite < H.reflexivity. +qed. + +theorem times_f_ftimes: \forall n,m. +frac (nat_fact_to_fraction (times_f n m)) += ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m). +intro. +elim n + [elim m + [simplify. + rewrite < plus_n_Sm.reflexivity + |elim n2 + [simplify.rewrite < plus_n_O.reflexivity + |simplify.reflexivity. + ] + ] + |elim m + [elim n1 + [simplify.reflexivity + |simplify.rewrite < plus_n_Sm.reflexivity + ] + |simplify. + cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h) + [elim Hcut. + rewrite > H2. + simplify.apply eq_f. + apply eq_f2 + [apply eq_plus_Zplus + |apply injective_frac. + rewrite < H2. + apply H + ] + |generalize in match n4. + elim n2 + [cases n6;simplify;autobatch + |cases n7;simplify + [autobatch + |elim (H2 n9). + rewrite > H3. + simplify. + autobatch + ] + ] + ] + ] + ] +qed. + +theorem times_fa_Qtimes: \forall f,g. nat_fact_all_to_Q (times_fa f g) = +Qtimes (nat_fact_all_to_Q f) (nat_fact_all_to_Q g). +intros. +cases f;simplify + [reflexivity + |cases g;reflexivity + |cases g;simplify + [reflexivity + |reflexivity + |rewrite > times_f_ftimes.reflexivity + ] + ] +qed. + +theorem times_Qtimes: \forall p,q. +(nat_to_Q (p*q)) = Qtimes (nat_to_Q p) (nat_to_Q q). +intros.unfold nat_to_Q. +rewrite < times_fa_Qtimes. +rewrite < eq_times_times_fa. +reflexivity. +qed. + +theorem rtimes_Zplus: \forall x,y. +rtimes (Z_to_ratio x) (Z_to_ratio y) = +Z_to_ratio (x + y). +intro. +elim x + [reflexivity + |elim y;reflexivity + |elim y;reflexivity + ] +qed. + +theorem rtimes_Zplus1: \forall x,y,f. +rtimes (Z_to_ratio x) (frac (cons y f)) = +frac (cons ((x + y)) f). +intro. +elim x + [reflexivity + |elim y;reflexivity + |elim y;reflexivity + ] +qed. + +theorem rtimes_Zplus2: \forall x,y,f. +rtimes (frac (cons y f)) (Z_to_ratio x) = +frac (cons ((y + x)) f). +intros. +elim x + [elim y;reflexivity + |elim y;reflexivity + |elim y;reflexivity + ] +qed. + +theorem or_one_frac: \forall f,g. +rtimes (frac f) (frac g) = one \lor +\exists h.rtimes (frac f) (frac g) = frac h. +intros. +elim (rtimes (frac f) (frac g)) + [left.reflexivity + |right.apply (ex_intro ? ? f1).reflexivity + ] +qed. + +theorem one_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction. +rtimes (frac f) (frac g) = one \to +rtimes (frac (cons x f)) (frac (cons y g)) = Z_to_ratio (x + y). +intros.simplify.simplify in H.rewrite > H.simplify. +reflexivity. +qed. + +theorem frac_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction. +\forall h.rtimes (frac f) (frac g) = frac h \to +rtimes (frac (cons x f)) (frac (cons y g)) = frac (cons (x + y) h). +intros.simplify.simplify in H.rewrite > H.simplify. +reflexivity. +qed. + +theorem rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction. +(rtimes (frac f) (frac g) = one \land + rtimes (frac (cons x f)) (frac (cons y g)) = Z_to_ratio (x + y)) +\lor (\exists h.rtimes (frac f) (frac g) = frac h \land +rtimes (frac (cons x f)) (frac (cons y g)) = +frac (cons (x + y) h)). +intros. +simplify. +elim (rtimes (frac f) (frac g));simplify + [left.split;reflexivity + |right. + apply (ex_intro ? ? f1). + split;reflexivity + ] +qed. + +theorem Z_to_ratio_frac_frac: \forall z,f1,f2. +rtimes (rtimes (Z_to_ratio z) (frac f1)) (frac f2) +=rtimes (Z_to_ratio z) (rtimes (frac f1) (frac f2)). +intros 2.elim f1 + [elim f2 + [change with + (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1)) + =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))). + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (neg n1)) + =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (neg n1)))). + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (frac (cons z1 f)) + = rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (frac (cons z1 f)))). + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1. + rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1. + rewrite > assoc_Zplus.reflexivity + ] + |elim f2 + [change with + (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (Z_to_ratio (pos n1)) + =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (pos n1)))). + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (Z_to_ratio (neg n1)) + =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (neg n1)))). + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (frac (cons z1 f)) + = rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (frac (cons z1 f)))). + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1. + rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1. + rewrite > assoc_Zplus.reflexivity + ] + |elim f2 + [change with + (rtimes (rtimes (Z_to_ratio z) (frac (cons z1 f))) (Z_to_ratio (pos n)) + =rtimes (Z_to_ratio z) (rtimes (frac (cons z1 f)) (Z_to_ratio (pos n)))). + rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2. + rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (Z_to_ratio z) (frac (cons z1 f))) (Z_to_ratio (neg n)) + =rtimes (Z_to_ratio z) (rtimes (frac (cons z1 f)) (Z_to_ratio (neg n)))). + rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2. + rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1. + rewrite > assoc_Zplus.reflexivity + |elim (or_one_frac f f3) + [rewrite > rtimes_Zplus1. + rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2). + rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2). + rewrite > rtimes_Zplus. + rewrite > assoc_Zplus.reflexivity + |elim H2.clear H2. + rewrite > rtimes_Zplus1. + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3). + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3). + rewrite > rtimes_Zplus1. + rewrite > assoc_Zplus.reflexivity + ] + ] + ] +qed. + +theorem cons_frac_frac: \forall f1,z,f,f2. +rtimes (rtimes (frac (cons z f)) (frac f1)) (frac f2) +=rtimes (frac (cons z f)) (rtimes (frac f1) (frac f2)). +intro.elim f1 + [elim f2 + [change with + (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1)) + =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))). + rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2. + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (Z_to_ratio (neg n1)) + =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (neg n1)))). + rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2. + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (frac (cons z1 f3)) + = rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (frac (cons z1 f3)))). + rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1. + elim (or_one_frac f f3) + [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1). + rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1). + rewrite > assoc_Zplus.reflexivity + |elim H1.clear H1. + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2). + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2). + rewrite > assoc_Zplus.reflexivity + ] + ] + |elim f2 + [change with + (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (Z_to_ratio (pos n1)) + =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (pos n1)))). + rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2. + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (Z_to_ratio (neg n1)) + =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (neg n1)))). + rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2. + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (frac (cons z1 f3)) + = rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (frac (cons z1 f3)))). + rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1. + elim (or_one_frac f f3) + [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1). + rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1). + rewrite > assoc_Zplus.reflexivity + |elim H1.clear H1. + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2). + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2). + rewrite > assoc_Zplus.reflexivity + ] + ] + |elim f3 + [change with + (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (Z_to_ratio (pos n)) + =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (Z_to_ratio (pos n)))). + rewrite > rtimes_Zplus2. + elim (or_one_frac f2 f) + [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1). + rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1). + rewrite > rtimes_Zplus. + rewrite > assoc_Zplus.reflexivity + |elim H1.clear H1. + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2). + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2). + rewrite > rtimes_Zplus2. + rewrite > assoc_Zplus.reflexivity + ] + |change with + (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (Z_to_ratio (neg n)) + =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (Z_to_ratio (neg n)))). + rewrite > rtimes_Zplus2. + elim (or_one_frac f2 f) + [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1). + rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1). + rewrite > rtimes_Zplus. + rewrite > assoc_Zplus.reflexivity + |elim H1.clear H1. + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2). + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2). + rewrite > rtimes_Zplus2. + rewrite > assoc_Zplus.reflexivity + ] + |elim (or_one_frac f2 f) + [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2). + rewrite > rtimes_Zplus1. + elim (or_one_frac f f4) + [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H3). + rewrite > rtimes_Zplus2. + cut (f4 = f2) + [rewrite > Hcut. + rewrite > assoc_Zplus.reflexivity + |apply injective_frac. + rewrite < rtimes_onel. + rewrite < H2. + (* problema inaspettato: mi serve l'unicita' dell'inversa, + che richiede (?) l'associativita. Per fortuna basta + l'ipotesi induttiva. *) + cases f2 + [change with + (rtimes (rtimes (Z_to_ratio (pos n)) (frac f)) (frac f4)=Z_to_ratio (pos n)). + rewrite > Z_to_ratio_frac_frac. + rewrite > H3. + rewrite > rtimes_oner. + reflexivity + |change with + (rtimes (rtimes (Z_to_ratio (neg n)) (frac f)) (frac f4)=Z_to_ratio (neg n)). + rewrite > Z_to_ratio_frac_frac. + rewrite > H3. + rewrite > rtimes_oner. + reflexivity + |rewrite > H. + rewrite > H3. + rewrite > rtimes_oner. + reflexivity + ] + ] + |elim H3.clear H3. + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H4). + cut (rtimes (frac f2) (frac a) = frac f4) + [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f4 Hcut). + rewrite > assoc_Zplus.reflexivity + |rewrite < H4. + generalize in match H2. + cases f2;intro + [change with + (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) =frac f4). + rewrite < Z_to_ratio_frac_frac. + rewrite > H3. + rewrite > rtimes_onel. + reflexivity + |change with + (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) =frac f4). + rewrite < Z_to_ratio_frac_frac. + rewrite > H3. + rewrite > rtimes_onel. + reflexivity + |rewrite < H. + rewrite > H3. + rewrite > rtimes_onel. + reflexivity + ] + ] + ] + |elim H2.clear H2. + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3). + elim (or_one_frac f f4) + [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2). + rewrite > rtimes_Zplus2. + cut (rtimes (frac a) (frac f4) = frac f2) + [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f2 Hcut). + rewrite > assoc_Zplus.reflexivity + |rewrite < H3. + generalize in match H2. + cases f2;intro + [change with + (rtimes (rtimes (Z_to_ratio (pos n)) (frac f)) (frac f4)=Z_to_ratio (pos n)). + rewrite > Z_to_ratio_frac_frac. + rewrite > H4. + rewrite > rtimes_oner. + reflexivity + |change with + (rtimes (rtimes (Z_to_ratio (neg n)) (frac f)) (frac f4)=Z_to_ratio (neg n)). + rewrite > Z_to_ratio_frac_frac. + rewrite > H4. + rewrite > rtimes_oner. + reflexivity + |rewrite > H. + rewrite > H4. + rewrite > rtimes_oner. + reflexivity + ] + ] + |elim H2.clear H2. + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a1 H4). + elim (or_one_frac a f4) + [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2). + cut (rtimes (frac f2) (frac a1) = one) + [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? Hcut). + rewrite > assoc_Zplus.reflexivity + |rewrite < H4. + generalize in match H3. + cases f2;intro + [change with + (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = one). + rewrite < Z_to_ratio_frac_frac. + rewrite > H5. + assumption + |change with + (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = one). + rewrite < Z_to_ratio_frac_frac. + rewrite > H5. + assumption + |rewrite < H. + rewrite > H5. + assumption + ] + ] + |elim H2.clear H2. + rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 H5). + cut (rtimes (frac f2) (frac a1) = frac a2) + [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 Hcut). + rewrite > assoc_Zplus.reflexivity + |rewrite < H4. + generalize in match H3. + cases f2;intro + [change with + (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = frac a2). + rewrite < Z_to_ratio_frac_frac. + rewrite > H2. + assumption + |change with + (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = frac a2). + rewrite < Z_to_ratio_frac_frac. + rewrite > H2. + assumption + |rewrite < H. + rewrite > H2. + assumption + ] + ] + ] + ] + ] + ] + ] +qed. + +theorem frac_frac_fracaux: \forall f,f1,f2. +rtimes (rtimes (frac f) (frac f1)) (frac f2) +=rtimes (frac f) (rtimes (frac f1) (frac f2)). +intros. +cases f + [change with + (rtimes (rtimes (Z_to_ratio (pos n)) (frac f1)) (frac f2) + =rtimes (Z_to_ratio (pos n)) (rtimes (frac f1) (frac f2))). + apply Z_to_ratio_frac_frac + |change with + (rtimes (rtimes (Z_to_ratio (neg n)) (frac f1)) (frac f2) + =rtimes (Z_to_ratio (neg n)) (rtimes (frac f1) (frac f2))). + apply Z_to_ratio_frac_frac + |apply cons_frac_frac + ] +qed. + +theorem associative_rtimes:associative ? rtimes. +unfold.intros. +cases x + [reflexivity + |cases y + [reflexivity. + |cases z + [rewrite > rtimes_oner.rewrite > rtimes_oner.reflexivity + |apply frac_frac_fracaux + ] + ] + ] +qed. + +theorem associative_Qtimes:associative ? Qtimes. +unfold.intros. +cases x + [reflexivity + (* non posso scrivere 2,3: ... ?? *) + |cases y + [reflexivity. + |cases z + [reflexivity + |simplify.rewrite > associative_rtimes. + reflexivity. + |simplify.rewrite > associative_rtimes. + reflexivity + ] + |cases z + [reflexivity + |simplify.rewrite > associative_rtimes. + reflexivity. + |simplify.rewrite > associative_rtimes. + reflexivity + ] + ] + |cases y + [reflexivity. + |cases z + [reflexivity + |simplify.rewrite > associative_rtimes. + reflexivity. + |simplify.rewrite > associative_rtimes. + reflexivity + ] + |cases z + [reflexivity + |simplify.rewrite > associative_rtimes. + reflexivity. + |simplify.rewrite > associative_rtimes. + reflexivity + ] + ] + ] +qed. + +theorem Qtimes_OQ: \forall q.Qtimes q OQ = OQ. +intro.cases q;reflexivity. +qed. + +theorem symmetric_Qtimes: symmetric ? Qtimes. +unfold.intros. +cases x + [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity + |elim y + [reflexivity + |simplify.rewrite > symmetric_rtimes.reflexivity + |simplify.rewrite > symmetric_rtimes.reflexivity + ] + |elim y + [reflexivity + |simplify.rewrite > symmetric_rtimes.reflexivity + |simplify.rewrite > symmetric_rtimes.reflexivity + ] + ] +qed. + +theorem Qtimes_Qinv: \forall q. q \neq OQ \to Qtimes q (Qinv q) = Qone. +intro. +cases q;intro + [elim H.reflexivity + |simplify.rewrite > rtimes_rinv.reflexivity + |simplify.rewrite > rtimes_rinv.reflexivity + ] +qed. + +theorem eq_Qtimes_OQ_to_eq_OQ: \forall p,q. +Qtimes p q = OQ \to p = OQ \lor q = OQ. +intros 2. +cases p + [intro.left.reflexivity + |cases q + [intro.right.reflexivity + |simplify.intro.destruct H + |simplify.intro.destruct H + ] + |cases q + [intro.right.reflexivity + |simplify.intro.destruct H + |simplify.intro.destruct H + ] + ] +qed. + +theorem Qinv_Qtimes: \forall p,q. +p \neq OQ \to q \neq OQ \to +Qinv(Qtimes p q) = +Qtimes (Qinv p) (Qinv q). +intros. +rewrite < Qtimes_Qonel in ⊢ (? ? ? %). +rewrite < (Qtimes_Qinv (Qtimes p q)) + [lapply (Qtimes_Qinv ? H). + lapply (Qtimes_Qinv ? H1). + rewrite > symmetric_Qtimes in ⊢ (? ? ? (? % ?)). + rewrite > associative_Qtimes. + rewrite > associative_Qtimes. + rewrite < associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))). + rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))). + rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))). + rewrite > Hletin1. + rewrite > Qtimes_Qoner. + rewrite > Hletin. + rewrite > Qtimes_Qoner. + reflexivity + |intro. + elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2) + [apply (H H3)|apply (H1 H3)] + ] +qed. + +(* a stronger version, taking advantage of inv(O) = O *) +theorem Qinv_Qtimes': \forall p,q. +Qinv(Qtimes p q) = +Qtimes (Qinv p) (Qinv q). +intros. +cases p + [reflexivity + |cases q + [reflexivity + |apply Qinv_Qtimes;intro;destruct H + |apply Qinv_Qtimes;intro;destruct H + ] + |cases q + [reflexivity + |apply Qinv_Qtimes;intro;destruct H + |apply Qinv_Qtimes;intro;destruct H + ] + ] +qed. + +theorem Qtimes_frac_frac: \forall p,q,r,s. +Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)). +intros. +unfold frac. +rewrite > associative_Qtimes. +rewrite < associative_Qtimes in ⊢ (? ? (? ? %) ?). +rewrite > symmetric_Qtimes in ⊢ (? ? (? ? (? % ?)) ?). +rewrite > associative_Qtimes in ⊢ (? ? (? ? %) ?). +rewrite < associative_Qtimes. +rewrite < times_Qtimes. +rewrite < Qinv_Qtimes'. +rewrite < times_Qtimes. +reflexivity. +qed. + + +(* la prova seguente e' tutta una ripetizione. Sistemare. *) + +theorem Qtimes1: \forall f:fraction. +Qtimes (nat_fact_all_to_Q (numerator f)) +(Qinv (nat_fact_all_to_Q (numerator (finv f)))) += Qpos (frac f). +simplify. +intro.elim f + [reflexivity + |reflexivity + |elim (or_numerator_nfa_one_nfa_proper f1) + [elim H1.clear H1. + elim H3.clear H3. + cut (finv (nat_fact_to_fraction a) = f1) + [elim z + [simplify. + rewrite > H2.rewrite > H1.simplify. + rewrite > Hcut.reflexivity + |simplify. + rewrite > H2.rewrite > H1.simplify. + rewrite > Hcut.reflexivity + |simplify. + rewrite > H2.rewrite > H1.simplify. + rewrite > Hcut.reflexivity + ] + |generalize in match H. + rewrite > H2.rewrite > H1.simplify. + intro.destruct H3.assumption + ] + |elim H1.clear H1. + elim z + [simplify. + rewrite > H2.rewrite > H2.simplify. + elim (or_numerator_nfa_one_nfa_proper (finv f1)) + [elim H1.clear H1. + rewrite > H3.simplify. + cut (nat_fact_to_fraction a = f1) + [rewrite > Hcut.reflexivity + |generalize in match H. + rewrite > H2. + rewrite > H3. + rewrite > Qtimes_Qoner. + intro. + destruct H1. + assumption + ] + |elim H1.clear H1. + generalize in match H. + rewrite > H2. + rewrite > H3.simplify. + intro. + destruct H1. + rewrite > Hcut. + simplify.reflexivity + ] + |simplify.rewrite > H2.simplify. + elim (or_numerator_nfa_one_nfa_proper (finv f1)) + [elim H1.clear H1. + rewrite > H3.simplify. + cut (nat_fact_to_fraction a = f1) + [rewrite > Hcut.reflexivity + |generalize in match H. + rewrite > H2. + rewrite > H3. + rewrite > Qtimes_Qoner. + intro. + destruct H1. + assumption + ] + |elim H1.clear H1. + generalize in match H. + rewrite > H2. + rewrite > H3.simplify. + intro. + destruct H1. + rewrite > Hcut. + simplify.reflexivity + ] + |simplify.rewrite > H2.simplify. + elim (or_numerator_nfa_one_nfa_proper (finv f1)) + [elim H1.clear H1. + rewrite > H3.simplify. + cut (nat_fact_to_fraction a = f1) + [rewrite > Hcut.reflexivity + |generalize in match H. + rewrite > H2. + rewrite > H3. + rewrite > Qtimes_Qoner. + intro. + destruct H1. + assumption + ] + |elim H1.clear H1. + generalize in match H. + rewrite > H2. + rewrite > H3.simplify. + intro. + destruct H1. + rewrite > Hcut. + simplify.reflexivity + ] + ] + ] + ] +qed. + +(* +definition numQ:Q \to Z \def +\lambda q. +match q with +[OQ \Rightarrow OZ +|Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r))) +|Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r))) +]. +*) + +definition numQ:Q \to nat \def +\lambda q. defactorize (numeratorQ q). + +definition denomQ:Q \to nat \def +\lambda q. defactorize (numeratorQ (Qinv q)). + +definition Qopp:Q \to Q \def \lambda q. +match q with +[OQ \Rightarrow OQ +|Qpos q \Rightarrow Qneg q +|Qneg q \Rightarrow Qpos q +]. + +theorem frac_numQ_denomQ1: \forall r:ratio. +frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r). +intro. +unfold frac.unfold denomQ.unfold numQ. +unfold nat_to_Q. +rewrite > factorize_defactorize. +rewrite > factorize_defactorize. +elim r + [reflexivity + |elim f + [reflexivity + |reflexivity + |apply Qtimes1. + ] + ] +qed. + +theorem frac_numQ_denomQ2: \forall r:ratio. +frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r). +intro. +unfold frac.unfold denomQ.unfold numQ. +unfold nat_to_Q. +rewrite > factorize_defactorize. +rewrite > factorize_defactorize. +elim r + [reflexivity + |elim f + [reflexivity + |reflexivity + |apply Qtimes1. + ] + ] +qed. + +definition Qabs:Q \to Q \def \lambda q. +match q with +[OQ \Rightarrow OQ +|Qpos q \Rightarrow Qpos q +|Qneg q \Rightarrow Qpos q +]. + +theorem frac_numQ_denomQ: \forall q. +frac (numQ q) (denomQ q) = (Qabs q). +intros. +cases q + [reflexivity + |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1 + |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2 + ] +qed. + +definition Qfrac: Z \to nat \to Q \def +\lambda z,n.match z with +[OZ \Rightarrow OQ +|Zpos m \Rightarrow (frac (S m) n) +|Zneg m \Rightarrow Qopp (frac (S m) n) +]. + +definition QnumZ \def \lambda q. +match q with +[OQ \Rightarrow OZ +|Qpos r \Rightarrow Z_of_nat (numQ (Qpos r)) +|Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r)) +]. + +theorem Qfrac_Z_of_nat: \forall n,m. +Qfrac (Z_of_nat n) m = frac n m. +intros.cases n;reflexivity. +qed. + +theorem Qfrac_neg_Z_of_nat: \forall n,m. +Qfrac (neg_Z_of_nat n) m = Qopp (frac n m). +intros.cases n;reflexivity. +qed. + +theorem Qfrac_QnumZ_denomQ: \forall q. +Qfrac (QnumZ q) (denomQ q) = q. +intros. +cases q + [reflexivity + |change with + (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r). + rewrite > Qfrac_Z_of_nat. + apply frac_numQ_denomQ1. + |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2 + ] +qed. +