+++ /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".
-
-(* 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