1 | (**************************************************************************) |
---|
2 | (* ___ *) |
---|
3 | (* ||M|| *) |
---|
4 | (* ||A|| A project by Andrea Asperti *) |
---|
5 | (* ||T|| *) |
---|
6 | (* ||I|| Developers: *) |
---|
7 | (* ||T|| The HELM team. *) |
---|
8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
9 | (* \ / *) |
---|
10 | (* \ / This file is distributed under the terms of the *) |
---|
11 | (* v GNU General Public License Version 2 *) |
---|
12 | (* *) |
---|
13 | (**************************************************************************) |
---|
14 | |
---|
15 | include "datatypes/sums.ma". |
---|
16 | include "datatypes/list.ma". |
---|
17 | include "Plogic/equality.ma". |
---|
18 | include "binary/Z.ma". |
---|
19 | include "binary/positive.ma". |
---|
20 | |
---|
21 | nlemma eq_rect_Type0_r: |
---|
22 | ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. |
---|
23 | #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ??? p0); nassumption. |
---|
24 | nqed. |
---|
25 | |
---|
26 | nlemma eq_rect_r2: |
---|
27 | ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p. |
---|
28 | #A; #a; #x; #p; ncases p; #P; #H; nassumption. |
---|
29 | nqed. |
---|
30 | |
---|
31 | nlemma eq_rect_Type2_r: |
---|
32 | ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. |
---|
33 | #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r2 ??? p0); nassumption. |
---|
34 | nqed. |
---|
35 | |
---|
36 | nlemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x. |
---|
37 | #A;#x;#y;*;#H;napply nmk;#H';/2/; |
---|
38 | nqed. |
---|
39 | |
---|
40 | (* stolen from logic/connectives.ma to give Prop version. *) |
---|
41 | notation > "hvbox(a break \liff b)" |
---|
42 | left associative with precedence 25 |
---|
43 | for @{ 'iff $a $b }. |
---|
44 | |
---|
45 | notation "hvbox(a break \leftrightarrow b)" |
---|
46 | left associative with precedence 25 |
---|
47 | for @{ 'iff $a $b }. |
---|
48 | |
---|
49 | interpretation "logical iff" 'iff x y = (iff x y). |
---|
50 | |
---|
51 | (* bool *) |
---|
52 | |
---|
53 | ndefinition xorb : bool → bool → bool ≝ |
---|
54 | λx,y. match x with [ false ⇒ y | true ⇒ notb y ]. |
---|
55 | |
---|
56 | |
---|
57 | (* TODO: move to Z.ma *) |
---|
58 | |
---|
59 | nlemma eqZb_z_z : ∀z.eqZb z z = true. |
---|
60 | #z;ncases z;nnormalize;//; |
---|
61 | nqed. |
---|
62 | |
---|
63 | (* XXX: divides goes to arithmetics *) |
---|
64 | ninductive dividesP (n,m:Pos) : Prop ≝ |
---|
65 | | witness : ∀p:Pos.m = times n p → dividesP n m. |
---|
66 | interpretation "positive divides" 'divides n m = (dividesP n m). |
---|
67 | interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)). |
---|
68 | |
---|
69 | ndefinition dividesZ : Z → Z → Prop ≝ |
---|
70 | λx,y. match x with |
---|
71 | [ OZ ⇒ False |
---|
72 | | pos n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ] |
---|
73 | | neg n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ] |
---|
74 | ]. |
---|
75 | |
---|
76 | interpretation "integer divides" 'divides n m = (dividesZ n m). |
---|
77 | interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)). |
---|
78 | |
---|
79 | (* should be proved in nat.ma, but it's not! *) |
---|
80 | naxiom eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. |
---|
81 | |
---|
82 | nlemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. |
---|
83 | #n m; napply eqb_elim; //; nqed. |
---|
84 | |
---|
85 | nlemma injective_Z_of_nat : injective ? ? Z_of_nat. |
---|
86 | nnormalize; |
---|
87 | #n;#m;ncases n;ncases m;nnormalize;//; |
---|
88 | ##[ ##1,2: #n';#H;ndestruct |
---|
89 | ##| #n';#m'; #H; ndestruct; nrewrite > (succ_pos_of_nat_inj … e0); // |
---|
90 | ##] nqed. |
---|
91 | |
---|
92 | nlemma reflexive_Zle : reflexive ? Zle. |
---|
93 | #x; ncases x; //; nqed. |
---|
94 | |
---|
95 | nlemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n). |
---|
96 | #n;ncases n;nnormalize;//;nqed. |
---|
97 | |
---|
98 | nlemma Zsucc_le : ∀x:Z. x ≤ Zsucc x. |
---|
99 | #x; ncases x; //; |
---|
100 | #n; ncases n; //; nqed. |
---|
101 | |
---|
102 | nlemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n. |
---|
103 | #x;#y; |
---|
104 | napply pos_elim |
---|
105 | ##[ ##2: #n'; #IH; ##] |
---|
106 | nrewrite > (Zplus_Zsucc_Zpred y ?); |
---|
107 | ##[ nrewrite > (Zpred_Zsucc (pos n')); |
---|
108 | #H; napply (transitive_Zle ??? (IH H)); nrewrite > (Zplus_Zsucc ??); |
---|
109 | napply Zsucc_le; |
---|
110 | ##| #H; napply (transitive_Zle ??? H); nrewrite > (Zplus_z_OZ ?); napply Zsucc_le; |
---|
111 | ##] nqed. |
---|
112 | |
---|
113 | (* XXX: Zmax must go to arithmetics *) |
---|
114 | ndefinition Zmax : Z → Z → Z ≝ |
---|
115 | λx,y.match Z_compare x y with |
---|
116 | [ LT ⇒ y |
---|
117 | | _ ⇒ x ]. |
---|
118 | |
---|
119 | nlemma Zmax_l: ∀x,y. x ≤ Zmax x y. |
---|
120 | #x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y); |
---|
121 | /3/; nqed. |
---|
122 | |
---|
123 | nlemma Zmax_r: ∀x,y. y ≤ Zmax x y. |
---|
124 | #x;#y;nwhd in ⊢ (??%); nlapply (Z_compare_to_Prop x y); ncases (Z_compare x y); |
---|
125 | /3/; #H; nrewrite > H; //; nqed. |
---|
126 | |
---|
127 | ntheorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y. |
---|
128 | #x y; ncases x; |
---|
129 | ##[ ncases y; |
---|
130 | ##[ ##1,2: // |
---|
131 | ##| #n; napply False_ind; |
---|
132 | ##] |
---|
133 | ##| #n; ncases y; |
---|
134 | ##[ nnormalize; napply False_ind; |
---|
135 | ##| #m; napply (pos_cases … n); /2/; |
---|
136 | ##| #m; nnormalize; napply False_ind; |
---|
137 | ##] |
---|
138 | ##| #n; ncases y; /2/; |
---|
139 | ##] nqed. |
---|
140 | |
---|
141 | ntheorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p. |
---|
142 | #n m p Hlt Hle; nrewrite < (Zpred_Zsucc n); napply Zle_to_Zlt; |
---|
143 | napply (transitive_Zle … Hle); /2/; |
---|
144 | nqed. |
---|
145 | |
---|
146 | ndefinition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2). |
---|
147 | #z1;#z2;nlapply (eqZb_to_Prop z1 z2);ncases (eqZb z1 z2);nnormalize;#H; |
---|
148 | ##[@;// |
---|
149 | ##|@2;//##] |
---|
150 | nqed. |
---|
151 | |
---|
152 | nlemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false. |
---|
153 | #z1;#z2;nlapply (eqZb_to_Prop z1 z2); ncases (eqZb z1 z2); //; |
---|
154 | #H; #H'; napply False_ind; napply (absurd ? H H'); |
---|
155 | nqed. |
---|
156 | |
---|
157 | (* Z.ma *) |
---|
158 | |
---|
159 | ndefinition Zge: Z → Z → Prop ≝ |
---|
160 | λn,m:Z.m ≤ n. |
---|
161 | |
---|
162 | interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y). |
---|
163 | |
---|
164 | ndefinition Zgt: Z → Z → Prop ≝ |
---|
165 | λn,m:Z.m<n. |
---|
166 | |
---|
167 | interpretation "integer 'greater than'" 'gt x y = (Zgt x y). |
---|
168 | |
---|
169 | interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)). |
---|
170 | |
---|
171 | ndefinition Zleb : Z → Z → bool ≝ |
---|
172 | λx,y:Z. |
---|
173 | match x with |
---|
174 | [ OZ ⇒ |
---|
175 | match y with |
---|
176 | [ OZ ⇒ true |
---|
177 | | pos m ⇒ true |
---|
178 | | neg m ⇒ false ] |
---|
179 | | pos n ⇒ |
---|
180 | match y with |
---|
181 | [ OZ ⇒ false |
---|
182 | | pos m ⇒ leb n m |
---|
183 | | neg m ⇒ false ] |
---|
184 | | neg n ⇒ |
---|
185 | match y with |
---|
186 | [ OZ ⇒ true |
---|
187 | | pos m ⇒ true |
---|
188 | | neg m ⇒ leb m n ]]. |
---|
189 | |
---|
190 | ndefinition Zltb : Z → Z → bool ≝ |
---|
191 | λx,y:Z. |
---|
192 | match x with |
---|
193 | [ OZ ⇒ |
---|
194 | match y with |
---|
195 | [ OZ ⇒ false |
---|
196 | | pos m ⇒ true |
---|
197 | | neg m ⇒ false ] |
---|
198 | | pos n ⇒ |
---|
199 | match y with |
---|
200 | [ OZ ⇒ false |
---|
201 | | pos m ⇒ leb (succ n) m |
---|
202 | | neg m ⇒ false ] |
---|
203 | | neg n ⇒ |
---|
204 | match y with |
---|
205 | [ OZ ⇒ true |
---|
206 | | pos m ⇒ true |
---|
207 | | neg m ⇒ leb (succ m) n ]]. |
---|
208 | |
---|
209 | |
---|
210 | |
---|
211 | ntheorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true. |
---|
212 | #n;#m;ncases n;ncases m; //; |
---|
213 | ##[ ##1,2: #m'; nnormalize; #H; napply (False_ind ? H) |
---|
214 | ##| ##3,5: #n';#m'; nnormalize; napply le_to_leb_true; |
---|
215 | ##| ##4: #n';#m'; nnormalize; #H; napply (False_ind ? H) |
---|
216 | ##] nqed. |
---|
217 | |
---|
218 | ntheorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m. |
---|
219 | #n;#m;ncases n;ncases m; //; |
---|
220 | ##[ ##1,2: #m'; nnormalize; #H; ndestruct |
---|
221 | ##| ##3,5: #n';#m'; nnormalize; napply leb_true_to_le; |
---|
222 | ##| ##4: #n';#m'; nnormalize; #H; ndestruct |
---|
223 | ##] nqed. |
---|
224 | |
---|
225 | ntheorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m. |
---|
226 | #n m H. @; #H'; nrewrite > (Zle_to_Zleb_true … H') in H; #H; ndestruct; |
---|
227 | nqed. |
---|
228 | |
---|
229 | ntheorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true. |
---|
230 | #n;#m;ncases n;ncases m; //; |
---|
231 | ##[ nnormalize; #H; napply (False_ind ? H) |
---|
232 | ##| ##2,3: #m'; nnormalize; #H; napply (False_ind ? H) |
---|
233 | ##| ##4,6: #n';#m'; nnormalize; napply le_to_leb_true; |
---|
234 | ##| #n';#m'; nnormalize; #H; napply (False_ind ? H) |
---|
235 | ##] nqed. |
---|
236 | |
---|
237 | ntheorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m. |
---|
238 | #n;#m;ncases n;ncases m; //; |
---|
239 | ##[ nnormalize; #H; ndestruct |
---|
240 | ##| ##2,3: #m'; nnormalize; #H; ndestruct |
---|
241 | ##| ##4,6: #n';#m'; napply leb_true_to_le; |
---|
242 | ##| #n';#m'; nnormalize; #H; ndestruct |
---|
243 | ##] nqed. |
---|
244 | |
---|
245 | ntheorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m. |
---|
246 | #n m H; @; #H'; nrewrite > (Zlt_to_Zltb_true … H') in H; #H; ndestruct; |
---|
247 | nqed. |
---|
248 | |
---|
249 | ntheorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. |
---|
250 | (n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m). |
---|
251 | #n;#m;#P;#Hle;#Hnle; |
---|
252 | nlapply (refl ? (Zleb n m)); |
---|
253 | nelim (Zleb n m) in ⊢ ((???%)→%); |
---|
254 | #Hb; |
---|
255 | ##[ napply Hle; napply (Zleb_true_to_Zle … Hb) |
---|
256 | ##| napply Hnle; napply (Zleb_false_to_not_Zle … Hb) |
---|
257 | ##] nqed. |
---|
258 | |
---|
259 | ntheorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. |
---|
260 | (n < m → P true) → (n ≮ m → P false) → P (Zltb n m). |
---|
261 | #n;#m;#P;#Hlt;#Hnlt; |
---|
262 | nlapply (refl ? (Zltb n m)); |
---|
263 | nelim (Zltb n m) in ⊢ ((???%)→%); |
---|
264 | #Hb; |
---|
265 | ##[ napply Hlt; napply (Zltb_true_to_Zlt … Hb) |
---|
266 | ##| napply Hnlt; napply (Zltb_false_to_not_Zlt … Hb) |
---|
267 | ##] nqed. |
---|
268 | |
---|
269 | ndefinition Z_times : Z → Z → Z ≝ |
---|
270 | λx,y. match x with |
---|
271 | [ OZ ⇒ OZ |
---|
272 | | pos n ⇒ |
---|
273 | match y with |
---|
274 | [ OZ ⇒ OZ |
---|
275 | | pos m ⇒ pos (n*m) |
---|
276 | | neg m ⇒ neg (n*m) |
---|
277 | ] |
---|
278 | | neg n ⇒ |
---|
279 | match y with |
---|
280 | [ OZ ⇒ OZ |
---|
281 | | pos m ⇒ neg (n*m) |
---|
282 | | neg m ⇒ pos (n*m) |
---|
283 | ] |
---|
284 | ]. |
---|
285 | interpretation "integer multiplication" 'times x y = (Z_times x y). |
---|
286 | |
---|
287 | (* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *) |
---|
288 | notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. |
---|
289 | notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. |
---|
290 | interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f). |
---|
291 | |
---|
292 | (* datatypes/list.ma *) |
---|
293 | |
---|
294 | ntheorem nil_append_nil_both: |
---|
295 | ∀A:Type. ∀l1,l2:list A. |
---|
296 | l1 @ l2 = [] → l1 = [] ∧ l2 = []. |
---|
297 | #A l1 l2; ncases l1; |
---|
298 | ##[ ncases l2; |
---|
299 | ##[ /2/ |
---|
300 | ##| #h t H; ndestruct; |
---|
301 | ##] |
---|
302 | ##| ncases l2; |
---|
303 | ##[ nnormalize; #h t H; ndestruct; |
---|
304 | ##| nnormalize; #h1 t1 h2 h3 H; ndestruct; |
---|
305 | ##] |
---|
306 | ##] nqed. |
---|
307 | |
---|
308 | (* division *) |
---|
309 | |
---|
310 | ninductive natp : Type ≝ |
---|
311 | | pzero : natp |
---|
312 | | ppos : Pos → natp. |
---|
313 | |
---|
314 | ndefinition natp0 ≝ |
---|
315 | λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ]. |
---|
316 | |
---|
317 | ndefinition natp1 ≝ |
---|
318 | λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ]. |
---|
319 | |
---|
320 | nlet rec divide (m,n:Pos) on m ≝ |
---|
321 | match m with |
---|
322 | [ one ⇒ |
---|
323 | match n with |
---|
324 | [ one ⇒ 〈ppos one,pzero〉 |
---|
325 | | _ ⇒ 〈pzero,ppos one〉 |
---|
326 | ] |
---|
327 | | p0 m' ⇒ |
---|
328 | match divide m' n with |
---|
329 | [ mk_pair q r ⇒ |
---|
330 | match r with |
---|
331 | [ pzero ⇒ 〈natp0 q,pzero〉 |
---|
332 | | ppos r' ⇒ |
---|
333 | match partial_minus (p0 r') n with |
---|
334 | [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉 |
---|
335 | | MinusZero ⇒ 〈natp1 q, pzero〉 |
---|
336 | | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉 |
---|
337 | ] |
---|
338 | ] |
---|
339 | ] |
---|
340 | | p1 m' ⇒ |
---|
341 | match divide m' n with |
---|
342 | [ mk_pair q r ⇒ |
---|
343 | match r with |
---|
344 | [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ] |
---|
345 | | ppos r' ⇒ |
---|
346 | match partial_minus (p1 r') n with |
---|
347 | [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉 |
---|
348 | | MinusZero ⇒ 〈natp1 q, pzero〉 |
---|
349 | | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉 |
---|
350 | ] |
---|
351 | ] |
---|
352 | ] |
---|
353 | ]. |
---|
354 | |
---|
355 | ndefinition div ≝ λm,n. fst ?? (divide m n). |
---|
356 | ndefinition mod ≝ λm,n. snd ?? (divide m n). |
---|
357 | |
---|
358 | ndefinition pairdisc ≝ |
---|
359 | λA,B.λx,y:pair A B. |
---|
360 | match x with |
---|
361 | [(mk_pair t0 t1) ⇒ |
---|
362 | match y with |
---|
363 | [(mk_pair u0 u1) ⇒ |
---|
364 | ∀P: Type[1]. |
---|
365 | (∀e0: (eq A (R0 ? t0) u0). |
---|
366 | ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ]. |
---|
367 | |
---|
368 | nlemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y. |
---|
369 | #A;#B;#x;#y;#e;nrewrite > e;ncases y; |
---|
370 | #a;#b;nnormalize;#P;#PH;napply PH;@; |
---|
371 | nqed. |
---|
372 | |
---|
373 | nlemma pred_minus: ∀n,m. pred n - m = pred (n-m). |
---|
374 | napply pos_elim; /3/; |
---|
375 | nqed. |
---|
376 | |
---|
377 | nlemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p. |
---|
378 | napply pos_elim; |
---|
379 | ##[ // |
---|
380 | ##| #n IH m p; nrewrite > (succ_plus_one …); nrewrite > (IH m one); /2/; |
---|
381 | ##] nqed. |
---|
382 | |
---|
383 | ntheorem plus_minus_r: |
---|
384 | ∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m. |
---|
385 | #m;#n;#p;#le;nrewrite > (symmetric_plus …); |
---|
386 | nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed. |
---|
387 | |
---|
388 | nlemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p. |
---|
389 | #m;#n;#p;nelim m;/2/; nqed. |
---|
390 | (* |
---|
391 | nlemma le_to_minus: ∀m,n. m≤n → m-n = 0. |
---|
392 | #m;#n;nelim n; |
---|
393 | ##[ nrewrite < (minus_n_O …); /2/; |
---|
394 | ##| #n'; #IH; #le; ninversion le; /2/; #n''; #A;#B;#C; ndestruct; |
---|
395 | nrewrite > (eq_minus_S_pred …); nrewrite > (IH A); /2/ |
---|
396 | ##] nqed. |
---|
397 | *) |
---|
398 | nlemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n). |
---|
399 | #n;#m;#p;(*nelim (decidable_lt n m);*)#lt; |
---|
400 | (*##[*) napply (pos_elim … p); //;#p'; #IH; |
---|
401 | nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); |
---|
402 | nrewrite > (minus_plus_distrib …); |
---|
403 | nrewrite < (plus_minus … lt); nrewrite < IH; |
---|
404 | nrewrite > (plus_minus_r …); /2/; |
---|
405 | nqed. |
---|
406 | (*##| |
---|
407 | nlapply (not_lt_to_le … lt); #le; |
---|
408 | napply (pos_elim … p); //; #p'; |
---|
409 | ncut (m-n = one); ##[ /3/ ##] |
---|
410 | #mn; nrewrite > mn; nrewrite > (times_n_one …); nrewrite > (times_n_one …); |
---|
411 | #H; nrewrite < H in ⊢ (???%); |
---|
412 | napply sym_eq; napply le_n_one_to_eq; nrewrite < H; |
---|
413 | nrewrite > (minus_plus_distrib …); napply monotonic_le_minus_l; |
---|
414 | /2/; |
---|
415 | ##] nqed. |
---|
416 | |
---|
417 | nlemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n. |
---|
418 | #m;#n;#H;nlapply (refl ? (m-n));nelim (m-n) in ⊢ (???% → %);//; |
---|
419 | #H'; nlapply (minus_to_plus … H'); /2/; |
---|
420 | nrewrite < (plus_n_O …); #H''; nrewrite > H'' in H; #H; |
---|
421 | napply False_ind; napply (absurd ? H ( not_le_Sn_n n)); |
---|
422 | nqed. |
---|
423 | *) |
---|
424 | |
---|
425 | nlet rec natp_plus (n,m:natp) ≝ |
---|
426 | match n with |
---|
427 | [ pzero ⇒ m |
---|
428 | | ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ] |
---|
429 | ]. |
---|
430 | |
---|
431 | nlet rec natp_times (n,m:natp) ≝ |
---|
432 | match n with |
---|
433 | [ pzero ⇒ pzero |
---|
434 | | ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ] |
---|
435 | ]. |
---|
436 | |
---|
437 | ninductive natp_lt : natp → Pos → Prop ≝ |
---|
438 | | plt_zero : ∀n. natp_lt pzero n |
---|
439 | | plt_pos : ∀n,m. n < m → natp_lt (ppos n) m. |
---|
440 | |
---|
441 | nlemma lt_p0: ∀n:Pos. one < p0 n. |
---|
442 | #n; nnormalize; /2/; nqed. |
---|
443 | |
---|
444 | nlemma lt_p1: ∀n:Pos. one < p1 n. |
---|
445 | #n'; nnormalize; nrewrite > (?:p1 n' = succ (p0 n')); //; nqed. |
---|
446 | |
---|
447 | nlemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉. |
---|
448 | #m; nelim m; |
---|
449 | ##[ //; |
---|
450 | ##| ##2,3: #m' IH; nnormalize; nrewrite > IH; //; |
---|
451 | ##] nqed. |
---|
452 | |
---|
453 | nlemma pos_nonzero2: ∀n. ∀P:Pos→Type. ∀Q:Type. match succ n with [ one ⇒ Q | p0 p ⇒ P (p0 p) | p1 p ⇒ P (p1 p) ] = P (succ n). |
---|
454 | #n P Q; napply succ_elim; /2/; nqed. |
---|
455 | |
---|
456 | nlemma partial_minus_to_Prop: ∀n,m. |
---|
457 | match partial_minus n m with |
---|
458 | [ MinusNeg ⇒ n < m |
---|
459 | | MinusZero ⇒ n = m |
---|
460 | | MinusPos r ⇒ n = m+r |
---|
461 | ]. |
---|
462 | #n m; nlapply (pos_compare_to_Prop n m); nlapply (minus_to_plus n m); |
---|
463 | nnormalize; ncases (partial_minus n m); /2/; nqed. |
---|
464 | |
---|
465 | nlemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m. |
---|
466 | #n m lt; nelim lt; /2/; |
---|
467 | nqed. |
---|
468 | |
---|
469 | nlemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m. |
---|
470 | #n m lt; napply (transitive_lt ? (p0 m) ?); /2/; |
---|
471 | nqed. |
---|
472 | |
---|
473 | nlemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m. |
---|
474 | #n m lt; ninversion lt; |
---|
475 | ##[ #H; nrewrite > (succ_injective … H); //; |
---|
476 | ##| #p H1 H2 H3;nrewrite > (succ_injective … H3); |
---|
477 | napply (transitive_lt ? (p0 p) ?); /2/; |
---|
478 | ##] |
---|
479 | nqed. |
---|
480 | |
---|
481 | nlemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m. |
---|
482 | #n m lt; nelim lt; /2/; |
---|
483 | nqed. |
---|
484 | |
---|
485 | |
---|
486 | |
---|
487 | nlemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m. |
---|
488 | #n m lt;ninversion lt; |
---|
489 | ##[ #p H; ndestruct; |
---|
490 | ##| #n' m' lt e1 e2; ndestruct; //; |
---|
491 | ##] nqed. |
---|
492 | |
---|
493 | nlemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b. |
---|
494 | #a b; /2/; nqed. |
---|
495 | |
---|
496 | nlemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b. |
---|
497 | #a b; nrewrite > (?:p1 b = succ (p0 b)); /2/; nqed. |
---|
498 | |
---|
499 | nlemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m. |
---|
500 | /2/; nqed. |
---|
501 | |
---|
502 | nlemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2. |
---|
503 | #A B a1 a2 b1 b2 H; ndestruct; //; |
---|
504 | nqed. |
---|
505 | |
---|
506 | nlemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2. |
---|
507 | #A B a1 a2 b1 b2 H; ndestruct; //; |
---|
508 | nqed. |
---|
509 | |
---|
510 | ntheorem divide_ok : ∀m,n,dv,md. |
---|
511 | divide m n = 〈dv,md〉 → |
---|
512 | ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n. |
---|
513 | #m n; napply (pos_cases … n); |
---|
514 | ##[ nrewrite > (divide_by_one m); #dv md H; ndestruct; /2/; |
---|
515 | ##| #n'; nelim m; |
---|
516 | ##[ #dv md; nnormalize; nrewrite > (pos_nonzero …); #H; ndestruct; /3/; |
---|
517 | ##| #m' IH dv md; nnormalize; |
---|
518 | nlapply (refl ? (divide m' (succ n'))); |
---|
519 | nelim (divide m' (succ n')) in ⊢ (???% → % → ?); |
---|
520 | #dv' md' DIVr; nelim (IH … DIVr); |
---|
521 | nnormalize; ncases md'; |
---|
522 | ##[ ncases dv'; nnormalize; |
---|
523 | ##[ #H; ndestruct; |
---|
524 | ##| #dv'' Hr1 Hr2; nrewrite > (pos_nonzero …); #H; ndestruct; /3/; |
---|
525 | ##] |
---|
526 | ##| ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim; |
---|
527 | nnormalize; #n md'' Hr1 Hr2; |
---|
528 | nlapply (plt_lt … Hr2); #Hr2'; |
---|
529 | nlapply (partial_minus_to_Prop md'' n); |
---|
530 | ncases (partial_minus md'' n); ##[ ##3,6,9,12: #r'' ##] nnormalize; |
---|
531 | #lt; #e; ndestruct; @; /2/; napply plt_pos; |
---|
532 | ##[ ##1,3,5,7: napply double_lt1; /2/; |
---|
533 | ##| ##2,4: napply double_lt3; /2/; |
---|
534 | ##| ##*: napply double_lt2; /2/; |
---|
535 | ##] |
---|
536 | ##] |
---|
537 | ##| #m' IH dv md; nwhd in ⊢ (??%? → ?); |
---|
538 | nlapply (refl ? (divide m' (succ n'))); |
---|
539 | nelim (divide m' (succ n')) in ⊢ (???% → % → ?); |
---|
540 | #dv' md' DIVr; nelim (IH … DIVr); |
---|
541 | nwhd in ⊢ (? → ? → ??%? → ?); ncases md'; |
---|
542 | ##[ ncases dv'; nnormalize; |
---|
543 | ##[ #H; ndestruct; |
---|
544 | ##| #dv'' Hr1 Hr2; #H; ndestruct; /3/; |
---|
545 | ##] |
---|
546 | ##| (*ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim; |
---|
547 | nnormalize; #n md'' Hr1 Hr2;*) #md'' Hr1 Hr2; |
---|
548 | nlapply (plt_lt … Hr2); #Hr2'; |
---|
549 | nwhd in ⊢ (??%? → ?); |
---|
550 | nlapply (partial_minus_to_Prop (p0 md'') (succ n')); |
---|
551 | ncases (partial_minus (p0 md'') (succ n')); ##[ ##3(*,6,9,12*): #r'' ##] |
---|
552 | ncases dv' in Hr1 ⊢ %; ##[ ##2,4,6: #dv'' ##] nnormalize; |
---|
553 | #Hr1; ndestruct; ##[ ##1,2,3: nrewrite > (p0_plus ? md''); ##] |
---|
554 | #lt; #e; ##[ ##1,3,4,6: nrewrite > lt; ##] |
---|
555 | nrewrite < (pair_eq1 … e); nrewrite < (pair_eq2 … e); |
---|
556 | nnormalize in ⊢ (?(???%)?); @; /2/; napply plt_pos; |
---|
557 | ##[ ncut (succ n' + r'' < p0 (succ n')); /2/; |
---|
558 | ##| ncut (succ n' + r'' < p0 (succ n')); /2/; |
---|
559 | ##| /2/; |
---|
560 | ##| /2/; |
---|
561 | ##] |
---|
562 | ##] |
---|
563 | ##] |
---|
564 | ##] nqed. |
---|
565 | |
---|
566 | nlemma mod0_divides: ∀m,n,dv:Pos. |
---|
567 | divide n m = 〈ppos dv,pzero〉 → m∣n. |
---|
568 | #m;#n;#dv;#DIVIDE;@ dv; nlapply (divide_ok … DIVIDE); *; |
---|
569 | nnormalize; #H; ndestruct; //; |
---|
570 | nqed. |
---|
571 | |
---|
572 | nlemma divides_mod0: ∀dv,m,n:Pos. |
---|
573 | n = dv*m → divide n m = 〈ppos dv,pzero〉. |
---|
574 | #dv;#m;#n;#DIV;nlapply (refl ? (divide n m)); |
---|
575 | nelim (divide n m) in ⊢ (???% → ?); #dv' md' DIVIDE; |
---|
576 | nlapply (divide_ok … DIVIDE); *; |
---|
577 | ncases dv' in DIVIDE ⊢ %; ##[ ##2: #dv''; ##] |
---|
578 | ncases md'; ##[ ##2,4: #md''; ##] #DIVIDE; nnormalize; |
---|
579 | nrewrite > DIV in ⊢ (% → ?); #H lt; ndestruct; |
---|
580 | ##[ nlapply (plus_to_minus … e0); |
---|
581 | nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv'' …); |
---|
582 | ncut (dv'' < dv); ##[ ncut (dv''*m < dv*m); /2/; ##] #dvlt; |
---|
583 | nrewrite > (minus_times_distrib_l …); //; |
---|
584 | |
---|
585 | (*ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##] |
---|
586 | #Hdv;*) #H'; ncut (md'' ≥ m); /2/; nlapply (plt_lt … lt); #A;#B; napply False_ind; |
---|
587 | napply (absurd ? B (lt_to_not_le … A)); |
---|
588 | |
---|
589 | ##| napply False_ind; napply (absurd ? (plt_lt … lt) ?); /2/; |
---|
590 | |
---|
591 | ##| nrewrite > DIVIDE; ncut (dv = dv''); /2/; |
---|
592 | ##] |
---|
593 | nqed. |
---|
594 | |
---|
595 | nlemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n). |
---|
596 | #m;#n; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %); |
---|
597 | #dv;#md; ncases md; ncases dv; |
---|
598 | ##[ #DIVIDES; nlapply (divide_ok … DIVIDES); *; nnormalize; #H; ndestruct |
---|
599 | ##| #dv'; #H; @1; napply mod0_divides; /2/; |
---|
600 | ##| #md'; #DIVIDES; @2; napply nmk; *; #dv'; |
---|
601 | nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H); |
---|
602 | nrewrite > DIVIDES; #H'; |
---|
603 | ndestruct; |
---|
604 | ##| #md'; #dv'; #DIVIDES; @2; napply nmk; *; #dv'; |
---|
605 | nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H); |
---|
606 | nrewrite > DIVIDES; #H'; |
---|
607 | ndestruct; |
---|
608 | ##] nqed. |
---|
609 | |
---|
610 | ntheorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q). |
---|
611 | #p;#q;ncases p; |
---|
612 | ##[ ncases q; nnormalize; ##[ @2; /2/; ##| ##*: #m; @2; /2/; ##] |
---|
613 | ##| ##*: #n; ncases q; nnormalize; /2/; |
---|
614 | ##] nqed. |
---|
615 | |
---|
616 | ndefinition natp_to_Z ≝ |
---|
617 | λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ]. |
---|
618 | |
---|
619 | ndefinition natp_to_negZ ≝ |
---|
620 | λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ]. |
---|
621 | |
---|
622 | (* TODO: check these definitions are right. They are supposed to be the same |
---|
623 | as Zdiv/Zmod in Coq. *) |
---|
624 | ndefinition divZ ≝ λx,y. |
---|
625 | match x with |
---|
626 | [ OZ ⇒ OZ |
---|
627 | | pos n ⇒ |
---|
628 | match y with |
---|
629 | [ OZ ⇒ OZ |
---|
630 | | pos m ⇒ natp_to_Z (fst ?? (divide n m)) |
---|
631 | | neg m ⇒ match divide n m with [ mk_pair q r ⇒ |
---|
632 | match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ] |
---|
633 | ] |
---|
634 | | neg n ⇒ |
---|
635 | match y with |
---|
636 | [ OZ ⇒ OZ |
---|
637 | | pos m ⇒ match divide n m with [ mk_pair q r ⇒ |
---|
638 | match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ] |
---|
639 | | neg m ⇒ natp_to_Z (fst ?? (divide n m)) |
---|
640 | ] |
---|
641 | ]. |
---|
642 | |
---|
643 | ndefinition modZ ≝ λx,y. |
---|
644 | match x with |
---|
645 | [ OZ ⇒ OZ |
---|
646 | | pos n ⇒ |
---|
647 | match y with |
---|
648 | [ OZ ⇒ OZ |
---|
649 | | pos m ⇒ natp_to_Z (snd ?? (divide n m)) |
---|
650 | | neg m ⇒ match divide n m with [ mk_pair q r ⇒ |
---|
651 | match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ] |
---|
652 | ] |
---|
653 | | neg n ⇒ |
---|
654 | match y with |
---|
655 | [ OZ ⇒ OZ |
---|
656 | | pos m ⇒ match divide n m with [ mk_pair q r ⇒ |
---|
657 | match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ] |
---|
658 | | neg m ⇒ natp_to_Z (snd ?? (divide n m)) |
---|
659 | ] |
---|
660 | ]. |
---|
661 | |
---|
662 | interpretation "natural division" 'divide m n = (div m n). |
---|
663 | interpretation "natural modulus" 'module m n = (mod m n). |
---|
664 | interpretation "integer division" 'divide m n = (divZ m n). |
---|
665 | interpretation "integer modulus" 'module m n = (modZ m n). |
---|