source: C-semantics/extralib.ma @ 14

Last change on this file since 14 was 14, checked in by campbell, 10 years ago

Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.

File size: 22.0 KB
Line 
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
15include "datatypes/sums.ma".
16include "datatypes/list.ma".
17include "Plogic/equality.ma".
18include "binary/Z.ma".
19include "binary/positive.ma".
20
21nlemma 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.
24nqed.
25
26nlemma 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.
29nqed.
30
31nlemma 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.
34nqed.
35
36nlemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x.
37#A;#x;#y;*;#H;napply nmk;#H';/2/;
38nqed.
39
40(* stolen from logic/connectives.ma to give Prop version. *)
41notation > "hvbox(a break \liff b)"
42  left associative with precedence 25
43for @{ 'iff $a $b }.
44
45notation "hvbox(a break \leftrightarrow b)"
46  left associative with precedence 25
47for @{ 'iff $a $b }.
48
49interpretation "logical iff" 'iff x y = (iff x y).
50
51(* bool *)
52
53ndefinition xorb : bool → bool → bool ≝
54  λx,y. match x with [ false ⇒ y | true ⇒ notb y ].
55 
56
57(* TODO: move to Z.ma *)
58
59nlemma eqZb_z_z : ∀z.eqZb z z = true.
60#z;ncases z;nnormalize;//;
61nqed.
62
63(* XXX: divides goes to arithmetics *)
64ninductive dividesP (n,m:Pos) : Prop ≝
65| witness : ∀p:Pos.m = times n p → dividesP n m.
66interpretation "positive divides" 'divides n m = (dividesP n m).
67interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)).
68
69ndefinition 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
76interpretation "integer divides" 'divides n m = (dividesZ n m).
77interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)).
78
79(* should be proved in nat.ma, but it's not! *)
80naxiom eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
81
82nlemma 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
85nlemma injective_Z_of_nat : injective ? ? Z_of_nat.
86nnormalize;
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
92nlemma reflexive_Zle : reflexive ? Zle.
93#x; ncases x; //; nqed.
94
95nlemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).
96#n;ncases n;nnormalize;//;nqed.
97
98nlemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.
99#x; ncases x; //;
100#n; ncases n; //; nqed.
101
102nlemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
103#x;#y;
104napply pos_elim
105 ##[ ##2: #n'; #IH; ##]
106nrewrite > (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 *)
114ndefinition Zmax : Z → Z → Z ≝
115  λx,y.match Z_compare x y with
116  [ LT ⇒ y
117  | _ ⇒ x ].
118
119nlemma 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
123nlemma 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
127ntheorem 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   
141ntheorem 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;
143napply (transitive_Zle … Hle); /2/;
144nqed.
145
146ndefinition 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;//##]
150nqed.
151
152nlemma 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');
155nqed.
156
157(* Z.ma *)
158
159ndefinition Zge: Z → Z → Prop ≝
160λn,m:Z.m ≤ n.
161
162interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y).
163
164ndefinition Zgt: Z → Z → Prop ≝
165λn,m:Z.m<n.
166
167interpretation "integer 'greater than'" 'gt x y = (Zgt x y).
168
169interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)).
170
171ndefinition 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   
190ndefinition 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
211ntheorem 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
218ntheorem 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
225ntheorem 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;
227nqed.
228
229ntheorem 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
237ntheorem 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
245ntheorem 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;
247nqed.
248
249ntheorem 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;
252nlapply (refl ? (Zleb n m));
253nelim (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
259ntheorem 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;
262nlapply (refl ? (Zltb n m));
263nelim (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
269ndefinition 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].
285interpretation "integer multiplication" 'times x y = (Z_times x y).
286
287(* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *)
288notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
289notation < "'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 }.
290interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
291
292(* datatypes/list.ma *)
293
294ntheorem 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
310ninductive natp : Type ≝
311| pzero : natp
312| ppos  : Pos → natp.
313
314ndefinition natp0 ≝
315λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ].
316
317ndefinition natp1 ≝
318λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ].
319
320nlet rec divide (m,n:Pos) on m ≝
321match 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
355ndefinition div ≝ λm,n. fst ?? (divide m n).
356ndefinition mod ≝ λm,n. snd ?? (divide m n).
357
358ndefinition pairdisc ≝
359λA,B.λx,y:pair A B.
360match x with
361[(mk_pair t0 t1) ⇒
362match 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
368nlemma 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;@;
371nqed.
372
373nlemma pred_minus: ∀n,m. pred n - m = pred (n-m).
374napply pos_elim; /3/;
375nqed.
376
377nlemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
378napply pos_elim;
379##[ //
380##| #n IH m p; nrewrite > (succ_plus_one …); nrewrite > (IH m one); /2/;
381##] nqed.
382
383ntheorem plus_minus_r:
384∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
385#m;#n;#p;#le;nrewrite > (symmetric_plus …);
386nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed.
387
388nlemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
389#m;#n;#p;nelim m;/2/; nqed.
390(*
391nlemma 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*)
398nlemma 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/;
405nqed.
406(*##|
407nlapply (not_lt_to_le … lt); #le;
408napply (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
417nlemma 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/;
420nrewrite < (plus_n_O …); #H''; nrewrite > H'' in H; #H;
421napply False_ind; napply (absurd ? H ( not_le_Sn_n n));
422nqed.
423*)
424
425nlet rec natp_plus (n,m:natp) ≝
426match n with
427[ pzero ⇒ m
428| ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ]
429].
430
431nlet rec natp_times (n,m:natp) ≝
432match n with
433[ pzero ⇒ pzero
434| ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ]
435].
436
437ninductive 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
441nlemma lt_p0: ∀n:Pos. one < p0 n.
442#n; nnormalize; /2/; nqed.
443
444nlemma lt_p1: ∀n:Pos. one < p1 n.
445#n'; nnormalize; nrewrite > (?:p1 n' = succ (p0 n')); //; nqed.
446
447nlemma 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
453nlemma 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
456nlemma 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);
463nnormalize; ncases (partial_minus n m); /2/; nqed.
464
465nlemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
466#n m lt; nelim lt; /2/;
467nqed.
468
469nlemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
470#n m lt; napply (transitive_lt ? (p0 m) ?); /2/;
471nqed.
472
473nlemma 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##]
479nqed.
480
481nlemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
482#n m lt; nelim lt; /2/;
483nqed.
484
485
486
487nlemma 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
493nlemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
494#a b; /2/; nqed.
495
496nlemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
497#a b; nrewrite > (?:p1 b = succ (p0 b)); /2/; nqed.
498
499nlemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
500/2/; nqed.
501
502nlemma 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; //;
504nqed.
505
506nlemma 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; //;
508nqed.
509
510ntheorem 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
566nlemma 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); *;
569nnormalize; #H; ndestruct; //;
570nqed.
571
572nlemma 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));
575nelim (divide n m) in ⊢ (???% → ?); #dv' md' DIVIDE;
576nlapply (divide_ok … DIVIDE); *;
577ncases dv' in DIVIDE ⊢ %; ##[ ##2: #dv''; ##]
578ncases md'; ##[ ##2,4: #md''; ##] #DIVIDE;  nnormalize;
579nrewrite > 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##]
593nqed.
594
595nlemma 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
610ntheorem 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
616ndefinition natp_to_Z ≝
617λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ].
618
619ndefinition 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. *)
624ndefinition 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
643ndefinition 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
662interpretation "natural division" 'divide m n = (div m n).
663interpretation "natural modulus" 'module m n = (mod m n).
664interpretation "integer division" 'divide m n = (divZ m n).
665interpretation "integer modulus" 'module m n = (modZ m n).
666
667nlemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
668#x y; ncases y;
669##[ #H; napply (False_ind … H);
670##| #m; #_; ncases x; //; #n;
671    nwhd in ⊢ (?%?);
672    nlapply (pos_compare_to_Prop n m);
673    ncases (pos_compare n m); /2/;
674    #lt; nwhd; nrewrite < (minus_Sn_m … lt); /2/;
675##| #m H; napply (False_ind … H);
676##] nqed.
677
678nlemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
679#n m lt; nlapply (pos_compare_to_Prop n m); ncases (pos_compare n m);
680##[ //;
681##| ##2,3: #H; napply False_ind; napply (absurd ? lt ?); /3/;
682##] nqed.
683
684ntheorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.
685#x y; ncases y;
686##[ #H; napply (False_ind … H);
687##| #m; #_; ncases x;
688  ##[ @;//;
689  ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
690      ncases (divide n m) in ⊢ (???% → %); #dv md H;
691      nelim (divide_ok … H); #e l; nelim l; /2/;
692  ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
693      ncases (divide n m) in ⊢ (???% → %); #dv md H;
694      nelim (divide_ok … H); #e l; nelim l;
695      ##[ /2/;
696      ##| #md' m' l'; @;
697        ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …);
698            nrewrite > (pos_compare_lt … l'); //;
699        ##| /2/;
700        ##]
701      ##]
702  ##]
703##| #m H; napply (False_ind … H);
704##] nqed.
Note: See TracBrowser for help on using the repository browser.