--- /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/frac".
+
+include "nat/factorization.ma".
+include "Q/q.ma".
+
+(* transformation from nat_fact to fracion *)
+let rec nat_fact_to_fraction l \def
+ match l with
+ [nf_last a \Rightarrow pp a
+ |nf_cons a p \Rightarrow
+ cons (Z_of_nat a) (nat_fact_to_fraction p)
+ ]
+.
+
+(* returns the numerator of a fraction in the form of a nat_fact_all *)
+let rec numerator f \def
+ match f with
+ [pp a \Rightarrow nfa_proper (nf_last a)
+ |nn a \Rightarrow nfa_one
+ |cons a l \Rightarrow
+ let n \def numerator l in
+ match n with
+ [nfa_zero \Rightarrow (* this case is vacuous *) nfa_zero
+ |nfa_one \Rightarrow
+ match a with
+ [OZ \Rightarrow nfa_one
+ |pos x \Rightarrow nfa_proper (nf_last x)
+ |neg x \Rightarrow nfa_one
+ ]
+ |nfa_proper g \Rightarrow
+ match a with
+ [OZ \Rightarrow nfa_proper (nf_cons O g)
+ |pos x \Rightarrow nfa_proper (nf_cons (S x) g)
+ |neg x \Rightarrow nfa_proper (nf_cons O g)
+ ]
+ ]
+ ]
+.
+
+theorem not_eq_numerator_nfa_zero:
+\forall f.numerator f \neq nfa_zero.
+intro.elim f
+ [simplify.intro.destruct H
+ |simplify.intro.destruct H
+ |simplify.generalize in match H.
+ cases (numerator f1)
+ [intro.elim H1.reflexivity
+ |simplify.intro.
+ cases z;simplify;intro;destruct H2
+ |simplify.intro.
+ cases z;simplify;intro;destruct H2
+ ]
+ ]
+qed.
+
+theorem or_numerator_nfa_one_nfa_proper:
+\forall f.(numerator f = nfa_one \land \exists g.numerator (finv f) =
+nfa_proper g) \lor \exists g.numerator f = nfa_proper g.
+intro.elim f
+ [simplify.right.
+ apply (ex_intro ? ? (nf_last n)).reflexivity
+ |simplify.left.split
+ [reflexivity
+ |apply (ex_intro ? ? (nf_last n)).reflexivity
+ ]
+ |elim H;clear H
+ [elim H1.clear H1.
+ elim H2.clear H2.
+ elim z
+ [simplify.
+ rewrite > H.rewrite > H1.simplify.
+ left.split
+ [reflexivity
+ |apply (ex_intro ? ? (nf_cons O a)).reflexivity
+ ]
+ |simplify.
+ rewrite > H.rewrite > H1.simplify.
+ right.apply (ex_intro ? ? (nf_last n)).reflexivity
+ |simplify.
+ rewrite > H.rewrite > H1.simplify.
+ left.split
+ [reflexivity
+ |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
+ ]
+ ]
+ |elim H1.clear H1.
+ elim z
+ [simplify.
+ rewrite > H.simplify.
+ right.
+ apply (ex_intro ? ? (nf_cons O a)).reflexivity
+ |simplify.
+ rewrite > H.simplify.
+ right.apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
+ |simplify.
+ rewrite > H.simplify.
+ right.
+ apply (ex_intro ? ? (nf_cons O a)).reflexivity
+ ]
+ ]
+ ]
+qed.
+
+theorem eq_nfa_one_to_eq_finv_nfa_proper:
+\forall f.numerator f = nfa_one \to
+\exist h.numerator (finv f) = nfa_proper h.
+intro.elim f
+ [simplify in H.destruct H
+ |simplify.apply (ex_intro ? ? (nf_last n)).reflexivity
+ |generalize in match H1.clear H1.
+ generalize in match H.clear H.
+ simplify.
+ cases (numerator f1);simplify
+ [intros;destruct H1
+ |intros;elim (H (refl_eq ? ?)).
+ rewrite > H2.simplify.
+ elim z;simplify
+ [apply (ex_intro ? ? (nf_cons O a)).reflexivity
+ |apply (ex_intro ? ? (nf_cons O a)).reflexivity
+ |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
+ ]
+ |elim z;destruct H1
+ ]
+ ]
+qed.
+
+theorem numerator_nat_fact_to_fraction: \forall g:nat_fact.
+numerator (nat_fact_to_fraction g) = nfa_proper g.
+intro.
+elim g
+ [simplify.reflexivity.
+ |simplify.rewrite > H.simplify.
+ cases n;reflexivity
+ ]
+qed.
+
+definition numeratorQ \def
+\lambda q.match q with
+ [OQ \Rightarrow nfa_zero
+ |pos r \Rightarrow
+ match r with
+ [one \Rightarrow nfa_one
+ |frac x \Rightarrow numerator x
+ ]
+ |neg r \Rightarrow
+ match r with
+ [one \Rightarrow nfa_one
+ |frac x \Rightarrow numerator x
+ ]
+ ]
+.
+
+definition nat_fact_all_to_Q \def
+\lambda n.
+ match n with
+ [nfa_zero \Rightarrow OQ
+ |nfa_one \Rightarrow Qpos one
+ |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction l))
+ ]
+.
+
+theorem numeratorQ_nat_fact_all_to_Q: \forall g.
+numeratorQ (nat_fact_all_to_Q g) = g.
+intro.cases g
+ [reflexivity
+ |reflexivity
+ |apply numerator_nat_fact_to_fraction
+ ]
+qed.
+
+definition nat_to_Q \def
+\lambda n. nat_fact_all_to_Q (factorize n).
+
+let rec nat_fact_to_fraction_inv l \def
+ match l with
+ [nf_last a \Rightarrow nn a
+ |nf_cons a p \Rightarrow
+ cons (neg_Z_of_nat a) (nat_fact_to_fraction_inv p)
+ ]
+.
+
+(*
+definition nat_fact_all_to_Q_inv \def
+\lambda n.
+ match n with
+ [nfa_zero \Rightarrow OQ
+ |nfa_one \Rightarrow Qpos one
+ |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction_inv l))
+ ]
+.
+
+definition nat_to_Q_inv \def
+\lambda n. nat_fact_all_to_Q_inv (factorize n).
+*)
+
+definition Qinv \def
+\lambda q.match q with
+[OQ \Rightarrow OQ
+|Qpos r \Rightarrow Qpos (rinv r)
+|Qneg r \Rightarrow Qneg (rinv r)
+].
+
+definition frac:nat \to nat \to Q \def
+\lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
+
+theorem rtimes_oner: \forall r.rtimes r one = r.
+intro.cases r;reflexivity.
+qed.
+
+theorem rtimes_onel: \forall r.rtimes one r = r.
+intro.cases r;reflexivity.
+qed.
+
+definition Qone \def Qpos one.
+
+theorem Qtimes_Qoner: \forall q.Qtimes q Qone = q.
+intro.cases q
+ [reflexivity
+ |cases r
+ [reflexivity
+ |reflexivity
+ ]
+ |cases r
+ [reflexivity
+ |reflexivity
+ ]
+ ]
+qed.
+
+theorem Qtimes_Qonel: \forall q.Qtimes Qone q = q.
+intros.cases q
+ [reflexivity
+ |cases r
+ [reflexivity
+ |reflexivity
+ ]
+ |cases r
+ [reflexivity
+ |reflexivity
+ ]
+ ]
+qed.
+
+let rec times_f h g \def
+ match h with
+ [nf_last a \Rightarrow
+ match g with
+ [nf_last b \Rightarrow nf_last (S (a+b))
+ |nf_cons b g1 \Rightarrow nf_cons (S (a+b)) g1
+ ]
+ |nf_cons a h1 \Rightarrow
+ match g with
+ [nf_last b \Rightarrow nf_cons (S (a+b)) h1
+ |nf_cons b g1 \Rightarrow nf_cons (a+b) (times_f h1 g1)
+ ]
+ ]
+.
+
+definition times_fa \def
+\lambda f,g.
+match f with
+[nfa_zero \Rightarrow nfa_zero
+|nfa_one \Rightarrow g
+|nfa_proper f1 \Rightarrow match g with
+ [nfa_zero \Rightarrow nfa_zero
+ |nfa_one \Rightarrow nfa_proper f1
+ |nfa_proper g1 \Rightarrow nfa_proper (times_f f1 g1)
+ ]
+]
+.
+
+theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
+=defactorize_aux g m*defactorize_aux h m.
+intro.elim g
+ [elim h;simplify;autobatch
+ |elim h
+ [simplify;autobatch
+ |simplify.rewrite > (H n3 (S m)).autobatch
+ ]
+ ]
+qed.
+
+theorem eq_times_fa_times: \forall f,g.
+defactorize (times_fa f g) = defactorize f*defactorize g.
+intros.
+elim f
+ [reflexivity
+ |simplify.apply plus_n_O
+ |elim g;simplify
+ [apply times_n_O
+ |apply times_n_SO
+ |apply eq_times_f_times1
+ ]
+ ]
+qed.
+
+theorem eq_times_times_fa: \forall n,m.
+factorize (n*m) = times_fa (factorize n) (factorize m).
+intros.
+rewrite <(factorize_defactorize (times_fa (factorize n) (factorize m))).
+rewrite > eq_times_fa_times.
+rewrite > defactorize_factorize.
+rewrite > defactorize_factorize.
+reflexivity.
+qed.
+
+
+theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
+Z_of_nat n + Z_of_nat m.
+intro.cases n;intro
+ [reflexivity
+ |cases m
+ [simplify.rewrite < plus_n_O.reflexivity
+ |simplify.reflexivity.
+ ]
+ ]
+qed.
+
+definition unfrac \def \lambda f.
+match f with
+ [one \Rightarrow pp O
+ |frac f \Rightarrow f
+ ]
+.
+
+lemma injective_frac: injective fraction ratio frac.
+unfold.intros.
+change with ((unfrac (frac x)) = (unfrac (frac y))).
+rewrite < H.reflexivity.
+qed.
+
+theorem times_f_ftimes: \forall n,m.
+frac (nat_fact_to_fraction (times_f n m))
+= ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m).
+intro.
+elim n
+ [elim m
+ [simplify.
+ rewrite < plus_n_Sm.reflexivity
+ |elim n2
+ [simplify.rewrite < plus_n_O.reflexivity
+ |simplify.reflexivity.
+ ]
+ ]
+ |elim m
+ [elim n1
+ [simplify.reflexivity
+ |simplify.rewrite < plus_n_Sm.reflexivity
+ ]
+ |simplify.
+ cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h)
+ [elim Hcut.
+ rewrite > H2.
+ simplify.apply eq_f.
+ apply eq_f2
+ [apply eq_plus_Zplus
+ |apply injective_frac.
+ rewrite < H2.
+ apply H
+ ]
+ |generalize in match n4.
+ elim n2
+ [cases n6;simplify;autobatch
+ |cases n7;simplify
+ [autobatch
+ |elim (H2 n9).
+ rewrite > H3.
+ simplify.
+ autobatch
+ ]
+ ]
+ ]
+ ]
+ ]
+qed.
+
+theorem times_fa_Qtimes: \forall f,g. nat_fact_all_to_Q (times_fa f g) =
+Qtimes (nat_fact_all_to_Q f) (nat_fact_all_to_Q g).
+intros.
+cases f;simplify
+ [reflexivity
+ |cases g;reflexivity
+ |cases g;simplify
+ [reflexivity
+ |reflexivity
+ |rewrite > times_f_ftimes.reflexivity
+ ]
+ ]
+qed.
+
+theorem times_Qtimes: \forall p,q.
+(nat_to_Q (p*q)) = Qtimes (nat_to_Q p) (nat_to_Q q).
+intros.unfold nat_to_Q.
+rewrite < times_fa_Qtimes.
+rewrite < eq_times_times_fa.
+reflexivity.
+qed.
+
+theorem rtimes_Zplus: \forall x,y.
+rtimes (Z_to_ratio x) (Z_to_ratio y) =
+Z_to_ratio (x + y).
+intro.
+elim x
+ [reflexivity
+ |elim y;reflexivity
+ |elim y;reflexivity
+ ]
+qed.
+
+theorem rtimes_Zplus1: \forall x,y,f.
+rtimes (Z_to_ratio x) (frac (cons y f)) =
+frac (cons ((x + y)) f).
+intro.
+elim x
+ [reflexivity
+ |elim y;reflexivity
+ |elim y;reflexivity
+ ]
+qed.
+
+theorem rtimes_Zplus2: \forall x,y,f.
+rtimes (frac (cons y f)) (Z_to_ratio x) =
+frac (cons ((y + x)) f).
+intros.
+elim x
+ [elim y;reflexivity
+ |elim y;reflexivity
+ |elim y;reflexivity
+ ]
+qed.
+
+theorem or_one_frac: \forall f,g.
+rtimes (frac f) (frac g) = one \lor
+\exists h.rtimes (frac f) (frac g) = frac h.
+intros.
+elim (rtimes (frac f) (frac g))
+ [left.reflexivity
+ |right.apply (ex_intro ? ? f1).reflexivity
+ ]
+qed.
+
+theorem one_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
+rtimes (frac f) (frac g) = one \to
+rtimes (frac (cons x f)) (frac (cons y g)) = Z_to_ratio (x + y).
+intros.simplify.simplify in H.rewrite > H.simplify.
+reflexivity.
+qed.
+
+theorem frac_to_rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
+\forall h.rtimes (frac f) (frac g) = frac h \to
+rtimes (frac (cons x f)) (frac (cons y g)) = frac (cons (x + y) h).
+intros.simplify.simplify in H.rewrite > H.simplify.
+reflexivity.
+qed.
+
+theorem rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
+(rtimes (frac f) (frac g) = one \land
+ rtimes (frac (cons x f)) (frac (cons y g)) = Z_to_ratio (x + y))
+\lor (\exists h.rtimes (frac f) (frac g) = frac h \land
+rtimes (frac (cons x f)) (frac (cons y g)) =
+frac (cons (x + y) h)).
+intros.
+simplify.
+elim (rtimes (frac f) (frac g));simplify
+ [left.split;reflexivity
+ |right.
+ apply (ex_intro ? ? f1).
+ split;reflexivity
+ ]
+qed.
+
+theorem Z_to_ratio_frac_frac: \forall z,f1,f2.
+rtimes (rtimes (Z_to_ratio z) (frac f1)) (frac f2)
+=rtimes (Z_to_ratio z) (rtimes (frac f1) (frac f2)).
+intros 2.elim f1
+ [elim f2
+ [change with
+ (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1))
+ =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))).
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+ rewrite > assoc_Zplus.reflexivity
+ |change with
+ (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (Z_to_ratio (neg n1))
+ =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (neg n1)))).
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+ rewrite > assoc_Zplus.reflexivity
+ |change with
+ (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (pos n))) (frac (cons z1 f))
+ = rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (pos n)) (frac (cons z1 f)))).
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
+ rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
+ rewrite > assoc_Zplus.reflexivity
+ ]
+ |elim f2
+ [change with
+ (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (Z_to_ratio (pos n1))
+ =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (pos n1)))).
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+ rewrite > assoc_Zplus.reflexivity
+ |change with
+ (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (Z_to_ratio (neg n1))
+ =rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (neg n1)))).
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus.
+ rewrite > assoc_Zplus.reflexivity
+ |change with
+ (rtimes (rtimes (Z_to_ratio z) (Z_to_ratio (neg n))) (frac (cons z1 f))
+ = rtimes (Z_to_ratio z) (rtimes (Z_to_ratio (neg n)) (frac (cons z1 f)))).
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus1.
+ rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus1.
+ rewrite > assoc_Zplus.reflexivity
+ ]
+ |elim f2
+ [change with
+ (rtimes (rtimes (Z_to_ratio z) (frac (cons z1 f))) (Z_to_ratio (pos n))
+ =rtimes (Z_to_ratio z) (rtimes (frac (cons z1 f)) (Z_to_ratio (pos n)))).
+ rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
+ rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
+ rewrite > assoc_Zplus.reflexivity
+ |change with
+ (rtimes (rtimes (Z_to_ratio z) (frac (cons z1 f))) (Z_to_ratio (neg n))
+ =rtimes (Z_to_ratio z) (rtimes (frac (cons z1 f)) (Z_to_ratio (neg n)))).
+ rewrite > rtimes_Zplus1.rewrite > rtimes_Zplus2.
+ rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
+ rewrite > assoc_Zplus.reflexivity
+ |elim (or_one_frac f f3)
+ [rewrite > rtimes_Zplus1.
+ rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
+ rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
+ rewrite > rtimes_Zplus.
+ rewrite > assoc_Zplus.reflexivity
+ |elim H2.clear H2.
+ rewrite > rtimes_Zplus1.
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
+ rewrite > rtimes_Zplus1.
+ rewrite > assoc_Zplus.reflexivity
+ ]
+ ]
+ ]
+qed.
+
+theorem cons_frac_frac: \forall f1,z,f,f2.
+rtimes (rtimes (frac (cons z f)) (frac f1)) (frac f2)
+=rtimes (frac (cons z f)) (rtimes (frac f1) (frac f2)).
+intro.elim f1
+ [elim f2
+ [change with
+ (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (Z_to_ratio (pos n1))
+ =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (pos n1)))).
+ rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
+ rewrite > assoc_Zplus.reflexivity
+ |change with
+ (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (Z_to_ratio (neg n1))
+ =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (Z_to_ratio (neg n1)))).
+ rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
+ rewrite > assoc_Zplus.reflexivity
+ |change with
+ (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (pos n))) (frac (cons z1 f3))
+ = rtimes (frac (cons z f)) (rtimes (Z_to_ratio (pos n)) (frac (cons z1 f3)))).
+ rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
+ elim (or_one_frac f f3)
+ [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+ rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+ rewrite > assoc_Zplus.reflexivity
+ |elim H1.clear H1.
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+ rewrite > assoc_Zplus.reflexivity
+ ]
+ ]
+ |elim f2
+ [change with
+ (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (Z_to_ratio (pos n1))
+ =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (pos n1)))).
+ rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
+ rewrite > assoc_Zplus.reflexivity
+ |change with
+ (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (Z_to_ratio (neg n1))
+ =rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (Z_to_ratio (neg n1)))).
+ rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus2.
+ rewrite > rtimes_Zplus.rewrite > rtimes_Zplus2.
+ rewrite > assoc_Zplus.reflexivity
+ |change with
+ (rtimes (rtimes (frac (cons z f)) (Z_to_ratio (neg n))) (frac (cons z1 f3))
+ = rtimes (frac (cons z f)) (rtimes (Z_to_ratio (neg n)) (frac (cons z1 f3)))).
+ rewrite > rtimes_Zplus2.rewrite > rtimes_Zplus1.
+ elim (or_one_frac f f3)
+ [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+ rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+ rewrite > assoc_Zplus.reflexivity
+ |elim H1.clear H1.
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+ rewrite > assoc_Zplus.reflexivity
+ ]
+ ]
+ |elim f3
+ [change with
+ (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (Z_to_ratio (pos n))
+ =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (Z_to_ratio (pos n)))).
+ rewrite > rtimes_Zplus2.
+ elim (or_one_frac f2 f)
+ [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+ rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+ rewrite > rtimes_Zplus.
+ rewrite > assoc_Zplus.reflexivity
+ |elim H1.clear H1.
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+ rewrite > rtimes_Zplus2.
+ rewrite > assoc_Zplus.reflexivity
+ ]
+ |change with
+ (rtimes (rtimes (frac (cons z1 f2)) (frac (cons z f))) (Z_to_ratio (neg n))
+ =rtimes (frac (cons z1 f2)) (rtimes (frac (cons z f)) (Z_to_ratio (neg n)))).
+ rewrite > rtimes_Zplus2.
+ elim (or_one_frac f2 f)
+ [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+ rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H1).
+ rewrite > rtimes_Zplus.
+ rewrite > assoc_Zplus.reflexivity
+ |elim H1.clear H1.
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H2).
+ rewrite > rtimes_Zplus2.
+ rewrite > assoc_Zplus.reflexivity
+ ]
+ |elim (or_one_frac f2 f)
+ [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
+ rewrite > rtimes_Zplus1.
+ elim (or_one_frac f f4)
+ [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H3).
+ rewrite > rtimes_Zplus2.
+ cut (f4 = f2)
+ [rewrite > Hcut.
+ rewrite > assoc_Zplus.reflexivity
+ |apply injective_frac.
+ rewrite < rtimes_onel.
+ rewrite < H2.
+ (* problema inaspettato: mi serve l'unicita' dell'inversa,
+ che richiede (?) l'associativita. Per fortuna basta
+ l'ipotesi induttiva. *)
+ cases f2
+ [change with
+ (rtimes (rtimes (Z_to_ratio (pos n)) (frac f)) (frac f4)=Z_to_ratio (pos n)).
+ rewrite > Z_to_ratio_frac_frac.
+ rewrite > H3.
+ rewrite > rtimes_oner.
+ reflexivity
+ |change with
+ (rtimes (rtimes (Z_to_ratio (neg n)) (frac f)) (frac f4)=Z_to_ratio (neg n)).
+ rewrite > Z_to_ratio_frac_frac.
+ rewrite > H3.
+ rewrite > rtimes_oner.
+ reflexivity
+ |rewrite > H.
+ rewrite > H3.
+ rewrite > rtimes_oner.
+ reflexivity
+ ]
+ ]
+ |elim H3.clear H3.
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H4).
+ cut (rtimes (frac f2) (frac a) = frac f4)
+ [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f4 Hcut).
+ rewrite > assoc_Zplus.reflexivity
+ |rewrite < H4.
+ generalize in match H2.
+ cases f2;intro
+ [change with
+ (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) =frac f4).
+ rewrite < Z_to_ratio_frac_frac.
+ rewrite > H3.
+ rewrite > rtimes_onel.
+ reflexivity
+ |change with
+ (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) =frac f4).
+ rewrite < Z_to_ratio_frac_frac.
+ rewrite > H3.
+ rewrite > rtimes_onel.
+ reflexivity
+ |rewrite < H.
+ rewrite > H3.
+ rewrite > rtimes_onel.
+ reflexivity
+ ]
+ ]
+ ]
+ |elim H2.clear H2.
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a H3).
+ elim (or_one_frac f f4)
+ [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
+ rewrite > rtimes_Zplus2.
+ cut (rtimes (frac a) (frac f4) = frac f2)
+ [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? f2 Hcut).
+ rewrite > assoc_Zplus.reflexivity
+ |rewrite < H3.
+ generalize in match H2.
+ cases f2;intro
+ [change with
+ (rtimes (rtimes (Z_to_ratio (pos n)) (frac f)) (frac f4)=Z_to_ratio (pos n)).
+ rewrite > Z_to_ratio_frac_frac.
+ rewrite > H4.
+ rewrite > rtimes_oner.
+ reflexivity
+ |change with
+ (rtimes (rtimes (Z_to_ratio (neg n)) (frac f)) (frac f4)=Z_to_ratio (neg n)).
+ rewrite > Z_to_ratio_frac_frac.
+ rewrite > H4.
+ rewrite > rtimes_oner.
+ reflexivity
+ |rewrite > H.
+ rewrite > H4.
+ rewrite > rtimes_oner.
+ reflexivity
+ ]
+ ]
+ |elim H2.clear H2.
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a1 H4).
+ elim (or_one_frac a f4)
+ [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? H2).
+ cut (rtimes (frac f2) (frac a1) = one)
+ [rewrite > (one_to_rtimes_Zplus3 ? ? ? ? Hcut).
+ rewrite > assoc_Zplus.reflexivity
+ |rewrite < H4.
+ generalize in match H3.
+ cases f2;intro
+ [change with
+ (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = one).
+ rewrite < Z_to_ratio_frac_frac.
+ rewrite > H5.
+ assumption
+ |change with
+ (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = one).
+ rewrite < Z_to_ratio_frac_frac.
+ rewrite > H5.
+ assumption
+ |rewrite < H.
+ rewrite > H5.
+ assumption
+ ]
+ ]
+ |elim H2.clear H2.
+ rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 H5).
+ cut (rtimes (frac f2) (frac a1) = frac a2)
+ [rewrite > (frac_to_rtimes_Zplus3 ? ? ? ? a2 Hcut).
+ rewrite > assoc_Zplus.reflexivity
+ |rewrite < H4.
+ generalize in match H3.
+ cases f2;intro
+ [change with
+ (rtimes (Z_to_ratio (pos n)) (rtimes (frac f)(frac f4)) = frac a2).
+ rewrite < Z_to_ratio_frac_frac.
+ rewrite > H2.
+ assumption
+ |change with
+ (rtimes (Z_to_ratio (neg n)) (rtimes (frac f)(frac f4)) = frac a2).
+ rewrite < Z_to_ratio_frac_frac.
+ rewrite > H2.
+ assumption
+ |rewrite < H.
+ rewrite > H2.
+ assumption
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+qed.
+
+theorem frac_frac_fracaux: \forall f,f1,f2.
+rtimes (rtimes (frac f) (frac f1)) (frac f2)
+=rtimes (frac f) (rtimes (frac f1) (frac f2)).
+intros.
+cases f
+ [change with
+ (rtimes (rtimes (Z_to_ratio (pos n)) (frac f1)) (frac f2)
+ =rtimes (Z_to_ratio (pos n)) (rtimes (frac f1) (frac f2))).
+ apply Z_to_ratio_frac_frac
+ |change with
+ (rtimes (rtimes (Z_to_ratio (neg n)) (frac f1)) (frac f2)
+ =rtimes (Z_to_ratio (neg n)) (rtimes (frac f1) (frac f2))).
+ apply Z_to_ratio_frac_frac
+ |apply cons_frac_frac
+ ]
+qed.
+
+theorem associative_rtimes:associative ? rtimes.
+unfold.intros.
+cases x
+ [reflexivity
+ |cases y
+ [reflexivity.
+ |cases z
+ [rewrite > rtimes_oner.rewrite > rtimes_oner.reflexivity
+ |apply frac_frac_fracaux
+ ]
+ ]
+ ]
+qed.
+
+theorem associative_Qtimes:associative ? Qtimes.
+unfold.intros.
+cases x
+ [reflexivity
+ (* non posso scrivere 2,3: ... ?? *)
+ |cases y
+ [reflexivity.
+ |cases z
+ [reflexivity
+ |simplify.rewrite > associative_rtimes.
+ reflexivity.
+ |simplify.rewrite > associative_rtimes.
+ reflexivity
+ ]
+ |cases z
+ [reflexivity
+ |simplify.rewrite > associative_rtimes.
+ reflexivity.
+ |simplify.rewrite > associative_rtimes.
+ reflexivity
+ ]
+ ]
+ |cases y
+ [reflexivity.
+ |cases z
+ [reflexivity
+ |simplify.rewrite > associative_rtimes.
+ reflexivity.
+ |simplify.rewrite > associative_rtimes.
+ reflexivity
+ ]
+ |cases z
+ [reflexivity
+ |simplify.rewrite > associative_rtimes.
+ reflexivity.
+ |simplify.rewrite > associative_rtimes.
+ reflexivity
+ ]
+ ]
+ ]
+qed.
+
+theorem Qtimes_OQ: \forall q.Qtimes q OQ = OQ.
+intro.cases q;reflexivity.
+qed.
+
+theorem symmetric_Qtimes: symmetric ? Qtimes.
+unfold.intros.
+cases x
+ [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity
+ |elim y
+ [reflexivity
+ |simplify.rewrite > symmetric_rtimes.reflexivity
+ |simplify.rewrite > symmetric_rtimes.reflexivity
+ ]
+ |elim y
+ [reflexivity
+ |simplify.rewrite > symmetric_rtimes.reflexivity
+ |simplify.rewrite > symmetric_rtimes.reflexivity
+ ]
+ ]
+qed.
+
+theorem Qtimes_Qinv: \forall q. q \neq OQ \to Qtimes q (Qinv q) = Qone.
+intro.
+cases q;intro
+ [elim H.reflexivity
+ |simplify.rewrite > rtimes_rinv.reflexivity
+ |simplify.rewrite > rtimes_rinv.reflexivity
+ ]
+qed.
+
+theorem eq_Qtimes_OQ_to_eq_OQ: \forall p,q.
+Qtimes p q = OQ \to p = OQ \lor q = OQ.
+intros 2.
+cases p
+ [intro.left.reflexivity
+ |cases q
+ [intro.right.reflexivity
+ |simplify.intro.destruct H
+ |simplify.intro.destruct H
+ ]
+ |cases q
+ [intro.right.reflexivity
+ |simplify.intro.destruct H
+ |simplify.intro.destruct H
+ ]
+ ]
+qed.
+
+theorem Qinv_Qtimes: \forall p,q.
+p \neq OQ \to q \neq OQ \to
+Qinv(Qtimes p q) =
+Qtimes (Qinv p) (Qinv q).
+intros.
+rewrite < Qtimes_Qonel in ⊢ (? ? ? %).
+rewrite < (Qtimes_Qinv (Qtimes p q))
+ [lapply (Qtimes_Qinv ? H).
+ lapply (Qtimes_Qinv ? H1).
+ rewrite > symmetric_Qtimes in ⊢ (? ? ? (? % ?)).
+ rewrite > associative_Qtimes.
+ rewrite > associative_Qtimes.
+ rewrite < associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
+ rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
+ rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
+ rewrite > Hletin1.
+ rewrite > Qtimes_Qoner.
+ rewrite > Hletin.
+ rewrite > Qtimes_Qoner.
+ reflexivity
+ |intro.
+ elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
+ [apply (H H3)|apply (H1 H3)]
+ ]
+qed.
+
+(* a stronger version, taking advantage of inv(O) = O *)
+theorem Qinv_Qtimes': \forall p,q.
+Qinv(Qtimes p q) =
+Qtimes (Qinv p) (Qinv q).
+intros.
+cases p
+ [reflexivity
+ |cases q
+ [reflexivity
+ |apply Qinv_Qtimes;intro;destruct H
+ |apply Qinv_Qtimes;intro;destruct H
+ ]
+ |cases q
+ [reflexivity
+ |apply Qinv_Qtimes;intro;destruct H
+ |apply Qinv_Qtimes;intro;destruct H
+ ]
+ ]
+qed.
+
+theorem Qtimes_frac_frac: \forall p,q,r,s.
+Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)).
+intros.
+unfold frac.
+rewrite > associative_Qtimes.
+rewrite < associative_Qtimes in ⊢ (? ? (? ? %) ?).
+rewrite > symmetric_Qtimes in ⊢ (? ? (? ? (? % ?)) ?).
+rewrite > associative_Qtimes in ⊢ (? ? (? ? %) ?).
+rewrite < associative_Qtimes.
+rewrite < times_Qtimes.
+rewrite < Qinv_Qtimes'.
+rewrite < times_Qtimes.
+reflexivity.
+qed.
+
+
+(* la prova seguente e' tutta una ripetizione. Sistemare. *)
+
+theorem Qtimes1: \forall f:fraction.
+Qtimes (nat_fact_all_to_Q (numerator f))
+(Qinv (nat_fact_all_to_Q (numerator (finv f))))
+= Qpos (frac f).
+simplify.
+intro.elim f
+ [reflexivity
+ |reflexivity
+ |elim (or_numerator_nfa_one_nfa_proper f1)
+ [elim H1.clear H1.
+ elim H3.clear H3.
+ cut (finv (nat_fact_to_fraction a) = f1)
+ [elim z
+ [simplify.
+ rewrite > H2.rewrite > H1.simplify.
+ rewrite > Hcut.reflexivity
+ |simplify.
+ rewrite > H2.rewrite > H1.simplify.
+ rewrite > Hcut.reflexivity
+ |simplify.
+ rewrite > H2.rewrite > H1.simplify.
+ rewrite > Hcut.reflexivity
+ ]
+ |generalize in match H.
+ rewrite > H2.rewrite > H1.simplify.
+ intro.destruct H3.assumption
+ ]
+ |elim H1.clear H1.
+ elim z
+ [simplify.
+ rewrite > H2.rewrite > H2.simplify.
+ elim (or_numerator_nfa_one_nfa_proper (finv f1))
+ [elim H1.clear H1.
+ rewrite > H3.simplify.
+ cut (nat_fact_to_fraction a = f1)
+ [rewrite > Hcut.reflexivity
+ |generalize in match H.
+ rewrite > H2.
+ rewrite > H3.
+ rewrite > Qtimes_Qoner.
+ intro.
+ destruct H1.
+ assumption
+ ]
+ |elim H1.clear H1.
+ generalize in match H.
+ rewrite > H2.
+ rewrite > H3.simplify.
+ intro.
+ destruct H1.
+ rewrite > Hcut.
+ simplify.reflexivity
+ ]
+ |simplify.rewrite > H2.simplify.
+ elim (or_numerator_nfa_one_nfa_proper (finv f1))
+ [elim H1.clear H1.
+ rewrite > H3.simplify.
+ cut (nat_fact_to_fraction a = f1)
+ [rewrite > Hcut.reflexivity
+ |generalize in match H.
+ rewrite > H2.
+ rewrite > H3.
+ rewrite > Qtimes_Qoner.
+ intro.
+ destruct H1.
+ assumption
+ ]
+ |elim H1.clear H1.
+ generalize in match H.
+ rewrite > H2.
+ rewrite > H3.simplify.
+ intro.
+ destruct H1.
+ rewrite > Hcut.
+ simplify.reflexivity
+ ]
+ |simplify.rewrite > H2.simplify.
+ elim (or_numerator_nfa_one_nfa_proper (finv f1))
+ [elim H1.clear H1.
+ rewrite > H3.simplify.
+ cut (nat_fact_to_fraction a = f1)
+ [rewrite > Hcut.reflexivity
+ |generalize in match H.
+ rewrite > H2.
+ rewrite > H3.
+ rewrite > Qtimes_Qoner.
+ intro.
+ destruct H1.
+ assumption
+ ]
+ |elim H1.clear H1.
+ generalize in match H.
+ rewrite > H2.
+ rewrite > H3.simplify.
+ intro.
+ destruct H1.
+ rewrite > Hcut.
+ simplify.reflexivity
+ ]
+ ]
+ ]
+ ]
+qed.
+
+(*
+definition numQ:Q \to Z \def
+\lambda q.
+match q with
+[OQ \Rightarrow OZ
+|Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r)))
+|Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r)))
+].
+*)
+
+definition numQ:Q \to nat \def
+\lambda q. defactorize (numeratorQ q).
+
+definition denomQ:Q \to nat \def
+\lambda q. defactorize (numeratorQ (Qinv q)).
+
+definition Qopp:Q \to Q \def \lambda q.
+match q with
+[OQ \Rightarrow OQ
+|Qpos q \Rightarrow Qneg q
+|Qneg q \Rightarrow Qpos q
+].
+
+theorem frac_numQ_denomQ1: \forall r:ratio.
+frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
+intro.
+unfold frac.unfold denomQ.unfold numQ.
+unfold nat_to_Q.
+rewrite > factorize_defactorize.
+rewrite > factorize_defactorize.
+elim r
+ [reflexivity
+ |elim f
+ [reflexivity
+ |reflexivity
+ |apply Qtimes1.
+ ]
+ ]
+qed.
+
+theorem frac_numQ_denomQ2: \forall r:ratio.
+frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
+intro.
+unfold frac.unfold denomQ.unfold numQ.
+unfold nat_to_Q.
+rewrite > factorize_defactorize.
+rewrite > factorize_defactorize.
+elim r
+ [reflexivity
+ |elim f
+ [reflexivity
+ |reflexivity
+ |apply Qtimes1.
+ ]
+ ]
+qed.
+
+definition Qabs:Q \to Q \def \lambda q.
+match q with
+[OQ \Rightarrow OQ
+|Qpos q \Rightarrow Qpos q
+|Qneg q \Rightarrow Qpos q
+].
+
+theorem frac_numQ_denomQ: \forall q.
+frac (numQ q) (denomQ q) = (Qabs q).
+intros.
+cases q
+ [reflexivity
+ |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
+ |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
+ ]
+qed.
+
+definition Qfrac: Z \to nat \to Q \def
+\lambda z,n.match z with
+[OZ \Rightarrow OQ
+|Zpos m \Rightarrow (frac (S m) n)
+|Zneg m \Rightarrow Qopp (frac (S m) n)
+].
+
+definition QnumZ \def \lambda q.
+match q with
+[OQ \Rightarrow OZ
+|Qpos r \Rightarrow Z_of_nat (numQ (Qpos r))
+|Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r))
+].
+
+theorem Qfrac_Z_of_nat: \forall n,m.
+Qfrac (Z_of_nat n) m = frac n m.
+intros.cases n;reflexivity.
+qed.
+
+theorem Qfrac_neg_Z_of_nat: \forall n,m.
+Qfrac (neg_Z_of_nat n) m = Qopp (frac n m).
+intros.cases n;reflexivity.
+qed.
+
+theorem Qfrac_QnumZ_denomQ: \forall q.
+Qfrac (QnumZ q) (denomQ q) = q.
+intros.
+cases q
+ [reflexivity
+ |change with
+ (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r).
+ rewrite > Qfrac_Z_of_nat.
+ apply frac_numQ_denomQ1.
+ |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
+ ]
+qed.
+
projects / helm.git / commitdiff