From: Claudio Sacerdoti Coen Date: Fri, 6 Jun 2008 13:26:27 +0000 (+0000) Subject: More Q stuff organized in a coherent way. X-Git-Tag: make_still_working~5071 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9d7d400d540ba79edaab1e0c8345127e1a79bb53;p=helm.git More Q stuff organized in a coherent way. --- diff --git a/helm/software/matita/library/Q/Qplus_andrea.ma b/helm/software/matita/library/Q/Qplus_andrea.ma deleted file mode 100644 index 64c74dc90..000000000 --- a/helm/software/matita/library/Q/Qplus_andrea.ma +++ /dev/null @@ -1,889 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/Qplus". - -include "nat/factorization.ma". -include "Q/frac.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 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. - - diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma index 334f1c868..de156e2db 100644 --- a/helm/software/matita/library/Q/frac.ma +++ b/helm/software/matita/library/Q/frac.ma @@ -12,49 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/Q/frac". - -include "nat/factorization.ma". -include "Q/q.ma". - - -definition numeratorQ \def -\lambda q.match q with - [OQ \Rightarrow nfa_zero - |Qpos r \Rightarrow - match r with - [one \Rightarrow nfa_one - |frac x \Rightarrow numerator x - ] - |Qneg 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 @@ -63,8 +21,6 @@ let rec nat_fact_to_fraction_inv l \def ] . - -(* definition nat_fact_all_to_Q_inv \def \lambda n. match n with @@ -78,13 +34,6 @@ 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)). @@ -96,36 +45,6 @@ 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 @@ -359,7 +278,7 @@ 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 + [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. @@ -745,8 +664,7 @@ cases x [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity |elim y [reflexivity - |simplify.alias id "symmetric_rtimes" = "cic:/matita/Q/times/symmetric_rtimes.con". -rewrite > symmetric_rtimes.reflexivity + |simplify.rewrite > symmetric_rtimes.reflexivity |simplify.rewrite > symmetric_rtimes.reflexivity ] |elim y @@ -761,8 +679,7 @@ theorem Qtimes_Qinv: \forall q. q \neq OQ \to Qtimes q (Qinv q) = Qone. intro. cases q;intro [elim H.reflexivity - |simplify.alias id "rtimes_rinv" = "cic:/matita/Q/times/rtimes_rinv.con". -rewrite > rtimes_rinv.reflexivity + |simplify.rewrite > rtimes_rinv.reflexivity |simplify.rewrite > rtimes_rinv.reflexivity ] qed. @@ -790,7 +707,7 @@ p \neq OQ \to q \neq OQ \to Qinv(Qtimes p q) = Qtimes (Qinv p) (Qinv q). intros. -rewrite < Qtimes_Qonel in ⊢ (? ? ? %). +rewrite < Qtimes_Qone_q in ⊢ (? ? ? %). rewrite < (Qtimes_Qinv (Qtimes p q)) [lapply (Qtimes_Qinv ? H). lapply (Qtimes_Qinv ? H1). @@ -801,9 +718,9 @@ rewrite < (Qtimes_Qinv (Qtimes p q)) rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))). rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))). rewrite > Hletin1. - rewrite > Qtimes_Qoner. + rewrite > Qtimes_q_Qone. rewrite > Hletin. - rewrite > Qtimes_Qoner. + rewrite > Qtimes_q_Qone. reflexivity |intro. elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2) @@ -888,7 +805,7 @@ intro.elim f |generalize in match H. rewrite > H2. rewrite > H3. - rewrite > Qtimes_Qoner. + rewrite > Qtimes_q_Qone. intro. destruct H1. assumption @@ -911,7 +828,7 @@ intro.elim f |generalize in match H. rewrite > H2. rewrite > H3. - rewrite > Qtimes_Qoner. + rewrite > Qtimes_q_Qone. intro. destruct H1. assumption @@ -934,7 +851,7 @@ intro.elim f |generalize in match H. rewrite > H2. rewrite > H3. - rewrite > Qtimes_Qoner. + rewrite > Qtimes_q_Qone. intro. destruct H1. assumption diff --git a/helm/software/matita/library/Q/fraction/finv.ma b/helm/software/matita/library/Q/fraction/finv.ma index d9bf715b1..2868bece0 100644 --- a/helm/software/matita/library/Q/fraction/finv.ma +++ b/helm/software/matita/library/Q/fraction/finv.ma @@ -32,7 +32,6 @@ theorem finv_finv: ∀f. finv (finv f) = f. ] qed. - theorem or_numerator_nfa_one_nfa_proper: ∀f. (numerator f = nfa_one ∧ ∃g.numerator (finv f) = nfa_proper g) ∨ diff --git a/helm/software/matita/library/Q/q/q.ma b/helm/software/matita/library/Q/q/q.ma index 86f6d1dcf..43b090fef 100644 --- a/helm/software/matita/library/Q/q/q.ma +++ b/helm/software/matita/library/Q/q/q.ma @@ -20,10 +20,54 @@ inductive Q : Set \def | Qpos : ratio \to Q | Qneg : ratio \to Q. -definition Q_of_nat ≝ - λn. - match factorize n with - [ nfa_zero ⇒ OQ - | nfa_one ⇒ Qpos one - | nfa_proper l ⇒ Qpos (frac (nat_fact_to_fraction l)) +definition Qone ≝ Qpos one. + +definition Qopp ≝ + λq. + match q with + [ OQ ⇒ OQ + | Qpos r ⇒ Qneg r + | Qneg r ⇒ Qpos r ]. + +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)) + ]. + +definition nat_to_Q ≝ λn.nat_fact_all_to_Q (factorize n). + +definition Z_to_Q ≝ + λz. + match z with + [ OZ ⇒ OQ + | pos n ⇒ nat_to_Q (S n) + | neg n ⇒ Qopp (nat_to_Q (S n)) + ]. + +definition numeratorQ \def +\lambda q.match q with + [OQ \Rightarrow nfa_zero + |Qpos r \Rightarrow + match r with + [one \Rightarrow nfa_one + |frac x \Rightarrow numerator x + ] + |Qneg r \Rightarrow + match r with + [one \Rightarrow nfa_one + |frac x \Rightarrow numerator x + ] + ]. + +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. diff --git a/helm/software/matita/library/Q/q/qtimes.ma b/helm/software/matita/library/Q/q/qtimes.ma index 8a94d2b35..e288ef412 100644 --- a/helm/software/matita/library/Q/q/qtimes.ma +++ b/helm/software/matita/library/Q/q/qtimes.ma @@ -39,7 +39,7 @@ theorem Qtimes_q_OQ: ∀q. q * OQ = OQ. intro; elim q; reflexivity. -qed. +qed. theorem symmetric_Qtimes: symmetric ? Qtimes. intros 2; @@ -52,6 +52,20 @@ theorem symmetric_Qtimes: symmetric ? Qtimes. ] qed. +theorem Qtimes_q_Qone: ∀q.q * Qone = q. + intro.cases q + [reflexivity + |2,3: cases r; reflexivity + ] +qed. + +theorem Qtimes_Qone_q: ∀q.Qone * q = q. + intro.cases q + [reflexivity + |2,3: cases r; reflexivity + ] +qed. + theorem Qtimes_Qinv: ∀q. q ≠ OQ → q * (Qinv q) = Qpos one. intro; elim q; diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index bbf2c8079..328e2088f 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -21,9 +21,8 @@ higher_order_defs/ordering.ma logic/equality.ma higher_order_defs/relations.ma logic/connectives.ma Q/q.ma Z/compare.ma Z/plus.ma nat/factorization.ma Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma -Q/frac.ma Q/q.ma nat/factorization.ma +Q/frac.ma Q/inv.ma Q/q.ma -Q/Qplus_andrea.ma Q/frac.ma nat/factorization.ma Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma Q/q/q.ma Q/ratio/ratio.ma Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma