]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/Q/q.ma
A few changes to factorization and gcd.
[helm.git] / helm / matita / library / Q / q.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/Q/q".
16
17 include "Z/compare.ma".
18 include "Z/plus.ma".
19
20 (* a fraction is a list of Z-coefficients for primes, in natural
21 order. The last coefficient must eventually be different from 0 *)
22
23 inductive fraction : Set \def
24   pp : nat \to fraction
25 | nn: nat \to fraction
26 | cons : Z \to fraction \to fraction.
27
28 inductive ratio : Set \def
29       one :  ratio
30     | frac : fraction \to ratio.
31
32 (* a rational number is either O or a ratio with a sign *)
33 inductive Q : Set \def 
34     OQ : Q
35   | Qpos : ratio  \to Q
36   | Qneg : ratio  \to Q.
37
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.
47 intros 7.elim f.
48   apply H.
49   apply H1.
50   elim g.
51     apply H2.
52     apply H3.
53     apply H4.apply H5.
54 qed. 
55
56 (* boolean equality *)
57 let rec eqfb f g \def
58 match f with
59 [ (pp n) \Rightarrow 
60   match g with 
61   [ (pp m) \Rightarrow eqb n m
62   | (nn m) \Rightarrow false
63   | (cons y g1) \Rightarrow false]
64 | (nn n) \Rightarrow 
65   match g with 
66   [ (pp m) \Rightarrow false
67   | (nn m) \Rightarrow eqb n m
68   | (cons y g1) \Rightarrow false] 
69 | (cons x f1) \Rightarrow 
70   match g with 
71   [ (pp m) \Rightarrow false
72   | (nn m) \Rightarrow false
73   | (cons y g1) \Rightarrow andb (eqZb x y) (eqfb f1 g1)]]. 
74
75 (* discrimination *)
76 definition aux \def
77   \lambda f. match f with
78     [ (pp n) \Rightarrow n
79     | (nn n) \Rightarrow n
80     | (cons x f) \Rightarrow O].
81
82 definition fhd \def
83 \lambda f. match f with
84     [ (pp n) \Rightarrow (pos n)
85     | (nn n) \Rightarrow (neg n)
86     | (cons x f) \Rightarrow x].
87
88 definition ftl \def
89 \lambda f. match f with
90     [ (pp n) \Rightarrow (pp n)
91     | (nn n) \Rightarrow (nn n)
92     | (cons x f) \Rightarrow f].
93     
94 theorem injective_pp : injective nat fraction pp.
95 simplify.intros.
96 change with (aux (pp x)) = (aux (pp y)).
97 apply eq_f.assumption.
98 qed.
99
100 theorem injective_nn : injective nat fraction nn.
101 simplify.intros.
102 change with (aux (nn x)) = (aux (nn y)).
103 apply eq_f.assumption.
104 qed.
105
106 theorem eq_cons_to_eq1: \forall f,g:fraction.\forall x,y:Z. 
107 (cons x f) = (cons y g) \to x = y.
108 intros.
109 change with (fhd (cons x f)) = (fhd (cons y g)).
110 apply eq_f.assumption.
111 qed.
112
113 theorem eq_cons_to_eq2: \forall x,y:Z.\forall f,g:fraction.
114 (cons x f) = (cons y g) \to f = g.
115 intros.
116 change with (ftl (cons x f)) = (ftl (cons y g)).
117 apply eq_f.assumption.
118 qed.
119
120 theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
121 intros.simplify. intro.
122 change with match (pp n) with
123 [ (pp n) \Rightarrow False
124 | (nn n) \Rightarrow True
125 | (cons x f) \Rightarrow True].
126 rewrite > H.
127 simplify.exact I.
128 qed.
129
130 theorem not_eq_pp_cons: 
131 \forall n:nat.\forall x:Z. \forall f:fraction. 
132 pp n \neq cons x f.
133 intros.simplify. intro.
134 change with match (pp n) with
135 [ (pp n) \Rightarrow False
136 | (nn n) \Rightarrow True
137 | (cons x f) \Rightarrow True].
138 rewrite > H.
139 simplify.exact I.
140 qed.
141
142 theorem not_eq_nn_cons: 
143 \forall n:nat.\forall x:Z. \forall f:fraction. 
144 nn n \neq cons x f.
145 intros.simplify. intro.
146 change with match (nn n) with
147 [ (pp n) \Rightarrow True
148 | (nn n) \Rightarrow False
149 | (cons x f) \Rightarrow True].
150 rewrite > H.
151 simplify.exact I.
152 qed.
153
154 theorem decidable_eq_fraction: \forall f,g:fraction.
155 decidable (f = g).
156 intros.simplify.
157 apply fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False)).
158   intros.elim g1.
159     elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
160       left.apply eq_f. assumption.
161       right.intro.apply H.apply injective_pp.assumption.
162     right.apply not_eq_pp_nn.
163     right.apply not_eq_pp_cons.
164   intros. elim g1.
165       right.intro.apply not_eq_pp_nn n1 n.apply sym_eq. assumption.
166       elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
167         left. apply eq_f. assumption.
168         right.intro.apply H.apply injective_nn.assumption.
169       right.apply not_eq_nn_cons.
170   intros.right.intro.apply not_eq_pp_cons m x f1.apply sym_eq.assumption.
171   intros.right.intro.apply not_eq_nn_cons m x f1.apply sym_eq.assumption.
172   intros.elim H.
173     elim ((decidable_eq_Z x y) : x=y \lor (x=y \to False)).
174       left.apply eq_f2.assumption.
175       assumption.
176     right.intro.apply H2.apply eq_cons_to_eq1 f1 g1.assumption.
177     right.intro.apply H1.apply eq_cons_to_eq2 x y f1 g1.assumption.
178 qed.
179
180 theorem eqfb_to_Prop: \forall f,g:fraction.
181 match (eqfb f g) with
182 [true \Rightarrow f=g
183 |false \Rightarrow f \neq g].
184 intros.apply fraction_elim2 
185 (\lambda f,g.match (eqfb f g) with
186 [true \Rightarrow f=g
187 |false \Rightarrow f \neq g]).
188   intros.elim g1.
189     simplify.apply eqb_elim.
190       intro.simplify.apply eq_f.assumption.
191       intro.simplify.intro.apply H.apply injective_pp.assumption.
192     simplify.apply not_eq_pp_nn.
193     simplify.apply not_eq_pp_cons.
194   intros.elim g1.
195     simplify.intro.apply not_eq_pp_nn n1 n.apply sym_eq. assumption.
196     simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
197     intro.simplify.intro.apply H.apply injective_nn.assumption.
198   simplify.apply not_eq_nn_cons.
199   intros.simplify.intro.apply not_eq_pp_cons m x f1.apply sym_eq. assumption.
200   intros.simplify.intro.apply not_eq_nn_cons m x f1.apply sym_eq. assumption.
201   intros.
202    change in match (eqfb (cons x f1) (cons y g1)) 
203    with (andb (eqZb x y) (eqfb f1 g1)).
204     apply eqZb_elim.
205       intro.generalize in match H.elim (eqfb f1 g1).
206         simplify.apply eq_f2.assumption.
207         apply H2.
208       simplify.intro.apply H2.apply eq_cons_to_eq2 x y.assumption.
209       intro.simplify.intro.apply H1.apply eq_cons_to_eq1 f1 g1.assumption.
210 qed.
211
212 let rec finv f \def
213   match f with
214   [ (pp n) \Rightarrow (nn n)
215   | (nn n) \Rightarrow (pp n)
216   | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
217
218 definition Z_to_ratio :Z \to ratio \def
219 \lambda x:Z. match x with
220 [ OZ \Rightarrow one
221 | (pos n) \Rightarrow frac (pp n)
222 | (neg n) \Rightarrow frac (nn n)].
223
224 let rec ftimes f g \def
225   match f with
226   [ (pp n) \Rightarrow 
227     match g with
228     [(pp m) \Rightarrow Z_to_ratio (pos n + pos m)
229     | (nn m) \Rightarrow Z_to_ratio (pos n + neg m)
230     | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)]
231   | (nn n) \Rightarrow 
232     match g with
233     [(pp m) \Rightarrow Z_to_ratio (neg n + pos m)
234     | (nn m) \Rightarrow Z_to_ratio (neg n + neg m)
235     | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)]
236   | (cons x f1) \Rightarrow
237     match g with
238     [ (pp m) \Rightarrow frac (cons (x + pos m) f1)
239     | (nn m) \Rightarrow frac (cons (x + neg m) f1)
240     | (cons y g1) \Rightarrow 
241       match ftimes f1 g1 with
242         [ one \Rightarrow Z_to_ratio (x + y)
243         | (frac h) \Rightarrow frac (cons (x + y) h)]]].
244         
245 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
246 simplify. intros.apply fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f).
247   intros.elim g.
248     change with Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n).
249      apply eq_f.apply sym_Zplus.
250     change with Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n).
251      apply eq_f.apply sym_Zplus.
252     change with frac (cons (pos n + z) f) = frac (cons (z + pos n) f).
253      rewrite < sym_Zplus.reflexivity.
254   intros.elim g.
255     change with Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n).
256      apply eq_f.apply sym_Zplus.
257     change with Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n).
258      apply eq_f.apply sym_Zplus.
259     change with frac (cons (neg n + z) f) = frac (cons (z + neg n) f).
260      rewrite < sym_Zplus.reflexivity.
261   intros.change with frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f).
262    rewrite < sym_Zplus.reflexivity.
263   intros.change with frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f).
264    rewrite < sym_Zplus.reflexivity.
265   intros.
266    change with 
267    match ftimes f g with
268    [ one \Rightarrow Z_to_ratio (x1 + y1)
269    | (frac h) \Rightarrow frac (cons (x1 + y1) h)] =
270    match ftimes g f with
271    [ one \Rightarrow Z_to_ratio (y1 + x1)
272    | (frac h) \Rightarrow frac (cons (y1 + x1) h)].
273     rewrite < H.rewrite < sym_Zplus.reflexivity.
274 qed.
275
276 theorem ftimes_finv : \forall f:fraction. ftimes f (finv f) = one.
277 intro.elim f.
278   change with Z_to_ratio (pos n + - (pos n)) = one.
279    rewrite > Zplus_Zopp.reflexivity.
280   change with Z_to_ratio (neg n + - (neg n)) = one.
281    rewrite > Zplus_Zopp.reflexivity.
282 (* again: we would need something to help finding the right change *)
283   change with 
284   match ftimes f1 (finv f1) with
285   [ one \Rightarrow Z_to_ratio (z + - z)
286   | (frac h) \Rightarrow frac (cons (z + - z) h)] = one.
287   rewrite > H.rewrite > Zplus_Zopp.reflexivity.
288 qed.
289
290 definition rtimes : ratio \to ratio \to ratio \def
291 \lambda r,s:ratio.
292   match r with
293   [one \Rightarrow s
294   | (frac f) \Rightarrow 
295       match s with 
296       [one \Rightarrow frac f
297       | (frac g) \Rightarrow ftimes f g]].
298
299 theorem symmetric_rtimes : symmetric ratio rtimes.
300 change with \forall r,s:ratio. rtimes r s = rtimes s r.
301 intros.
302 elim r. elim s.
303 reflexivity.
304 reflexivity.
305 elim s.
306 reflexivity.
307 simplify.apply symmetric2_ftimes.
308 qed.
309
310 definition rinv : ratio \to ratio \def
311 \lambda r:ratio.
312   match r with
313   [one \Rightarrow one
314   | (frac f) \Rightarrow frac (finv f)].
315
316 theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one.
317 intro.elim r.
318 reflexivity.
319 simplify.apply ftimes_finv.
320 qed.