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).
37 definition frac:nat \to nat \to Q \def
38 \lambda p,q. Qtimes (nat_to_Q p) (Qinv (nat_to_Q q)).
40 let rec times_f h g \def
42 [nf_last a \Rightarrow
44 [nf_last b \Rightarrow nf_last (S (a+b))
45 |nf_cons b g1 \Rightarrow nf_cons (S (a+b)) g1
47 |nf_cons a h1 \Rightarrow
49 [nf_last b \Rightarrow nf_cons (S (a+b)) h1
50 |nf_cons b g1 \Rightarrow nf_cons (a+b) (times_f h1 g1)
55 definition times_fa \def
58 [nfa_zero \Rightarrow nfa_zero
59 |nfa_one \Rightarrow g
60 |nfa_proper f1 \Rightarrow match g with
61 [nfa_zero \Rightarrow nfa_zero
62 |nfa_one \Rightarrow nfa_proper f1
63 |nfa_proper g1 \Rightarrow nfa_proper (times_f f1 g1)
68 theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
69 =defactorize_aux g m*defactorize_aux h m.
71 [elim h;simplify;autobatch
74 |simplify.rewrite > (H n3 (S m)).autobatch
79 theorem eq_times_fa_times: \forall f,g.
80 defactorize (times_fa f g) = defactorize f*defactorize g.
84 |simplify.apply plus_n_O
88 |apply eq_times_f_times1
93 theorem eq_times_times_fa: \forall n,m.
94 factorize (n*m) = times_fa (factorize n) (factorize m).
96 rewrite <(factorize_defactorize (times_fa (factorize n) (factorize m))).
97 rewrite > eq_times_fa_times.
98 rewrite > defactorize_factorize.
99 rewrite > defactorize_factorize.
104 theorem eq_plus_Zplus: \forall n,m:nat. Z_of_nat (n+m) =
105 Z_of_nat n + Z_of_nat m.
109 [simplify.rewrite < plus_n_O.reflexivity
110 |simplify.reflexivity.
115 theorem times_f_ftimes: \forall n,m.
116 frac (nat_fact_to_fraction (times_f n m))
117 = ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m).
122 rewrite < plus_n_Sm.reflexivity
124 [simplify.rewrite < plus_n_O.reflexivity
125 |simplify.reflexivity.
130 [simplify.reflexivity
131 |simplify.rewrite < plus_n_Sm.reflexivity
134 cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h)
140 |apply injective_frac.
144 |generalize in match n4.
146 [cases n6;simplify;autobatch
160 theorem times_fa_Qtimes: \forall f,g. nat_fact_all_to_Q (times_fa f g) =
161 Qtimes (nat_fact_all_to_Q f) (nat_fact_all_to_Q g).
169 |rewrite > times_f_ftimes.reflexivity
174 theorem times_Qtimes: \forall p,q.
175 (nat_to_Q (p*q)) = Qtimes (nat_to_Q p) (nat_to_Q q).
176 intros.unfold nat_to_Q.
177 rewrite < times_fa_Qtimes.
178 rewrite < eq_times_times_fa.
182 theorem rtimes_Zplus3: \forall x,y:Z.\forall f,g:fraction.
183 (rtimes (frac f) (frac g) = one \land
184 rtimes (frac (cons x f)) (frac (cons y g)) = nat_frac_item_to_ratio (x + y))
185 \lor (\exists h.rtimes (frac f) (frac g) = frac h \land
186 rtimes (frac (cons x f)) (frac (cons y g)) =
187 frac (cons (x + y) h)).
190 elim (rtimes (frac f) (frac g));simplify
191 [left.split;reflexivity
193 apply (ex_intro ? ? f1).
198 theorem associative_Qtimes:associative ? Qtimes.
202 (* non posso scrivere 2,3: ... ?? *)
207 |simplify.rewrite > associative_rtimes.
209 |simplify.rewrite > associative_rtimes.
214 |simplify.rewrite > associative_rtimes.
216 |simplify.rewrite > associative_rtimes.
224 |simplify.rewrite > associative_rtimes.
226 |simplify.rewrite > associative_rtimes.
231 |simplify.rewrite > associative_rtimes.
233 |simplify.rewrite > associative_rtimes.
240 theorem Qtimes_OQ: \forall q.Qtimes q OQ = OQ.
241 intro.cases q;reflexivity.
244 theorem symmetric_Qtimes: symmetric ? Qtimes.
247 [simplify in ⊢ (? ? % ?).rewrite > Qtimes_OQ.reflexivity
250 |simplify.rewrite > symmetric_rtimes.reflexivity
251 |simplify.rewrite > symmetric_rtimes.reflexivity
255 |simplify.rewrite > symmetric_rtimes.reflexivity
256 |simplify.rewrite > symmetric_rtimes.reflexivity
261 theorem Qtimes_Qinv: \forall q. q \neq OQ \to Qtimes q (Qinv q) = Qone.
265 |simplify.rewrite > rtimes_rinv.reflexivity
266 |simplify.rewrite > rtimes_rinv.reflexivity
270 theorem eq_Qtimes_OQ_to_eq_OQ: \forall p,q.
271 Qtimes p q = OQ \to p = OQ \lor q = OQ.
274 [intro.left.reflexivity
276 [intro.right.reflexivity
277 |simplify.intro.destruct H
278 |simplify.intro.destruct H
281 [intro.right.reflexivity
282 |simplify.intro.destruct H
283 |simplify.intro.destruct H
288 theorem Qinv_Qtimes: \forall p,q.
289 p \neq OQ \to q \neq OQ \to
291 Qtimes (Qinv p) (Qinv q).
293 rewrite < Qtimes_Qone_q in ⊢ (? ? ? %).
294 rewrite < (Qtimes_Qinv (Qtimes p q))
295 [lapply (Qtimes_Qinv ? H).
296 lapply (Qtimes_Qinv ? H1).
297 rewrite > symmetric_Qtimes in ⊢ (? ? ? (? % ?)).
298 rewrite > associative_Qtimes.
299 rewrite > associative_Qtimes.
300 rewrite < associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
301 rewrite < symmetric_Qtimes in ⊢ (? ? ? (? ? (? ? (? % ?)))).
302 rewrite > associative_Qtimes in ⊢ (? ? ? (? ? (? ? %))).
304 rewrite > Qtimes_q_Qone.
306 rewrite > Qtimes_q_Qone.
309 elim (eq_Qtimes_OQ_to_eq_OQ ? ? H2)
310 [apply (H H3)|apply (H1 H3)]
314 (* a stronger version, taking advantage of inv(O) = O *)
315 theorem Qinv_Qtimes': \forall p,q.
317 Qtimes (Qinv p) (Qinv q).
323 |apply Qinv_Qtimes;intro;destruct H
324 |apply Qinv_Qtimes;intro;destruct H
328 |apply Qinv_Qtimes;intro;destruct H
329 |apply Qinv_Qtimes;intro;destruct H
334 theorem Qtimes_frac_frac: \forall p,q,r,s.
335 Qtimes (frac p q) (frac r s) = (frac (p*r) (q*s)).
338 rewrite > associative_Qtimes.
339 rewrite < associative_Qtimes in ⊢ (? ? (? ? %) ?).
340 rewrite > symmetric_Qtimes in ⊢ (? ? (? ? (? % ?)) ?).
341 rewrite > associative_Qtimes in ⊢ (? ? (? ? %) ?).
342 rewrite < associative_Qtimes.
343 rewrite < times_Qtimes.
344 rewrite < Qinv_Qtimes'.
345 rewrite < times_Qtimes.
350 (* la prova seguente e' tutta una ripetizione. Sistemare. *)
352 theorem Qtimes1: \forall f:fraction.
353 Qtimes (nat_fact_all_to_Q (numerator f))
354 (Qinv (nat_fact_all_to_Q (numerator (finv f))))
360 |elim (or_numerator_nfa_one_nfa_proper f1)
363 cut (finv (nat_fact_to_fraction a) = f1)
366 rewrite > H2.rewrite > H1.simplify.
367 rewrite > Hcut.reflexivity
369 rewrite > H2.rewrite > H1.simplify.
370 rewrite > Hcut.reflexivity
372 rewrite > H2.rewrite > H1.simplify.
373 rewrite > Hcut.reflexivity
375 |generalize in match H.
376 rewrite > H2.rewrite > H1.simplify.
377 intro.destruct H3.assumption
382 rewrite > H2.rewrite > H2.simplify.
383 elim (or_numerator_nfa_one_nfa_proper (finv f1))
385 rewrite > H3.simplify.
386 cut (nat_fact_to_fraction a = f1)
387 [rewrite > Hcut.reflexivity
388 |generalize in match H.
391 rewrite > Qtimes_q_Qone.
397 generalize in match H.
399 rewrite > H3.simplify.
405 |simplify.rewrite > H2.simplify.
406 elim (or_numerator_nfa_one_nfa_proper (finv f1))
408 rewrite > H3.simplify.
409 cut (nat_fact_to_fraction a = f1)
410 [rewrite > Hcut.reflexivity
411 |generalize in match H.
414 rewrite > Qtimes_q_Qone.
420 generalize in match H.
422 rewrite > H3.simplify.
428 |simplify.rewrite > H2.simplify.
429 elim (or_numerator_nfa_one_nfa_proper (finv f1))
431 rewrite > H3.simplify.
432 cut (nat_fact_to_fraction a = f1)
433 [rewrite > Hcut.reflexivity
434 |generalize in match H.
437 rewrite > Qtimes_q_Qone.
443 generalize in match H.
445 rewrite > H3.simplify.
457 definition numQ:Q \to Z \def
461 |Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r)))
462 |Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r)))
466 definition numQ:Q \to nat \def
467 \lambda q. defactorize (numeratorQ q).
469 definition denomQ:Q \to nat \def
470 \lambda q. defactorize (numeratorQ (Qinv q)).
472 definition Qopp:Q \to Q \def \lambda q.
475 |Qpos q \Rightarrow Qneg q
476 |Qneg q \Rightarrow Qpos q
479 theorem frac_numQ_denomQ1: \forall r:ratio.
480 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
482 unfold frac.unfold denomQ.unfold numQ.
484 rewrite > factorize_defactorize.
485 rewrite > factorize_defactorize.
497 theorem frac_numQ_denomQ2: \forall r:ratio.
498 frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
500 unfold frac.unfold denomQ.unfold numQ.
502 rewrite > factorize_defactorize.
503 rewrite > factorize_defactorize.
514 definition Qabs:Q \to Q \def \lambda q.
517 |Qpos q \Rightarrow Qpos q
518 |Qneg q \Rightarrow Qpos q
521 theorem frac_numQ_denomQ: \forall q.
522 frac (numQ q) (denomQ q) = (Qabs q).
526 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
527 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
531 definition Qfrac: Z \to nat \to Q \def
532 \lambda z,n.match z with
534 |Zpos m \Rightarrow (frac (S m) n)
535 |Zneg m \Rightarrow Qopp (frac (S m) n)
538 definition QnumZ \def \lambda q.
541 |Qpos r \Rightarrow Z_of_nat (numQ (Qpos r))
542 |Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r))
545 theorem Qfrac_Z_of_nat: \forall n,m.
546 Qfrac (Z_of_nat n) m = frac n m.
547 intros.cases n;reflexivity.
550 theorem Qfrac_neg_Z_of_nat: \forall n,m.
551 Qfrac (neg_Z_of_nat n) m = Qopp (frac n m).
552 intros.cases n;reflexivity.
555 theorem Qfrac_QnumZ_denomQ: \forall q.
556 Qfrac (QnumZ q) (denomQ q) = q.
561 (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r).
562 rewrite > Qfrac_Z_of_nat.
563 apply frac_numQ_denomQ1.
564 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2