source: src/utilities/extralib.ma @ 1516

Last change on this file since 1516 was 1516, checked in by sacerdot, 8 years ago

Ported to syntax of Matita 0.99.1.

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 by le_to_le_to_eq, le_n, eq_f/ | *: normalize /2 by plt_zero, plt_pos/ ] @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.