source: src/utilities/binary/positive.ma @ 697

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

Merge Clight branch of vectors and friends.
Start making stuff build.

File size: 29.1 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
15(* little endian positive binary numbers. *)
16
17include "basics/logic.ma".
18include "arithmetics/nat.ma".
19include "utilities/oldlib/eq.ma".
20
21(* arithmetics/comparison.ma --> *)
22inductive compare : Type[0] ≝
23| LT : compare
24| EQ : compare
25| GT : compare.
26
27definition compare_invert: compare → compare ≝
28  λc.match c with
29      [ LT ⇒ GT
30      | EQ ⇒ EQ
31      | GT ⇒ LT ].
32
33(* <-- *)
34
35inductive Pos : Type[0] ≝
36  | one : Pos
37  |  p1 : Pos → Pos
38  |  p0 : Pos → Pos.
39
40let rec pred (n:Pos) ≝
41  match n with
42  [ one ⇒ one
43  | p1 ps ⇒ p0 ps
44  | p0 ps ⇒ match ps with [ one ⇒ one | _ ⇒ p1 (pred ps) ]
45  ].
46
47example test : pred (p0 (p0 (p0 one))) = p1 (p1 one).
48//; qed.
49
50let rec succ (n:Pos) ≝
51  match n with
52  [ one ⇒ p0 one
53  | p0 ps ⇒ p1 ps
54  | p1 ps ⇒ p0 (succ ps)
55  ].
56
57lemma succ_elim : ∀P:Pos → Prop. (∀n. P (p0 n)) → (∀n. P (p1 n)) → ∀n. P (succ n).
58#P #H0 #H1 #n cases n; normalize; //; qed.
59
60theorem pred_succ_n : ∀n. n = pred (succ n).
61#n elim n;
62[ 1,3: //
63| #p' normalize; @succ_elim /2/;
64] qed.
65(*
66theorem succ_pred_n : ∀n. n≠one → n = succ (pred n).
67#n elim n;
68[ #H @False_ind elim H; /2/;
69| //;
70| #n' cases n'; /2/; #n'' #IH #_ <IH normalize; 
71*)
72theorem succ_injective: injective Pos Pos succ.
73//; qed.
74
75let rec nat_of_pos (p:Pos) : nat ≝
76  match p with
77  [ one ⇒ 1
78  | p0 ps ⇒ 2 * (nat_of_pos ps)
79  | p1 ps ⇒ S (2 * (nat_of_pos ps))
80  ].
81
82let rec succ_pos_of_nat (n:nat) : Pos ≝
83  match n with
84  [ O ⇒ one
85  | S n' ⇒ succ (succ_pos_of_nat n')
86  ].
87
88theorem succ_nat_pos: ∀n:nat. succ_pos_of_nat (S n) = succ (succ_pos_of_nat n).
89//; qed.
90
91theorem succ_pos_of_nat_inj: injective ?? succ_pos_of_nat.
92#n elim n;
93[ #m cases m;
94  [ //
95  | #m' normalize; @succ_elim #p #H destruct
96  ]
97| #n' #IH #m cases m;
98  [ normalize; @succ_elim #p #H destruct;
99  | normalize; #m' #H >(IH m' ?) //;
100  ]
101] qed.
102
103example test2 : nat_of_pos (p0 (p1 one)) = 6. //; qed.
104
105(* Usual induction principle; proof roughly following Coq's,
106   apparently due to Conor McBride. *)
107
108inductive possucc : Pos → Prop ≝
109  | psone  : possucc one
110  | pssucc : ∀n. possucc n → possucc (succ n).
111
112let rec possucc0 (n:Pos) (p:possucc n) on p : possucc (p0 n) ≝
113  match p return λn',p'.possucc (p0 n') with
114  [ psone ⇒ pssucc ? psone
115  | pssucc _ p'' ⇒ pssucc ? (pssucc ? (possucc0 ? p''))
116  ].
117
118let rec possucc1 (n:Pos) (p:possucc n) on p : possucc (p1 n) ≝
119  match p return λn',p'. possucc (p1 n') with
120  [ psone ⇒ pssucc ? (pssucc ? psone)
121  | pssucc _ p' ⇒ pssucc ? (pssucc ? (pssucc ? (possucc0 ? p')))
122  ].
123
124let rec possuccinj (n:Pos) : possucc n ≝
125  match n with
126  [ one ⇒ psone
127  | p0 ps ⇒ possucc0 ? (possuccinj ps)
128  | p1 ps ⇒ possucc1 ? (possuccinj ps)
129  ].
130
131let rec possucc_elim
132  (P : Pos → Prop)
133  (Pone : P one)
134  (Psucc : ∀n. P n → P (succ n))
135  (n : Pos)
136  (p:possucc n) on p : P n ≝
137  match p with
138  [ psone ⇒ Pone
139  | pssucc _ p' ⇒ Psucc ? (possucc_elim P Pone Psucc ? p')
140  ].
141
142definition pos_elim : ∀P:Pos → Prop. P one → (∀n. P n → P (succ n)) → ∀n. P n.
143#P #Pone #Psucc #n @(possucc_elim … (possuccinj n)) /2/; qed.
144
145let rec possucc_cases
146  (P : Pos → Prop)
147  (Pone : P one)
148  (Psucc : ∀n. P (succ n))
149  (n : Pos)
150  (p:possucc n) on p : P n ≝
151  match p with
152  [ psone ⇒ Pone
153  | pssucc _ p' ⇒ Psucc ?
154  ].
155
156definition pos_cases : ∀P:Pos → Prop. P one → (∀n. P (succ n)) → ∀n. P n.
157#P #Pone #Psucc #n @(possucc_cases … (possuccinj n)) /2/; qed.
158
159theorem succ_pred_n : ∀n. n≠one → n = succ (pred n).
160@pos_elim
161[ #H @False_ind elim H; /2/;
162| //;
163] qed.
164
165theorem not_eq_one_succ : ∀n:Pos. one ≠ succ n.
166#n elim n; normalize;
167[ % #H destruct;
168| 2,3: #n' #H % #H' destruct;
169] qed.
170
171theorem not_eq_n_succn: ∀n:Pos. n ≠ succ n.
172#n elim n;
173[ //;
174| *: #n' #IH normalize; % #H destruct
175] qed.
176
177theorem pos_elim2:
178 ∀R:Pos → Pos → Prop.
179  (∀n:Pos. R one n)
180  → (∀n:Pos. R (succ n) one)
181  → (∀n,m:Pos. R n m → R (succ n) (succ m))
182  → ∀n,m:Pos. R n m.
183#R #ROn #RSO #RSS @pos_elim //;
184#n0 #Rn0m @pos_elim /2/; qed.
185
186
187theorem decidable_eq_pos: ∀n,m:Pos. decidable (n=m).
188@pos_elim2 #n
189[ @(pos_elim ??? n) /2/;
190| /3/;
191| #m #Hind cases Hind; /3/;
192] qed.
193
194let rec plus n m ≝
195  match n with
196  [ one ⇒ succ m
197  | p0 n' ⇒
198    match m with
199    [ one ⇒ p1 n'
200    | p0 m' ⇒ p0 (plus n' m')
201    | p1 m' ⇒ p1 (plus n' m')
202    ]
203  | p1 n' ⇒
204    match m with
205    [ one ⇒ succ n
206    | p0 m' ⇒ p1 (plus n' m')
207    | p1 m' ⇒ p0 (succ (plus n' m'))
208    ]
209  ].
210
211interpretation "positive plus" 'plus x y = (plus x y).
212
213theorem plus_n_succm: ∀n,m. succ (n + m) = n + (succ m).
214#n elim n; normalize;
215[ //
216| 2,3: #n' #IH #m cases m; /3/;
217    normalize; cases n'; //;
218] qed.
219
220theorem commutative_plus : commutative ? plus.
221#n elim n;
222[ #y cases y; normalize; //;
223| 2,3: #n' #IH #y cases y; normalize; //;
224] qed.
225
226theorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m.
227#n #m >(commutative_plus (succ n) m)
228<(plus_n_succm …) //; qed.
229
230theorem associative_plus : associative Pos plus.
231@pos_elim
232[ normalize; //;
233| #x' #IHx @pos_elim
234  [ #z <(pluss_succn_m …) <(pluss_succn_m …)
235      <(pluss_succn_m …) //;
236  | #y' #IHy' #z
237      <(pluss_succn_m y' …)
238      <(plus_n_succm …)
239      <(plus_n_succm …)
240      <(pluss_succn_m ? z) >(IHy' …) //;
241  ]
242] qed.
243
244theorem injective_plus_r: ∀n:Pos.injective Pos Pos (λm.n+m).
245@pos_elim normalize; /3/; qed.
246
247theorem injective_plus_l: ∀n:Pos.injective Pos Pos (λm.m+n).
248/2/; qed.
249
250theorem nat_plus_pos_plus: ∀n,m:nat. succ_pos_of_nat (n+m) = pred (succ_pos_of_nat n + succ_pos_of_nat m).
251#n elim n;
252[ normalize; //;
253| #n' #IH #m normalize; >(IH m) <(pluss_succn_m …)
254    <(pred_succ_n ?) <(succ_pred_n …) //;
255    elim n'; normalize; /2/;
256] qed.
257
258let rec times n m ≝
259match n with
260[ one ⇒ m
261| p0 n' ⇒ p0 (times n' m)
262| p1 n' ⇒ m + p0 (times n' m)
263].
264
265interpretation "positive times" 'times x y = (times x y).
266
267lemma p0_times2: ∀n. p0 n = (succ one) * n.
268//; qed.
269
270lemma plus_times2: ∀n. n + n = (succ one) * n.
271#n elim n;
272[ //;
273| 2,3: #n' #IH normalize; >IH //;
274] qed.
275
276
277theorem times_succn_m: ∀n,m. m+n*m = (succ n)*m.
278#n elim n;
279[ /2/
280| #n' #IH normalize; #m <(IH m) //;
281| /2/
282] qed.
283
284theorem times_n_succm: ∀n,m:Pos. n+(n*m) = n*(succ m).
285@pos_elim
286[ //
287| #n #IH #m <(times_succn_m …) <(times_succn_m …) /3/;
288] qed.
289
290theorem times_n_one: ∀n:Pos. n * one = n.
291#n elim n; /3/; qed.
292
293theorem commutative_times: commutative Pos times.
294@pos_elim /2/; qed.
295
296theorem distributive_times_plus : distributive Pos times plus.
297@pos_elim /2/; qed.
298
299theorem distributive_times_plus_r: ∀a,b,c:Pos. (b+c)*a = b*a + c*a.
300//; qed.
301
302theorem associative_times: associative Pos times.
303@pos_elim
304[ //;
305| #x #IH #y #z <(times_succn_m …) <(times_succn_m …) //;
306] qed.
307
308lemma times_times: ∀x,y,z:Pos. x*(y*z) = y*(x*z).
309//; qed.
310
311(*** ordering relations ***)
312
313(* sticking closely to the unary version; not sure if this is a good idea,
314   but it means the proofs are much the same. *)
315
316inductive le (n:Pos) : Pos → Prop ≝
317  | le_n : le n n
318  | le_S : ∀m:Pos. le n m → le n (succ m).
319
320interpretation "positive 'less than or equal to'" 'leq x y = (le x y).
321interpretation "positive 'neither less than or equal to'" 'nleq x y = (Not (le x y)).
322
323definition lt: Pos → Pos → Prop ≝ λn,m. succ n ≤ m.
324
325interpretation "positive 'less than'" 'lt x y = (lt x y).
326interpretation "positive 'not less than'" 'nless x y = (Not (lt x y)).
327
328definition ge: Pos → Pos → Prop ≝ λn,m:Pos. m ≤ n.
329
330interpretation "positive 'greater than or equal to'" 'geq x y = (ge x y).
331interpretation "positive 'neither greater than or equal to'" 'ngeq x y = (Not (ge x y)).
332
333definition gt: Pos → Pos → Prop ≝ λn,m. m<n.
334
335interpretation "positive 'greater than'" 'gt x y = (gt x y).
336interpretation "positive 'not greater than'" 'ngtr x y = (Not (gt x y)).
337
338theorem transitive_le: transitive Pos le.
339#a #b #c #leab #lebc elim lebc; /2/; qed.
340
341theorem transitive_lt: transitive Pos lt.
342#a #b #c #ltab #ltbc elim ltbc; /2/; qed.
343
344theorem le_succ_succ: ∀n,m:Pos. n ≤ m → succ n ≤ succ m.
345#n #m #lenm elim lenm; /2/; qed.
346
347theorem le_one_n : ∀n:Pos. one ≤ n.
348@pos_elim /2/; qed.
349
350theorem le_n_succn : ∀n:Pos. n ≤ succ n.
351/2/; qed.
352
353theorem le_pred_n : ∀n:Pos. pred n ≤ n.
354@pos_elim //; qed.
355
356theorem monotonic_pred: monotonic Pos le pred.
357#n #m #lenm elim lenm; /2/;qed.
358
359theorem le_S_S_to_le: ∀n,m:Pos. succ n ≤ succ m → n ≤ m.
360/2/; qed.
361
362(* lt vs. le *)
363theorem not_le_succ_one: ∀ n:Pos. succ n ≰ one.
364#n % #H inversion H /2/; qed.
365
366theorem not_le_to_not_le_succ_succ: ∀ n,m:Pos. n ≰ m → succ n ≰ succ m.
367#n #m @not_to_not @le_S_S_to_le qed.
368
369theorem not_le_succ_succ_to_not_le: ∀ n,m:Pos. succ n ≰ succ m → n ≰ m.
370#n #m @not_to_not /2/ qed.
371
372theorem decidable_le: ∀n,m:Pos. decidable (n≤m).
373@pos_elim2 #n /2/;
374#m *; /3/; qed.
375
376theorem decidable_lt: ∀n,m:Pos. decidable (n < m).
377#n #m @decidable_le  qed.
378
379theorem not_le_succ_n: ∀n:Pos. succ n ≰ n.
380@pos_elim //;
381#m #IH @not_le_to_not_le_succ_succ //;
382qed.
383
384theorem not_le_to_lt: ∀n,m:Pos. n ≰ m → m < n.
385@pos_elim2 #n
386 [#abs @False_ind /2/;
387 |/2/;
388 |#m #Hind #HnotleSS @le_succ_succ /3/;
389 ]
390qed.
391
392theorem lt_to_not_le: ∀n,m:Pos. n < m → m ≰ n.
393#n #m #Hltnm elim Hltnm;
394[ //
395| #p #H @not_to_not /2/;
396] qed.
397
398theorem not_lt_to_le: ∀n,m:Pos. n ≮ m → m ≤ n.
399/4/; qed.
400
401
402theorem le_to_not_lt: ∀n,m:Pos. n ≤ m → m ≮ n.
403#n #m #H @lt_to_not_le /2/;qed.
404
405(* lt and le trans *)
406
407theorem lt_to_le_to_lt: ∀n,m,p:Pos. n < m → m ≤ p → n < p.
408#n #m #p #H #H1 elim H1; /2/; qed.
409
410theorem le_to_lt_to_lt: ∀n,m,p:Pos. n ≤ m → m < p → n < p.
411#n #m #p #H elim H; /3/; qed.
412
413theorem lt_succ_to_lt: ∀n,m:Pos. succ n < m → n < m.
414/2/; qed.
415
416theorem ltn_to_lt_one: ∀n,m:Pos. n < m → one < m.
417/2/; qed.
418
419theorem lt_one_n_elim: ∀n:Pos. one < n →
420  ∀P:Pos → Prop.(∀m:Pos.P (succ m)) → P n.
421@pos_elim //; #abs @False_ind /2/;
422qed.
423
424(* le to lt or eq *)
425theorem le_to_or_lt_eq: ∀n,m:Pos. n ≤ m → n < m ∨ n = m.
426#n #m #lenm elim lenm; /3/; qed.
427
428(* not eq *)
429theorem lt_to_not_eq : ∀n,m:Pos. n < m → n ≠ m.
430#n #m #H @not_to_not /2/; qed.
431
432theorem not_eq_to_le_to_lt: ∀n,m:Pos. n≠m → n≤m → n<m.
433#n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle); //;
434#Heq /3/; qed.
435
436(* le elimination *)
437theorem le_n_one_to_eq : ∀n:Pos. n ≤ one → one=n.
438@pos_cases //; #a ; #abs
439@False_ind /2/;qed.
440
441theorem le_n_one_elim: ∀n:Pos. n ≤ one → ∀P: Pos →Prop. P one → P n.
442@pos_cases //; #a #abs
443@False_ind /2/; qed.
444
445theorem le_n_Sm_elim : ∀n,m:Pos.n ≤ succ m →
446∀P:Prop. (succ n ≤ succ m → P) → (n=succ m → P) → P.
447#n #m #Hle #P elim Hle; /3/; qed.
448
449(* le and eq *)
450
451theorem le_to_le_to_eq: ∀n,m:Pos. n ≤ m → m ≤ n → n = m.
452@pos_elim2 /4/;
453qed.
454
455theorem lt_one_S : ∀n:Pos. one < succ n.
456/2/; qed.
457
458(* well founded induction principles *)
459
460theorem pos_elim1 : ∀n:Pos.∀P:Pos → Prop.
461(∀m.(∀p. p < m → P p) → P m) → P n.
462#n #P #H
463cut (∀q:Pos. q ≤ n → P q);/2/;
464@(pos_elim … n)
465 [#q #HleO (* applica male *)
466    @(le_n_one_elim ? HleO)
467    @H #p #ltpO
468    @False_ind /2/; (* 3 *)
469 |#p #Hind #q #HleS
470    @H #a #lta @Hind
471    @le_S_S_to_le /2/;
472 ]
473qed.
474
475(*********************** monotonicity ***************************)
476theorem monotonic_le_plus_r:
477∀n:Pos.monotonic Pos le (λm.n + m).
478#n #a #b @(pos_elim … n) normalize; /2/;
479#m #H #leab /3/; qed.
480
481theorem monotonic_le_plus_l:
482∀m:Pos.monotonic Pos le (λn.n + m).
483/2/; qed.
484
485theorem le_plus: ∀n1,n2,m1,m2:Pos. n1 ≤ n2  → m1 ≤ m2
486→ n1 + m1 ≤ n2 + m2.
487#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
488/2/; qed.
489
490theorem le_plus_n :∀n,m:Pos. m ≤ n + m.
491/3/; qed.
492
493lemma le_plus_a: ∀a,n,m:Pos. n ≤ m → n ≤ a + m.
494/2/; qed.
495
496lemma le_plus_b: ∀b,n,m:Pos. n + b ≤ m → n ≤ m.
497/2/; qed.
498
499theorem le_plus_n_r :∀n,m:Pos. m ≤ m + n.
500/2/; qed.
501
502theorem eq_plus_to_le: ∀n,m,p:Pos.n=m+p → m ≤ n.
503//; qed.
504
505theorem le_plus_to_le: ∀a,n,m:Pos. a + n ≤ a + m → n ≤ m.
506@pos_elim normalize; /3/; qed.
507
508theorem le_plus_to_le_r: ∀a,n,m:Pos. n + a ≤ m +a → n ≤ m.
509/2/; qed.
510
511(* plus & lt *)
512
513theorem monotonic_lt_plus_r:
514∀n:Pos.monotonic Pos lt (λm.n+m).
515/2/; qed.
516
517theorem monotonic_lt_plus_l:
518∀n:Pos.monotonic Pos lt (λm.m+n).
519/2/; qed.
520
521theorem lt_plus: ∀n,m,p,q:Pos. n < m → p < q → n + p < m + q.
522#n #m #p #q #ltnm #ltpq
523@(transitive_lt ? (n+q)) /2/; qed.
524
525theorem le_lt_plus_pos: ∀n,m,p:Pos. n ≤ m → n < m + p.
526#n #m #p #H @(le_to_lt_to_lt … H)
527/2/; qed.
528
529theorem lt_plus_to_lt_l :∀n,p,q:Pos. p+n < q+n → p<q.
530/2/; qed.
531
532theorem lt_plus_to_lt_r :∀n,p,q:Pos. n+p < n+q → p<q.
533/2/; qed.
534
535(* times *)
536theorem monotonic_le_times_r:
537∀n:Pos.monotonic Pos le (λm. n * m).
538#n #x #y #lexy @(pos_elim … n) normalize;//;(* lento /2/;*)
539#a #lea /2/;
540qed.
541
542theorem le_times: ∀n1,n2,m1,m2:Pos.
543n1 ≤ n2  → m1 ≤ m2 → n1*m1 ≤ n2*m2.
544#n1 #n2 #m1 #m2 #len #lem
545@(transitive_le ? (n1*m2)) (* /2/ slow *)
546 [ @monotonic_le_times_r //;
547 | applyS monotonic_le_times_r;//;
548 ]
549qed.
550
551theorem lt_times_n: ∀n,m:Pos. m ≤ n*m.
552#n #m /2/; qed.
553
554theorem le_times_to_le:
555∀a,n,m:Pos. a * n ≤ a * m → n ≤ m.
556#a @pos_elim2 normalize;
557  [//;
558  |#n >(times_n_one …) <(times_n_succm …)
559     #H @False_ind
560     elim (lt_to_not_le ?? (le_lt_plus_pos a a (a*n) …)); /2/;
561  |#n #m #H #le
562     @le_succ_succ @H /2/;
563  ]
564qed.
565
566theorem le_S_times_2: ∀n,m:Pos. n ≤ m → succ n ≤ (succ one)*m.
567#n #m #lenm  (* interessante *)
568applyS (le_plus n m); //; qed.
569
570(* prove injectivity of times from above *)
571theorem injective_times_r: ∀n:Pos.injective Pos Pos (λm.n*m).
572#n #m #p #H @le_to_le_to_eq
573/2/;
574qed.
575
576theorem injective_times_l: ∀n:Pos.injective Pos Pos (λm.m*n).
577/2/; qed.
578
579(* times & lt *)
580
581theorem monotonic_lt_times_l:
582  ∀c:Pos. monotonic Pos lt (λt.(t*c)).
583#c #n #m #ltnm
584elim ltnm; normalize;
585  [/2/;
586  |#a #_ #lt1 @(transitive_le ??? lt1) //;
587  ]
588qed.
589
590theorem monotonic_lt_times_r:
591  ∀c:Pos. monotonic Pos lt (λt.(c*t)).
592#a #b #c #H
593>(commutative_times a b) >(commutative_times a c)
594/2/; qed.
595
596theorem lt_to_le_to_lt_times:
597∀n,m,p,q:Pos. n < m → p ≤ q → n*p < m*q.
598#n #m #p #q #ltnm #lepq
599@(le_to_lt_to_lt ? (n*q))
600  [@monotonic_le_times_r //;
601  |@monotonic_lt_times_l //;
602  ]
603qed.
604
605theorem lt_times:∀n,m,p,q:Pos. n<m → p<q → n*p < m*q.
606#n #m #p #q #ltnm #ltpq
607@lt_to_le_to_lt_times /2/;
608qed.
609
610theorem lt_times_n_to_lt_l:
611∀n,p,q:Pos. p*n < q*n → p < q.
612#n #p #q #Hlt
613elim (decidable_lt p q);//;
614#nltpq @False_ind
615@(absurd ? ? (lt_to_not_le ? ? Hlt))
616applyS monotonic_le_times_r;/2/;
617qed.
618
619theorem lt_times_n_to_lt_r:
620∀n,p,q:Pos. n*p < n*q → p < q.
621/2/; qed.
622
623(**** minus ****)
624
625inductive minusresult : Type[0] ≝
626 | MinusNeg: minusresult
627 | MinusZero: minusresult
628 | MinusPos: Pos → minusresult.
629
630let rec partial_minus (n,m:Pos) : minusresult ≝
631match n with
632[ one ⇒ match m with [ one ⇒ MinusZero | _ ⇒ MinusNeg ]
633| p0 n' ⇒
634  match m with
635  [ one ⇒ MinusPos (pred n)
636  | p0 m' ⇒ match partial_minus n' m' with
637            [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusZero | MinusPos p ⇒ MinusPos (p0 p) ]
638  | p1 m' ⇒ match partial_minus n' m' with
639            [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusNeg | MinusPos p ⇒ MinusPos (pred (p0 p)) ]
640  ]
641| p1 n' ⇒
642  match m with
643  [ one ⇒ MinusPos (p0 n')
644  | p0 m' ⇒ match partial_minus n' m' with
645            [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusPos one | MinusPos p ⇒ MinusPos (p1 p) ]
646  | p1 m' ⇒ match partial_minus n' m' with
647            [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusZero | MinusPos p ⇒ MinusPos (p0 p) ]
648  ]
649].
650
651example testminus0: partial_minus (p0 one) (p1 one) = MinusNeg. //; qed.
652example testminus1: partial_minus (p0 one) (p0 (p0 one)) = MinusNeg. //; qed.
653example testminus2: partial_minus (p0 (p0 one)) (p0 one) = MinusPos (p0 one). //; qed.
654example testminus3: partial_minus (p0 one) one = MinusPos one. //; qed.
655example testminus4: partial_minus (succ (p1 one)) (p1 one) = MinusPos one. //; qed.
656
657definition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p | _ ⇒ one ].
658
659interpretation "natural minus" 'minus x y = (minus x y).
660
661lemma partialminus_S: ∀n,m:Pos.
662match partial_minus (succ n) m with
663[ MinusPos p ⇒ match p with [ one ⇒ partial_minus n m = MinusZero | _ ⇒ partial_minus n m = MinusPos (pred p) ]
664| _ ⇒ partial_minus n m = MinusNeg
665].
666#n elim n;
667[ #m cases m;
668  [ //;
669  | 2,3: #m' cases m'; //;
670  ]
671(* The other two cases are the same.  I'd combine them, but the numbering
672   would be even more horrific. *)
673| #n' #IH #m cases m;
674  [ normalize; <(pred_succ_n n') cases n'; //;
675  | 2,3: #m' normalize; lapply (IH m'); cases (partial_minus (succ n') m');
676    [ 1,2,4,5: normalize; #H >H //;
677    | 3,6: #p cases p; [ 1,4: normalize; #H >H //;
678                      | 2,3,5,6: #p' normalize; #H >H //;
679                      ]
680    ]
681  ]
682| #n' #IH #m cases m;
683  [ normalize; <(pred_succ_n n') cases n'; //;
684  | 2,3: #m' normalize; lapply (IH m'); cases (partial_minus (succ n') m');
685    [ 1,2,4,5: normalize; #H >H //;
686    | 3,6: #p cases p; [ 1,4: normalize; #H >H //;
687                      | 2,3,5,6: #p' normalize; #H >H //;
688                      ]
689    ]
690  ]
691] qed.
692
693lemma partialminus_n_S: ∀n,m:Pos.
694  match partial_minus n m with
695  [ MinusPos p ⇒ match p with [ one ⇒ partial_minus n (succ m) = MinusZero
696                              | _ ⇒ partial_minus n (succ m) = MinusPos (pred p)
697                              ]
698  | _ ⇒ partial_minus n (succ m) = MinusNeg
699  ].
700#n elim n;
701[ #m cases m; //;
702(* Again, lots of unnecessary duplication! *)
703| #n' #IH #m cases m;
704  [ normalize; cases n'; //;
705  | #m' normalize; lapply (IH m'); cases (partial_minus n' m');
706    [ 1,2: normalize; #H >H //;
707    | #p cases p; normalize; [ #H >H //;
708                                  | 2,3: #p' #H >H //;
709                                  ]
710    ]
711  |  #m' normalize; lapply (IH m'); cases (partial_minus n' m');
712    [ 1,2: normalize; #H >H //;
713    | #p cases p; normalize; [ #H >H //;
714                                  | 2,3: #p' #H >H //;
715                                  ]
716    ]
717  ]
718| #n' #IH #m cases m;
719  [ normalize; cases n'; //;
720  | #m' normalize; lapply (IH m'); cases (partial_minus n' m');
721    [ 1,2: normalize; #H >H //;
722    | #p cases p; normalize; [ #H >H //;
723                                  | 2,3: #p' #H >H //;
724                                  ]
725    ]
726  |  #m' normalize; lapply (IH m'); cases (partial_minus n' m');
727    [ 1,2: normalize; #H >H //;
728    | #p cases p; normalize; [ #H >H //;
729                                  | 2,3: #p' #H >H //;
730                                  ]
731    ]
732  ]
733] qed.
734
735theorem partialminus_S_S: ∀n,m:Pos. partial_minus (succ n) (succ m) = partial_minus n m.
736#n elim n;
737[ #m cases m;
738  [ //;
739  | 2,3: #m' cases m'; //;
740  ]
741| #n' #IH #m cases m;
742  [ normalize; cases n'; /2/; normalize; #n'' <(pred_succ_n n'') cases n'';//;
743  | #m' normalize; >(IH ?) //;
744  | #m' normalize; lapply (partialminus_S n' m'); cases (partial_minus (succ n') m');
745    [ 1,2: normalize; #H >H //;
746    | #p cases p; [ normalize; #H >H //;
747                      | 2,3: #p' normalize; #H >H //;
748                      ]
749    ]
750  ]
751|  #n' #IH #m cases m;
752  [ normalize; cases n'; /2/;
753  | #m' normalize; lapply (partialminus_n_S n' m'); cases (partial_minus n' m');
754    [ 1,2: normalize; #H >H //;
755    | #p cases p;   [ normalize; #H >H //;
756                      | 2,3: #p' normalize; #H >H //;
757                      ]
758    ]
759  | #m' normalize; >(IH ?) //;
760  ]
761] qed.
762
763theorem minus_S_S: ∀n,m:Pos. (succ n) - (succ m) = n-m.
764#n #m normalize; >(partialminus_S_S n m) //; qed.
765
766theorem minus_one_n: ∀n:Pos.one=one-n.
767#n cases n; //; qed.
768
769theorem minus_n_one: ∀n:Pos.pred n=n-one.
770#n cases n; //; qed.
771
772lemma partial_minus_n_n: ∀n. partial_minus n n = MinusZero.
773#n elim n;
774[ //;
775| 2,3: normalize; #n' #IH >IH //
776] qed.
777
778theorem minus_n_n: ∀n:Pos.one=n-n.
779#n normalize; >(partial_minus_n_n n) //;
780qed.
781
782theorem minus_Sn_n: ∀n:Pos. one = (succ n)-n.
783#n cut (partial_minus (succ n) n = MinusPos one);
784[ elim n;
785  [ //;
786  | normalize; #n' #IH >IH //;
787  | normalize; #n' #IH >(partial_minus_n_n n') //;
788  ]
789| #H normalize; >H //;
790] qed.
791
792theorem minus_Sn_m: ∀m,n:Pos. m < n → succ n -m = succ (n-m).
793(* qualcosa da capire qui
794#n #m #lenm elim lenm; napplyS refl_eq. *)
795@pos_elim2
796  [#n #H @(lt_one_n_elim n H) //;
797  |#n #abs @False_ind /2/
798  |#n #m #Hind #c applyS Hind; /2/;
799  ]
800qed.
801
802theorem not_eq_to_le_to_le_minus:
803  ∀n,m:Pos.n ≠ m → n ≤ m → n ≤ m - one.
804#n @pos_cases //; #m
805#H #H1 @le_S_S_to_le
806applyS (not_eq_to_le_to_lt n (succ m) H H1);
807qed.
808
809theorem eq_minus_S_pred: ∀n,m:Pos. n - (succ m) = pred(n -m).
810@pos_elim2
811[ #n cases n; normalize; //;
812| #n @(pos_elim … n) //;
813| //;
814] qed.
815
816lemma pred_Sn_plus: ∀n,m:Pos. one < n → (pred n)+m = pred (n+m).
817#n #m #H
818@(lt_one_n_elim … H) /3/;
819qed.
820
821theorem plus_minus:
822∀m,n,p:Pos. m < n → (n-m)+p = (n+p)-m.
823@pos_elim2
824  [ #n #p #H <(minus_n_one ?) <(minus_n_one ?) /2/;
825  |#n #p #abs @False_ind /2/;
826  |#n #m #IH #p #H >(eq_minus_S_pred …) >(eq_minus_S_pred …)
827     cut (n<m); [ /2/ ] #H'
828     >(pred_Sn_plus …)
829     [ >(minus_Sn_m …) /2/;
830         <(pluss_succn_m …)
831         <(pluss_succn_m …)
832         >(minus_Sn_m …)
833         [ <(pred_succ_n …)
834             <(pred_succ_n …)
835             @IH /2/;
836         | /2/;
837         ]
838     | >(minus_Sn_m … H') //;
839     ]
840  ] qed.
841
842(* XXX: putting this in the appropriate case screws up auto?! *)
843theorem succ_plus_one: ∀n. succ n = n + one.
844#n elim n; //; qed.
845
846theorem nat_possucc: ∀p. nat_of_pos (succ p) = S (nat_of_pos p).
847#p elim p; normalize;
848[ //;
849| #q #IH <(plus_n_O …) <(plus_n_O …)
850    >IH <(plus_n_Sm …) //;
851| //;
852] qed.
853
854theorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n.
855#n elim n; //; qed.
856
857theorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)-m.
858#n @pos_elim
859[ //;
860| #m #IH <(plus_n_succm …)
861    >(eq_minus_S_pred …)
862    >(minus_Sn_m …) /2/;
863] qed.
864
865theorem plus_minus_m_m: ∀n,m:Pos.
866  m < n → n = (n-m)+m.
867#n #m #lemn applyS sym_eq;
868applyS (plus_minus m n m); //; qed.
869
870theorem le_plus_minus_m_m: ∀n,m:Pos. n ≤ (n-m)+m.
871@pos_elim
872  [//
873  |#a #Hind @pos_cases //; 
874     #n
875     >(minus_S_S …)
876     /2/;
877  ]
878qed.
879
880theorem minus_to_plus :∀n,m,p:Pos.
881  m < n → n-m = p → n = m+p.
882#n #m #p #lemn #eqp applyS plus_minus_m_m; //;
883qed.
884
885theorem plus_to_minus :∀n,m,p:Pos.n = m+p → n-m = p.
886(* /4/ done in 43.5 *)
887#n #m #p #eqp
888@sym_eq
889applyS (minus_plus_m_m p m);
890qed.
891
892theorem minus_pred_pred : ∀n,m:Pos. one < n → one < m →
893pred n - pred m = n - m.
894#n #m #posn #posm
895@(lt_one_n_elim n posn)
896@(lt_one_n_elim m posm) //.
897qed.
898
899(* monotonicity and galois *)
900
901theorem monotonic_le_minus_l:
902∀p,q,n:Pos. q ≤ p → q-n ≤ p-n.
903@pos_elim2 #p #q
904  [#lePO @(le_n_one_elim ? lePO) //;
905  |//;
906  |#Hind @pos_cases
907    [/2/;
908    |#a #leSS >(minus_S_S …) >(minus_S_S …) @Hind /2/;
909    ]
910  ]
911qed.
912
913theorem le_minus_to_plus: ∀n,m,p:Pos. n-m ≤ p → n≤ p+m.
914#n #m #p #lep
915@transitive_le
916  [|apply le_plus_minus_m_m
917  |@monotonic_le_plus_l //;
918  ]
919qed.
920
921theorem le_plus_to_minus: ∀n,m,p:Pos. n ≤ p+m → n-m ≤ p.
922#n #m #p #lep
923(* bello *)
924applyS monotonic_le_minus_l;//;
925(* /2/; *)
926qed.
927
928theorem monotonic_le_minus_r:
929∀p,q,n:Pos. q ≤ p → n-p ≤ n-q.
930#p #q #n #lepq
931@le_plus_to_minus
932@(transitive_le ??? (le_plus_minus_m_m ? q)) /2/;
933qed.
934
935(*********************** boolean arithmetics ********************)
936include "basics/bool.ma".
937
938let rec eqb n m ≝
939match n with
940  [ one ⇒ match m with [ one ⇒ true | _ ⇒ false]
941  | p0 p ⇒ match m with [ p0 q ⇒ eqb p q | _ ⇒ false]
942  | p1 p ⇒ match m with [ p1 q ⇒ eqb p q | _ ⇒ false]
943  ].
944
945theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Prop.
946(n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)).
947#n elim n;
948[ #m cases m normalize
949  [ /2/
950  | 2,3: #m' #P #t #f @f % #H destruct
951  ]
952| #n' #IH #m cases m normalize
953  [ #P #t #f @f % #H destruct
954  | #m' #P #t #f @IH
955    [ /2/
956    | * #ne @f % #e @ne destruct @refl
957    ]
958  | #m' #P #t #f @f % #H destruct;
959  ]
960| #n' #IH #m cases m; normalize;
961  [ #P #t #f @f % #H destruct;
962  | #m' #P #t #f @f % #H destruct;
963  | #m' #P #t #f @IH
964    [ /2/;
965    | * #ne @f % #e @ne destruct @refl
966    ]
967  ]
968] qed.
969
970theorem eqb_n_n: ∀n:Pos. eqb n n = true.
971#n elim n; normalize; //.
972qed.
973
974theorem eqb_true_to_eq: ∀n,m:Pos. eqb n m = true → n = m.
975#n #m @(eqb_elim n m) //;
976#_ #abs @False_ind /2/;
977qed.
978
979theorem eqb_false_to_not_eq: ∀n,m:Pos. eqb n m = false → n ≠ m.
980#n #m @(eqb_elim n m) /2/;
981qed.
982
983theorem eq_to_eqb_true: ∀n,m:Pos.
984  n = m → eqb n m = true.
985//; qed.
986
987theorem not_eq_to_eqb_false: ∀n,m:Pos.
988  n ≠  m → eqb n m = false.
989#n #m #noteq
990@eqb_elim //;
991#Heq @False_ind /2/;
992qed.
993
994let rec leb n m ≝
995match partial_minus n m with
996[ MinusNeg ⇒ true
997| MinusZero ⇒ true
998| MinusPos _ ⇒ false
999].
1000
1001lemma leb_unfold_hack: ∀n,m:Pos. leb n m =
1002match partial_minus n m with
1003[ MinusNeg ⇒ true
1004| MinusZero ⇒ true
1005| MinusPos _ ⇒ false
1006]. #n #m (* XXX: why on earth do I need to case split? *) cases n; //; qed.
1007
1008theorem leb_elim: ∀n,m:Pos. ∀P:bool → Prop.
1009(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
1010@pos_elim2
1011[ #n cases n; normalize; /2/;
1012| #n cases n; normalize;
1013  [ /2/;
1014  | 2,3: #m' #P #t #f @f /2/; % #H inversion H;
1015    [ #H' destruct;
1016    | #p /2/;
1017    ]
1018  ]
1019| #n #m #IH #P #t #f >(leb_unfold_hack …)
1020    >(partialminus_S_S n m)
1021    <(leb_unfold_hack …)
1022    @IH #H /3/;
1023] qed.
1024
1025theorem leb_true_to_le:∀n,m:Pos.leb n m = true → n ≤ m.
1026#n #m @leb_elim
1027  [//;
1028  |#_ #abs @False_ind /2/;
1029  ]
1030qed.
1031
1032theorem leb_false_to_not_le:∀n,m:Pos.
1033  leb n m = false → n ≰ m.
1034#n #m @leb_elim
1035  [#_ #abs @False_ind /2/;
1036  |//;
1037  ]
1038qed.
1039
1040theorem le_to_leb_true: ∀n,m:Pos. n ≤ m → leb n m = true.
1041#n #m @leb_elim //;
1042#H #H1 @False_ind /2/;
1043qed.
1044
1045theorem not_le_to_leb_false: ∀n,m:Pos. n ≰ m → leb n m = false.
1046#n #m @leb_elim //;
1047#H #H1 @False_ind /2/;
1048qed.
1049
1050theorem lt_to_leb_false: ∀n,m:Pos. m < n → leb n m = false.
1051/3/; qed.
1052
1053
1054(***** comparison *****)
1055
1056definition pos_compare : Pos → Pos → compare ≝
1057λn,m.match partial_minus n m with
1058[ MinusNeg ⇒ LT
1059| MinusZero ⇒ EQ
1060| MinusPos _ ⇒ GT
1061].
1062
1063theorem pos_compare_n_n: ∀n:Pos. pos_compare n n = EQ.
1064#n normalize; >(partial_minus_n_n n)
1065//; qed.
1066
1067theorem pos_compare_S_S: ∀n,m:Pos.pos_compare n m = pos_compare (succ n) (succ m).
1068#n #m normalize;
1069>(partialminus_S_S …)
1070//;
1071qed.
1072
1073theorem pos_compare_pred_pred:
1074  ∀n,m.one < n → one < m → pos_compare n m = pos_compare (pred n) (pred m).
1075#n #m #Hn #Hm
1076@(lt_one_n_elim n Hn)
1077@(lt_one_n_elim m Hm)
1078#p #q <(pred_succ_n ?) <(pred_succ_n ?)
1079<(pos_compare_S_S …) //;
1080qed.
1081
1082theorem pos_compare_S_one: ∀n:Pos. pos_compare (succ n) one = GT.
1083#n elim n; //; qed.
1084
1085theorem pos_compare_one_S: ∀n:Pos. pos_compare one (succ n) = LT.
1086#n elim n; //; qed.
1087
1088theorem pos_compare_to_Prop:
1089  ∀n,m.match (pos_compare n m) with
1090    [ LT ⇒ n < m
1091    | EQ ⇒ n = m
1092    | GT ⇒ m < n ].
1093#n #m
1094@(pos_elim2 (λn,m.match (pos_compare n m) with
1095  [ LT ⇒ n < m
1096  | EQ ⇒ n = m
1097  | GT ⇒ m < n ]) ?????) (* FIXME: don't want to put all these ?, especially when … does not work! *)
1098[1,2:@pos_cases
1099  [ 1,3: /2/;
1100  | 2,4: #m' cases m'; //;
1101  ]
1102|#n1 #m1 normalize;<(pos_compare_S_S …) cases (pos_compare n1 m1);
1103   [1,3:normalize;#IH @le_succ_succ //;
1104   |normalize;#IH >IH //]
1105qed.
1106
1107theorem pos_compare_n_m_m_n:
1108  ∀n,m:Pos.pos_compare n m = compare_invert (pos_compare m n).
1109#n #m
1110@(pos_elim2 (λn,m. pos_compare n m = compare_invert (pos_compare m n)))
1111[1,2:#n1 cases n1;/2/;
1112|#n1 #m1
1113<(pos_compare_S_S …)
1114<(pos_compare_S_S …)
1115#IH normalize @IH]
1116qed.
1117     
1118theorem pos_compare_elim :
1119  ∀n,m:Pos. ∀P:compare → Prop.
1120    (n < m → P LT) → (n=m → P EQ) → (m < n → P GT) → P (pos_compare n m).
1121#n #m #P #Hlt #Heq #Hgt
1122cut (match (pos_compare n m) with
1123    [ LT ⇒ n < m
1124    | EQ ⇒ n=m
1125    | GT ⇒ m < n] →
1126  P (pos_compare n m))
1127[cases (pos_compare n m);
1128   [@Hlt
1129   |@Heq
1130   |@Hgt]
1131|#Hcut @Hcut //;
1132qed.
1133
1134inductive cmp_cases (n,m:Pos) : CProp[0] ≝
1135  | cmp_le : n ≤ m → cmp_cases n m
1136  | cmp_gt : m < n → cmp_cases n m.
1137
1138theorem lt_to_le : ∀n,m:Pos. n < m → n ≤ m.
1139(* sic
1140#n #m #H elim H
1141[//
1142|/2/] *)
1143/2/; qed.
1144
1145lemma cmp_nat: ∀n,m:Pos.cmp_cases n m.
1146#n #m lapply (pos_compare_to_Prop n m)
1147cases (pos_compare n m);normalize; /3/;
1148qed.
1149
1150
1151
1152
1153let rec two_power_nat (n:nat) : Pos ≝
1154match n with
1155[ O ⇒ one
1156| S n' ⇒ p0 (two_power_nat n')
1157].
1158
1159definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p).
Note: See TracBrowser for help on using the repository browser.