(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) (* little endian positive binary numbers. *) include "basics/logic.ma". include "arithmetics/nat.ma". (* arithmetics/comparison.ma --> *) inductive compare : Type[0] ≝ | LT : compare | EQ : compare | GT : compare. definition compare_invert: compare → compare ≝ λc.match c with [ LT ⇒ GT | EQ ⇒ EQ | GT ⇒ LT ]. (* <-- *) inductive Pos : Type[0] ≝ | one : Pos | p1 : Pos → Pos | p0 : Pos → Pos. let rec pred (n:Pos) ≝ match n with [ one ⇒ one | p1 ps ⇒ p0 ps | p0 ps ⇒ match ps with [ one ⇒ one | _ ⇒ p1 (pred ps) ] ]. example test : pred (p0 (p0 (p0 one))) = p1 (p1 one). //; qed. let rec succ (n:Pos) ≝ match n with [ one ⇒ p0 one | p0 ps ⇒ p1 ps | p1 ps ⇒ p0 (succ ps) ]. lemma succ_elim : ∀P:Pos → Prop. (∀n. P (p0 n)) → (∀n. P (p1 n)) → ∀n. P (succ n). #P #H0 #H1 #n cases n; normalize; //; qed. theorem pred_succ_n : ∀n. n = pred (succ n). #n elim n; [ 1,3: // | #p' normalize; @succ_elim /2/; ] qed. (* theorem succ_pred_n : ∀n. n≠one → n = succ (pred n). #n elim n; [ #H @False_ind elim H; /2/; | //; | #n' cases n'; /2/; #n'' #IH #_ (IH m' ?) //; ] ] qed. example test2 : nat_of_pos (p0 (p1 one)) = 6. //; qed. (* Usual induction principle; proof roughly following Coq's, apparently due to Conor McBride. *) inductive possucc : Pos → Prop ≝ | psone : possucc one | pssucc : ∀n. possucc n → possucc (succ n). let rec possucc0 (n:Pos) (p:possucc n) on p : possucc (p0 n) ≝ match p return λn',p'.possucc (p0 n') with [ psone ⇒ pssucc ? psone | pssucc _ p'' ⇒ pssucc ? (pssucc ? (possucc0 ? p'')) ]. let rec possucc1 (n:Pos) (p:possucc n) on p : possucc (p1 n) ≝ match p return λn',p'. possucc (p1 n') with [ psone ⇒ pssucc ? (pssucc ? psone) | pssucc _ p' ⇒ pssucc ? (pssucc ? (pssucc ? (possucc0 ? p'))) ]. let rec possuccinj (n:Pos) : possucc n ≝ match n with [ one ⇒ psone | p0 ps ⇒ possucc0 ? (possuccinj ps) | p1 ps ⇒ possucc1 ? (possuccinj ps) ]. let rec possucc_elim (P : Pos → Prop) (Pone : P one) (Psucc : ∀n. P n → P (succ n)) (n : Pos) (p:possucc n) on p : P n ≝ match p with [ psone ⇒ Pone | pssucc _ p' ⇒ Psucc ? (possucc_elim P Pone Psucc ? p') ]. definition pos_elim : ∀P:Pos → Prop. P one → (∀n. P n → P (succ n)) → ∀n. P n. #P #Pone #Psucc #n @(possucc_elim … (possuccinj n)) /2/; qed. let rec possucc_cases (P : Pos → Prop) (Pone : P one) (Psucc : ∀n. P (succ n)) (n : Pos) (p:possucc n) on p : P n ≝ match p with [ psone ⇒ Pone | pssucc _ p' ⇒ Psucc ? ]. definition pos_cases : ∀P:Pos → Prop. P one → (∀n. P (succ n)) → ∀n. P n. #P #Pone #Psucc #n @(possucc_cases … (possuccinj n)) /2/; qed. theorem succ_pred_n : ∀n. n≠one → n = succ (pred n). @pos_elim [ #H @False_ind elim H; /2/; | //; ] qed. theorem not_eq_one_succ : ∀n:Pos. one ≠ succ n. #n elim n; normalize; [ % #H destruct; | 2,3: #n' #H % #H' destruct; ] qed. theorem not_eq_n_succn: ∀n:Pos. n ≠ succ n. #n elim n; [ //; | *: #n' #IH normalize; % #H destruct ] qed. theorem pos_elim2: ∀R:Pos → Pos → Prop. (∀n:Pos. R one n) → (∀n:Pos. R (succ n) one) → (∀n,m:Pos. R n m → R (succ n) (succ m)) → ∀n,m:Pos. R n m. #R #ROn #RSO #RSS @pos_elim //; #n0 #Rn0m @pos_elim /2/; qed. theorem decidable_eq_pos: ∀n,m:Pos. decidable (n=m). @pos_elim2 #n [ @(pos_elim ??? n) /2/; | /3/; | #m #Hind cases Hind; /3/; ] qed. let rec plus n m ≝ match n with [ one ⇒ succ m | p0 n' ⇒ match m with [ one ⇒ p1 n' | p0 m' ⇒ p0 (plus n' m') | p1 m' ⇒ p1 (plus n' m') ] | p1 n' ⇒ match m with [ one ⇒ succ n | p0 m' ⇒ p1 (plus n' m') | p1 m' ⇒ p0 (succ (plus n' m')) ] ]. interpretation "positive plus" 'plus x y = (plus x y). theorem plus_n_succm: ∀n,m. succ (n + m) = n + (succ m). #n elim n; normalize; [ // | 2,3: #n' #IH #m cases m; /3 by eq_f, sym_eq/ normalize; cases n' // ] qed. theorem commutative_plus_pos : commutative ? plus. #n elim n; [ #y cases y; normalize; //; | 2,3: #n' #IH #y cases y; normalize; //; ] qed. theorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m. #n #m >(commutative_plus_pos (succ n) m) <(plus_n_succm …) //; qed. theorem associative_plus : associative Pos plus. @pos_elim [ normalize; //; | #x' #IHx @pos_elim [ #z <(pluss_succn_m …) <(pluss_succn_m …) <(pluss_succn_m …) //; | #y' #IHy' #z <(pluss_succn_m y' …) <(plus_n_succm …) <(plus_n_succm …) <(pluss_succn_m ? z) >(IHy' …) //; ] ] qed. theorem injective_plus_r: ∀n:Pos.injective Pos Pos (λm.n+m). @pos_elim normalize; /3/; qed. theorem injective_plus_l: ∀n:Pos.injective Pos Pos (λm.m+n). /2/; qed. theorem nat_plus_pos_plus: ∀n,m:nat. succ_pos_of_nat (n+m) = pred (succ_pos_of_nat n + succ_pos_of_nat m). #n elim n; [ normalize; //; | #n' #IH #m normalize; >(IH m) <(pluss_succn_m …) <(pred_succ_n ?) <(succ_pred_n …) //; elim n'; normalize; /2/; ] qed. let rec times n m ≝ match n with [ one ⇒ m | p0 n' ⇒ p0 (times n' m) | p1 n' ⇒ m + p0 (times n' m) ]. interpretation "positive times" 'times x y = (times x y). lemma p0_times2: ∀n. p0 n = (succ one) * n. //; qed. lemma plus_times2: ∀n. n + n = (succ one) * n. #n elim n; [ //; | 2,3: #n' #IH normalize; >IH //; ] qed. theorem times_succn_m: ∀n,m. m+n*m = (succ n)*m. #n elim n; [ /2/ | #n' #IH normalize; #m <(IH m) //; | /2/ ] qed. theorem times_n_succm: ∀n,m:Pos. n+(n*m) = n*(succ m). @pos_elim [ // | #n #IH #m <(times_succn_m …) <(times_succn_m …) /3 by succ_injective, trans_eq/ ] qed. theorem times_n_one: ∀n:Pos. n * one = n. #n elim n; /3/; qed. theorem commutative_times: commutative Pos times. @pos_elim /2/; qed. theorem distributive_times_plus : distributive Pos times plus. @pos_elim /2/; qed. theorem distributive_times_plus_r: ∀a,b,c:Pos. (b+c)*a = b*a + c*a. //; qed. theorem associative_times: associative Pos times. @pos_elim [ //; | #x #IH #y #z <(times_succn_m …) <(times_succn_m …) //; ] qed. lemma times_times: ∀x,y,z:Pos. x*(y*z) = y*(x*z). //; qed. (*** ordering relations ***) (* sticking closely to the unary version; not sure if this is a good idea, but it means the proofs are much the same. *) inductive le (n:Pos) : Pos → Prop ≝ | le_n : le n n | le_S : ∀m:Pos. le n m → le n (succ m). interpretation "positive 'less than or equal to'" 'leq x y = (le x y). interpretation "positive 'neither less than or equal to'" 'nleq x y = (Not (le x y)). definition lt: Pos → Pos → Prop ≝ λn,m. succ n ≤ m. interpretation "positive 'less than'" 'lt x y = (lt x y). interpretation "positive 'not less than'" 'nless x y = (Not (lt x y)). definition ge: Pos → Pos → Prop ≝ λn,m:Pos. m ≤ n. interpretation "positive 'greater than or equal to'" 'geq x y = (ge x y). interpretation "positive 'neither greater than or equal to'" 'ngeq x y = (Not (ge x y)). definition gt: Pos → Pos → Prop ≝ λn,m. m(times_n_one …) <(times_n_succm …) #H @False_ind elim (lt_to_not_le ?? (le_lt_plus_pos a a (a*n) …)); /2/; |#n #m #H #le @le_succ_succ @H /2/; ] qed. theorem le_S_times_2: ∀n,m:Pos. n ≤ m → succ n ≤ (succ one)*m. #n #m #lenm (* interessante *) applyS (le_plus n m); //; qed. (* prove injectivity of times from above *) theorem injective_times_r: ∀n:Pos.injective Pos Pos (λm.n*m). #n #m #p #H @le_to_le_to_eq /2/; qed. theorem injective_times_l: ∀n:Pos.injective Pos Pos (λm.m*n). /2/; qed. (* times & lt *) theorem monotonic_lt_times_l: ∀c:Pos. monotonic Pos lt (λt.(t*c)). #c #n #m #ltnm elim ltnm; normalize; [/2/; |#a #_ #lt1 @(transitive_le ??? lt1) //; ] qed. theorem monotonic_lt_times_r: ∀c:Pos. monotonic Pos lt (λt.(c*t)). #a #b #c #H >(commutative_times a b) >(commutative_times a c) /2/; qed. theorem lt_to_le_to_lt_times: ∀n,m,p,q:Pos. n < m → p ≤ q → n*p < m*q. #n #m #p #q #ltnm #lepq @(le_to_lt_to_lt ? (n*q)) [@monotonic_le_times_r //; |@monotonic_lt_times_l //; ] qed. theorem lt_times:∀n,m,p,q:Pos. nH //; | 3,6: #p cases p; [ 1,4: normalize; #H >H //; | 2,3,5,6: #p' normalize; #H >H //; ] ] ] | #n' #IH #m cases m; [ normalize; <(pred_succ_n n') cases n'; //; | 2,3: #m' normalize; lapply (IH m'); cases (partial_minus (succ n') m'); [ 1,2,4,5: normalize; #H >H //; | 3,6: #p cases p; [ 1,4: normalize; #H >H //; | 2,3,5,6: #p' normalize; #H >H //; ] ] ] ] qed. lemma partialminus_n_S: ∀n,m:Pos. match partial_minus n m with [ MinusPos p ⇒ match p with [ one ⇒ partial_minus n (succ m) = MinusZero | _ ⇒ partial_minus n (succ m) = MinusPos (pred p) ] | _ ⇒ partial_minus n (succ m) = MinusNeg ]. #n elim n; [ #m cases m; //; (* Again, lots of unnecessary duplication! *) | #n' #IH #m cases m; [ normalize; cases n'; //; | #m' normalize; lapply (IH m'); cases (partial_minus n' m'); [ 1,2: normalize; #H >H //; | #p cases p; normalize; [ #H >H //; | 2,3: #p' #H >H //; ] ] | #m' normalize; lapply (IH m'); cases (partial_minus n' m'); [ 1,2: normalize; #H >H //; | #p cases p; normalize; [ #H >H //; | 2,3: #p' #H >H //; ] ] ] | #n' #IH #m cases m; [ normalize; cases n'; //; | #m' normalize; lapply (IH m'); cases (partial_minus n' m'); [ 1,2: normalize; #H >H //; | #p cases p; normalize; [ #H >H //; | 2,3: #p' #H >H //; ] ] | #m' normalize; lapply (IH m'); cases (partial_minus n' m'); [ 1,2: normalize; #H >H //; | #p cases p; normalize; [ #H >H //; | 2,3: #p' #H >H //; ] ] ] ] qed. theorem partialminus_S_S: ∀n,m:Pos. partial_minus (succ n) (succ m) = partial_minus n m. #n elim n; [ #m cases m; [ //; | 2,3: #m' cases m'; //; ] | #n' #IH #m cases m; [ normalize; cases n'; /2/; normalize; #n'' <(pred_succ_n n'') cases n'';//; | #m' normalize; >(IH ?) //; | #m' normalize; lapply (partialminus_S n' m'); cases (partial_minus (succ n') m'); [ 1,2: normalize; #H >H //; | #p cases p; [ normalize; #H >H //; | 2,3: #p' normalize; #H >H //; ] ] ] | #n' #IH #m cases m; [ normalize; cases n'; /2/; | #m' normalize; lapply (partialminus_n_S n' m'); cases (partial_minus n' m'); [ 1,2: normalize; #H >H //; | #p cases p; [ normalize; #H >H //; | 2,3: #p' normalize; #H >H //; ] ] | #m' normalize; >(IH ?) //; ] ] qed. theorem minus_S_S: ∀n,m:Pos. (succ n) - (succ m) = n-m. #n #m normalize; >(partialminus_S_S n m) //; qed. theorem minus_one_n: ∀n:Pos.one=one-n. #n cases n; //; qed. theorem minus_n_one: ∀n:Pos.pred n=n-one. #n cases n; //; qed. lemma partial_minus_n_n: ∀n. partial_minus n n = MinusZero. #n elim n; [ //; | 2,3: normalize; #n' #IH >IH // ] qed. theorem minus_n_n_pos: ∀n:Pos.one=n-n. #n normalize; >(partial_minus_n_n n) //; qed. theorem minus_Sn_n: ∀n:Pos. one = (succ n)-n. #n cut (partial_minus (succ n) n = MinusPos one); [ elim n; [ //; | normalize; #n' #IH >IH //; | normalize; #n' #IH >(partial_minus_n_n n') //; ] | #H normalize; >H //; ] qed. theorem minus_Sn_m: ∀m,n:Pos. m < n → succ n -m = succ (n-m). (* qualcosa da capire qui #n #m #lenm elim lenm; napplyS refl_eq. *) @pos_elim2 [#n #H @(lt_one_n_elim n H) //; |#n #abs @False_ind /2/ |#n #m #Hind #c applyS Hind; /2/; ] qed. theorem not_eq_to_le_to_le_minus: ∀n,m:Pos.n ≠ m → n ≤ m → n ≤ m - one. #n @pos_cases //; #m #H #H1 @le_S_S_to_le applyS (not_eq_to_le_to_lt n (succ m) H H1); qed. theorem eq_minus_S_pred: ∀n,m:Pos. n - (succ m) = pred(n -m). @pos_elim2 [ #n cases n; normalize; //; | #n @(pos_elim … n) //; | //; ] qed. lemma pred_Sn_plus: ∀n,m:Pos. one < n → (pred n)+m = pred (n+m). #n #m #H @(lt_one_n_elim … H) /3/; qed. theorem plus_minus: ∀m,n,p:Pos. m < n → (n-m)+p = (n+p)-m. @pos_elim2 [ #n #p #H <(minus_n_one ?) <(minus_n_one ?) /2/; |#n #p #abs @False_ind /2/; |#n #m #IH #p #H >(eq_minus_S_pred …) >(eq_minus_S_pred …) cut (n(pred_Sn_plus …) [ >(minus_Sn_m …) /2/; <(pluss_succn_m …) <(pluss_succn_m …) >(minus_Sn_m …) [ <(pred_succ_n …) <(pred_succ_n …) @IH /2/; | /2/; ] | >(minus_Sn_m … H') //; ] ] qed. (* XXX: putting this in the appropriate case screws up auto?! *) theorem succ_plus_one: ∀n. succ n = n + one. #n elim n; //; qed. theorem nat_possucc: ∀p. nat_of_pos (succ p) = S (nat_of_pos p). #p elim p; normalize; [ //; | #q #IH <(plus_n_O …) <(plus_n_O …) >IH <(plus_n_Sm …) //; | //; ] qed. theorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n. #n elim n; //; qed-. theorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)-m. #n @pos_elim [ //; | #m #IH <(plus_n_succm …) >(eq_minus_S_pred …) >(minus_Sn_m …) /2/; ] qed. theorem plus_minus_m_m: ∀n,m:Pos. m < n → n = (n-m)+m. #n #m #lemn applyS sym_eq; applyS (plus_minus m n m); //; qed. theorem le_plus_minus_m_m: ∀n,m:Pos. n ≤ (n-m)+m. @pos_elim [// |#a #Hind @pos_cases //; #n >(minus_S_S …) /2/; ] qed. theorem minus_to_plus_pos :∀n,m,p:Pos. m < n → n-m = p → n = m+p. #n #m #p #lemn #eqp applyS plus_minus_m_m; //; qed. theorem plus_to_minus_pos :∀n,m,p:Pos.n = m+p → n-m = p. (* /4/ done in 43.5 *) #n #m #p #eqp @sym_eq applyS (minus_plus_m_m p m); qed. theorem minus_pred_pred : ∀n,m:Pos. one < n → one < m → pred n - pred m = n - m. #n #m #posn #posm @(lt_one_n_elim n posn) @(lt_one_n_elim m posm) //. qed. (* monotonicity and galois *) theorem monotonic_le_minus_l: ∀p,q,n:Pos. q ≤ p → q-n ≤ p-n. @pos_elim2 #p #q [#lePO @(le_n_one_elim ? lePO) //; |//; |#Hind @pos_cases [/2/; |#a #leSS >(minus_S_S …) >(minus_S_S …) @Hind /2/; ] ] qed. theorem le_minus_to_plus: ∀n,m,p:Pos. n-m ≤ p → n≤ p+m. #n #m #p #lep @transitive_le [|@le_plus_minus_m_m |@monotonic_le_plus_l //; ] qed. theorem le_plus_to_minus: ∀n,m,p:Pos. n ≤ p+m → n-m ≤ p. #n #m #p #lep (* bello *) applyS monotonic_le_minus_l;//; (* /2/; *) qed. theorem monotonic_le_minus_r: ∀p,q,n:Pos. q ≤ p → n-p ≤ n-q. #p #q #n #lepq @le_plus_to_minus @(transitive_le ??? (le_plus_minus_m_m ? q)) /2/; qed. (*********************** boolean arithmetics ********************) include "basics/bool.ma". let rec eqb n m ≝ match n with [ one ⇒ match m with [ one ⇒ true | _ ⇒ false] | p0 p ⇒ match m with [ p0 q ⇒ eqb p q | _ ⇒ false] | p1 p ⇒ match m with [ p1 q ⇒ eqb p q | _ ⇒ false] ]. theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Type[0]. (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). #n elim n; [ #m cases m normalize [ /2/ | 2,3: #m' #P #t #f @f % #H destruct ] | #n' #IH #m cases m normalize [ #P #t #f @f % #H destruct | #m' #P #t #f @IH [ /2/ | * #ne @f % #e @ne destruct @refl ] | #m' #P #t #f @f % #H destruct; ] | #n' #IH #m cases m; normalize; [ #P #t #f @f % #H destruct; | #m' #P #t #f @f % #H destruct; | #m' #P #t #f @IH [ /2/; | * #ne @f % #e @ne destruct @refl ] ] ] qed. theorem eqb_n_n: ∀n:Pos. eqb n n = true. #n elim n; normalize; //. qed. theorem eqb_true_to_eq: ∀n,m:Pos. eqb n m = true → n = m. #n #m @(eqb_elim n m) //; #_ #abs @False_ind /2/; qed. theorem eqb_false_to_not_eq: ∀n,m:Pos. eqb n m = false → n ≠ m. #n #m @(eqb_elim n m) /2/; qed. theorem eq_to_eqb_true: ∀n,m:Pos. n = m → eqb n m = true. //; qed. theorem not_eq_to_eqb_false: ∀n,m:Pos. n ≠ m → eqb n m = false. #n #m #noteq @eqb_elim //; #Heq @False_ind /2/; qed. let rec leb n m ≝ match partial_minus n m with [ MinusNeg ⇒ true | MinusZero ⇒ true | MinusPos _ ⇒ false ]. lemma leb_unfold_hack: ∀n,m:Pos. leb n m = match partial_minus n m with [ MinusNeg ⇒ true | MinusZero ⇒ true | MinusPos _ ⇒ false ]. #n #m (* XXX: why on earth do I need to case split? *) cases n; //; qed. theorem leb_elim: ∀n,m:Pos. ∀P:bool → Prop. (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m). @pos_elim2 [ #n cases n; normalize; /2/; | #n cases n; normalize; [ /2/; | 2,3: #m' #P #t #f @f /2/; % #H inversion H; [ #H' destruct; | #p /2/; ] ] | #n #m #IH #P #t #f >(leb_unfold_hack …) >(partialminus_S_S n m) <(leb_unfold_hack …) @IH #H /3/; ] qed. theorem leb_true_to_le:∀n,m:Pos.leb n m = true → n ≤ m. #n #m @leb_elim [//; |#_ #abs @False_ind /2/; ] qed. theorem leb_false_to_not_le:∀n,m:Pos. leb n m = false → n ≰ m. #n #m @leb_elim [#_ #abs @False_ind /2/; |//; ] qed. theorem le_to_leb_true: ∀n,m:Pos. n ≤ m → leb n m = true. #n #m @leb_elim //; #H #H1 @False_ind /2/; qed. theorem not_le_to_leb_false: ∀n,m:Pos. n ≰ m → leb n m = false. #n #m @leb_elim //; #H #H1 @False_ind /2/; qed. theorem lt_to_leb_false: ∀n,m:Pos. m < n → leb n m = false. /3/; qed. (***** comparison *****) definition pos_compare : Pos → Pos → compare ≝ λn,m.match partial_minus n m with [ MinusNeg ⇒ LT | MinusZero ⇒ EQ | MinusPos _ ⇒ GT ]. theorem pos_compare_n_n: ∀n:Pos. pos_compare n n = EQ. #n normalize; >(partial_minus_n_n n) //; qed. theorem pos_compare_S_S: ∀n,m:Pos.pos_compare n m = pos_compare (succ n) (succ m). #n #m normalize; >(partialminus_S_S …) //; qed. theorem pos_compare_pred_pred: ∀n,m.one < n → one < m → pos_compare n m = pos_compare (pred n) (pred m). #n #m #Hn #Hm @(lt_one_n_elim n Hn) @(lt_one_n_elim m Hm) #p #q <(pred_succ_n ?) <(pred_succ_n ?) <(pos_compare_S_S …) //; qed. theorem pos_compare_S_one: ∀n:Pos. pos_compare (succ n) one = GT. #n elim n; //; qed. theorem pos_compare_one_S: ∀n:Pos. pos_compare one (succ n) = LT. #n elim n; //; qed. theorem pos_compare_to_Prop: ∀n,m.match (pos_compare n m) with [ LT ⇒ n < m | EQ ⇒ n = m | GT ⇒ m < n ]. #n #m @(pos_elim2 (λn,m.match (pos_compare n m) with [ LT ⇒ n < m | EQ ⇒ n = m | GT ⇒ m < n ])) [1,2:@pos_cases [ 1,3: /2/; | 2,4: #m' cases m'; //; ] |#n1 #m1 IH // ] ] qed. theorem pos_compare_n_m_m_n: ∀n,m:Pos.pos_compare n m = compare_invert (pos_compare m n). #n #m @(pos_elim2 (λn,m. pos_compare n m = compare_invert (pos_compare m n))) [1,2:#n1 cases n1;/2/; |#n1 #m1 <(pos_compare_S_S …) <(pos_compare_S_S …) #IH normalize @IH] qed. theorem pos_compare_elim : ∀n,m:Pos. ∀P:compare → Prop. (n < m → P LT) → (n=m → P EQ) → (m < n → P GT) → P (pos_compare n m). #n #m #P #Hlt #Heq #Hgt cut (match (pos_compare n m) with [ LT ⇒ n < m | EQ ⇒ n=m | GT ⇒ m < n] → P (pos_compare n m)) [cases (pos_compare n m); [@Hlt |@Heq |@Hgt] |#Hcut @Hcut //; qed. inductive cmp_cases (n,m:Pos) : CProp[0] ≝ | cmp_le : n ≤ m → cmp_cases n m | cmp_gt : m < n → cmp_cases n m. theorem lt_to_le : ∀n,m:Pos. n < m → n ≤ m. /2/; qed. lemma cmp_nat: ∀n,m:Pos.cmp_cases n m. #n #m lapply (pos_compare_to_Prop n m) cases (pos_compare n m);normalize; /3 by lt_times_n_to_lt_l, le_n, cmp_le, cmp_gt, lt_to_le/ qed. let rec two_power_nat (n:nat) : Pos ≝ match n with [ O ⇒ one | S n' ⇒ p0 (two_power_nat n') ]. definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p). definition max : Pos → Pos → Pos ≝ λn,m. match leb n m with [ true ⇒ m | _ ⇒ n]. lemma commutative_max : commutative Pos max. #n #m whd in ⊢ (??%%); lapply (pos_compare_to_Prop n m) cases (pos_compare n m) whd in ⊢ (% → ?); #H [ >(le_to_leb_true n m) >(not_le_to_leb_false m n) /2/ | >H @refl | >(le_to_leb_true m n) >(not_le_to_leb_false n m) /2/ ] qed. lemma max_l : ∀m,n:Pos. m ≤ max m n. #m #n normalize @leb_elim // qed. lemma max_r : ∀m,n:Pos. n ≤ max m n. #m #n >commutative_max // qed. lemma pos_compare_lt: ∀n,m:Pos. n