1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
16 let rec nat_fact_to_fraction_inv l \def
18 [nf_last a \Rightarrow nn a
19 |nf_cons a p \Rightarrow
20 cons (neg_Z_of_nat a) (nat_fact_to_fraction_inv p)
24 definition nat_fact_all_to_Q_inv \def
27 [nfa_zero \Rightarrow OQ
28 |nfa_one \Rightarrow Qpos one
29 |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction_inv l))
33 definition nat_to_Q_inv \def
34 \lambda n. nat_fact_all_to_Q_inv (factorize n).
36 definition frac:nat \to nat \to Q \def
37 \lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
39 theorem Qtimes_frac_frac: \forall p,q,r,s.
40 Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)).
43 rewrite > associative_Qtimes.
44 rewrite < associative_Qtimes in ⊢ (? ? (? ? %) ?).
45 rewrite > symmetric_Qtimes in ⊢ (? ? (? ? (? % ?)) ?).
46 rewrite > associative_Qtimes in ⊢ (? ? (? ? %) ?).
47 rewrite < associative_Qtimes.
48 rewrite < times_Qtimes.
49 rewrite < Qinv_Qtimes'.
50 rewrite < times_Qtimes.
55 (* la prova seguente e' tutta una ripetizione. Sistemare. *)
57 theorem Qtimes1: \forall f:fraction.
58 Qtimes (nat_fact_all_to_Q (numerator f))
59 (Qinv (nat_fact_all_to_Q (numerator (finv f))))
65 |elim (or_numerator_nfa_one_nfa_proper f1)
68 cut (finv (nat_fact_to_fraction a) = f1)
71 rewrite > H2.rewrite > H1.simplify.
72 rewrite > Hcut.reflexivity
74 rewrite > H2.rewrite > H1.simplify.
75 rewrite > Hcut.reflexivity
77 rewrite > H2.rewrite > H1.simplify.
78 rewrite > Hcut.reflexivity
80 |generalize in match H.
81 rewrite > H2.rewrite > H1.simplify.
82 intro.destruct H3.assumption
87 rewrite > H2.rewrite > H2.simplify.
88 elim (or_numerator_nfa_one_nfa_proper (finv f1))
90 rewrite > H3.simplify.
91 cut (nat_fact_to_fraction a = f1)
92 [rewrite > Hcut.reflexivity
93 |generalize in match H.
96 rewrite > Qtimes_q_Qone.
102 generalize in match H.
104 rewrite > H3.simplify.
110 |simplify.rewrite > H2.simplify.
111 elim (or_numerator_nfa_one_nfa_proper (finv f1))
113 rewrite > H3.simplify.
114 cut (nat_fact_to_fraction a = f1)
115 [rewrite > Hcut.reflexivity
116 |generalize in match H.
119 rewrite > Qtimes_q_Qone.
125 generalize in match H.
127 rewrite > H3.simplify.
133 |simplify.rewrite > H2.simplify.
134 elim (or_numerator_nfa_one_nfa_proper (finv f1))
136 rewrite > H3.simplify.
137 cut (nat_fact_to_fraction a = f1)
138 [rewrite > Hcut.reflexivity
139 |generalize in match H.
142 rewrite > Qtimes_q_Qone.
148 generalize in match H.
150 rewrite > H3.simplify.
162 definition numQ:Q \to Z \def
166 |Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r)))
167 |Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r)))
171 definition numQ:Q \to nat \def
172 \lambda q. defactorize (numeratorQ q).
174 definition denomQ:Q \to nat \def
175 \lambda q. defactorize (numeratorQ (Qinv q)).
178 theorem frac_numQ_denomQ1: \forall r:ratio.
179 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
181 unfold frac.unfold denomQ.unfold numQ.
183 rewrite > factorize_defactorize.
184 rewrite > factorize_defactorize.
196 theorem frac_numQ_denomQ2: \forall r:ratio.
197 frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
199 unfold frac.unfold denomQ.unfold numQ.
201 rewrite > factorize_defactorize.
202 rewrite > factorize_defactorize.
213 definition Qabs:Q \to Q \def \lambda q.
216 |Qpos q \Rightarrow Qpos q
217 |Qneg q \Rightarrow Qpos q
220 theorem frac_numQ_denomQ: \forall q.
221 frac (numQ q) (denomQ q) = (Qabs q).
225 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
226 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
230 definition Qfrac: Z \to nat \to Q \def
231 \lambda z,n.match z with
233 |Zpos m \Rightarrow (frac (S m) n)
234 |Zneg m \Rightarrow Qopp (frac (S m) n)
237 definition QnumZ \def \lambda q.
240 |Qpos r \Rightarrow Z_of_nat (numQ (Qpos r))
241 |Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r))
244 theorem Qfrac_Z_of_nat: \forall n,m.
245 Qfrac (Z_of_nat n) m = frac n m.
246 intros.cases n;reflexivity.
249 theorem Qfrac_neg_Z_of_nat: \forall n,m.
250 Qfrac (neg_Z_of_nat n) m = Qopp (frac n m).
251 intros.cases n;reflexivity.
254 theorem Qfrac_QnumZ_denomQ: \forall q.
255 Qfrac (QnumZ q) (denomQ q) = q.
260 (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r).
261 rewrite > Qfrac_Z_of_nat.
262 apply frac_numQ_denomQ1.
263 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2