source: C-semantics/extralib.ma @ 11

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

Fill in some axioms to aid executablity.
Implement global variable lookups and funtion returns.
Update compcert patch to use binary representation.

File size: 20.7 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).
Note: See TracBrowser for help on using the repository browser.