definition nat_to_Q_inv \def
\lambda n. nat_fact_all_to_Q_inv (factorize n).
-*)
definition frac:nat \to nat \to Q \def
\lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
-let rec times_f h g \def
- match h with
- [nf_last a \Rightarrow
- match g with
- [nf_last b \Rightarrow nf_last (S (a+b))
- |nf_cons b g1 \Rightarrow nf_cons (S (a+b)) g1
- ]
- |nf_cons a h1 \Rightarrow
- match g with
- [nf_last b \Rightarrow nf_cons (S (a+b)) h1
- |nf_cons b g1 \Rightarrow nf_cons (a+b) (times_f h1 g1)
- ]
- ]
-.
-
-definition times_fa \def
-\lambda f,g.
-match f with
-[nfa_zero \Rightarrow nfa_zero
-|nfa_one \Rightarrow g
-|nfa_proper f1 \Rightarrow match g with
- [nfa_zero \Rightarrow nfa_zero
- |nfa_one \Rightarrow nfa_proper f1
- |nfa_proper g1 \Rightarrow nfa_proper (times_f f1 g1)
- ]
-]
-.
-
-theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
-=defactorize_aux g m*defactorize_aux h m.
-intro.elim g
- [elim h;simplify;autobatch
- |elim h
- [simplify;autobatch
- |simplify.rewrite > (H n3 (S m)).autobatch
- ]
- ]
-qed.
-
-theorem eq_times_fa_times: \forall f,g.
-defactorize (times_fa f g) = defactorize f*defactorize g.
-intros.
-elim f
- [reflexivity
- |simplify.apply plus_n_O
- |elim g;simplify
- [apply times_n_O
- |apply times_n_SO
- |apply eq_times_f_times1
- ]
- ]
-qed.
-
-theorem eq_times_times_fa: \forall n,m.
-factorize (n*m) = times_fa (factorize n) (factorize m).
-intros.
-rewrite <(factorize_defactorize (times_fa (factorize n) (factorize m))).
-rewrite > eq_times_fa_times.
-rewrite > defactorize_factorize.
-rewrite > defactorize_factorize.
-reflexivity.
-qed.
-
-
-theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
-Z_of_nat n + Z_of_nat m.
-intro.cases n;intro
- [reflexivity
- |cases m
- [simplify.rewrite < plus_n_O.reflexivity
- |simplify.reflexivity.
- ]
- ]
-qed.
-
-theorem times_f_ftimes: \forall n,m.
-frac (nat_fact_to_fraction (times_f n m))
-= ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m).
-intro.
-elim n
- [elim m
- [simplify.
- rewrite < plus_n_Sm.reflexivity
- |elim n2
- [simplify.rewrite < plus_n_O.reflexivity
- |simplify.reflexivity.
- ]
- ]
- |elim m
- [elim n1
- [simplify.reflexivity
- |simplify.rewrite < plus_n_Sm.reflexivity
- ]
- |simplify.
- cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h)
- [elim Hcut.
- rewrite > H2.
- simplify.apply eq_f.
- apply eq_f2
- [apply eq_plus_Zplus
- |apply injective_frac.
- rewrite < H2.
- apply H
- ]
- |generalize in match n4.
- elim n2
- [cases n6;simplify;autobatch
- |cases n7;simplify
- [autobatch
- |elim (H2 n9).
- rewrite > H3.
- simplify.
- autobatch
- ]
- ]
- ]
- ]
- ]
-qed.
-
-theorem times_fa_Qtimes: \forall f,g. nat_fact_all_to_Q (times_fa f g) =
-Qtimes (nat_fact_all_to_Q f) (nat_fact_all_to_Q g).
-intros.
-cases f;simplify
- [reflexivity
- |cases g;reflexivity
- |cases g;simplify
- [reflexivity
- |reflexivity
- |rewrite > times_f_ftimes.reflexivity
- ]
- ]
-qed.
-
-theorem times_Qtimes: \forall p,q.
-(nat_to_Q (p*q)) = Qtimes (nat_to_Q p) (nat_to_Q q).
-intros.unfold nat_to_Q.
-rewrite < times_fa_Qtimes.
-rewrite < eq_times_times_fa.
-reflexivity.
-qed.
-
-theorem rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
-(rtimes (frac f) (frac g) = one \land
- rtimes (frac (cons x f)) (frac (cons y g)) = nat_frac_item_to_ratio (x + y))
-\lor (\exists h.rtimes (frac f) (frac g) = frac h \land
-rtimes (frac (cons x f)) (frac (cons y g)) =
-frac (cons (x + y) h)).
-intros.
-simplify.
-elim (rtimes (frac f) (frac g));simplify
- [left.split;reflexivity
- |right.
- apply (ex_intro ? ? f1).
- split;reflexivity
- ]
-qed.
-
-theorem associative_Qtimes:associative ? Qtimes.
-unfold.intros.
-cases x
- [reflexivity
- (* non posso scrivere 2,3: ... ?? *)
- |cases y
- [reflexivity.
- |cases z
- [reflexivity
- |simplify.rewrite > associative_rtimes.
- reflexivity.
- |simplify.rewrite > associative_rtimes.
- reflexivity
- ]
- |cases z
- [reflexivity
- |simplify.rewrite > associative_rtimes.
- reflexivity.
- |simplify.rewrite > associative_rtimes.
- reflexivity
- ]
- ]
- |cases y
- [reflexivity.
- |cases z
- [reflexivity
- |simplify.rewrite > associative_rtimes.
- reflexivity.
- |simplify.rewrite > associative_rtimes.
- reflexivity
- ]
- |cases z
- [reflexivity
- |simplify.rewrite > associative_rtimes.
- reflexivity.
- |simplify.rewrite > associative_rtimes.
- reflexivity
- ]
- ]
- ]
-qed.
-
-theorem Qtimes_OQ: \forall q.Qtimes q OQ = OQ.
-intro.cases q;reflexivity.
-qed.
-
-theorem symmetric_Qtimes: symmetric ? Qtimes.
-unfold.intros.
-cases x
- [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity
- |elim y
- [reflexivity
- |simplify.rewrite > symmetric_rtimes.reflexivity
- |simplify.rewrite > symmetric_rtimes.reflexivity
- ]
- |elim y
- [reflexivity
- |simplify.rewrite > symmetric_rtimes.reflexivity
- |simplify.rewrite > symmetric_rtimes.reflexivity
- ]
- ]
-qed.
-
-theorem Qtimes_Qinv: \forall q. q \neq OQ \to Qtimes q (Qinv q) = Qone.
-intro.
-cases q;intro
- [elim H.reflexivity
- |simplify.rewrite > rtimes_rinv.reflexivity
- |simplify.rewrite > rtimes_rinv.reflexivity
- ]
-qed.
-
-theorem eq_Qtimes_OQ_to_eq_OQ: \forall p,q.
-Qtimes p q = OQ \to p = OQ \lor q = OQ.
-intros 2.
-cases p
- [intro.left.reflexivity
- |cases q
- [intro.right.reflexivity
- |simplify.intro.destruct H
- |simplify.intro.destruct H
- ]
- |cases q
- [intro.right.reflexivity
- |simplify.intro.destruct H
- |simplify.intro.destruct H
- ]
- ]
-qed.
-
-theorem Qinv_Qtimes: \forall p,q.
-p \neq OQ \to q \neq OQ \to
-Qinv(Qtimes p q) =
-Qtimes (Qinv p) (Qinv q).
-intros.
-rewrite < Qtimes_Qone_q in ⊢ (? ? ? %).
-rewrite < (Qtimes_Qinv (Qtimes p q))
- [lapply (Qtimes_Qinv ? H).
- lapply (Qtimes_Qinv ? H1).
- rewrite > symmetric_Qtimes in ⊢ (? ? ? (? % ?)).
- rewrite > associative_Qtimes.
- rewrite > associative_Qtimes.
- rewrite < associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
- rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
- rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
- rewrite > Hletin1.
- rewrite > Qtimes_q_Qone.
- rewrite > Hletin.
- rewrite > Qtimes_q_Qone.
- reflexivity
- |intro.
- elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
- [apply (H H3)|apply (H1 H3)]
- ]
-qed.
-
-(* a stronger version, taking advantage of inv(O) = O *)
-theorem Qinv_Qtimes': \forall p,q.
-Qinv(Qtimes p q) =
-Qtimes (Qinv p) (Qinv q).
-intros.
-cases p
- [reflexivity
- |cases q
- [reflexivity
- |apply Qinv_Qtimes;intro;destruct H
- |apply Qinv_Qtimes;intro;destruct H
- ]
- |cases q
- [reflexivity
- |apply Qinv_Qtimes;intro;destruct H
- |apply Qinv_Qtimes;intro;destruct H
- ]
- ]
-qed.
-
theorem Qtimes_frac_frac: \forall p,q,r,s.
Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)).
intros.
rewrite < times_Qtimes.
reflexivity.
qed.
-
+*)
(* la prova seguente e' tutta una ripetizione. Sistemare. *)
(*CSC
definition denomQ:Q \to nat \def
\lambda q. defactorize (numeratorQ (Qinv q)).
-definition Qopp:Q \to Q \def \lambda q.
-match q with
-[OQ \Rightarrow OQ
-|Qpos q \Rightarrow Qneg q
-|Qneg q \Rightarrow Qpos q
-].
(*CSC
theorem frac_numQ_denomQ1: \forall r:ratio.
frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
projects / helm.git / blobdiff