source:C-semantics/extralib.ma@10

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

Add binary arithmetic libraries, use for integers and identifiers (but
we're not doing modular arithmetic yet.)
Add a dummy "tree" implementation to make environment lookups executable.
Fix if .. then .. else .. precedence.

File size: 20.5 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
269naxiom Z_times : Z → Z → Z.
270interpretation "integer multiplication" 'times x y = (Z_times x y).
271
272(* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *)
273notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else \$e \$t \$f }.
274notation < "'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 }.
275interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
276
277(* datatypes/list.ma *)
278
279ntheorem nil_append_nil_both:
280  ∀A:Type. ∀l1,l2:list A.
281    l1 @ l2 = [] → l1 = [] ∧ l2 = [].
282#A l1 l2; ncases l1;
283##[ ncases l2;
284  ##[ /2/
285  ##| #h t H; ndestruct;
286  ##]
287##| ncases l2;
288  ##[ nnormalize; #h t H; ndestruct;
289  ##| nnormalize; #h1 t1 h2 h3 H; ndestruct;
290  ##]
291##] nqed.
292
293(* division *)
294
295ninductive natp : Type ≝
296| pzero : natp
297| ppos  : Pos → natp.
298
299ndefinition natp0 ≝
300λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ].
301
302ndefinition natp1 ≝
303λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ].
304
305nlet rec divide (m,n:Pos) on m ≝
306match m with
307[ one ⇒
308  match n with
309  [ one ⇒ 〈ppos one,pzero〉
310  | _ ⇒ 〈pzero,ppos one〉
311  ]
312| p0 m' ⇒
313  match divide m' n with
314  [ mk_pair q r ⇒
315    match r with
316    [ pzero ⇒ 〈natp0 q,pzero〉
317    | ppos r' ⇒
318      match partial_minus (p0 r') n with
319      [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉
320      | MinusZero ⇒ 〈natp1 q, pzero〉
321      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
322      ]
323    ]
324  ]
325| p1 m' ⇒
326  match divide m' n with
327  [ mk_pair q r ⇒
328    match r with
329    [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ]
330    | ppos r' ⇒
331      match partial_minus (p1 r') n with
332      [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉
333      | MinusZero ⇒ 〈natp1 q, pzero〉
334      | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉
335      ]
336    ]
337  ]
338].
339
340ndefinition div ≝ λm,n. fst ?? (divide m n).
341ndefinition mod ≝ λm,n. snd ?? (divide m n).
342
343ndefinition pairdisc ≝
344λA,B.λx,y:pair A B.
345match x with
346[(mk_pair t0 t1) ⇒
347match y with
348[(mk_pair u0 u1) ⇒
349  ∀P: Type[1].
350  (∀e0: (eq A (R0 ? t0) u0).
351   ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ].
352
353nlemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.
354#A;#B;#x;#y;#e;nrewrite > e;ncases y;
355#a;#b;nnormalize;#P;#PH;napply PH;@;
356nqed.
357
358nlemma pred_minus: ∀n,m. pred n - m = pred (n-m).
359napply pos_elim; /3/;
360nqed.
361
362nlemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
363napply pos_elim;
364##[ //
365##| #n IH m p; nrewrite > (succ_plus_one …); nrewrite > (IH m one); /2/;
366##] nqed.
367
368ntheorem plus_minus_r:
369∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
370#m;#n;#p;#le;nrewrite > (symmetric_plus …);
371nrewrite > (symmetric_plus p ?); napply plus_minus; //; nqed.
372
373nlemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
374#m;#n;#p;nelim m;/2/; nqed.
375(*
376nlemma le_to_minus: ∀m,n. m≤n → m-n = 0.
377#m;#n;nelim n;
378##[ nrewrite < (minus_n_O …); /2/;
379##| #n'; #IH; #le; ninversion le; /2/; #n''; #A;#B;#C; ndestruct;
380    nrewrite > (eq_minus_S_pred …); nrewrite > (IH A); /2/
381##] nqed.
382*)
383nlemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n).
384#n;#m;#p;(*nelim (decidable_lt n m);*)#lt;
385(*##[*) napply (pos_elim … p); //;#p'; #IH;
386    nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); nrewrite < (times_succn_m …);
387    nrewrite > (minus_plus_distrib …);
388    nrewrite < (plus_minus … lt); nrewrite < IH;
389    nrewrite > (plus_minus_r …); /2/;
390nqed.
391(*##|
392nlapply (not_lt_to_le … lt); #le;
393napply (pos_elim … p); //; #p';
394 ncut (m-n = one); ##[ /3/ ##]
395  #mn; nrewrite > mn; nrewrite > (times_n_one …); nrewrite > (times_n_one …);
396  #H; nrewrite < H in ⊢ (???%);
397  napply sym_eq; napply  le_n_one_to_eq; nrewrite < H;
398  nrewrite > (minus_plus_distrib …); napply monotonic_le_minus_l;
399  /2/;
400##] nqed.
401
402nlemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n.
403#m;#n;#H;nlapply (refl ? (m-n));nelim (m-n) in ⊢ (???% → %);//;
404#H'; nlapply (minus_to_plus … H'); /2/;
405nrewrite < (plus_n_O …); #H''; nrewrite > H'' in H; #H;
406napply False_ind; napply (absurd ? H ( not_le_Sn_n n));
407nqed.
408*)
409
410nlet rec natp_plus (n,m:natp) ≝
411match n with
412[ pzero ⇒ m
413| ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ]
414].
415
416nlet rec natp_times (n,m:natp) ≝
417match n with
418[ pzero ⇒ pzero
419| ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ]
420].
421
422ninductive natp_lt : natp → Pos → Prop ≝
423| plt_zero : ∀n. natp_lt pzero n
424| plt_pos : ∀n,m. n < m → natp_lt (ppos n) m.
425
426nlemma lt_p0: ∀n:Pos. one < p0 n.
427#n; nnormalize; /2/; nqed.
428
429nlemma lt_p1: ∀n:Pos. one < p1 n.
430#n'; nnormalize; nrewrite > (?:p1 n' = succ (p0 n')); //; nqed.
431
432nlemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.
433#m; nelim m;
434##[ //;
435##| ##2,3: #m' IH; nnormalize; nrewrite > IH; //;
436##] nqed.
437
438nlemma 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).
439#n P Q; napply succ_elim; /2/; nqed.
440
441nlemma partial_minus_to_Prop: ∀n,m.
442  match partial_minus n m with
443  [ MinusNeg ⇒ n < m
444  | MinusZero ⇒ n = m
445  | MinusPos r ⇒ n = m+r
446  ].
447#n m; nlapply (pos_compare_to_Prop n m); nlapply (minus_to_plus n m);
448nnormalize; ncases (partial_minus n m); /2/; nqed.
449
450nlemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
451#n m lt; nelim lt; /2/;
452nqed.
453
454nlemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
455#n m lt; napply (transitive_lt ? (p0 m) ?); /2/;
456nqed.
457
458nlemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.
459#n m lt; ninversion lt;
460##[ #H; nrewrite > (succ_injective … H); //;
461##| #p H1 H2 H3;nrewrite > (succ_injective … H3);
462    napply (transitive_lt ? (p0 p) ?); /2/;
463##]
464nqed.
465
466nlemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
467#n m lt; nelim lt; /2/;
468nqed.
469
470
471
472nlemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.
473#n m lt;ninversion lt;
474##[ #p H; ndestruct;
475##| #n' m' lt e1 e2; ndestruct; //;
476##] nqed.
477
478nlemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
479#a b; /2/; nqed.
480
481nlemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
482#a b; nrewrite > (?:p1 b = succ (p0 b)); /2/; nqed.
483
484nlemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
485/2/; nqed.
486
487nlemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
488#A B a1 a2 b1 b2 H; ndestruct; //;
489nqed.
490
491nlemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
492#A B a1 a2 b1 b2 H; ndestruct; //;
493nqed.
494
495ntheorem divide_ok : ∀m,n,dv,md.
496 divide m n = 〈dv,md〉 →
497 ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n.
498#m n; napply (pos_cases … n);
499##[ nrewrite > (divide_by_one m); #dv md H; ndestruct; /2/;
500##| #n'; nelim m;
501  ##[ #dv md; nnormalize; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
502  ##| #m' IH dv md; nnormalize;
503      nlapply (refl ? (divide m' (succ n')));
504      nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
505      #dv' md' DIVr; nelim (IH … DIVr);
506      nnormalize; ncases md';
507      ##[ ncases dv'; nnormalize;
508        ##[ #H; ndestruct;
509        ##| #dv'' Hr1 Hr2; nrewrite > (pos_nonzero …); #H; ndestruct; /3/;
510        ##]
511      ##| ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
512          nnormalize; #n md'' Hr1 Hr2;
513          nlapply (plt_lt … Hr2); #Hr2';
514          nlapply (partial_minus_to_Prop md'' n);
515          ncases (partial_minus md'' n); ##[ ##3,6,9,12: #r'' ##] nnormalize;
516          #lt; #e; ndestruct; @; /2/; napply plt_pos;
517          ##[ ##1,3,5,7: napply double_lt1; /2/;
518          ##| ##2,4: napply double_lt3; /2/;
519          ##| ##*: napply double_lt2; /2/;
520          ##]
521      ##]
522  ##| #m' IH dv md; nwhd in ⊢ (??%? → ?);
523      nlapply (refl ? (divide m' (succ n')));
524      nelim (divide m' (succ n')) in ⊢ (???% → % → ?);
525      #dv' md' DIVr; nelim (IH … DIVr);
526      nwhd in ⊢ (? → ? → ??%? → ?); ncases md';
527      ##[ ncases dv'; nnormalize;
528        ##[ #H; ndestruct;
529        ##| #dv'' Hr1 Hr2; #H; ndestruct; /3/;
530        ##]
531      ##| (*ncases dv'; ##[ ##2: #dv''; ##] napply succ_elim;
532          nnormalize; #n md'' Hr1 Hr2;*) #md'' Hr1 Hr2;
533          nlapply (plt_lt … Hr2); #Hr2';
534          nwhd in ⊢ (??%? → ?);
535          nlapply (partial_minus_to_Prop (p0 md'') (succ n'));
536          ncases (partial_minus (p0 md'') (succ n')); ##[ ##3(*,6,9,12*): #r'' ##]
537          ncases dv' in Hr1 ⊢ %; ##[ ##2,4,6: #dv'' ##] nnormalize;
538          #Hr1; ndestruct; ##[ ##1,2,3: nrewrite > (p0_plus ? md''); ##]
539          #lt; #e; ##[ ##1,3,4,6: nrewrite > lt; ##]
540          nrewrite < (pair_eq1 … e); nrewrite < (pair_eq2 … e);
541          nnormalize in ⊢ (?(???%)?); @; /2/; napply plt_pos;
542          ##[ ncut (succ n' + r'' < p0 (succ n')); /2/;
543          ##| ncut (succ n' + r'' < p0 (succ n')); /2/;
544          ##| /2/;
545          ##| /2/;
546          ##]
547      ##]
548  ##]
549##] nqed.
550
551nlemma mod0_divides: ∀m,n,dv:Pos.
552  divide n m = 〈ppos dv,pzero〉 → m∣n.
553#m;#n;#dv;#DIVIDE;@ dv; nlapply (divide_ok … DIVIDE); *;
554nnormalize; #H; ndestruct; //;
555nqed.
556
557nlemma divides_mod0: ∀dv,m,n:Pos.
558  n = dv*m → divide n m = 〈ppos dv,pzero〉.
559#dv;#m;#n;#DIV;nlapply (refl ? (divide n m));
560nelim (divide n m) in ⊢ (???% → ?); #dv' md' DIVIDE;
561nlapply (divide_ok … DIVIDE); *;
562ncases dv' in DIVIDE ⊢ %; ##[ ##2: #dv''; ##]
563ncases md'; ##[ ##2,4: #md''; ##] #DIVIDE;  nnormalize;
564nrewrite > DIV in ⊢ (% → ?); #H lt; ndestruct;
565##[ nlapply (plus_to_minus … e0);
566    nrewrite > (symmetric_times …); nrewrite > (symmetric_times dv'' …);
567    ncut (dv'' < dv); ##[ ncut (dv''*m < dv*m); /2/; ##] #dvlt;
568    nrewrite > (minus_times_distrib_l …); //;
569
570 (*ncut (0 < dv-dv'); ##[ nlapply (not_le_to_lt … nle); /2/ ##]
571    #Hdv;*) #H'; ncut (md'' ≥ m); /2/; nlapply (plt_lt … lt); #A;#B; napply False_ind;
572    napply (absurd ? B (lt_to_not_le … A));
573
574##| napply False_ind; napply (absurd ? (plt_lt … lt) ?); /2/;
575
576##| nrewrite > DIVIDE; ncut (dv = dv''); /2/;
577##]
578nqed.
579
580nlemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).
581#m;#n; nlapply (refl ? (divide n m)); nelim (divide n m) in ⊢ (???% → %);
582#dv;#md; ncases md; ncases dv;
583##[ #DIVIDES; nlapply (divide_ok … DIVIDES); *; nnormalize; #H; ndestruct
584##| #dv'; #H; @1; napply mod0_divides; /2/;
585##| #md'; #DIVIDES; @2; napply nmk; *; #dv';
586    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
587    nrewrite > DIVIDES; #H';
588    ndestruct;
589##| #md'; #dv'; #DIVIDES; @2; napply nmk; *; #dv';
590    nrewrite > (symmetric_times …); #H; nlapply (divides_mod0 … H);
591    nrewrite > DIVIDES; #H';
592    ndestruct;
593##] nqed.
594
595ntheorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
596#p;#q;ncases p;
597##[ ncases q; nnormalize; ##[ @2; /2/; ##| ##*: #m; @2; /2/; ##]
598##| ##*: #n; ncases q; nnormalize; /2/;
599##] nqed.
600
601ndefinition natp_to_Z ≝
602λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ].
603
604ndefinition natp_to_negZ ≝
605λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ].
606
607(* TODO: check these definitions are right.  They are supposed to be the same
608   as Zdiv/Zmod in Coq. *)
609ndefinition divZ ≝ λx,y.
610  match x with
611  [ OZ ⇒ OZ
612  | pos n ⇒
613    match y with
614    [ OZ ⇒ OZ
615    | pos m ⇒ natp_to_Z (fst ?? (divide n m))
616    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
617                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
618    ]
619  | neg n ⇒
620    match y with
621    [ OZ ⇒ OZ
622    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
623                match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ]
624    | neg m ⇒ natp_to_Z (fst ?? (divide n m))
625    ]
626  ].
627
628ndefinition modZ ≝ λx,y.
629  match x with
630  [ OZ ⇒ OZ
631  | pos n ⇒
632    match y with
633    [ OZ ⇒ OZ
634    | pos m ⇒ natp_to_Z (snd ?? (divide n m))
635    | neg m ⇒ match divide n m with [ mk_pair q r ⇒
636                match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ]
637    ]
638  | neg n ⇒
639    match y with
640    [ OZ ⇒ OZ
641    | pos m ⇒ match divide n m with [ mk_pair q r ⇒
642                match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ]
643    | neg m ⇒ natp_to_Z (snd ?? (divide n m))
644    ]
645  ].
646
647interpretation "natural division" 'divide m n = (div m n).
648interpretation "natural modulus" 'module m n = (mod m n).
649interpretation "integer division" 'divide m n = (divZ m n).
650interpretation "integer modulus" 'module m n = (modZ m n).
Note: See TracBrowser for help on using the repository browser.