--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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".
+
+definition Qplus: \lambda p,q.
+
+
+
+
+(* 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.
+
+
projects / helm.git / commitdiff