source: src/utilities/extralib.ma @ 936

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

Revise proofs affected by recent matita change.

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