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.
56 definition numQ:Q \to Z \def
60 |Qpos r \Rightarrow Z_of_nat (defactorize (numeratorQ (Qpos r)))
61 |Qneg r \Rightarrow neg_Z_of_nat (defactorize (numeratorQ (Qpos r)))
65 definition numQ:Q \to nat \def
66 \lambda q. defactorize (numeratorQ q).
68 definition denomQ:Q \to nat \def
69 \lambda q. defactorize (numeratorQ (Qinv q)).
72 theorem frac_numQ_denomQ1: \forall r:ratio.
73 frac (numQ (Qpos r)) (denomQ (Qpos r)) = (Qpos r).
75 unfold frac.unfold denomQ.unfold numQ.
77 rewrite > factorize_defactorize.
78 rewrite > factorize_defactorize.
84 |apply Qtimes_numerator_denominator.
90 theorem frac_numQ_denomQ2: \forall r:ratio.
91 frac (numQ (Qneg r)) (denomQ (Qneg r)) = (Qpos r).
93 unfold frac.unfold denomQ.unfold numQ.
95 rewrite > factorize_defactorize.
96 rewrite > factorize_defactorize.
102 |apply Qtimes_numerator_denominator.
107 definition Qabs:Q \to Q \def \lambda q.
110 |Qpos q \Rightarrow Qpos q
111 |Qneg q \Rightarrow Qpos q
114 theorem frac_numQ_denomQ: \forall q.
115 frac (numQ q) (denomQ q) = (Qabs q).
119 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ1
120 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2
124 definition Qfrac: Z \to nat \to Q \def
125 \lambda z,n.match z with
127 |Zpos m \Rightarrow (frac (S m) n)
128 |Zneg m \Rightarrow Qopp (frac (S m) n)
131 definition QnumZ \def \lambda q.
134 |Qpos r \Rightarrow Z_of_nat (numQ (Qpos r))
135 |Qneg r \Rightarrow neg_Z_of_nat (numQ (Qpos r))
138 theorem Qfrac_Z_of_nat: \forall n,m.
139 Qfrac (Z_of_nat n) m = frac n m.
140 intros.cases n;reflexivity.
143 theorem Qfrac_neg_Z_of_nat: \forall n,m.
144 Qfrac (neg_Z_of_nat n) m = Qopp (frac n m).
145 intros.cases n;reflexivity.
148 theorem Qfrac_QnumZ_denomQ: \forall q.
149 Qfrac (QnumZ q) (denomQ q) = q.
154 (Qfrac (Z_of_nat (numQ (Qpos r))) (denomQ (Qpos r))=Qpos r).
155 rewrite > Qfrac_Z_of_nat.
156 apply frac_numQ_denomQ1.
157 |simplify in ⊢ (? ? ? %).apply frac_numQ_denomQ2