]> matita.cs.unibo.it Git - helm.git/blob - matita/library/Q/q.ma
developments added
[helm.git] / 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 unfold injective.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 unfold injective.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.unfold Not. 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.unfold Not. 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.unfold Not. 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.unfold decidable.
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.unfold Not.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.unfold Not.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.unfold Not.intro.apply H.apply injective_nn.assumption.
198   simplify.apply not_eq_nn_cons.
199   intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
200   intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
201   intros.
202    simplify.
203    apply eqZb_elim.
204       intro.generalize in match H.elim (eqfb f1 g1).
205         simplify.apply eq_f2.assumption.
206         apply H2.
207       simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
208       intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
209 qed.
210
211 let rec finv f \def
212   match f with
213   [ (pp n) \Rightarrow (nn n)
214   | (nn n) \Rightarrow (pp n)
215   | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
216
217 definition Z_to_ratio :Z \to ratio \def
218 \lambda x:Z. match x with
219 [ OZ \Rightarrow one
220 | (pos n) \Rightarrow frac (pp n)
221 | (neg n) \Rightarrow frac (nn n)].
222
223 let rec ftimes f g \def
224   match f with
225   [ (pp n) \Rightarrow 
226     match g with
227     [(pp m) \Rightarrow Z_to_ratio (pos n + pos m)
228     | (nn m) \Rightarrow Z_to_ratio (pos n + neg m)
229     | (cons y g1) \Rightarrow frac (cons (pos n + y) g1)]
230   | (nn n) \Rightarrow 
231     match g with
232     [(pp m) \Rightarrow Z_to_ratio (neg n + pos m)
233     | (nn m) \Rightarrow Z_to_ratio (neg n + neg m)
234     | (cons y g1) \Rightarrow frac (cons (neg n + y) g1)]
235   | (cons x f1) \Rightarrow
236     match g with
237     [ (pp m) \Rightarrow frac (cons (x + pos m) f1)
238     | (nn m) \Rightarrow frac (cons (x + neg m) f1)
239     | (cons y g1) \Rightarrow 
240       match ftimes f1 g1 with
241         [ one \Rightarrow Z_to_ratio (x + y)
242         | (frac h) \Rightarrow frac (cons (x + y) h)]]].
243         
244 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
245 unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
246   intros.elim g.
247     change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)).
248      apply eq_f.apply sym_Zplus.
249     change with (Z_to_ratio (pos n + neg n1) = Z_to_ratio (neg n1 + pos n)).
250      apply eq_f.apply sym_Zplus.
251     change with (frac (cons (pos n + z) f) = frac (cons (z + pos n) f)).
252      rewrite < sym_Zplus.reflexivity.
253   intros.elim g.
254     change with (Z_to_ratio (neg n + pos n1) = Z_to_ratio (pos n1 + neg n)).
255      apply eq_f.apply sym_Zplus.
256     change with (Z_to_ratio (neg n + neg n1) = Z_to_ratio (neg n1 + neg n)).
257      apply eq_f.apply sym_Zplus.
258     change with (frac (cons (neg n + z) f) = frac (cons (z + neg n) f)).
259      rewrite < sym_Zplus.reflexivity.
260   intros.change with (frac (cons (x1 + pos m) f) = frac (cons (pos m + x1) f)).
261    rewrite < sym_Zplus.reflexivity.
262   intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
263    rewrite < sym_Zplus.reflexivity.
264   intros.
265    (*CSC: simplify does something nasty here because of a redex in Zplus *)
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    (*CSC: simplify does something nasty here because of a redex in Zplus *)
283 (* again: we would need something to help finding the right change *)
284   change with 
285   (match ftimes f1 (finv f1) with
286   [ one \Rightarrow Z_to_ratio (z + - z)
287   | (frac h) \Rightarrow frac (cons (z + - z) h)] = one).
288   rewrite > H.rewrite > Zplus_Zopp.reflexivity.
289 qed.
290
291 definition rtimes : ratio \to ratio \to ratio \def
292 \lambda r,s:ratio.
293   match r with
294   [one \Rightarrow s
295   | (frac f) \Rightarrow 
296       match s with 
297       [one \Rightarrow frac f
298       | (frac g) \Rightarrow ftimes f g]].
299
300 theorem symmetric_rtimes : symmetric ratio rtimes.
301 change with (\forall r,s:ratio. rtimes r s = rtimes s r).
302 intros.
303 elim r. elim s.
304 reflexivity.
305 reflexivity.
306 elim s.
307 reflexivity.
308 simplify.apply symmetric2_ftimes.
309 qed.
310
311 definition rinv : ratio \to ratio \def
312 \lambda r:ratio.
313   match r with
314   [one \Rightarrow one
315   | (frac f) \Rightarrow frac (finv f)].
316
317 theorem rtimes_rinv: \forall r:ratio. rtimes r (rinv r) = one.
318 intro.elim r.
319 reflexivity.
320 simplify.apply ftimes_finv.
321 qed.