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