source: src/utilities/extralib.ma @ 695

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

Rearrange Clight files a bit - will try to make them work again soon...

File size: 21.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 "basics/types.ma".
16include "basics/list.ma".
17include "basics/logic.ma".
18include "binary/Z.ma".
19include "binary/positive.ma".
20
21lemma 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 @(eq_rect_r ??? p0) assumption.
24qed.
25
26lemma 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 cases p; #P #H assumption.
29qed.
30
31lemma 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 @(eq_rect_r2 ??? p0) assumption.
34qed.
35
36lemma 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 @(eq_rect_r2 ??? p0) assumption.
39qed.
40
41lemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x.
42#A #x #y *;#H @nmk #H' /2/;
43qed.
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
58definition xorb : bool → bool → bool ≝
59  λx,y. match x with [ false ⇒ y | true ⇒ notb y ].
60 
61
62(* TODO: move to Z.ma *)
63
64lemma eqZb_z_z : ∀z.eqZb z z = true.
65#z cases z;normalize;//;
66qed.
67
68(* XXX: divides goes to arithmetics *)
69inductive 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
74definition 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! *)
85lemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
86#n elim n;
87[ #m cases m; //;
88| #n' #IH #m cases m; [ /2/; | #m' whd in match (eqb (S n') (S m')) in ⊢ %;
89  lapply (IH m'); cases (eqb n' m'); /2/; ]
90] qed.
91
92lemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
93#n #m @eqb_elim //; qed.
94
95lemma injective_Z_of_nat : injective ? ? Z_of_nat.
96normalize;
97#n #m cases n;cases m;normalize;//;
98[ 1,2: #n' #H destruct
99| #n' #m' #H destruct; >(succ_pos_of_nat_inj … e0) //
100] qed.
101
102lemma reflexive_Zle : reflexive ? Zle.
103#x cases x; //; qed.
104
105lemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).
106#n cases n;normalize;//;qed.
107
108lemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.
109#x cases x; //;
110#n cases n; //; qed.
111
112lemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
113#x #y
114@pos_elim
115 [ 2: #n' #IH ]
116>(Zplus_Zsucc_Zpred y ?)
117[ >(Zpred_Zsucc (pos n'))
118 #H @(transitive_Zle ??? (IH H)) >(Zplus_Zsucc ??)
119    @Zsucc_le
120| #H @(transitive_Zle ??? H) >(Zplus_z_OZ ?) @Zsucc_le
121] qed.
122
123(* XXX: Zmax must go to arithmetics *)
124definition Zmax : Z → Z → Z ≝
125  λx,y.match Z_compare x y with
126  [ LT ⇒ y
127  | _ ⇒ x ].
128
129lemma Zmax_l: ∀x,y. x ≤ Zmax x y.
130#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y); cases (Z_compare x y);
131/3/; cases x; /3/; qed.
132
133lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
134#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y); cases (Z_compare x y);
135cases x; /3/; qed.
136
137theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
138#x #y cases x;
139[ cases y;
140  [ 1,2: //
141  | #n @False_ind
142  ]
143| #n cases y;
144  [ normalize; @False_ind
145  | #m @(pos_cases … n) /2/;
146  | #m normalize; @False_ind
147  ]
148| #n cases y; /2/;
149] qed.
150   
151theorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.
152#n #m #p #Hlt #Hle <(Zpred_Zsucc n) @Zle_to_Zlt
153@(transitive_Zle … Hle) /2/;
154qed.
155
156definition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2).
157#z1 #z2 lapply (eqZb_to_Prop z1 z2);cases (eqZb z1 z2);normalize;#H
158[% //
159|%2 //]
160qed.
161
162lemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false.
163#z1 #z2 lapply (eqZb_to_Prop z1 z2); cases (eqZb z1 z2); //;
164#H #H' @False_ind @(absurd ? H H')
165qed.
166
167(* Z.ma *)
168
169definition Zge: Z → Z → Prop ≝
170λn,m:Z.m ≤ n.
171
172interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y).
173
174definition 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
181let 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   
199let 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
219theorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.
220#n #m cases n;cases m; //;
221[ 1,2: #m' normalize; #H @(False_ind ? H)
222| 3,5: #n' #m' normalize; @le_to_leb_true
223| 4: #n' #m' normalize; #H @(False_ind ? H)
224] qed.
225
226theorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.
227#n #m cases n;cases m; //;
228[ 1,2: #m' normalize; #H destruct
229| 3,5: #n' #m' normalize; @leb_true_to_le
230| 4: #n' #m' normalize; #H destruct
231] qed.
232
233theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
234#n #m #H % #H' >(Zle_to_Zleb_true … H') in H #H destruct;
235qed.
236
237theorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.
238#n #m cases n;cases m; //;
239[ normalize; #H @(False_ind ? H)
240| 2,3: #m' normalize; #H @(False_ind ? H)
241| 4,6: #n' #m' normalize; @le_to_leb_true
242| #n' #m' normalize; #H @(False_ind ? H)
243] qed.
244
245theorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.
246#n #m cases n;cases m; //;
247[ normalize; #H destruct
248| 2,3: #m' normalize; #H destruct
249| 4,6: #n' #m' @leb_true_to_le
250| #n' #m' normalize; #H destruct
251] qed.
252
253theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
254#n #m #H % #H' >(Zlt_to_Zltb_true … H') in H #H destruct;
255qed.
256
257theorem 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
260lapply (refl ? (Zleb n m));
261elim (Zleb n m) in ⊢ ((???%)→%);
262#Hb
263[ @Hle @(Zleb_true_to_Zle … Hb)
264| @Hnle @(Zleb_false_to_not_Zle … Hb)
265] qed.
266
267theorem 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
270lapply (refl ? (Zltb n m));
271elim (Zltb n m) in ⊢ ((???%)→%);
272#Hb
273[ @Hlt @(Zltb_true_to_Zlt … Hb)
274| @Hnlt @(Zltb_false_to_not_Zlt … Hb)
275] qed.
276
277lemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc.
278#x #y cases x; cases y; /2/;
279#n #m @(pos_cases … n) @(pos_cases … m)
280[ //;
281| #n' /2/;
282| #m' #H @False_ind normalize in H; @(absurd … (not_le_succ_one m')) /2/;
283| #n' #m' #H normalize in H;
284    >(Zsucc_neg_succ n') >(Zsucc_neg_succ m') /2/;
285] qed.
286
287lemma monotonic_Zle_Zpred: monotonic Z Zle Zpred.
288#x #y cases x; cases y;
289[ 1,2,7,8,9: /2/;
290| 3,4: #m normalize; *;
291| #m #n @(pos_cases … n) @(pos_cases … m)
292  [ 1,2: /2/;
293  | #n' normalize; #H @False_ind @(absurd … (not_le_succ_one n')) /2/;
294  | #n' #m' >(Zpred_pos_succ n') >(Zpred_pos_succ m') /2/;
295  ]
296| #m #n normalize; *;
297] qed.
298
299lemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m).
300#n cases n; //; #n' #a #b #H
301[ @(pos_elim … n')
302  [ <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) /2/;
303  | #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //;
304      >(Zplus_Zsucc …) >(Zplus_Zsucc …) /2/;
305  ]
306| @(pos_elim … n')
307  [ <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/;
308  | #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //;
309      >(Zplus_Zpred …) >(Zplus_Zpred …) /2/;
310  ]
311] qed.
312
313lemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n).
314/2/; qed.
315
316let 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(* Now in cerco/Util.ma
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
341theorem nil_append_nil_both:
342  ∀A:Type[0]. ∀l1,l2:list A.
343    l1 @ l2 = [] → l1 = [] ∧ l2 = [].
344#A #l1 #l2 cases l1;
345[ cases l2;
346  [ /2/
347  | #h #t #H destruct;
348  ]
349| cases l2;
350  [ normalize; #h #t #H destruct;
351  | normalize; #h1 #t1 #h2 #h3 #H destruct;
352  ]
353] qed.
354
355(* division *)
356
357inductive natp : Type[0] ≝
358| pzero : natp
359| ppos  : Pos → natp.
360
361definition natp0 ≝
362λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ].
363
364definition natp1 ≝
365λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ].
366
367let 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  [ 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  [ 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
402definition div ≝ λm,n. fst ?? (divide m n).
403definition mod ≝ λm,n. snd ?? (divide m n).
404
405definition pairdisc ≝
406λA,B.λx,y:Prod A B.
407match x with
408[(pair t0 t1) ⇒
409match y with
410[(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
415lemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y.
416#A #B #x #y #e >e cases y;
417#a #b normalize;#P #PH @PH %
418qed.
419
420lemma pred_minus: ∀n,m. pred n - m = pred (n-m).
421@pos_elim /3/;
422qed.
423
424lemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p.
425@pos_elim
426[ //
427| #n #IH #m #p >(succ_plus_one …) >(IH m one) /2/;
428] qed.
429
430theorem plus_minus_r:
431∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
432#m #n #p #le >(commutative_plus …)
433>(commutative_plus p ?) @plus_minus //; qed.
434
435lemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
436#m #n #p elim m;/2/; qed.
437(*
438lemma le_to_minus: ∀m,n. m≤n → m-n = 0.
439#m #n elim n;
440[ <(minus_n_O …) /2/;
441| #n' #IH #le inversion le; /2/; #n'' #A #B #C destruct;
442    >(eq_minus_S_pred …) >(IH A) /2/
443] qed.
444*)
445lemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n).
446#n #m #p (*elim (decidable_lt n m);*)#lt
447(*[*) @(pos_elim … p) //;#p' #IH
448    <(times_succn_m …) <(times_succn_m …) <(times_succn_m …)
449    >(minus_plus_distrib …)
450    <(plus_minus … lt) <IH
451    >(plus_minus_r …) /2/;
452qed.
453(*|
454lapply (not_lt_to_le … lt); #le
455@(pos_elim … p) //; #p'
456 cut (m-n = one); [ /3/ ]
457  #mn >mn >(times_n_one …) >(times_n_one …)
458  #H <H in ⊢ (???%)
459  @sym_eq @le_n_one_to_eq <H
460  >(minus_plus_distrib …) @monotonic_le_minus_l
461  /2/;
462] qed.
463
464lemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n.
465#m #n #H lapply (refl ? (m-n));elim (m-n) in ⊢ (???% → %);//;
466#H' lapply (minus_to_plus … H'); /2/;
467<(plus_n_O …) #H'' >H'' in H #H
468@False_ind @(absurd ? H ( not_le_Sn_n n))
469qed.
470*)
471
472let 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
478let 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
484inductive 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
488lemma lt_p0: ∀n:Pos. one < p0 n.
489#n normalize; /2/; qed.
490
491lemma lt_p1: ∀n:Pos. one < p1 n.
492#n' normalize; >(?:p1 n' = succ (p0 n')) //; qed.
493
494lemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉.
495#m elim m;
496[ //;
497| 2,3: #m' #IH normalize; >IH //;
498] qed.
499
500lemma pos_nonzero2: ∀n. ∀P:Pos→Type[0]. ∀Q:Type[0]. match succ n with [ one ⇒ Q | p0 p ⇒ P (p0 p) | p1 p ⇒ P (p1 p) ] = P (succ n).
501#n #P #Q @succ_elim /2/; qed.
502
503lemma 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 lapply (pos_compare_to_Prop n m); lapply (minus_to_plus n m);
510normalize; cases (partial_minus n m); /2/; qed.
511
512lemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m.
513#n #m #lt elim lt; /2/;
514qed.
515
516lemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m.
517#n #m #lt @(transitive_lt ? (p0 m) ?) /2/;
518qed.
519
520lemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m.
521#n #m #lt inversion lt;
522[ #H >(succ_injective … H) //;
523| #p #H1 #H2 #H3 >(succ_injective … H3)
524    @(transitive_lt ? (p0 p) ?) /2/;
525]
526qed.
527
528lemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m.
529#n #m #lt elim lt; /2/;
530qed.
531
532
533
534lemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m.
535#n #m #lt inversion lt;
536[ #p #H destruct;
537| #n' #m' #lt #e1 #e2 destruct @lt
538] qed.
539
540lemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b.
541#a #b /2/; qed.
542
543lemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b.
544#a #b >(?:p1 b = succ (p0 b)) /2/; qed.
545
546lemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
547/2/; qed.
548
549lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
550#A #B #a1 #a2 #b1 #b2 #H destruct //
551qed.
552
553lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
554#A #B #a1 #a2 #b1 #b2 #H destruct //
555qed.
556
557theorem 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 @(pos_cases … n)
561[ >(divide_by_one m) #dv #md #H destruct /2/
562| #n' elim m;
563  [ #dv #md normalize; >(pos_nonzero …) #H destruct /3/
564  | #m' #IH #dv #md whd in ⊢ (??%? → ?(???%)?);
565      lapply (refl ? (divide m' (succ n')));
566      elim (divide m' (succ n')) in ⊢ (???% → % → ?);
567      #dv' #md' #DIVr elim (IH … DIVr);
568      whd in ⊢ (? → ? → ??%? → ?);
569      cases md';
570      [ cases dv'; normalize;
571        [ #H destruct
572        | #dv'' #Hr1 #Hr2 >(pos_nonzero …) #H destruct % /2/
573        ]
574      | cases dv'; [ 2: #dv'' ] @succ_elim
575          normalize; #n #md'' #Hr1 #Hr2
576          lapply (plt_lt … Hr2); #Hr2'
577          lapply (partial_minus_to_Prop md'' n);
578          cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize
579          #lt #e destruct % [ /3/ | *: /2/ ] @plt_pos
580          [ 1,3,5,7: @double_lt1 /2/;
581          | 2,4: @double_lt3 /2/;
582          | *: @double_lt2 /2/;
583          ]
584      ]
585  | #m' #IH #dv #md whd in ⊢ (??%? → ?);
586      lapply (refl ? (divide m' (succ n')));
587      elim (divide m' (succ n')) in ⊢ (???% → % → ?);
588      #dv' #md' #DIVr elim (IH … DIVr);
589      whd in ⊢ (? → ? → ??%? → ?); cases md';
590      [ cases dv'; normalize;
591        [ #H destruct;
592        | #dv'' #Hr1 #Hr2 #H destruct; /3/;
593        ]
594      | (*cases dv'; [ 2: #dv'' ] @succ_elim
595          normalize; #n #md'' #Hr1 #Hr2 *) #md'' #Hr1 #Hr2
596          lapply (plt_lt … Hr2); #Hr2'
597          whd in ⊢ (??%? → ?);
598          lapply (partial_minus_to_Prop (p0 md'') (succ n'));
599          cases (partial_minus (p0 md'') (succ n')); [ 3(*,6,9,12*): #r'' ]
600          cases dv' in Hr1 ⊢ %; [ 2,4,6: #dv'' ] normalize
601          #Hr1 destruct [ 1,2,3: >(p0_plus ? md'') ]
602          #lt #e [ 1,3,4,6: >lt ]
603          <(pair_eq1 ?????? e) <(pair_eq2 ?????? e)
604          normalize in ⊢ (?(???%)?); % /2/; @plt_pos
605          [ cut (succ n' + r'' < p0 (succ n')); /2/;
606          | cut (succ n' + r'' < p0 (succ n')); /2/;
607          | /2/;
608          | /2/;
609          ]
610      ]
611  ]
612] qed.
613
614lemma mod0_divides: ∀m,n,dv:Pos.
615  divide n m = 〈ppos dv,pzero〉 → m∣n.
616#m #n #dv #DIVIDE %{dv} lapply (divide_ok … DIVIDE) *; (* XXX: need ; or it eats normalize *)
617normalize #H destruct //
618qed.
619
620lemma divides_mod0: ∀dv,m,n:Pos.
621  n = dv*m → divide n m = 〈ppos dv,pzero〉.
622#dv #m #n #DIV lapply (refl ? (divide n m));
623elim (divide n m) in ⊢ (???% → ?); #dv' #md' #DIVIDE
624lapply (divide_ok … DIVIDE); *;
625cases dv' in DIVIDE ⊢ %; [ 2: #dv'' ]
626cases md'; [ 2,4: #md'' ] #DIVIDE  normalize;
627>DIV in ⊢ (% → ?) #H #lt destruct;
628[ lapply (plus_to_minus … e0);
629    >(commutative_times …) >(commutative_times dv'' …)
630    cut (dv'' < dv); [ cut (dv''*m < dv*m); /2/; ] #dvlt
631    >(minus_times_distrib_l …) //;
632
633 (*cut (0 < dv-dv'); [ lapply (not_le_to_lt … nle); /2/ ]
634    #Hdv *) #H' cut (md'' ≥ m); /2/; lapply (plt_lt … lt); #A #B @False_ind
635    @(absurd ? B (lt_to_not_le … A))
636
637| @False_ind @(absurd ? (plt_lt … lt) ?) /2/;
638
639| >DIVIDE cut (dv = dv''); /2/;
640]
641qed.
642
643lemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n).
644#m #n lapply (refl ? (divide n m)); elim (divide n m) in ⊢ (???% → %);
645#dv #md cases md; cases dv;
646[ #DIVIDES lapply (divide_ok … DIVIDES); *; normalize; #H destruct
647| #dv' #H %1 @mod0_divides /2/;
648| #md' #DIVIDES %2 @nmk *; #dv'
649    >(commutative_times …) #H lapply (divides_mod0 … H);
650    >DIVIDES #H'
651    destruct;
652| #md' #dv' #DIVIDES %2 @nmk *; #dv'
653    >(commutative_times …) #H lapply (divides_mod0 … H);
654    >DIVIDES #H'
655    destruct;
656] qed.
657
658theorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q).
659#p #q cases p;
660[ cases q; normalize; [ %2 /2/; | *: #m %2 /2/; ]
661| *: #n cases q; normalize; /2/;
662] qed.
663
664definition natp_to_Z ≝
665λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ].
666
667definition 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. *)
672definition 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 [ 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 [ 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
691definition 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 [ 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 [ 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
715lemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
716#x #y cases y;
717[ #H @(False_ind … H)
718| #m #_ cases x; //; #n
719    whd in ⊢ (?%?);
720    lapply (pos_compare_to_Prop n m);
721    cases (pos_compare n m); /2/
722    #lt whd <(minus_Sn_m … lt) /2/;
723| #m #H @(False_ind … H)
724] qed.
725
726lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
727#n #m #lt lapply (pos_compare_to_Prop n m); cases (pos_compare n m);
728[ //;
729| 2,3: #H @False_ind @(absurd ? lt ?) /3/;
730] qed.
731
732theorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y.
733#x #y cases y;
734[ #H @(False_ind … H)
735| #m #_ cases x;
736  [ % //;
737  | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m));
738      cases (divide n m) in ⊢ (???% → %); #dv #md #H
739      elim (divide_ok … H); #e #l elim l; /2/;
740  | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m));
741      cases (divide n m) in ⊢ (???% → %); #dv #md #H
742      elim (divide_ok … H); #e #l elim l;
743      [ /2/;
744      | #md' #m' #l' %
745        [ whd in ⊢ (??%); >(pos_compare_n_m_m_n …)
746            >(pos_compare_lt … l') //;
747        | @Zminus_Zlt //;
748        ]
749      ]
750  ]
751| #m #H @(False_ind … H)
752] qed.
Note: See TracBrowser for help on using the repository browser.