From: Claudio Sacerdoti Coen Date: Fri, 6 Jun 2008 13:45:38 +0000 (+0000) Subject: more stuff moved around X-Git-Tag: make_still_working~5070 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bb6f711dd0c8378d27118b73981515aff05f5750;p=helm.git more stuff moved around --- diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma index de156e2db..abc1fb4ce 100644 --- a/helm/software/matita/library/Q/frac.ma +++ b/helm/software/matita/library/Q/frac.ma @@ -37,14 +37,6 @@ definition nat_to_Q_inv \def 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. - let rec times_f h g \def match h with [nf_last a \Rightarrow @@ -120,19 +112,6 @@ intro.cases n;intro ] 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). @@ -200,66 +179,9 @@ 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)) + 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)). @@ -273,345 +195,6 @@ elim (rtimes (frac f) (frac g));simplify ] 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 diff --git a/helm/software/matita/library/Q/ratio/ratio.ma b/helm/software/matita/library/Q/ratio/ratio.ma index 38f2f07b1..754b7ad70 100644 --- a/helm/software/matita/library/Q/ratio/ratio.ma +++ b/helm/software/matita/library/Q/ratio/ratio.ma @@ -17,3 +17,16 @@ include "Q/fraction/fraction.ma". inductive ratio : Set \def one : ratio | frac : fraction \to ratio. + +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. diff --git a/helm/software/matita/library/Q/ratio/rtimes.ma b/helm/software/matita/library/Q/ratio/rtimes.ma index e11dbea9f..3c7859dbe 100644 --- a/helm/software/matita/library/Q/ratio/rtimes.ma +++ b/helm/software/matita/library/Q/ratio/rtimes.ma @@ -15,17 +15,17 @@ include "Q/ratio/rinv.ma". include "Q/fraction/ftimes.ma". -definition rtimes : ratio \to ratio \to ratio \def -\lambda r,s:ratio. +definition rtimes : ratio → ratio → ratio ≝ +λr,s:ratio. match r with - [one \Rightarrow s - | (frac f) \Rightarrow + [one ⇒ s + | (frac f) ⇒ match s with - [one \Rightarrow frac f - | (frac g) \Rightarrow ftimes f g]]. + [one ⇒ frac f + | (frac g) ⇒ ftimes f g]]. theorem symmetric_rtimes : symmetric ratio rtimes. -change with (\forall r,s:ratio. rtimes r s = rtimes s r). +change with (∀r,s:ratio. rtimes r s = rtimes s r). intros. elim r. elim s. reflexivity. @@ -37,8 +37,409 @@ qed. variant sym_rtimes : ∀x,y:ratio. rtimes x y = rtimes y x ≝ symmetric_rtimes. -theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one. +theorem rtimes_r_one: ∀r.rtimes r one = r. + intro; cases r;reflexivity. +qed. + +theorem rtimes_one_r: ∀r.rtimes one r = r. +intro; cases r;reflexivity. +qed. + +theorem rtimes_Zplus: \forall x,y. +rtimes (nat_frac_item_to_ratio x) (nat_frac_item_to_ratio y) = +nat_frac_item_to_ratio (x + y). +intro. +elim x + [reflexivity + |*:elim y;reflexivity + ] +qed. + +theorem rtimes_Zplus1: \forall x,y,f. +rtimes (nat_frac_item_to_ratio x) (frac (cons y f)) = +frac (cons ((x + y)) f). +intro. +elim x + [reflexivity + |*:elim y;reflexivity + ] +qed. + +theorem rtimes_Zplus2: \forall x,y,f. +rtimes (frac (cons y f)) (nat_frac_item_to_ratio x) = +frac (cons ((y + x)) f). +intros. +elim x + [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)) = nat_frac_item_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 nat_frac_item_to_ratio_frac_frac: \forall z,f1,f2. +rtimes (rtimes (nat_frac_item_to_ratio z) (frac f1)) (frac f2) +=rtimes (nat_frac_item_to_ratio z) (rtimes (frac f1) (frac f2)). +intros 2.elim f1 + [elim f2 + [change with + (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (pos n1)) + =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (pos n1)))). + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (neg n1)) + =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_to_ratio (neg n1)))). + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (pos n))) (frac (cons z1 f)) + = rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_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 (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (pos n1)) + =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (pos n1)))). + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (neg n1)) + =rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_to_ratio (neg n1)))). + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > rtimes_Zplus.rewrite > rtimes_Zplus. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (nat_frac_item_to_ratio z) (nat_frac_item_to_ratio (neg n))) (frac (cons z1 f)) + = rtimes (nat_frac_item_to_ratio z) (rtimes (nat_frac_item_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 (nat_frac_item_to_ratio z) (frac (cons z1 f))) (nat_frac_item_to_ratio (pos n)) + =rtimes (nat_frac_item_to_ratio z) (rtimes (frac (cons z1 f)) (nat_frac_item_to_ratio (pos n)))). + rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2. + rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1. + rewrite > assoc_Zplus.reflexivity + |change with + (rtimes (rtimes (nat_frac_item_to_ratio z) (frac (cons z1 f))) (nat_frac_item_to_ratio (neg n)) + =rtimes (nat_frac_item_to_ratio z) (rtimes (frac (cons z1 f)) (nat_frac_item_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)) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (pos n1)) + =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_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)) (nat_frac_item_to_ratio (pos n))) (nat_frac_item_to_ratio (neg n1)) + =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (pos n)) (nat_frac_item_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)) (nat_frac_item_to_ratio (pos n))) (frac (cons z1 f3)) + = rtimes (frac (cons z f)) (rtimes (nat_frac_item_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)) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (pos n1)) + =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_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)) (nat_frac_item_to_ratio (neg n))) (nat_frac_item_to_ratio (neg n1)) + =rtimes (frac (cons z f)) (rtimes (nat_frac_item_to_ratio (neg n)) (nat_frac_item_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)) (nat_frac_item_to_ratio (neg n))) (frac (cons z1 f3)) + = rtimes (frac (cons z f)) (rtimes (nat_frac_item_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))) (nat_frac_item_to_ratio (pos n)) + =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (nat_frac_item_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))) (nat_frac_item_to_ratio (neg n)) + =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (nat_frac_item_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_one_r. + 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 (nat_frac_item_to_ratio (pos n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (pos n)). + rewrite > nat_frac_item_to_ratio_frac_frac. + rewrite > H3. + rewrite > rtimes_r_one. + reflexivity + |change with + (rtimes (rtimes (nat_frac_item_to_ratio (neg n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (neg n)). + rewrite > nat_frac_item_to_ratio_frac_frac. + rewrite > H3. + rewrite > rtimes_r_one. + reflexivity + |rewrite > H. + rewrite > H3. + rewrite > rtimes_r_one. + 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 (nat_frac_item_to_ratio (pos n)) (rtimes (frac f)(frac f4)) =frac f4). + rewrite < nat_frac_item_to_ratio_frac_frac. + rewrite > H3. + rewrite > rtimes_one_r. + reflexivity + |change with + (rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f)(frac f4)) =frac f4). + rewrite < nat_frac_item_to_ratio_frac_frac. + rewrite > H3. + rewrite > rtimes_one_r. + reflexivity + |rewrite < H. + rewrite > H3. + rewrite > rtimes_one_r. + 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 (nat_frac_item_to_ratio (pos n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (pos n)). + rewrite > nat_frac_item_to_ratio_frac_frac. + rewrite > H4. + rewrite > rtimes_r_one. + reflexivity + |change with + (rtimes (rtimes (nat_frac_item_to_ratio (neg n)) (frac f)) (frac f4)=nat_frac_item_to_ratio (neg n)). + rewrite > nat_frac_item_to_ratio_frac_frac. + rewrite > H4. + rewrite > rtimes_r_one. + reflexivity + |rewrite > H. + rewrite > H4. + rewrite > rtimes_r_one. + 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 (nat_frac_item_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = one). + rewrite < nat_frac_item_to_ratio_frac_frac. + rewrite > H5. + assumption + |change with + (rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = one). + rewrite < nat_frac_item_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 (nat_frac_item_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = frac a2). + rewrite < nat_frac_item_to_ratio_frac_frac. + rewrite > H2. + assumption + |change with + (rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = frac a2). + rewrite < nat_frac_item_to_ratio_frac_frac. + rewrite > H2. + assumption + |rewrite < H. + rewrite > H2. + assumption + ] + ] + ] + ] + ] + ] + ] +qed. + +theorem frac_frac_fracaux: ∀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 (nat_frac_item_to_ratio (pos n)) (frac f1)) (frac f2) + =rtimes (nat_frac_item_to_ratio (pos n)) (rtimes (frac f1) (frac f2))). + apply nat_frac_item_to_ratio_frac_frac + |change with + (rtimes (rtimes (nat_frac_item_to_ratio (neg n)) (frac f1)) (frac f2) + =rtimes (nat_frac_item_to_ratio (neg n)) (rtimes (frac f1) (frac f2))). + apply nat_frac_item_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_r_one.rewrite > rtimes_r_one.reflexivity + |apply frac_frac_fracaux + ]]] +qed. + + +theorem rtimes_rinv: ∀r:ratio. rtimes r (rinv r) = one. intro.elim r. reflexivity. simplify.apply ftimes_finv. -qed. \ No newline at end of file +qed.