source: C-semantics/extralib.ma @ 173

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

Minor changes for newer versions of matita.

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