From: Claudio Sacerdoti Coen Date: Fri, 6 Jun 2008 16:48:01 +0000 (+0000) Subject: Even more Q stuff classified. X-Git-Tag: make_still_working~5068 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7a116453d799657958e32693be28d18a5aab84fc;p=helm.git Even more Q stuff classified. --- diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma index abc1fb4ce..d00cd3158 100644 --- a/helm/software/matita/library/Q/frac.ma +++ b/helm/software/matita/library/Q/frac.ma @@ -32,305 +32,10 @@ definition nat_fact_all_to_Q_inv \def definition nat_to_Q_inv \def \lambda n. nat_fact_all_to_Q_inv (factorize n). -*) definition frac:nat \to nat \to Q \def \lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)). -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. - -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_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)) = nat_frac_item_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 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_Qone_q 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_q_Qone. - rewrite > Hletin. - rewrite > Qtimes_q_Qone. - 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. @@ -345,7 +50,7 @@ rewrite < Qinv_Qtimes'. rewrite < times_Qtimes. reflexivity. qed. - +*) (* la prova seguente e' tutta una ripetizione. Sistemare. *) (*CSC @@ -469,12 +174,6 @@ definition numQ:Q \to nat \def 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 -]. (*CSC theorem frac_numQ_denomQ1: \forall r:ratio. frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r). diff --git a/helm/software/matita/library/Q/fraction/ftimes.ma b/helm/software/matita/library/Q/fraction/ftimes.ma index 2e5871d73..bcc7358b2 100644 --- a/helm/software/matita/library/Q/fraction/ftimes.ma +++ b/helm/software/matita/library/Q/fraction/ftimes.ma @@ -14,6 +14,8 @@ include "Q/ratio/ratio.ma". include "Q/fraction/finv.ma". +include "Q/nat_fact/times.ma". +include "Z/times.ma". definition nat_frac_item_to_ratio: Z \to ratio \def \lambda x:Z. match x with @@ -88,3 +90,44 @@ intro.elim f. | (frac h) \Rightarrow frac (cons (z + - z) h)] = one). rewrite > H.rewrite > Zplus_Zopp.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. \ No newline at end of file diff --git a/helm/software/matita/library/Q/nat_fact/times.ma b/helm/software/matita/library/Q/nat_fact/times.ma new file mode 100644 index 000000000..43c213c9b --- /dev/null +++ b/helm/software/matita/library/Q/nat_fact/times.ma @@ -0,0 +1,75 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "nat/factorization.ma". + +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) + ]]. + +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. + + +(******************* times_fa *********************) + +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_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. \ No newline at end of file diff --git a/helm/software/matita/library/Q/q/qtimes.ma b/helm/software/matita/library/Q/q/qtimes.ma index e288ef412..52246e5a5 100644 --- a/helm/software/matita/library/Q/q/qtimes.ma +++ b/helm/software/matita/library/Q/q/qtimes.ma @@ -75,3 +75,117 @@ theorem Qtimes_Qinv: ∀q. q ≠ OQ → q * (Qinv q) = Qpos one. reflexivity ] 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 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 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_Qone_q 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_q_Qone. + rewrite > Hletin. + rewrite > Qtimes_q_Qone. + 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. diff --git a/helm/software/matita/library/Q/ratio/rtimes.ma b/helm/software/matita/library/Q/ratio/rtimes.ma index 3c7859dbe..a8255afef 100644 --- a/helm/software/matita/library/Q/ratio/rtimes.ma +++ b/helm/software/matita/library/Q/ratio/rtimes.ma @@ -443,3 +443,18 @@ intro.elim r. reflexivity. simplify.apply ftimes_finv. 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)) = nat_frac_item_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. \ No newline at end of file diff --git a/helm/software/matita/library/Z/times.ma b/helm/software/matita/library/Z/times.ma index 90a71b520..c81c0dfca 100644 --- a/helm/software/matita/library/Z/times.ma +++ b/helm/software/matita/library/Z/times.ma @@ -251,3 +251,13 @@ qed. variant distr_Ztimes_Zplus: \forall x,y,z. x * (y + z) = x*y + x*z \def distributive_Ztimes_Zplus. + +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. diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index 328e2088f..b17029e92 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -33,6 +33,7 @@ Q/ratio/rtimes.ma Q/fraction/ftimes.ma Q/ratio/rinv.ma Q/fraction/fraction.ma Z/compare.ma nat/factorization.ma Q/fraction/finv.ma Q/fraction/fraction.ma Z/plus.ma Q/fraction/ftimes.ma Q/fraction/finv.ma Q/ratio/ratio.ma +Q/nat_fact/times.ma nat/factorization.ma datatypes/compare.ma datatypes/constructors.ma logic/equality.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma