source: C-semantics/extralib.ma @ 15

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

Make some definitions more normalization friendly by a little 'nlet rec'
abuse.

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/; ncases x; /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);
125ncases x; /3/; 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
171nlet rec Zleb (x:Z) (y:Z) : bool ≝
172  match x with
173  [ OZ ⇒
174    match y with
175    [ OZ ⇒ true
176    | pos m ⇒ true
177    | neg m ⇒ false ]
178  | pos n ⇒
179    match y with
180    [ OZ ⇒ false
181    | pos m ⇒ leb n m
182    | neg m ⇒ false ]
183  | neg n ⇒
184    match y with
185    [ OZ ⇒ true
186    | pos m ⇒ true
187    | neg m ⇒ leb m n ]].
188   
189nlet rec Zltb (x:Z) (y:Z) : bool ≝
190  match x with
191  [ OZ ⇒
192    match y with
193    [ OZ ⇒ false
194    | pos m ⇒ true
195    | neg m ⇒ false ]
196  | pos n ⇒
197    match y with
198    [ OZ ⇒ false
199    | pos m ⇒ leb (succ n) m
200    | neg m ⇒ false ]
201  | neg n ⇒
202    match y with
203    [ OZ ⇒ true
204    | pos m ⇒ true
205    | neg m ⇒ leb (succ m) n ]].
206
207
208
209ntheorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.
210#n;#m;ncases n;ncases m; //;
211##[ ##1,2: #m'; nnormalize; #H; napply (False_ind ? H)
212##| ##3,5: #n';#m'; nnormalize; napply le_to_leb_true;
213##| ##4: #n';#m'; nnormalize; #H; napply (False_ind ? H)
214##] nqed.
215
216ntheorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.
217#n;#m;ncases n;ncases m; //;
218##[ ##1,2: #m'; nnormalize; #H; ndestruct
219##| ##3,5: #n';#m'; nnormalize; napply leb_true_to_le;
220##| ##4: #n';#m'; nnormalize; #H; ndestruct
221##] nqed.
222
223ntheorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
224#n m H. @; #H'; nrewrite > (Zle_to_Zleb_true … H') in H; #H; ndestruct;
225nqed.
226
227ntheorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.
228#n;#m;ncases n;ncases m; //;
229##[ nnormalize; #H; napply (False_ind ? H)
230##| ##2,3: #m'; nnormalize; #H; napply (False_ind ? H)
231##| ##4,6: #n';#m'; nnormalize; napply le_to_leb_true;
232##| #n';#m'; nnormalize; #H; napply (False_ind ? H)
233##] nqed.
234
235ntheorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.
236#n;#m;ncases n;ncases m; //;
237##[ nnormalize; #H; ndestruct
238##| ##2,3: #m'; nnormalize; #H; ndestruct
239##| ##4,6: #n';#m'; napply leb_true_to_le;
240##| #n';#m'; nnormalize; #H; ndestruct
241##] nqed.
242
243ntheorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
244#n m H; @; #H'; nrewrite > (Zlt_to_Zltb_true … H') in H; #H; ndestruct;
245nqed.
246
247ntheorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
248(n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m).
249#n;#m;#P;#Hle;#Hnle;
250nlapply (refl ? (Zleb n m));
251nelim (Zleb n m) in ⊢ ((???%)→%);
252#Hb;
253##[ napply Hle; napply (Zleb_true_to_Zle … Hb)
254##| napply Hnle; napply (Zleb_false_to_not_Zle … Hb)
255##] nqed.
256
257ntheorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0].
258(n < m → P true) → (n ≮ m → P false) → P (Zltb n m).
259#n;#m;#P;#Hlt;#Hnlt;
260nlapply (refl ? (Zltb n m));
261nelim (Zltb n m) in ⊢ ((???%)→%);
262#Hb;
263##[ napply Hlt; napply (Zltb_true_to_Zlt … Hb)
264##| napply Hnlt; napply (Zltb_false_to_not_Zlt … Hb)
265##] nqed.
266
267nlet rec Z_times (x:Z) (y:Z) : Z ≝
268match x with
269[ OZ ⇒ OZ
270| pos n ⇒
271  match y with
272  [ OZ ⇒ OZ
273  | pos m ⇒ pos (n*m)
274  | neg m ⇒ neg (n*m)
275  ]
276| neg n ⇒
277  match y with
278  [ OZ ⇒ OZ
279  | pos m ⇒ neg (n*m)
280  | neg m ⇒ pos (n*m)
281  ]
282].
283interpretation "integer multiplication" 'times x y = (Z_times x y).
284
285(* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *)
286notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
287notation < "'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 }.
288interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
289
290(* datatypes/list.ma *)
291
292ntheorem nil_append_nil_both:
293  ∀A:Type. ∀l1,l2:list A.
294    l1 @ l2 = [] → l1 = [] ∧ l2 = [].
295#A l1 l2; ncases l1;
296##[ ncases l2;
297  ##[ /2/
298  ##| #h t H; ndestruct;
299  ##]
300##| ncases l2;
301  ##[ nnormalize; #h t H; ndestruct;
302  ##| nnormalize; #h1 t1 h2 h3 H; ndestruct;
303  ##]
304##] nqed.
305
306(* division *)
307
308ninductive natp : Type ≝
309| pzero : natp
310| ppos  : Pos → natp.
311
312ndefinition natp0 ≝
313λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ].
314
315ndefinition natp1 ≝
316λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ].
317
318nlet rec divide (m,n:Pos) on m ≝
319match m with
320[ one ⇒
321  match n with
322  [ one ⇒ 〈ppos one,pzero〉
323  | _ ⇒ 〈pzero,ppos one〉
324  ]
325| p0 m' ⇒
326  match divide m' n with
327  [ mk_pair q r ⇒
328    match r with
329    [ pzero ⇒ 〈natp0 q,pzero〉
330    | ppos r' ⇒
331      match partial_minus (p0 r') n with
332      [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉
333      | MinusZero ⇒ 〈natp1 q, pzero〉
334      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
335      ]
336    ]
337  ]
338| p1 m' ⇒
339  match divide m' n with
340  [ mk_pair q r ⇒
341    match r with
342    [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
343    | ppos r' ⇒
344      match partial_minus (p1 r') n with
345      [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉
346      | MinusZero ⇒ 〈natp1 q, pzero〉
347      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
348      ]
349    ]
350  ]
351].
352
353ndefinition div ≝ λm,n. fst ?? (divide m n).
354ndefinition mod ≝ λm,n. snd ?? (divide m n).
355
356ndefinition pairdisc ≝
357λA,B.λx,y:pair A B.
358match x with
359[(mk_pair t0 t1) ⇒
360match y with
361[(mk_pair u0 u1) ⇒
362  ∀P: Type[1].
363  (∀e0: (eq A (R0 ? t0) u0).
364   ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ].
365
366nlemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.
367#A;#B;#x;#y;#e;nrewrite > e;ncases y;
368#a;#b;nnormalize;#P;#PH;napply PH;@;
369nqed.
370
371nlemma pred_minus: ∀n,m. pred n - m = pred (n-m).
372napply pos_elim; /3/;
373nqed.
374
375nlemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
376napply pos_elim;
377##[ //
378##| #n IH m p; nrewrite > (succ_plus_one …); nrewrite > (IH m one); /2/;
379##] nqed.
380
381ntheorem plus_minus_r:
382∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
383#m;#n;#p;#le;nrewrite > (symmetric_plus …);
384nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed.
385
386nlemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
387#m;#n;#p;nelim m;/2/; nqed.
388(*
389nlemma le_to_minus: ∀m,n. m≤n → m-n = 0.
390#m;#n;nelim n;
391##[ nrewrite < (minus_n_O …); /2/;
392##| #n'; #IH; #le; ninversion le; /2/; #n''; #A;#B;#C; ndestruct;
393    nrewrite > (eq_minus_S_pred …); nrewrite > (IH A); /2/
394##] nqed.
395*)
396nlemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n).
397#n;#m;#p;(*nelim (decidable_lt n m);*)#lt;
398(*##[*) napply (pos_elim … p); //;#p'; #IH;
399    nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); nrewrite < (times_succn_m …);
400    nrewrite > (minus_plus_distrib …);
401    nrewrite < (plus_minus … lt); nrewrite < IH;
402    nrewrite > (plus_minus_r …); /2/;
403nqed.
404(*##|
405nlapply (not_lt_to_le … lt); #le;
406napply (pos_elim … p); //; #p';
407 ncut (m-n = one); ##[ /3/ ##]
408  #mn; nrewrite > mn; nrewrite > (times_n_one …); nrewrite > (times_n_one …);
409  #H; nrewrite < H in ⊢ (???%);
410  napply sym_eq; napply  le_n_one_to_eq; nrewrite < H;
411  nrewrite > (minus_plus_distrib …); napply monotonic_le_minus_l;
412  /2/;
413##] nqed.
414
415nlemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n.
416#m;#n;#H;nlapply (refl ? (m-n));nelim (m-n) in ⊢ (???% → %);//;
417#H'; nlapply (minus_to_plus … H'); /2/;
418nrewrite < (plus_n_O …); #H''; nrewrite > H'' in H; #H;
419napply False_ind; napply (absurd ? H ( not_le_Sn_n n));
420nqed.
421*)
422
423nlet rec natp_plus (n,m:natp) ≝
424match n with
425[ pzero ⇒ m
426| ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ]
427].
428
429nlet rec natp_times (n,m:natp) ≝
430match n with
431[ pzero ⇒ pzero
432| ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ]
433].
434
435ninductive natp_lt : natp → Pos → Prop ≝
436| plt_zero : ∀n. natp_lt pzero n
437| plt_pos : ∀n,m. n < m → natp_lt (ppos n) m.
438
439nlemma lt_p0: ∀n:Pos. one < p0 n.
440#n; nnormalize; /2/; nqed.
441
442nlemma lt_p1: ∀n:Pos. one < p1 n.
443#n'; nnormalize; nrewrite > (?:p1 n' = succ (p0 n')); //; nqed.
444
445nlemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.
446#m; nelim m;
447##[ //;
448##| ##2,3: #m' IH; nnormalize; nrewrite > IH; //;
449##] nqed.
450
451nlemma 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).
452#n P Q; napply succ_elim; /2/; nqed.
453
454nlemma partial_minus_to_Prop: ∀n,m.
455  match partial_minus n m with
456  [ MinusNeg ⇒ n < m
457  | MinusZero ⇒ n = m
458  | MinusPos r ⇒ n = m+r
459  ].
460#n m; nlapply (pos_compare_to_Prop n m); nlapply (minus_to_plus n m);
461nnormalize; ncases (partial_minus n m); /2/; nqed.
462
463nlemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
464#n m lt; nelim lt; /2/;
465nqed.
466
467nlemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
468#n m lt; napply (transitive_lt ? (p0 m) ?); /2/;
469nqed.
470
471nlemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.
472#n m lt; ninversion lt;
473##[ #H; nrewrite > (succ_injective … H); //;
474##| #p H1 H2 H3;nrewrite > (succ_injective … H3);
475    napply (transitive_lt ? (p0 p) ?); /2/;
476##]
477nqed.
478
479nlemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
480#n m lt; nelim lt; /2/;
481nqed.
482
483
484
485nlemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.
486#n m lt;ninversion lt;
487##[ #p H; ndestruct;
488##| #n' m' lt e1 e2; ndestruct; //;
489##] nqed.
490
491nlemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
492#a b; /2/; nqed.
493
494nlemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
495#a b; nrewrite > (?:p1 b = succ (p0 b)); /2/; nqed.
496
497nlemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
498/2/; nqed.
499
500nlemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
501#A B a1 a2 b1 b2 H; ndestruct; //;
502nqed.
503
504nlemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
505#A B a1 a2 b1 b2 H; ndestruct; //;
506nqed.
507
508ntheorem divide_ok : ∀m,n,dv,md.
509 divide m n = 〈dv,md〉 →
510 ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.
511#m n; napply (pos_cases … n);
512##[ nrewrite > (divide_by_one m); #dv md H; ndestruct; /2/;
513##| #n'; nelim m;
514  ##[ #dv md; nnormalize; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
515  ##| #m' IH dv md; nnormalize;
516      nlapply (refl ? (divide m' (succ n')));
517      nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
518      #dv' md' DIVr; nelim (IH … DIVr);
519      nnormalize; ncases md';
520      ##[ ncases dv'; nnormalize;
521        ##[ #H; ndestruct;
522        ##| #dv'' Hr1 Hr2; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
523        ##]
524      ##| ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
525          nnormalize; #n md'' Hr1 Hr2;
526          nlapply (plt_lt … Hr2); #Hr2';
527          nlapply (partial_minus_to_Prop md'' n);
528          ncases (partial_minus md'' n); ##[ ##3,6,9,12: #r'' ##] nnormalize;
529          #lt; #e; ndestruct; @; /2/; napply plt_pos;
530          ##[ ##1,3,5,7: napply double_lt1; /2/;
531          ##| ##2,4: napply double_lt3; /2/;
532          ##| ##*: napply double_lt2; /2/;
533          ##]
534      ##]
535  ##| #m' IH dv md; nwhd in ⊢ (??%? → ?);
536      nlapply (refl ? (divide m' (succ n')));
537      nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
538      #dv' md' DIVr; nelim (IH … DIVr);
539      nwhd in ⊢ (? → ? → ??%? → ?); ncases md';
540      ##[ ncases dv'; nnormalize;
541        ##[ #H; ndestruct;
542        ##| #dv'' Hr1 Hr2; #H; ndestruct; /3/;
543        ##]
544      ##| (*ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
545          nnormalize; #n md'' Hr1 Hr2;*) #md'' Hr1 Hr2;
546          nlapply (plt_lt … Hr2); #Hr2';
547          nwhd in ⊢ (??%? → ?);
548          nlapply (partial_minus_to_Prop (p0 md'') (succ n'));
549          ncases (partial_minus (p0 md'') (succ n')); ##[ ##3(*,6,9,12*): #r'' ##]
550          ncases dv' in Hr1 ⊢ %; ##[ ##2,4,6: #dv'' ##] nnormalize;
551          #Hr1; ndestruct; ##[ ##1,2,3: nrewrite > (p0_plus ? md''); ##]
552          #lt; #e; ##[ ##1,3,4,6: nrewrite > lt; ##]
553          nrewrite < (pair_eq1 … e); nrewrite < (pair_eq2 … e);
554          nnormalize in ⊢ (?(???%)?); @; /2/; napply plt_pos;
555          ##[ ncut (succ n' + r'' < p0 (succ n')); /2/;
556          ##| ncut (succ n' + r'' < p0 (succ n')); /2/;
557          ##| /2/;
558          ##| /2/;
559          ##]
560      ##]
561  ##]
562##] nqed.
563
564nlemma mod0_divides: ∀m,n,dv:Pos.
565  divide n m = 〈ppos dv,pzero〉 → m∣n.
566#m;#n;#dv;#DIVIDE;@ dv; nlapply (divide_ok … DIVIDE); *;
567nnormalize; #H; ndestruct; //;
568nqed.
569
570nlemma divides_mod0: ∀dv,m,n:Pos.
571  n = dv*m → divide n m = 〈ppos dv,pzero〉.
572#dv;#m;#n;#DIV;nlapply (refl ? (divide n m));
573nelim (divide n m) in ⊢ (???% → ?); #dv' md' DIVIDE;
574nlapply (divide_ok … DIVIDE); *;
575ncases dv' in DIVIDE ⊢ %; ##[ ##2: #dv''; ##]
576ncases md'; ##[ ##2,4: #md''; ##] #DIVIDE;  nnormalize;
577nrewrite > DIV in ⊢ (% → ?); #H lt; ndestruct;
578##[ nlapply (plus_to_minus … e0);
579    nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv'' …);
580    ncut (dv'' < dv); ##[ ncut (dv''*m < dv*m); /2/; ##] #dvlt;
581    nrewrite > (minus_times_distrib_l …); //;
582
583 (*ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##]
584    #Hdv;*) #H'; ncut (md'' ≥ m); /2/; nlapply (plt_lt … lt); #A;#B; napply False_ind;
585    napply (absurd ? B (lt_to_not_le … A));
586
587##| napply False_ind; napply (absurd ? (plt_lt … lt) ?); /2/;
588
589##| nrewrite > DIVIDE; ncut (dv = dv''); /2/;
590##]
591nqed.
592
593nlemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).
594#m;#n; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %);
595#dv;#md; ncases md; ncases dv;
596##[ #DIVIDES; nlapply (divide_ok … DIVIDES); *; nnormalize; #H; ndestruct
597##| #dv'; #H; @1; napply mod0_divides; /2/;
598##| #md'; #DIVIDES; @2; napply nmk; *; #dv';
599    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
600    nrewrite > DIVIDES; #H';
601    ndestruct;
602##| #md'; #dv'; #DIVIDES; @2; napply nmk; *; #dv';
603    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
604    nrewrite > DIVIDES; #H';
605    ndestruct;
606##] nqed.
607
608ntheorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
609#p;#q;ncases p;
610##[ ncases q; nnormalize; ##[ @2; /2/; ##| ##*: #m; @2; /2/; ##]
611##| ##*: #n; ncases q; nnormalize; /2/;
612##] nqed.
613
614ndefinition natp_to_Z ≝
615λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ].
616
617ndefinition natp_to_negZ ≝
618λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ].
619
620(* TODO: check these definitions are right.  They are supposed to be the same
621   as Zdiv/Zmod in Coq. *)
622ndefinition divZ ≝ λx,y.
623  match x with
624  [ OZ ⇒ OZ
625  | pos n ⇒
626    match y with
627    [ OZ ⇒ OZ
628    | pos m ⇒ natp_to_Z (fst ?? (divide n m))
629    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
630                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
631    ]
632  | neg n ⇒
633    match y with
634    [ OZ ⇒ OZ
635    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
636                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
637    | neg m ⇒ natp_to_Z (fst ?? (divide n m))
638    ]
639  ].
640
641ndefinition modZ ≝ λx,y.
642  match x with
643  [ OZ ⇒ OZ
644  | pos n ⇒
645    match y with
646    [ OZ ⇒ OZ
647    | pos m ⇒ natp_to_Z (snd ?? (divide n m))
648    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
649                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
650    ]
651  | neg n ⇒
652    match y with
653    [ OZ ⇒ OZ
654    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
655                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
656    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
657    ]
658  ].
659
660interpretation "natural division" 'divide m n = (div m n).
661interpretation "natural modulus" 'module m n = (mod m n).
662interpretation "integer division" 'divide m n = (divZ m n).
663interpretation "integer modulus" 'module m n = (modZ m n).
664
665nlemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
666#x y; ncases y;
667##[ #H; napply (False_ind … H);
668##| #m; #_; ncases x; //; #n;
669    nwhd in ⊢ (?%?);
670    nlapply (pos_compare_to_Prop n m);
671    ncases (pos_compare n m); /2/;
672    #lt; nwhd; nrewrite < (minus_Sn_m … lt); /2/;
673##| #m H; napply (False_ind … H);
674##] nqed.
675
676nlemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
677#n m lt; nlapply (pos_compare_to_Prop n m); ncases (pos_compare n m);
678##[ //;
679##| ##2,3: #H; napply False_ind; napply (absurd ? lt ?); /3/;
680##] nqed.
681
682ntheorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.
683#x y; ncases y;
684##[ #H; napply (False_ind … H);
685##| #m; #_; ncases x;
686  ##[ @;//;
687  ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
688      ncases (divide n m) in ⊢ (???% → %); #dv md H;
689      nelim (divide_ok … H); #e l; nelim l; /2/;
690  ##| #n; nwhd in ⊢ (?(??%)(?%?)); nlapply (refl ? (divide n m));
691      ncases (divide n m) in ⊢ (???% → %); #dv md H;
692      nelim (divide_ok … H); #e l; nelim l;
693      ##[ /2/;
694      ##| #md' m' l'; @;
695        ##[ nwhd in ⊢ (??%); nrewrite > (pos_compare_n_m_m_n …);
696            nrewrite > (pos_compare_lt … l'); //;
697        ##| napply Zminus_Zlt; //;
698        ##]
699      ##]
700  ##]
701##| #m H; napply (False_ind … H);
702##] nqed.
Note: See TracBrowser for help on using the repository browser.