source: C-semantics/extralib.ma @ 189

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

Sort out some axioms.

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