source: src/utilities/extralib.ma @ 1515

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

Add type of maps on positive binary numbers, and use them for identifers.

Also:

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