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 set "baseuri" "cic:/matita/library_autobatch/Q/q".
17 include "auto/Z/compare.ma".
18 include "auto/Z/plus.ma".
20 (* a fraction is a list of Z-coefficients for primes, in natural
21 order. The last coefficient must eventually be different from 0 *)
23 inductive fraction : Set \def
25 | nn: nat \to fraction
26 | cons : Z \to fraction \to fraction.
28 inductive ratio : Set \def
30 | frac : fraction \to ratio.
32 (* a rational number is either O or a ratio with a sign *)
33 inductive Q : Set \def
38 (* double elimination principles *)
39 theorem fraction_elim2:
40 \forall R:fraction \to fraction \to Prop.
41 (\forall n:nat.\forall g:fraction.R (pp n) g) \to
42 (\forall n:nat.\forall g:fraction.R (nn n) g) \to
43 (\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (pp m)) \to
44 (\forall x:Z.\forall f:fraction.\forall m:nat.R (cons x f) (nn m)) \to
45 (\forall x,y:Z.\forall f,g:fraction.R f g \to R (cons x f) (cons y g)) \to
46 \forall f,g:fraction. R f g.
61 (* boolean equality *)
66 [ (pp m) \Rightarrow eqb n m
67 | (nn m) \Rightarrow false
68 | (cons y g1) \Rightarrow false]
71 [ (pp m) \Rightarrow false
72 | (nn m) \Rightarrow eqb n m
73 | (cons y g1) \Rightarrow false]
74 | (cons x f1) \Rightarrow
76 [ (pp m) \Rightarrow false
77 | (nn m) \Rightarrow false
78 | (cons y g1) \Rightarrow andb (eqZb x y) (eqfb f1 g1)]].
82 \lambda f. match f with
83 [ (pp n) \Rightarrow n
84 | (nn n) \Rightarrow n
85 | (cons x f) \Rightarrow O].
88 \lambda f. match f with
89 [ (pp n) \Rightarrow (pos n)
90 | (nn n) \Rightarrow (neg n)
91 | (cons x f) \Rightarrow x].
94 \lambda f. match f with
95 [ (pp n) \Rightarrow (pp n)
96 | (nn n) \Rightarrow (nn n)
97 | (cons x f) \Rightarrow f].
99 theorem injective_pp : injective nat fraction pp.
102 change with ((aux(pp x)) = (aux (pp y))).
108 theorem injective_nn : injective nat fraction nn.
111 change with ((aux (nn x)) = (aux (nn y))).
117 theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z.
118 (cons x f) = (cons y g) \to x = y.
120 change with ((fhd (cons x f)) = (fhd (cons y g))).
122 (*apply eq_f.assumption.*)
125 theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction.
126 (cons x f) = (cons y g) \to f = g.
128 change with ((ftl (cons x f)) = (ftl (cons y g))).
130 (*apply eq_f.assumption.*)
133 theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
137 change with match (pp n) with
138 [ (pp n) \Rightarrow False
139 | (nn n) \Rightarrow True
140 | (cons x f) \Rightarrow True].
146 theorem not_eq_pp_cons:
147 \forall n:nat.\forall x:Z. \forall f:fraction.
152 change with match (pp n) with
153 [ (pp n) \Rightarrow False
154 | (nn n) \Rightarrow True
155 | (cons x f) \Rightarrow True].
161 theorem not_eq_nn_cons:
162 \forall n:nat.\forall x:Z. \forall f:fraction.
167 change with match (nn n) with
168 [ (pp n) \Rightarrow True
169 | (nn n) \Rightarrow False
170 | (cons x f) \Rightarrow True].
176 theorem decidable_eq_fraction: \forall f,g:fraction.
180 apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False)))
183 [ elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False))
200 apply not_eq_pp_cons*)
206 apply (not_eq_pp_nn n1 n).
210 | elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False))
224 apply not_eq_nn_cons*)
229 apply (not_eq_pp_cons m x f1).
236 apply (not_eq_nn_cons m x f1).
242 [ elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False))
251 apply (eq_cons_to_eq1 f1 g1).
258 apply (eq_cons_to_eq2 x y f1 g1).
264 theorem eqfb_to_Prop: \forall f,g:fraction.
265 match (eqfb f g) with
266 [true \Rightarrow f=g
267 |false \Rightarrow f \neq g].
269 apply (fraction_elim2
270 (\lambda f,g.match (eqfb f g) with
271 [true \Rightarrow f=g
272 |false \Rightarrow f \neq g]))
301 apply (not_eq_pp_nn n1 n).
328 apply (not_eq_pp_cons m x f1).
336 apply (not_eq_nn_cons m x f1).
344 generalize in match H.
349 | (*qui autobatch non chiude il goal*)
357 (*apply (eq_cons_to_eq2 x y).
366 apply (eq_cons_to_eq1 f1 g1).
374 [ (pp n) \Rightarrow (nn n)
375 | (nn n) \Rightarrow (pp n)
376 | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
378 definition Z_to_ratio :Z \to ratio \def
379 \lambda x:Z. match x with
381 | (pos n) \Rightarrow frac (pp n)
382 | (neg n) \Rightarrow frac (nn n)].
384 let rec ftimes f g \def
388 [(pp m) \Rightarrow Z_to_ratio (pos n + pos m)
389 | (nn m) \Rightarrow Z_to_ratio (pos n + neg m)
390 | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)]
393 [(pp m) \Rightarrow Z_to_ratio (neg n + pos m)
394 | (nn m) \Rightarrow Z_to_ratio (neg n + neg m)
395 | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)]
396 | (cons x f1) \Rightarrow
398 [ (pp m) \Rightarrow frac (cons (x + pos m) f1)
399 | (nn m) \Rightarrow frac (cons (x + neg m) f1)
400 | (cons y g1) \Rightarrow
401 match ftimes f1 g1 with
402 [ one \Rightarrow Z_to_ratio (x + y)
403 | (frac h) \Rightarrow frac (cons (x + y) h)]]].
405 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
408 apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f))
411 [ change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)).
415 | change with (Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n)).
419 | change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)).
421 (*rewrite < sym_Zplus.
426 [ change with (Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n)).
430 | change with (Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n)).
434 | change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)).
436 (*rewrite < sym_Zplus.
440 change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)).
442 (*rewrite < sym_Zplus.
445 change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
447 (*rewrite < sym_Zplus.
450 (*CSC: simplify does something nasty here because of a redex in Zplus *)
452 (match ftimes f g with
453 [ one \Rightarrow Z_to_ratio (x1 + y1)
454 | (frac h) \Rightarrow frac (cons (x1 + y1) h)] =
455 match ftimes g f with
456 [ one \Rightarrow Z_to_ratio (y1 + x1)
457 | (frac h) \Rightarrow frac (cons (y1 + x1) h)]).
464 theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one.
467 [ change with (Z_to_ratio (pos n + - (pos n)) = one).
469 (*rewrite > Zplus_Zopp.
471 | change with (Z_to_ratio (neg n + - (neg n)) = one).
473 (*rewrite > Zplus_Zopp.
476 (*CSC: simplify does something nasty here because of a redex in Zplus *)
477 (* again: we would need something to help finding the right change *)
479 (match ftimes f1 (finv f1) with
480 [ one \Rightarrow Z_to_ratio (z + - z)
481 | (frac h) \Rightarrow frac (cons (z + - z) h)] = one).
483 rewrite > Zplus_Zopp.
488 definition rtimes : ratio \to ratio \to ratio \def
492 | (frac f) \Rightarrow
494 [one \Rightarrow frac f
495 | (frac g) \Rightarrow ftimes f g]].
497 theorem symmetric_rtimes : symmetric ratio rtimes.
498 change with (\forall r,s:ratio. rtimes r s = rtimes s r).
505 apply symmetric2_ftimes
510 definition rinv : ratio \to ratio \def
514 | (frac f) \Rightarrow frac (finv f)].
516 theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one.