(**************************************************************************)
(*       ___                                                              *)
(*      ||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 normalize;  
*)
theorem succ_injective: injective Pos Pos succ.
//; qed.

let rec nat_of_pos (p:Pos) : nat ≝
  match p with
  [ one ⇒ 1
  | p0 ps ⇒ 2 * (nat_of_pos ps)
  | p1 ps ⇒ S (2 * (nat_of_pos ps))
  ].

let rec succ_pos_of_nat (n:nat) : Pos ≝
  match n with
  [ O ⇒ one
  | S n' ⇒ succ (succ_pos_of_nat n')
  ].

theorem succ_nat_pos: ∀n:nat. succ_pos_of_nat (S n) = succ (succ_pos_of_nat n).
//; qed.

theorem succ_pos_of_nat_inj: injective ?? succ_pos_of_nat.
#n elim n;
[ #m cases m;
  [ //
  | #m' normalize; @succ_elim #p #H destruct
  ]
| #n' #IH #m cases m;
  [ normalize; @succ_elim #p #H destruct;
  | normalize; #m' #H >(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<n.

interpretation "positive 'greater than'" 'gt x y = (gt x y).
interpretation "positive 'not greater than'" 'ngtr x y = (Not (gt x y)).

theorem transitive_le: transitive Pos le.
#a #b #c #leab #lebc elim lebc; /2/; qed.

theorem transitive_lt: transitive Pos lt.
#a #b #c #ltab #ltbc elim ltbc; /2/; qed.

theorem le_succ_succ: ∀n,m:Pos. n ≤ m → succ n ≤ succ m.
#n #m #lenm elim lenm; /2/; qed.

theorem le_one_n : ∀n:Pos. one ≤ n.
@pos_elim /2/; qed.

theorem le_n_succn : ∀n:Pos. n ≤ succ n.
/2/; qed.

theorem le_pred_n : ∀n:Pos. pred n ≤ n.
@pos_elim //; qed.

theorem monotonic_pred: monotonic Pos le pred.
#n #m #lenm elim lenm; /2/;qed.

theorem le_S_S_to_le: ∀n,m:Pos. succ n ≤ succ m → n ≤ m.
/2/; qed.

(* lt vs. le *)
theorem not_le_succ_one: ∀ n:Pos. succ n ≰ one.
#n % #H inversion H /2/; qed.

theorem not_le_to_not_le_succ_succ: ∀ n,m:Pos. n ≰ m → succ n ≰ succ m.
#n #m @not_to_not @le_S_S_to_le qed.

theorem not_le_succ_succ_to_not_le: ∀ n,m:Pos. succ n ≰ succ m → n ≰ m.
#n #m @not_to_not /2/ qed.

theorem decidable_le: ∀n,m:Pos. decidable (n≤m).
@pos_elim2 #n /2/;
#m *; /3/; qed.

theorem decidable_lt: ∀n,m:Pos. decidable (n < m).
#n #m @decidable_le  qed.

theorem not_le_succ_n: ∀n:Pos. succ n ≰ n.
@pos_elim //;
#m #IH @not_le_to_not_le_succ_succ //;
qed.

theorem not_le_to_lt: ∀n,m:Pos. n ≰ m → m < n.
@pos_elim2 #n
 [#abs @False_ind /2/;
 |/2/;
 |#m #Hind #HnotleSS @le_succ_succ /3/;
 ]
qed.

theorem lt_to_not_le: ∀n,m:Pos. n < m → m ≰ n.
#n #m #Hltnm elim Hltnm;
[ //
| #p #H @not_to_not /2/;
] qed.

theorem not_lt_to_le: ∀n,m:Pos. n ≮ m → m ≤ n.
/4/; qed.


theorem le_to_not_lt: ∀n,m:Pos. n ≤ m → m ≮ n.
#n #m #H @lt_to_not_le /2/;qed.

(* lt and le trans *)

theorem lt_to_le_to_lt: ∀n,m,p:Pos. n < m → m ≤ p → n < p.
#n #m #p #H #H1 elim H1; /2/; qed.

theorem le_to_lt_to_lt: ∀n,m,p:Pos. n ≤ m → m < p → n < p.
#n #m #p #H elim H; /3/; qed.

theorem lt_succ_to_lt: ∀n,m:Pos. succ n < m → n < m.
/2/; qed.

theorem ltn_to_lt_one: ∀n,m:Pos. n < m → one < m.
/2/; qed.

theorem lt_one_n_elim: ∀n:Pos. one < n → 
  ∀P:Pos → Prop.(∀m:Pos.P (succ m)) → P n.
@pos_elim //; #abs @False_ind /2/;
qed.

(* le to lt or eq *)
theorem le_to_or_lt_eq: ∀n,m:Pos. n ≤ m → n < m ∨ n = m.
#n #m #lenm elim lenm; /3/; qed.

(* not eq *)
theorem lt_to_not_eq : ∀n,m:Pos. n < m → n ≠ m.
#n #m #H @not_to_not /2/; qed.

theorem not_eq_to_le_to_lt: ∀n,m:Pos. n≠m → n≤m → n<m.
#n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle); //;
#Heq /3/; qed.

(* le elimination *)
theorem le_n_one_to_eq : ∀n:Pos. n ≤ one → one=n.
@pos_cases //; #a ; #abs
@False_ind /2/;qed.

theorem le_n_one_elim: ∀n:Pos. n ≤ one → ∀P: Pos →Prop. P one → P n.
@pos_cases //; #a #abs
@False_ind /2/; qed. 

theorem le_n_Sm_elim : ∀n,m:Pos.n ≤ succ m → 
∀P:Prop. (succ n ≤ succ m → P) → (n=succ m → P) → P.
#n #m #Hle #P elim Hle; /3/; qed.

(* le and eq *)

theorem le_to_le_to_eq: ∀n,m:Pos. n ≤ m → m ≤ n → n = m.
@pos_elim2 /4 by le_n_one_to_eq, monotonic_pred, eq_f, sym_eq/
qed. 

theorem lt_one_S : ∀n:Pos. one < succ n.
/2/; qed.

(* well founded induction principles *)

theorem pos_elim1 : ∀n:Pos.∀P:Pos → Prop. 
(∀m.(∀p. p < m → P p) → P m) → P n.
#n #P #H
cut (∀q:Pos. q ≤ n → P q);/2/;
@(pos_elim … n)
 [#q #HleO (* applica male *) 
    @(le_n_one_elim ? HleO)
    @H #p #ltpO
    @False_ind /2/; (* 3 *)
 |#p #Hind #q #HleS
    @H #a #lta @Hind
    @le_S_S_to_le /2/;
 ]
qed.

(*********************** monotonicity ***************************)
theorem monotonic_le_plus_r: 
∀n:Pos.monotonic Pos le (λm.n + m).
#n #a #b @(pos_elim … n) normalize; /2/;
#m #H #leab /3/; qed.

theorem monotonic_le_plus_l: 
∀m:Pos.monotonic Pos le (λn.n + m).
/2/; qed.

theorem le_plus: ∀n1,n2,m1,m2:Pos. n1 ≤ n2  → m1 ≤ m2 
→ n1 + m1 ≤ n2 + m2.
#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
/2/; qed.

theorem le_plus_n :∀n,m:Pos. m ≤ n + m.
/3/; qed. 

lemma le_plus_a: ∀a,n,m:Pos. n ≤ m → n ≤ a + m.
/2/; qed.

lemma le_plus_b: ∀b,n,m:Pos. n + b ≤ m → n ≤ m.
/2/; qed.

theorem le_plus_n_r :∀n,m:Pos. m ≤ m + n.
/2/; qed.

theorem eq_plus_to_le: ∀n,m,p:Pos.n=m+p → m ≤ n.
//; qed.

theorem le_plus_to_le: ∀a,n,m:Pos. a + n ≤ a + m → n ≤ m.
@pos_elim normalize; /3/; qed. 

theorem le_plus_to_le_r: ∀a,n,m:Pos. n + a ≤ m +a → n ≤ m.
/2/; qed. 

(* plus & lt *)

theorem monotonic_lt_plus_r: 
∀n:Pos.monotonic Pos lt (λm.n+m).
/2/; qed.

theorem monotonic_lt_plus_l: 
∀n:Pos.monotonic Pos lt (λm.m+n).
/2/; qed.

theorem lt_plus: ∀n,m,p,q:Pos. n < m → p < q → n + p < m + q.
#n #m #p #q #ltnm #ltpq
@(transitive_lt ? (n+q)) /2/; qed.

theorem le_lt_plus_pos: ∀n,m,p:Pos. n ≤ m → n < m + p.
#n #m #p #H @(le_to_lt_to_lt … H)
/2/; qed.

theorem lt_plus_to_lt_l :∀n,p,q:Pos. p+n < q+n → p<q.
/2/; qed.

theorem lt_plus_to_lt_r :∀n,p,q:Pos. n+p < n+q → p<q.
/2/; qed.

(* times *)
theorem monotonic_le_times_r: 
∀n:Pos.monotonic Pos le (λm. n * m).
#n #x #y #lexy @(pos_elim … n) normalize;//;(* lento /2/;*)
#a #lea /2/;
qed.

theorem le_times: ∀n1,n2,m1,m2:Pos. 
n1 ≤ n2  → m1 ≤ m2 → n1*m1 ≤ n2*m2.
#n1 #n2 #m1 #m2 #len #lem
@(transitive_le ? (n1*m2)) (* /2/ slow *)
 [ @monotonic_le_times_r //; 
 | applyS monotonic_le_times_r;//;
 ]
qed.

theorem lt_times_n: ∀n,m:Pos. m ≤ n*m.
#n #m /2/; qed.

theorem le_times_to_le: 
∀a,n,m:Pos. a * n ≤ a * m → n ≤ m.
#a @pos_elim2 normalize;
  [//;
  |#n >(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. n<m → p<q → n*p < m*q.
#n #m #p #q #ltnm #ltpq
@lt_to_le_to_lt_times /2/;
qed.

theorem lt_times_n_to_lt_l: 
∀n,p,q:Pos. p*n < q*n → p < q.
#n #p #q #Hlt
elim (decidable_lt p q);//;
#nltpq @False_ind
@(absurd ? ? (lt_to_not_le ? ? Hlt))
applyS monotonic_le_times_r;/2/;
qed.

theorem lt_times_n_to_lt_r: 
∀n,p,q:Pos. n*p < n*q → p < q.
/2/; qed.

(**** minus ****)

inductive minusresult : Type[0] ≝
 | MinusNeg: minusresult
 | MinusZero: minusresult
 | MinusPos: Pos → minusresult.

let rec partial_minus (n,m:Pos) : minusresult ≝
match n with
[ one ⇒ match m with [ one ⇒ MinusZero | _ ⇒ MinusNeg ]
| p0 n' ⇒
  match m with
  [ one ⇒ MinusPos (pred n)
  | p0 m' ⇒ match partial_minus n' m' with
            [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusZero | MinusPos p ⇒ MinusPos (p0 p) ]
  | p1 m' ⇒ match partial_minus n' m' with
            [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusNeg | MinusPos p ⇒ MinusPos (pred (p0 p)) ]
  ]
| p1 n' ⇒
  match m with
  [ one ⇒ MinusPos (p0 n')
  | p0 m' ⇒ match partial_minus n' m' with
            [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusPos one | MinusPos p ⇒ MinusPos (p1 p) ]
  | p1 m' ⇒ match partial_minus n' m' with
            [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusZero | MinusPos p ⇒ MinusPos (p0 p) ]
  ]
].

example testminus0: partial_minus (p0 one) (p1 one) = MinusNeg. //; qed.
example testminus1: partial_minus (p0 one) (p0 (p0 one)) = MinusNeg. //; qed.
example testminus2: partial_minus (p0 (p0 one)) (p0 one) = MinusPos (p0 one). //; qed.
example testminus3: partial_minus (p0 one) one = MinusPos one. //; qed.
example testminus4: partial_minus (succ (p1 one)) (p1 one) = MinusPos one. //; qed.

definition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p | _ ⇒ one ].

interpretation "positive minus" 'minus x y = (minus x y).

lemma partialminus_S: ∀n,m:Pos.
match partial_minus (succ n) m with
[ MinusPos p ⇒ match p with [ one ⇒ partial_minus n m = MinusZero | _ ⇒ partial_minus n m = MinusPos (pred p) ]
| _ ⇒ partial_minus n m = MinusNeg
].
#n elim n;
[ #m cases m;
  [ //;
  | 2,3: #m' cases m'; //;
  ]
(* The other two cases are the same.  I'd combine them, but the numbering
   would be even more horrific. *)
| #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 //;
                      ]
    ]
  ]
| #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<m); [ /2/ ] #H'
     >(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 <pos_compare_S_S cases (pos_compare n1 m1)
   [1,3: #IH @le_succ_succ //
   | #IH >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<m → pos_compare n m = LT.
#n #m #lt lapply (pos_compare_to_Prop n m); cases (pos_compare n m);
[ //;
| 2,3: #H @False_ind @(absurd ? lt ?) /3/;
] qed.

lemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ].
#n #m @eqb_elim //; qed.