source: src/utilities/binary/positive.ma

Last change on this file was 2310, checked in by garnier, 7 years ago

Moved a lemma from switchRemoval to positive.

File size: 32.6 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 by eq_f, sym_eq/
216    normalize; cases n' //
217] qed.
218
219theorem commutative_plus_pos : 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_pos (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 by succ_injective, trans_eq/
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 by le_n_one_to_eq, monotonic_pred, eq_f, sym_eq/
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_pos: ∀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_pos :∀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_pos :∀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  [|@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/2/; qed.
1141
1142lemma cmp_nat: ∀n,m:Pos.cmp_cases n m.
1143#n #m lapply (pos_compare_to_Prop n m)
1144cases (pos_compare n m);normalize; /3 by lt_times_n_to_lt_l, le_n, cmp_le, cmp_gt, lt_to_le/
1145qed.
1146
1147
1148
1149
1150let rec two_power_nat (n:nat) : Pos ≝
1151match n with
1152[ O ⇒ one
1153| S n' ⇒ p0 (two_power_nat n')
1154].
1155
1156definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p).
1157
1158
1159
1160definition max : Pos → Pos → Pos ≝
1161λn,m. match leb n m with [ true ⇒ m | _ ⇒ n].
1162
1163lemma commutative_max : commutative Pos max.
1164#n #m whd in ⊢ (??%%);
1165lapply (pos_compare_to_Prop n m)
1166cases (pos_compare n m) whd in ⊢ (% → ?); #H
1167[ >(le_to_leb_true n m) >(not_le_to_leb_false m n) /2/
1168| >H @refl
1169| >(le_to_leb_true m n) >(not_le_to_leb_false n m) /2/
1170] qed.
1171
1172lemma max_l : ∀m,n:Pos. m ≤ max m n.
1173#m #n normalize @leb_elim //
1174qed.
1175
1176lemma max_r : ∀m,n:Pos. n ≤ max m n.
1177#m #n >commutative_max //
1178qed.
1179
1180lemma max_one_neutral : ∀v. max v one = v.
1181* // qed.
1182
1183(* Auxilliary lemmas to prove associative_max. *)
1184lemma reflexive_leb : ∀a. leb a a = true.
1185#a @(le_to_leb_true a a) // qed.
1186
1187lemma le_S_weaken : ∀a,b. le (succ a) b → le a b.
1188#a #b /2/ qed.
1189
1190lemma le_S_contradiction_1 : ∀a. le (succ a) a → False.
1191* /2 by absurd/ qed.
1192
1193lemma le_S_contradiction_2 : ∀a,b. le (succ a) b → le (succ b) a → False.
1194#a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2))
1195#Heq @(le_S_contradiction_1 a) destruct // qed.
1196
1197lemma le_S_contradiction_3 : ∀a,b,c. le (succ a) b → le (succ b) c → le (succ c) a → False.
1198#a #b #c #H1 #H2 #H3 lapply (transitive_le … H1 (le_S_weaken ?? H2)) #H4
1199@(le_S_contradiction_2 … H3 H4)
1200qed.
1201
1202(* There ought to be a simpler proof. *)
1203lemma associative_max : associative ? max.
1204#a #b #c
1205whd in ⊢ (??%%); whd in match (max a b); whd in match (max b c);
1206lapply (pos_compare_to_Prop a b)
1207cases (pos_compare a b) whd in ⊢ (% → ?); #Hab
1208[ 1: >(le_to_leb_true a b) normalize nodelta /2/
1209     lapply (pos_compare_to_Prop b c)
1210     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
1211     [ 1: >(le_to_leb_true b c) normalize nodelta
1212          lapply (pos_compare_to_Prop a c)
1213          cases (pos_compare a c) whd in ⊢ (% → ?); #Hac
1214          [ 1: >(le_to_leb_true a c) /2/
1215          | 2: destruct cases (leb c c) //
1216          | 3: (* There is an obvious contradiction in the hypotheses. omega, I miss you *)
1217               @(False_ind … (le_S_contradiction_3 ??? Hab Hbc Hac))           
1218          ]
1219          @le_S_weaken //
1220     | 2: destruct
1221          cases (leb c c) normalize nodelta
1222          >(le_to_leb_true a c) /2/
1223     | 3: >(not_le_to_leb_false b c) normalize nodelta /2/
1224          >(le_to_leb_true a b) /2/
1225     ]
1226| 2: destruct (Hab) >reflexive_leb normalize nodelta
1227     lapply (pos_compare_to_Prop b c)
1228     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
1229     [ 1: >(le_to_leb_true b c) normalize nodelta
1230          >(le_to_leb_true b c) normalize nodelta
1231          /2/
1232     | 2: destruct >reflexive_leb normalize nodelta
1233          >reflexive_leb //
1234     | 3: >(not_le_to_leb_false b c) normalize nodelta
1235          >reflexive_leb /2/ ]
1236| 3: >(not_le_to_leb_false a b) normalize nodelta /2/
1237     lapply (pos_compare_to_Prop b c)
1238     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
1239     [ 1: >(le_to_leb_true b c) normalize nodelta /2/
1240     | 2: destruct >reflexive_leb normalize nodelta @refl
1241     | 3: >(not_le_to_leb_false b c) normalize nodelta
1242          >(not_le_to_leb_false a b) normalize nodelta
1243          >(not_le_to_leb_false a c) normalize nodelta
1244          lapply (transitive_le … Hbc (le_S_weaken … Hab))
1245          #Hca /2/
1246     ]
1247] qed.
1248
1249lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT.
1250#n #m #lt lapply (pos_compare_to_Prop n m); cases (pos_compare n m);
1251[ //;
1252| 2,3: #H @False_ind @(absurd ? lt ?) /3/;
1253] qed.
1254
1255lemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
1256#n #m @eqb_elim //; qed.
Note: See TracBrowser for help on using the repository browser.