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 (**************************************************************************)
15 include "Z/compare.ma".
17 include "nat/factorization.ma".
19 (* a fraction is a list of Z-coefficients for primes, in natural
20 order. The last coefficient must eventually be different from 0 *)
22 inductive fraction : Set \def
24 | nn: nat \to fraction
25 | cons : Z \to fraction \to fraction.
27 let rec fraction_of_nat_fact n ≝
30 | nf_cons m l ⇒ cons (Z_of_nat (S m)) (fraction_of_nat_fact l)
33 (* a fraction is integral if every coefficient is not negative *)
34 let rec nat_fact_of_integral_fraction n ≝
37 | nn _ ⇒ nf_last O (* dummy value *)
40 [ OZ ⇒ nf_cons O (nat_fact_of_integral_fraction l)
41 | pos n ⇒ nf_cons n (nat_fact_of_integral_fraction l)
42 | neg n ⇒ nf_last O (* dummy value *)
46 theorem nat_fact_of_integral_fraction_fraction_of_nat_fact:
47 ∀n. nat_fact_of_integral_fraction (fraction_of_nat_fact n) = n.
57 inductive ratio : Set \def
59 | frac : fraction \to ratio.
61 (* a rational number is either O or a ratio with a sign *)
62 inductive Q : Set \def
69 match factorize n with
72 | nfa_proper l ⇒ Qpos (frac (fraction_of_nat_fact l))
75 let rec enumerator_integral_fraction l ≝
80 match enumerator_integral_fraction r with
83 [ pos n ⇒ Some ? (pp n)
95 let rec denominator_integral_fraction l ≝
98 | nn n ⇒ Some ? (pp n)
100 match denominator_integral_fraction r with
103 [ neg n ⇒ Some ? (pp n)
110 | neg m ⇒ cons (pos m) r'
116 definition enumerator_of_fraction ≝
121 match enumerator_integral_fraction f with
123 | Some l ⇒ defactorize_aux (nat_fact_of_integral_fraction l) O
127 definition denominator_of_fraction ≝
132 match denominator_integral_fraction f with
134 | Some l ⇒ defactorize_aux (nat_fact_of_integral_fraction l) O
138 definition enumerator ≝
142 | Qpos r ⇒ (enumerator_of_fraction r : Z)
143 | Qneg r ⇒ neg(pred (enumerator_of_fraction r))
146 definition denominator ≝
150 | Qpos r ⇒ denominator_of_fraction r
151 | Qneg r ⇒ denominator_of_fraction r
154 (* double elimination principles *)
155 theorem fraction_elim2:
156 \forall R:fraction \to fraction \to Prop.
157 (\forall n:nat.\forall g:fraction.R (pp n) g) \to
158 (\forall n:nat.\forall g:fraction.R (nn n) g) \to
159 (\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (pp m)) \to
160 (\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (nn m)) \to
161 (\forall x,y:Z.\forall f,g:fraction.R f g \to R (cons x f) (cons y g)) \to
162 \forall f,g:fraction. R f g.
172 (* boolean equality *)
173 let rec eqfb f g \def
177 [ (pp m) \Rightarrow eqb n m
178 | (nn m) \Rightarrow false
179 | (cons y g1) \Rightarrow false]
182 [ (pp m) \Rightarrow false
183 | (nn m) \Rightarrow eqb n m
184 | (cons y g1) \Rightarrow false]
185 | (cons x f1) \Rightarrow
187 [ (pp m) \Rightarrow false
188 | (nn m) \Rightarrow false
189 | (cons y g1) \Rightarrow andb (eqZb x y) (eqfb f1 g1)]].
193 \lambda f. match f with
194 [ (pp n) \Rightarrow n
195 | (nn n) \Rightarrow n
196 | (cons x f) \Rightarrow O].
199 \lambda f. match f with
200 [ (pp n) \Rightarrow (pos n)
201 | (nn n) \Rightarrow (neg n)
202 | (cons x f) \Rightarrow x].
205 \lambda f. match f with
206 [ (pp n) \Rightarrow (pp n)
207 | (nn n) \Rightarrow (nn n)
208 | (cons x f) \Rightarrow f].
210 theorem injective_pp : injective nat fraction pp.
211 unfold injective.intros.
212 change with ((aux (pp x)) = (aux (pp y))).
213 apply eq_f.assumption.
216 theorem injective_nn : injective nat fraction nn.
217 unfold injective.intros.
218 change with ((aux (nn x)) = (aux (nn y))).
219 apply eq_f.assumption.
222 theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z.
223 (cons x f) = (cons y g) \to x = y.
225 change with ((fhd (cons x f)) = (fhd (cons y g))).
226 apply eq_f.assumption.
229 theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction.
230 (cons x f) = (cons y g) \to f = g.
232 change with ((ftl (cons x f)) = (ftl (cons y g))).
233 apply eq_f.assumption.
236 theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
237 intros.unfold Not. intro.
238 change with match (pp n) with
239 [ (pp n) \Rightarrow False
240 | (nn n) \Rightarrow True
241 | (cons x f) \Rightarrow True].
246 theorem not_eq_pp_cons:
247 \forall n:nat.\forall x:Z. \forall f:fraction.
249 intros.unfold Not. intro.
250 change with match (pp n) with
251 [ (pp n) \Rightarrow False
252 | (nn n) \Rightarrow True
253 | (cons x f) \Rightarrow True].
258 theorem not_eq_nn_cons:
259 \forall n:nat.\forall x:Z. \forall f:fraction.
261 intros.unfold Not. intro.
262 change with match (nn n) with
263 [ (pp n) \Rightarrow True
264 | (nn n) \Rightarrow False
265 | (cons x f) \Rightarrow True].
270 theorem decidable_eq_fraction: \forall f,g:fraction.
272 intros.unfold decidable.
273 apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))).
275 elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
276 left.apply eq_f. assumption.
277 right.intro.apply H.apply injective_pp.assumption.
278 right.apply not_eq_pp_nn.
279 right.apply not_eq_pp_cons.
281 right.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
282 elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
283 left. apply eq_f. assumption.
284 right.intro.apply H.apply injective_nn.assumption.
285 right.apply not_eq_nn_cons.
286 intros.right.intro.apply (not_eq_pp_cons m x f1).apply sym_eq.assumption.
287 intros.right.intro.apply (not_eq_nn_cons m x f1).apply sym_eq.assumption.
289 elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False)).
290 left.apply eq_f2.assumption.
292 right.intro.apply H2.apply (eq_cons_to_eq1 f1 g1).assumption.
293 right.intro.apply H1.apply (eq_cons_to_eq2 x y f1 g1).assumption.
296 theorem eqfb_to_Prop: \forall f,g:fraction.
297 match (eqfb f g) with
298 [true \Rightarrow f=g
299 |false \Rightarrow f \neq g].
300 intros.apply (fraction_elim2
301 (\lambda f,g.match (eqfb f g) with
302 [true \Rightarrow f=g
303 |false \Rightarrow f \neq g])).
305 simplify.apply eqb_elim.
306 intro.simplify.apply eq_f.assumption.
307 intro.simplify.unfold Not.intro.apply H.apply injective_pp.assumption.
308 simplify.apply not_eq_pp_nn.
309 simplify.apply not_eq_pp_cons.
311 simplify.unfold Not.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
312 simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
313 intro.simplify.unfold Not.intro.apply H.apply injective_nn.assumption.
314 simplify.apply not_eq_nn_cons.
315 intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
316 intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
320 intro.generalize in match H.elim (eqfb f1 g1).
321 simplify.apply eq_f2.assumption.
323 simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
324 intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.