Require Import List.
Require Import ZArith.
Require Import util.
Require Import listbit.
Require Import listbit_correct.
Require Import Classical.

Open Local Scope Z_scope.

Module Type MACHINE_INT.

  Set Implicit Arguments.

  Parameter int : nat -> Set.
  Parameter dec_equ_fin_int : forall n (a b:int n),
    {a = b} + {a <> b}.

  Parameter u2Z : forall n, int n -> Z.
  Parameter max_u2Z : forall n (a:int n), u2Z a < 2^^n.
  Parameter min_u2Z : forall n (a:int n), 0 <= u2Z a.
  Parameter u2Z_injection : forall n (v w:int n), u2Z v = u2Z w -> v = w.
  Parameter Z2u: forall n (z:Z), int n.
  Parameter Z2u_injection: forall z n, 0 <= z < 2^^n -> u2Z (Z2u n z) = z.
  Parameter Z2u_neg: forall z n, z < 0 -> u2Z (Z2u n z) = 0.
  Parameter Z2u_dis : forall n a b, 0 <= a < 2^^n -> 0 <= b < 2^^n -> 
    a <> b -> Z2u n a <> Z2u n b.

  (* basic arithmetic/logical operations and properties *)

  Parameter add : forall n, int n -> int n -> int n.
  Notation "a '(+)' b" := (add a b) (at level 35).
  Parameter add_com : forall n (a b:int n), a (+) b = b (+) a.
  Parameter add_assoc : forall n (a b c:int n), (a (+) b) (+) c = a (+) (b (+) c).
  Parameter sub : forall n, int n -> int n -> int n.
  Parameter mul : forall n, int n -> int n -> int n. (* unsigned multiplication with truncation *)
  Parameter umul : forall n (a b:int n), int (n+n).
  Notation "a '(.)' b" := (umul a b) (at level 50).
  Parameter umul_com : forall n (a b:int n), umul a b = umul b a.
  Parameter smul : forall n, int n -> int n -> int (2*n).
  Parameter rem : forall m n, int n -> int m. (*returns the n last bits of (int m)*)
  Notation "a % n" := (rem n a) (at level 50).
  Parameter zero_extend: forall m n (i:int n), int (m+n).
  Parameter sign_extend: forall m n (i:int n), int (n+m).
  Parameter shl : forall (m:nat) n (i:int n), int n.
  Parameter shl_extend : forall m n (i: int n), int (m+n).
  Parameter shrl : forall (m:nat) n (i:int n), int n.
  Parameter shra : forall (m:nat) n (i:int n), int n.
  Parameter shr_shrink : forall m n (i: int n), int (n-m).
  Parameter int_and : forall n (i:int n) (j:int n), int n.
  Parameter int_or : forall n (i:int n) (j:int n), int n.
  Parameter int_or_zero: forall n (v: int n), int_or v (Z2u n 0) = v.
  Parameter int_not : forall n (i:int n), int n.
  Parameter int_cplt2 : forall n (i:int n), int n.
  Parameter int_not_add1_cplt2: forall n (v: int n),
    (n > 1)%nat ->
    add (int_not v) (Z2u n 1) = int_cplt2 v.
  Parameter concat : forall n m (a:int n) (b:int m), int (n+m).
  
  Notation "a ||| b " := (concat a b) (at level 75).

  Parameter add_neutral : forall n (a:int n), add a (Z2u n 0) = a.
  Parameter umul_1 : forall n (x:int n), umul x (Z2u n 1) = zero_extend n x.
  Parameter sign_extend_Z2u: forall n m m', (m > 0)%nat -> n < 2^^m -> 
    sign_extend m' (Z2u (S m) n) = Z2u (S m + m') n.
  Parameter shr_shrink_overflow : forall n (a:int n) k, (k >= n)%nat ->
    shr_shrink k a = Z2u (n-k) 0.

  (*
   * interpretation of int as unsigned integers and related properties 
   *)

  Parameter add_u2Z : forall n (a b:int n), u2Z a + u2Z b < 2^^n ->
    u2Z (a (+) b) = u2Z a + u2Z b.
  Parameter add_u2Z_overflow : forall n (a b:int n), 2^^n <= u2Z a + u2Z b ->
    u2Z (a (+) b) + 2^^n = u2Z a + u2Z b.
  Parameter sub_u2Z : forall n (a b:int n), u2Z a >= u2Z b ->
    u2Z (sub a b) = u2Z a - u2Z b.
  Parameter sub_u2Z_overflow : forall n (a b:int n), u2Z a < u2Z b ->
    u2Z (sub a b) = u2Z a + 2^^n - u2Z b.
  Parameter mul_u2Z : forall n (a b:int n), u2Z a * u2Z b < 2^^n ->
    u2Z (mul a b) = u2Z a * u2Z b.
  Parameter umul_u2Z: forall (n:nat) (a b:int n), 
    u2Z (umul a b) = u2Z a * u2Z b.
  Parameter max_u2Z_umul : forall n (a b:int n),
    u2Z (umul a b) <= (2^^n - 1) * (2^^n - 1).

  Parameter shl_u2Z : forall k n (x:int n) m, (k + m <= n)%nat ->
    u2Z x < 2^^m -> u2Z (shl k x) = u2Z x * 2^^k.
  Parameter shl_u2Z' : forall n (x:int n),
    forall m, u2Z x < 2^^m ->
      forall k, (k + m <= n)%nat ->
	u2Z (shl k x) <= 2^^(m+k) - 2^^k.
  Parameter shl_u2Z'' : forall k n (x:int n), (k >= n)%nat ->
    u2Z (shl k x) = 0.
  Parameter shl_extend_u2Z : forall k n (x:int n),
    u2Z (shl_extend k x) = u2Z x * 2^^k.
  Parameter shl_extend_u2Z' : forall n (x:int n),
    forall m, u2Z x < 2^^m ->
      forall k, u2Z (shl_extend k x) <= 2^^(m+k) - 2^^k.
  Parameter shl_extend_u2Z'' : forall l (x:int l),
    forall k, u2Z x < 2^^k ->
      forall n, u2Z (shl_extend n x) + 2^^n <= 2^^(k+n).
  Parameter shr_shrink_le : forall n (a:int n) k,
    u2Z (shr_shrink k a) * 2^^k <= u2Z a.
  Parameter shr_shrink_u2Z : forall l (x:int l) n, (l >= n)%nat ->
    u2Z (shr_shrink n x) * 2^^n + u2Z (rem n x) = u2Z x.
  Parameter shr_shrink_u2Z': forall l (x:int l) (n:nat), (l >= n)%nat ->
      u2Z (shr_shrink n x) * 2^^n = u2Z x - u2Z (rem n x).

  Parameter rem_u2Z : forall l (x:int l) n, (l >= n)%nat ->
    u2Z (rem n x) = u2Z x - u2Z (shr_shrink n x) * 2^^n.
  Parameter concat_u2Z : forall (n l:nat) (a:int n) (b:int l),
    u2Z (a ||| b) = u2Z a * 2^^l + u2Z b.
  Parameter zero_extend_u2Z : forall (k:nat) n (a:int n), 
    u2Z (zero_extend k a) = u2Z a.
  Parameter sign_extend_u2Z : forall n (v:int n) k,
    0 <= u2Z v < 2^^(pred n) ->
    u2Z (sign_extend k v) = u2Z v.
  Parameter rem_concat : forall n (a:int n) m (b:int m),
      rem m (a ||| b) = b.
  Parameter rem_zero_extend : forall n (a:int n) k m,
    u2Z (rem m (zero_extend k a)) = u2Z (rem m a).

  Parameter s2Z : forall n, int n -> Z. 
  Parameter max_s2Z : forall n (a:int n), s2Z a < 2^^(pred n).
  Parameter s2Z_injection : forall n (v w:int n), s2Z v = s2Z w -> v = w.
  Parameter not_weird: forall (n: nat) (v: int n), Prop.
  Parameter s2Z_int_cplt2: forall n (v: int n),
    not_weird v ->
    s2Z (int_cplt2 v) = - (s2Z v).


  Parameter Z2s : forall n (z:Z), int n.
  Parameter Z2s_injection: forall (z:Z) m, 
    - 2^^m <= z < 2^^m -> s2Z (Z2s (S m) z) = z.



  (*
   * interpretation of int as relative integers and related properties 
   *)

  Parameter add_s2Z: forall n (a b:int (S n)), -2^^n <= s2Z a + s2Z b < 2^^n ->
    s2Z (add a b) = s2Z a + s2Z b.
  Parameter smul_s2Z : forall n (a b:int n), 
    s2Z (smul a b) = s2Z a * s2Z b.
  Parameter sign_extend_s2Z : forall n (v:int n) k,
    s2Z (sign_extend k v) = s2Z v.
  Parameter shl_s2Z : forall k n (x:int n) m,
    (k + S m <= n)%nat ->
    - 2^^m <= s2Z x < 2^^m ->
    s2Z (shl k x) = s2Z x * 2^^k.

  Parameter sign_extend_Z2s : forall m z n,
    - 2^^m <= z < 2^^m->
    sign_extend n (Z2s (S m) z) = Z2s (S m + n) z.

  (*
   * relations between u2Z and s2Z/Z2s
   *)

  Parameter s2Z_u2Z_pos : forall n (a:int n),
    0 <= s2Z a -> s2Z a = u2Z a.
  Parameter s2Z_u2Z_pos' : forall n (a:int n),
    0 <= u2Z a < 2^^(pred n) -> s2Z a = u2Z a.
  Parameter s2Z_u2Z_neg : forall (n:nat) (a:int n),
    s2Z a < 0 -> u2Z a = s2Z a + 2^^n. 
  Parameter u2Z_Z2s : forall (p:positive) n,
    - 2^^(pred n) < Zneg p < 0 -> 
    u2Z (Z2s n (Zneg p)) = 2^^n - Zpos p.

  Unset Implicit Arguments.

End MACHINE_INT.

Module MachineInt : MACHINE_INT.
  
  Import ListBit.
  
  (*
   * definition of machine integers:
   * a machine integer is a list of bits of a known length
   *)
  
  Inductive int' (n:nat) : Set := 
    mk_int : forall (lst:list bit), length lst = n -> int' n.
  Implicit Arguments mk_int.
  Definition mk_i (lst:list bit) := mk_int lst (refl_equal (length lst)).
  
  Definition int (n:nat) := int' n.
  
  Lemma mk_int_pi : forall l lst (H:length lst = l) lst' (H':length lst' = l),
    lst = lst' ->
    mk_int lst H = mk_int lst' H'.
    intros.
    subst lst.
    assert (H = H').
    apply proof_irrelevance.
    rewrite H0.
    reflexivity.
  Qed.

  Definition int_lst (n: nat) (b: int' n) : list bit :=
    match b with
      mk_int lst _ => lst
    end.
  Implicit Arguments int_lst.
  
  Definition int_prf (n: nat) (b: int' n) : length (int_lst b) = n :=
    match b return length (int_lst b) = n with
      mk_int l prf => prf
    end.
  Implicit Arguments int_prf.
  
  Lemma dec_equ_fin_int : forall (l:nat) (a b:int l),
    {a = b} + {a <> b}.
    intros.
    destruct a.
    destruct b.
    generalize (dec_equ_lst_bit lst lst0); intro.
    inversion_clear H.
    subst lst.
    left.
    apply (mk_int_pi l).
    auto.
    right.
    intro.
    apply H0.
    injection H.
    auto.
  Qed.

  Definition u2Z len (i:int' len) : Z := 
    match i with
      mk_int lst _ => ulst2Z lst
    end.
  Implicit Arguments u2Z.

  Lemma max_u2Z : forall l (a:int l),
    u2Z a < 2^^l.
    intros.
    destruct a.
    simpl.
    apply max_ulst2Z.
    rewrite e.
    constructor.
  Qed.

  Lemma min_u2Z : forall l (a:int l),
    0 <= u2Z a.
    intros.
    destruct a.
    simpl.
    apply ulst2Z_pos.
  Qed.

  Lemma u2Z_injection : forall l (v w:int l), 
    u2Z v = u2Z w -> v = w.
    destruct v.
    destruct w.
    unfold u2Z.
    intros.
    apply (mk_int_pi l).
    apply (ulst2Z_injection l); auto.
  Qed.
  Implicit Arguments u2Z_injection.

  Definition Z2u (n: nat) (l:Z): int n :=
    mk_int (adjust_ulist (Z2ulst l) n) (adjust_ulist_length n _).
  
  Lemma Z2u_injection: forall n m,
    0 <= n < 2^^m -> 
    u2Z (Z2u m n) = n.
    unfold u2Z.
    unfold Z2u.
    intros.
    destruct n.
    simpl.
    rewrite adjust_ulist_nil.
    rewrite ulst2Z_zeros.
    reflexivity.
    rewrite adjust_ulst2Z.
    apply ulst2Z2ulst.
    generalize (Zgt_pos_0 p); intro.
    omega.
    apply max_ulst2Z.
    destruct m.
    simpl in H.
    assert (Zpos p = 0).
    omega.
    discriminate.
    apply Z2ulst_length.
    omega.
    tauto.
    inversion_clear H.
    assert (Zneg p < 0).
    apply Zlt_neg_0.
    omega.
  Qed.

  Lemma Z2u_neg: forall n m, n < 0 ->
    u2Z (Z2u m n) = 0.
  intros.
  destruct n.
  inversion H.
  generalize (Zgt_pos_0 p); intro.
  assert (~(Zpos p < 0)).
  omega.
  tauto.
  simpl.
  rewrite adjust_ulist_nil.
  rewrite ulst2Z_zeros.
  auto.
  Qed.
  
  Lemma Z2u_dis : forall l a b, 0 <= a < 2^^l -> 0 <= b < 2^^l -> 
    a <> b -> Z2u l a <> Z2u l b.
    intros.
    intro.
    apply H1.
    rewrite <-(Z2u_injection a l); auto.
    rewrite <-(Z2u_injection b l); auto.
    rewrite H2.
    reflexivity.
  Qed.

  Definition add (l:nat) (a b:int' l) : int' l :=
    mk_int 
    (add_lst (int_lst a) (int_lst b) o)
    (add_lst_length l (int_lst a) (int_lst b) (int_prf a) (int_prf b) o).
  Implicit Arguments add.
  
  Lemma add_com : forall l (a b:int' l), add a b = add b a.
    intros.
    unfold add.
    destruct a.
    destruct b.
    simpl.
    apply (mk_int_pi l).
    unfold add_lst.
    rewrite (proj1 (add_lst'_com (rev lst) (rev lst0))).
    reflexivity.
  Qed.
  Implicit Arguments add_com.
  
  Lemma add_assoc : forall l (a b c : int' l), 
    add (add a b) c = add a (add b c).
    intros.
    destruct a; destruct b; destruct c.
    unfold add.
    simpl.
    apply (mk_int_pi l).
    apply add_lst_assoc with (n:=l) (c1:=o) (c2:=o); auto.
  Qed.
  
  Definition sub (n:nat) (a b:int' n) : int' n :=
    mk_int  
    (sub_lst (int_lst a) (int_lst b) o) 
    (sub_lst_length n (int_lst a) (int_lst b) o (int_prf a) (int_prf b)).
  Implicit Arguments sub.

  (* unsigned multiplication with truncation *)
  Definition mul (n:nat) (a b:int' n) : int' n :=
    mk_int  
    (adjust_ulist (umul_lst (int_lst a) (int_lst b)) n)
    (adjust_ulist_length n (umul_lst (int_lst a) (int_lst b))).
  Implicit Arguments mul.

  (* unsigned multiplication (traditional one, without truncation) *)
  Definition umul : forall l (a b:int' l), int' (l + l).
    intros.
    destruct a as [lsta].
    destruct b as [lstb].
    assert (sig (fun x => x = umul_lst lsta lstb /\
      length x = l + l)%nat).
    exists (umul_lst lsta lstb).
    split.
    reflexivity.
    rewrite umul_lst_length.
    rewrite e; rewrite e0; reflexivity.
    inversion_clear H.
    inversion_clear H0.
    exists x.
    exact H1.
  Defined.
  Implicit Arguments umul.
  
  Lemma umul_com : forall l (a b:int l), umul a b = umul b a.
    intros.
    destruct l; destruct a; destruct b.
    destruct lst; destruct lst0; try discriminate.
    simpl.
    apply mk_int_pi.
    auto.
    simpl.
    apply mk_int_pi.
    apply (umul_lst_com (S l)); auto.
    omega.
  Qed.
  Implicit Arguments umul_com.
  
  (* signed multiplication *)
  Lemma smul_lst_length_length : forall n (a b: int' n),
    (length (smul_lst (int_lst a) (int_lst b)) = 2*n)%nat.
    intros.
    destruct a as [l H].
    destruct b as [k K].
    simpl.
    rewrite (smul_lst_length n); auto.
  Qed.

  Definition smul (n:nat) (a b:int' n) : int' (2*n) :=
    mk_int
    (smul_lst (int_lst a) (int_lst b))
    (smul_lst_length_length n a b).
  Implicit Arguments smul.

  (* rem *)
  Definition rem (n:nat) (l:nat) (a:int' l) : int' n.
    intros.
    destruct a.
    exists (adjust_ulist lst n).
    rewrite adjust_ulist_length; auto.
  Defined.
  Implicit Arguments rem.
  
  Definition zero_extend (m: nat) (n: nat) (i: int n) : int (m+n) :=
    mk_int (zero_extend_lst m (int_lst i)) (zero_extend_lst_length n (int_lst i) (int_prf i) m).
  Implicit Arguments zero_extend.
  
  Definition sign_extend (m: nat) (n: nat) (i: int n) : int (n+m) :=
    mk_int (sign_extend_lst m (int_lst i)) (sign_extend_length m n (int_lst i) (int_prf i)).
  Implicit Arguments sign_extend.
  
  Definition shl (m: nat) (n: nat) (i: int n) : int n :=
    mk_int (shl_lst m (int_lst i)) (shl_length m n (int_lst i) (int_prf i)).
  Implicit Arguments shl.
  
  Definition shl_extend (m: nat) (n: nat) (i: int n) : int (m+n) :=
    mk_int (shl_extend_lst m (int_lst i)) (shl_extend_length n (int_lst i) (int_prf i) m).
  Implicit Arguments shl_extend.
  
  Definition shrl (m:nat) (n:nat) (i:int n) : int n :=
    mk_int (shrl_lst m (int_lst i)) (shrl_length n m (int_lst i) (int_prf i)).
  Implicit Arguments shrl.
  
  Definition shra (m:nat) (n:nat) (i:int n) : int n :=
    mk_int (shra_lst m (int_lst i)) (shra_length n m (int_lst i) (int_prf i)).
  Implicit Arguments shra.
  
  Definition shr_shrink (m:nat) (n:nat) (i:int n) : int (n-m) :=
    mk_int (shr_shrink_lst m (int_lst i)) (shr_shrink_length n m (int_lst i) (int_prf i)).
  Implicit Arguments shr_shrink.
  
  Definition int_and (n:nat) (i:int n) (j:int n) : int n :=
    mk_int (and_lst (int_lst i) (int_lst j)) (and_lst_length n (int_lst i) (int_lst j) (int_prf i) (int_prf j)).
  Implicit Arguments int_and.

  Definition int_or (n: nat) (i j: int n) : int n :=
    mk_int (or_lst (int_lst i) (int_lst j)) (or_lst_length n (int_lst i) (int_lst j) (int_prf i) (int_prf j)).
  Implicit Arguments int_or.

  Lemma int_or_zero: forall n (v: int n),  int_or v (Z2u n 0) = v.
    intros.
    unfold int_or.
    destruct v.
    simpl.
    assert (length (or_lst lst (adjust_ulist nil n)) = n).
    rewrite adjust_ulist_nil.
    rewrite or_lst_zeros.
    assumption.
    assumption.
    assert (or_lst lst (adjust_ulist nil n) = lst).
    rewrite adjust_ulist_nil.
    apply or_lst_zeros.
    assumption.
    generalize (mk_int_pi n (or_lst lst (adjust_ulist nil n)) H lst e H0); intro.
    assert ( (or_lst_length n lst (adjust_ulist nil n) e (adjust_ulist_length n nil))
= H).
    apply proof_irrelevance.
    rewrite H2.
    auto.
  Qed.

  Definition int_not (n:nat) (i:int n): int n :=
    mk_int (cplt1 (int_lst i)) (cplt1_length' n (int_lst i) (int_prf i)).
  Implicit Arguments int_not.

  Definition int_cplt2 (n:nat) (i:int n): int n :=
    mk_int (cplt2 (int_lst i)) (cplt2_length' n (int_lst i) (int_prf i)).  
  Implicit Arguments int_cplt2.

  Lemma int_not_add1_cplt2: forall n (v: int n),
    (n > 1)%nat ->
    add (int_not v) (Z2u n 1) = int_cplt2 v.
    intros.
    destruct v.
    unfold add.
    unfold int_cplt2.
    simpl.
    eapply mk_int_pi.
    unfold cplt2.
    rewrite zero_extend_lst_i.
    unfold adjust_ulist.
    simpl.
    destruct n.
    assert False; [omega | contradiction].
    destruct n.
    assert False; [omega | contradiction].
    simpl.
    unfold zero_extend_lst.
    rewrite e.
    auto.
  Qed.

  (* concatenation *)
  Definition concat_length : forall n m, int (n+m) -> int (m+n).
    intros.
    destruct H.
    exists lst.
    rewrite plus_comm.
    exact e.
  Defined.

  Definition concat (n m:nat) (a:int' n) (b:int' m) : int' (n+m) :=
    add (concat_length _ _ (shl_extend m a)) (zero_extend n b).
  Implicit Arguments concat.
  
  Notation "a ||| b " := (concat a b) (at level 75).

  Lemma add_neutral : forall l (a:int l), add a (Z2u l 0) = a.
    intros.
    destruct a.
    unfold add.
    simpl.
    apply mk_int_pi.
    rewrite adjust_ulist_nil.
    rewrite add_lst_neutral.
    reflexivity.
    rewrite e; reflexivity.
  Qed.
  
  Lemma umul_1 : forall l (x:int l),
    umul x (Z2u l 1) = zero_extend l x.
    intros.
    destruct x.
    simpl.
    unfold zero_extend.
    apply mk_int_pi.
    simpl.
    destruct l.
    destruct lst; try discriminate.
    simpl.
    unfold zero_extend_lst.
    simpl.
    auto.
    assert (adjust_ulist (i::nil) (S l) = zeros l ++ i::nil).
    rewrite (adjust_ulist_S'' (S l) 1).
    simpl.
    rewrite <-minus_n_O.
    auto.
    simpl; auto.
    omega.
    rewrite H.
    rewrite umul_lst_1.
    unfold zero_extend_lst.
    auto.
    assumption.
  Qed.
  
  Lemma sign_extend_Z2u: forall n m m',
    (m > 0)%nat ->
    n < Zpower 2 m -> 
    sign_extend m' (Z2u (S m) n) = Z2u (S m + m') n.
    unfold Z2u.
    unfold sign_extend.
    intros.
    apply (mk_int_pi (S m + m')); auto.
    simpl.
    apply sign_extend_lst_Z2ulst; try auto.
  Qed.
  
  Lemma shr_shrink_overflow : forall n (a:int n) k,
    (k >= n)%nat ->
    shr_shrink k a = Z2u (n-k) 0.
    intros.
    destruct a.
    assert (n-k=0)%nat.
    omega.
    unfold shr_shrink.
    simpl.
    unfold Z2u.
    apply (mk_int_pi (n-k)).
    rewrite H0.
    rewrite adjust_ulist_nil'.
    rewrite shr_shrink_lst_prop'.
    auto.
    omega.
  Qed.

  (*
   * interpretation of int as unsigned integers and related properties
   *)
  
  (* correctness of the addition w.r.t. unsigned integers *)
  Lemma add_u2Z : forall n (a b:int' n),
    u2Z a + u2Z b < Zpower 2 n ->
    u2Z (add a b) = u2Z a + u2Z b.
    intros.
    destruct a.
    destruct b.
    simpl.
    rewrite (add_lst_nat n); auto.
  Qed.

  Lemma add_u2Z_overflow : forall n (a b:int n), 
    Zpower 2 n <= u2Z a + u2Z b ->
    u2Z (add a b) + Zpower 2 n = u2Z a + u2Z b.
    intros.
    destruct a as [l1 H1].
    destruct b as [l2 H2].
    simpl.
    simpl in H.
    rewrite add_lst_nat_overflow; auto.
  Qed.

  (* correctness of subtraction w.r.t. unsigned integers *)
  Lemma sub_u2Z : forall n (a b:int n), 
    u2Z a >= u2Z b ->
    u2Z (sub a b) = u2Z a - u2Z b.
    intros.
    destruct a.
    destruct b.
    simpl.
    simpl in H.
    destruct n.
    destruct lst; try discriminate.
    destruct lst0; try discriminate.
    auto.
    lapply (sub_lst_nat _ _ _ o e e0 (gt_Sn_O n)).
    intros.
    simpl in H0.
    omega.
    simpl.
    omega.
  Qed.

  Lemma sub_u2Z_overflow : forall n (a b:int n), 
    u2Z a < u2Z b ->
    u2Z (sub a b) = u2Z a + Zpower 2 n - u2Z b.
    intros.
    destruct a.
    destruct b.
    simpl.
    simpl in H.
    destruct n.
    destruct lst; try discriminate.
    destruct lst0; try discriminate.
    simpl in H; inversion H.
    lapply (sub_lst_nat_overflow _ _ _ o e e0 (gt_Sn_O n)).
    simpl ulst2Z.
    intros.
    omega.
    simpl.
    omega.
  Qed.

  (* correctness of the unsigned multiplication (with truncation) *)
  Lemma mul_u2Z : forall n (a b: int' n),
    u2Z a * u2Z b < Zpower 2 n ->
    u2Z (mul a b) = u2Z a * u2Z b.
    destruct a.
    destruct b.
    unfold u2Z.
    intros.
    unfold mul.
    simpl.
    rewrite mul_lst_nat; [auto | auto | auto | auto].
  Qed.

  (* correctness of the unsigned multiplication *)
  Lemma umul_u2Z: forall (n:nat) (a b:int' n),
    u2Z (umul a b) = u2Z a * u2Z b.
    intros.
    destruct a; destruct b.
    destruct n.
    destruct lst; try discriminate.
    destruct lst0; try discriminate.
    auto.
    simpl.
    apply (umul_lst_nat n); auto.
  Qed.

  Lemma max_u2Z_umul : forall l (a b:int l),
    u2Z (umul a b) <= (Zpower 2 l - 1) * (Zpower 2 l - 1).
    intros.
    rewrite umul_u2Z.
    apply Zmult_le_compat.
    generalize (max_u2Z _ a); omega.
    generalize (max_u2Z _ b); omega.
    apply min_u2Z.
    apply min_u2Z.
  Qed.

  Lemma zero_extend_u2Z : forall (k:nat) l (a:int l),
    u2Z (zero_extend k a) = u2Z a.
    unfold u2Z.
    unfold zero_extend.
    destruct a.
    simpl.
    generalize k l lst e.
    clear k l lst e.
    induction k; auto.
  Qed.
  Implicit Arguments zero_extend_u2Z.
  
  Lemma sign_extend_u2Z : forall l (v:int l) n,
    0 <= u2Z v < Zpower 2 (pred l) ->
    u2Z (sign_extend n v) = u2Z v.
    intros.
    destruct v.
    simpl in H.
    simpl.
    eapply sign_extend_ulst2Z.
    apply e.
    auto.
  Qed.
  Implicit Arguments sign_extend_u2Z.

  Lemma shl_u2Z : forall n L (x:int L) l,
    (n+l <= L)%nat ->
    u2Z x < Zpower 2 l ->
    u2Z (shl n x) = u2Z x * Zpower 2 n.
    unfold u2Z.
    unfold shl.
    destruct x.
    simpl.
    intros.
    eapply (shl_lst_ulst2Z n).
    apply e.
    apply H.
    apply H0.
  Qed.
  Implicit Arguments shl_u2Z.

  Lemma shl_u2Z' : forall l (x:int l),
    forall L, u2Z x < Zpower 2 L ->
      forall n, (n + L <= l)%nat ->
	u2Z (shl n x) <= Zpower 2 (L+n) - Zpower 2 n.
    destruct x.
    simpl.
    intros.
    apply shl_ulst2Z' with l; auto.
  Qed.

  Lemma shl_u2Z'' : forall n l (x:int l),
    (n >= l)%nat ->
    u2Z (shl n x) = 0.
    unfold u2Z.
    unfold shl.
    destruct x.
    simpl.
    intros.
    rewrite (shl_lst_zeros n l); auto.
    rewrite ulst2Z_zeros.
    auto.
  Qed.

  Lemma shl_extend_u2Z : forall n l (x:int l),
    u2Z (shl_extend n x) = u2Z x * Zpower 2 n.
    intros.
    destruct x.
    simpl.
    apply shl_extend_ulst2Z with (length lst).
    auto.
  Qed.
  
  Lemma shl_extend_u2Z' : forall l (x:int l),
    forall k, u2Z x < Zpower 2 k ->
      forall n, 
	u2Z (shl_extend n x) <= Zpower 2 (k+n) - Zpower 2 n.
    destruct x.
    simpl.
    intros.
    apply shl_extend_ulst2Z' with l; auto.
  Qed.
  
  Lemma shl_extend_u2Z'' : forall l (x:int l),
    forall k, u2Z x < Zpower 2 k ->
      forall n,
	u2Z (shl_extend n x) + Zpower 2 n <= Zpower 2 (k+n).
    intros.
    generalize (shl_extend_u2Z' _ x _ H n); intro.
    lapply (power_2_ge (k+n) n).
    intro.
    omega.
    omega.
  Qed.

  Lemma shr_shrink_le : forall n (a:int n) k,
    u2Z (shr_shrink k a) * Zpower 2 k <= u2Z a.
    intros.
    destruct a.
    simpl.
    generalize lst e k; clear lst e k.
    induction n; intros.
    destruct lst; try discriminate.
    rewrite shr_shrink_lst_nil.
    simpl.
    omega.
    lapply (list_last _ lst).
    intro X; inversion_clear X as [tla Y]; inversion_clear Y as [hda].
    rewrite H.
    destruct k.
    simpl.
    omega.
    rewrite shr_shrink_S.
    rewrite Zpower_S.
    rewrite ulst2Z_last.
    assert (length tla = n).
    rewrite H in e.
    rewrite length_app in e.
    simpl in e.
    omega.
    generalize (IHn _ H0 k); intro.
    destruct hda.
    simpl ulst2Z.
    cutrewrite ( ulst2Z (shr_shrink_lst k tla) * (2 * Zpower 2 k) =
      2 * (ulst2Z (shr_shrink_lst k tla) * Zpower 2 k) ).
    omega.
    ring.
    simpl ulst2Z.
    cutrewrite ( ulst2Z (shr_shrink_lst k tla) * (2 * Zpower 2 k) =
      2 * (ulst2Z (shr_shrink_lst k tla) * Zpower 2 k) ).
    omega.
    ring.
    omega.
  Qed.
  
  Lemma shr_shrink_u2Z : forall l (x:int l) n,
    (l >= n)%nat ->
    u2Z (shr_shrink n x) * Zpower 2 n + u2Z (rem n x) =
    u2Z x.
    intros.
    destruct x.
    simpl.
    rewrite <-ulst2Z_app_zeros.
    assert (n = length (adjust_ulist lst n)).
    rewrite adjust_ulist_length.
    auto.
    pattern n at 2.
    rewrite H0.
    rewrite <-ulst2Z_app.
    rewrite (shr_shrink_lst_prop (length lst)).
    auto.
    auto.
    omega.
  Qed.

  Lemma shr_shrink_u2Z': forall l (x : int l) (n : nat),
      (l >= n)%nat ->
      u2Z (shr_shrink n x) * Zpower 2 n = u2Z x - u2Z (rem n x).
    intros.
    generalize (shr_shrink_u2Z _ x _ H); intro.
    omega.
  Qed.

  Lemma rem_u2Z : forall l (x:int l) n,
    (l >= n)%nat ->
    u2Z (rem n x) = u2Z x - u2Z (shr_shrink n x) * Zpower 2 n.
    intros.
    generalize (shr_shrink_u2Z _ x _ H); intro.
  omega.
  Qed.

  Lemma rem_zero_extend : forall l (a:int l) k n,
    u2Z (rem n (zero_extend k a)) = u2Z (rem n a).
    intros.
    destruct a.
    simpl.
    unfold zero_extend_lst.
    unfold adjust_ulist.
    rewrite length_app.
    rewrite zeros_length.
    rewrite e.
    assert ( k+l < n \/ k+l >= n )%nat.
    omega.
    inversion_clear H.
    rewrite nat_lt_true'; auto.
    assert (l<n)%nat.
    omega.
    rewrite nat_lt_true'; auto.
    unfold zero_extend_lst.
    rewrite <-app_ass.
    rewrite ulst2Z_app.
    rewrite zeros_app.
    rewrite zeros_app.
    rewrite ulst2Z_zeros.
    rewrite ulst2Z_app.
    rewrite zeros_app.
    rewrite ulst2Z_zeros.
    auto.
    rewrite nat_lt_false'.
    assert (l<n \/ l>=n)%nat.
    omega.
    inversion_clear H.
    rewrite nat_lt_true'.
    unfold zero_extend_lst.
    rewrite ulst2Z_app.
    rewrite zeros_app.
    rewrite ulst2Z_zeros.
    rewrite (del_heads_app' k).
    rewrite del_heads_zeros.
    rewrite ulst2Z_app.
    rewrite zeros_app.
    rewrite ulst2Z_zeros.
    auto.
    rewrite zeros_length.
    auto.
    omega.
    auto.
    rewrite nat_lt_false'; auto.
    cutrewrite (k+l-n=k+(l-n))%nat.
    rewrite del_heads_plus.
    rewrite del_heads_app.
    auto.
    rewrite zeros_length.
    auto.
    omega.
    auto.
  Qed.

  Lemma concat_u2Z : forall n l (a:int n) (b:int l),
    u2Z (a ||| b) = u2Z a * 2^^l + u2Z b.
    destruct a as [a Ha]; destruct b as [b Hb]; simpl.
    rewrite (add_lst_nat (n+l)).
    rewrite (shl_extend_ulst2Z l n); auto.
    unfold zero_extend_lst.
    rewrite ulst2Z_app.
    rewrite zeros_app.
    rewrite ulst2Z_zeros.
    ring.
    rewrite (shl_extend_length n a Ha l).
    apply plus_comm.
    rewrite (zero_extend_lst_length l).
    reflexivity.
    assumption.
    unfold zero_extend_lst.
    rewrite ulst2Z_app.
    rewrite zeros_app.
    rewrite ulst2Z_zeros.
    simpl.
    assert (length a <= n)%nat.
    rewrite Ha; constructor.
    generalize (max_ulst2Z _ _ H); intro.
    generalize (shl_extend_ulst2Z' _ _ Ha _ H0 l); intro.
    assert ([[ b ]]u < 2^^l).
    apply max_ulst2Z.
    rewrite Hb; constructor.
    assert ( [[ shl_extend_lst l a ]]u < 2^^(n + l) - [[ b ]]u).
    apply Zle_lt_trans with (2^^(n + l) - 2^^l).
    auto.
    omega.
    omega.
  Qed.

  Lemma rem_concat : forall l (a:int l) k (b:int k),
      rem k (a ||| b) = b.
    intros.
    destruct a.
    destruct b.
    simpl.
    apply mk_int_pi.
    unfold adjust_ulist.
    rewrite (add_lst_length (l+k)).
    rewrite nat_lt_false'.
    unfold zero_extend_lst.
    unfold shl_extend_lst.
    rewrite (add_lst_com (lst ++ zeros k) (zeros l ++ lst0) o).
    rewrite add_lst_app; auto.
    apply del_heads_app; auto.
    omega.
    omega.
    rewrite (shl_extend_length _ _ e k).
    apply plus_comm.
    rewrite (zero_extend_lst_length _ _ e0 l).
    reflexivity.
  Qed.
    
  (*
   * interpretation of int as relative integers and related properties
   *)

  Definition s2Z (l:nat) (a:int' l) : Z :=
    match a with
      mk_int lst _ => slst2Z lst
    end.
  Implicit Arguments s2Z.

  Lemma max_s2Z : forall l (a:int l),
    s2Z a < 2^^(pred l).
    intros.
    destruct a.
    simpl.
    destruct l.
    destruct lst; try discriminate.
    simpl.
    omega.
    simpl pred.
    apply max_slst2Z.
    auto.
  Qed.

  Lemma s2Z_injection : forall l (v w:int l), 
    s2Z v = s2Z w -> v = w.
    intros.
    destruct v.
    destruct w.
    simpl in H.
    apply (mk_int_pi l).
    eapply slst2Z_injection.
    apply e.
    auto.
    auto.
  Qed.

  (* correctness of the addition w.r.t. relative integers *)
  Lemma add_s2Z: forall n (a b:int' (S n)),
    - 2^^n <= s2Z a + s2Z b < 2^^n ->
    s2Z (add a b) = s2Z a + s2Z b.
    intros.
    destruct a.
    destruct b.
    simpl.
    rewrite (add_lst_Z n); auto.
  Qed.

  (* correctness of the signed multiplication w.r.t. relative integers *)
  Lemma smul_s2Z : forall n (a b:int n),
    s2Z (smul a b) = s2Z a * s2Z b.
    intros.
    destruct a.
    destruct b.
    simpl.
    apply (smul_lst_Z n); auto.
  Qed.

  Lemma sign_extend_s2Z : forall l (v:int l) n,
    s2Z (sign_extend n v) = s2Z v.
    intros.
    destruct v.
    simpl.
    apply sign_extend_lst_s2Z.
  Qed.  

  Lemma shl_s2Z : forall n l (x:int l) l',
    (n+ S l' <= l)%nat ->
    - 2^^l' <= s2Z x < 2^^l' ->
    s2Z (shl n x) = s2Z x * 2^^n.
    destruct x.
    unfold shl.
    unfold s2Z.
    intros.
    simpl.
    assert ( - 2^^l' <= slst2Z lst < 0 \/ 0 <= slst2Z lst < 2^^l').
    omega.
    inversion_clear H1.
    
    assert (l' < l)%nat.
    omega.
    generalize (slst2Z_neg_ones _ _ e _ H1 H2); intro. 
    inversion_clear H3.
    assert (l-l'>n)%nat.
    omega.
    lapply (slst2Z_shl_lst _ _ e _ _ H3 x).
    auto.
    auto.
    
    assert ( l' < l)%nat.
    omega.
    generalize (slst2Z_ulst2Z_pos_zeros _ _ e _ H1 H2); intro. 
    inversion_clear H3.
    assert (l-l'>n)%nat.
    omega.
    lapply (slst2Z_shl_lst _ _ e _ _ H3 x).
    auto.
    auto.
  Qed.

  Definition not_weird (n: nat) (v: int n) : Prop :=
    (n > 0)%nat /\ ~(exists k, (int_lst v) = i:: zeros k).
  Implicit Arguments not_weird.

  Lemma s2Z_int_cplt2: forall n (v: int n),
    not_weird v ->
    s2Z (int_cplt2 v) = - (s2Z v).
    intros.
    destruct v.
    simpl.
    destruct n.
    inversion H.
    inversion H0.
    eapply cplt2_correct.
    apply e.
    inversion H.
    simpl in H1.
    auto.
Qed.
    
    



  


  Definition Z2s (n:nat) (l:Z) : int n :=
    mk_int (adjust_slist (Z2slst l) n) (adjust_slist_length n _).

  Lemma Z2s_injection' : forall (z:Z) m, - 2^^m < z < 2^^m ->
    s2Z (Z2s (S m) z) = z.
    intros.
    destruct z.
    simpl.
    destruct m.
    simpl.
    auto.
    destruct m.
    simpl.
    auto.
    unfold adjust_slist.
    rewrite nat_lt_true'.
    simpl.
    rewrite sign_extend_0_lst.
    cutrewrite ( zeros (S m) ++ o :: nil = zeros (S (S m)) ).
    rewrite ulst2Z_zeros.
    auto.
    simpl.
    rewrite zeros_zero.
    rewrite <-app_nil_end.
    auto.
    simpl.
    omega.

    simpl.
    unfold adjust_slist.
    destruct m.
    simpl in H.
    assert (Zpos p = 0 \/ Zpos p = -1).
    omega.
    inversion_clear H0; discriminate.
    simpl.
    assert ( length (rev (pos2lst p)) <= S m )%nat.
    rewrite length_rev.
    apply pos2lst_length.
    omega.
    omega.
    assert ( length (rev (pos2lst p)) = S m \/ length (rev (pos2lst p)) < S m )%nat.
    omega.
    inversion_clear H1.
    rewrite nat_lt_false'.
    simpl.
    rewrite H2.
    cutrewrite (S m - S m = O)%nat.
    simpl.
    apply ulst2Z_rev_poslst.
    rewrite <-minus_n_n.
    reflexivity.
    omega.
    rewrite nat_lt_true'.
    rewrite sign_extend_0_lst.
    simpl.
    rewrite ulst2Z_app.
    rewrite ulst2Z_app_zeros.
    rewrite ulst2Z_zeros.
    simpl.
    apply ulst2Z_rev_poslst.
    assumption.

    simpl.
    unfold adjust_slist.
    destruct m.
    simpl in H.
    assert (Zneg p = -1 \/ Zneg p = 0).
    omega.
    inversion_clear H0.
    destruct p.
    rewrite Zneg_xI in H1.
    assert (Zneg p = 0).
    omega.
    discriminate.
    rewrite Zneg_xO in H1.
    omega.
    simpl.
    reflexivity.
    discriminate.
    rewrite cplt2_length.
    simpl.
    simpl.
    assert ( length (rev (pos2lst p)) <= S m )%nat.
    rewrite length_rev.
    apply pos2lst_length.
    omega.
    generalize (Zopp_neg p); intro.
    omega.
    assert ( length (rev (pos2lst p)) = S m \/ length (rev (pos2lst p)) < S m )%nat.
    omega.
    inversion_clear H1.
    rewrite nat_lt_false'.
    rewrite H2.
    cutrewrite (S m - S m = O)%nat.
    simpl.
    
    rewrite (cplt2_correct (S m)).
    rewrite slst2Z_o.
    rewrite ulst2Z_rev_poslst.
    generalize (Zopp_neg p); omega.
    simpl.
    rewrite H2.
    auto.
    intro.
    inversion_clear H1.
    discriminate.
    omega.
    omega.
    rewrite nat_lt_true'.
    rewrite sign_extend_lst_s2Z.
    rewrite (cplt2_correct (length (rev (pos2lst p)))).
    rewrite slst2Z_o.
    rewrite ulst2Z_rev_poslst.
    generalize (Zopp_neg p); omega.
    simpl; auto.
    intro.
    inversion H1; discriminate.
    assumption.
  Qed.

  Lemma Z2s_injection'': forall (z:Z) m, 
    z = - 2^^m ->
    s2Z (Z2s (S m) z) = z.
    intros.
    destruct m.
    simpl in H.
    subst z.
    simpl.
    auto.
    simpl.
    unfold adjust_slist.
    generalize (Z2slst_Zpower _ _ H); intro.
    rewrite H0.
    simpl length.
    rewrite zeros_length.
    rewrite nat_lt_false'.
    cutrewrite ( S (S (S m)) - S (S m) = 1 )%nat.
    simpl del_heads.
    rewrite slst2Z_i.
    simpl length.
    rewrite zeros_length.
    simpl ulst2Z.
    rewrite ulst2Z_zeros.
    omega.
    omega.
    omega.
  Qed.

  Lemma Z2s_injection : forall (z:Z) m, - Zpower 2 m <= z < Zpower 2 m ->
    s2Z (Z2s (S m) z) = z.
    intros.
    assert (z = - Zpower 2 m \/ - Zpower 2 m < z < Zpower 2 m).
    omega.
    inversion_clear H0.
    apply Z2s_injection''.
    auto.
    apply Z2s_injection'.
    auto.
  Qed.

  Lemma sign_extend_Z2s : forall m z n,
    - 2^^m <= z < 2^^m ->
    sign_extend n (Z2s (S m) z) = Z2s (S m + n) z.
    intros.
    apply s2Z_injection.
    rewrite sign_extend_s2Z.
    rewrite Z2s_injection.
    cutrewrite (S m + n = S (m+n) )%nat.
    rewrite Z2s_injection.
    auto.
    rewrite Zpower_is_exp.
    split.
    apply Zle_trans with (- (Zpower 2 m * 1))%Z.
    assert (Zpower 2 m * 1 <= Zpower 2 m * Zpower 2 n).
    apply Zmult_le_compat_l.
    apply Zpower_1.
    omega.
    omega.
    omega.
    apply Zlt_le_trans with ( Zpower 2 m * 1 ).
    omega.
    apply Zmult_le_compat_l.
    apply Zpower_1.
    omega.
    omega.
    auto.
  Qed.

  Lemma s2Z_u2Z_pos : forall l (a:int l),
    0 <= s2Z a -> s2Z a = u2Z a.
    intros.
    destruct a.
    simpl.
    simpl in H.
    eapply slst2Z_ulst2Z_pos.
    apply e.
    assumption.
  Qed.

  Lemma s2Z_u2Z_pos' : forall n (a:int n),
    0 <= u2Z a < 2^^(pred n) -> s2Z a = u2Z a.
    intros.
    destruct a as [a Ha].
    simpl.
    simpl in H.
    eapply slst2Z_ulst2Z_pos.
    apply Ha.
    generalize (slst2Z_ulst2Z_pos_equiv n a Ha); intro.
    tauto.
  Qed.
    
  Lemma s2Z_u2Z_neg : forall (l:nat) (a:int l),
    s2Z a < 0 ->
    u2Z a = s2Z a + Zpower 2 l. 
    do 2 intro.
    destruct a.
    simpl.
    intros.
    generalize (slst2Z_ulst2Z_neg l lst e H); intro.
    omega.
  Qed.

  Lemma u2Z_Z2s : forall (p:positive) l,
    - 2^^(pred l) < Zneg p < 0 -> 
    u2Z (Z2s l (Zneg p)) = 2^^l - Zpos p.
    intros.
    destruct l.

    simpl in H.
    assert (Zneg p = - 1).
    omega.
    assert (Zneg p = 0).
    omega.
    rewrite H1 in H0.
    discriminate.

    simpl u2Z.
    rewrite cplt2_prop.
    simpl cplt.
    unfold adjust_slist.
    simpl ulst2Z.
    rewrite cplt2_length.
    assert (0 < Zpos p < Zpower 2 l)%Z.
    simpl pred in H.
    assert ( Zneg p = - Zpos p).
    auto.
    omega.
    assert (Zpos p < Zpower 2 l).
    omega.
    destruct l.
    simpl in H1.
    assert (Zpos p =0).
    omega.
    discriminate.
    generalize (Z2ulst_length (Zpos p) (S l) (gt_Sn_O l) H1); intro.
    simpl in H2.
    assert (length (rev (pos2lst p)) < S l \/ length (rev (pos2lst p)) = S l )%nat.
    omega.
    inversion_clear H3.
    rewrite nat_lt_true'.
    rewrite sign_extend_lst_s2nat_i.
    rewrite cplt2_length.
    rewrite (ulst2Z_cplt2 (length (rev (pos2lst p)))).
    assert ( (length (rev (pos2lst p)) <= length (rev (pos2lst p))))%nat.
    omega.
    generalize (max_ulst2Z (length (rev (pos2lst p))) (rev (pos2lst p)) H3); intro.
    
    ring.
    rewrite ulst2Z_rev_poslst.
    rewrite <-Zpower_is_exp.
    cutrewrite ( (length (rev (pos2lst p)) +
       S (S l - length (rev (pos2lst p)))) = S (S l))%nat.
    ring.
    omega.
    omega.
    intro.
    rewrite <-rev_zeros in H3.
    generalize (rev_inj _ _ _ H3); intro.
    generalize (pos2lst_O p); intro.
    rewrite length_rev in H5.
    tauto.
    auto.
    rewrite nat_lt_false'.
    rewrite H4.
    cutrewrite (S l - S l = O)%nat.
    simpl ulst2Z.
    rewrite cplt2_length.
    rewrite (ulst2Z_cplt2 (length (rev (pos2lst p)))).
    rewrite H4.
    rewrite ulst2Z_rev_poslst.
    rewrite (Zpower_S 2 (S l)).
    ring.
    auto.
    intro.
    rewrite <-rev_zeros in H3.
    generalize (rev_inj _ _ _ H3); intro.
    generalize (pos2lst_O p); intro.
    rewrite length_rev in H5.
    tauto.
    auto.
    symmetry.
    apply minus_n_n.
    omega.
    intro.
    inversion_clear H0.
    generalize (pos2lst_O p); intros.
    assert (ulst2Z ( rev (pos2lst p) ) = ulst2Z ( zeros x ) ).
    rewrite ulst2Z_zeros.
    rewrite H1.
    rewrite ulst2Z_zeros.
    auto.
    rewrite ulst2Z_rev_poslst in H2.
    rewrite ulst2Z_zeros in H2.
    discriminate.
    intro.
    inversion_clear H0.
    discriminate.
  Qed.
  
End MachineInt.

Notation "a ||| b " := (MachineInt.concat a b) (at level 75).

Notation "a '(+)' b" := (MachineInt.add a b) (at level 35).
Notation "a '(.)' b" := (MachineInt.umul a b) (at level 50).
Notation "a % n" := (MachineInt.rem n a) (at level 50).

Import MachineInt.

Lemma add_u2Z_mod : forall n (a b:int n),
  u2Z (a (+) b) == u2Z a + u2Z b [[ 2^^n ]].
  intros.
  generalize (Z_le_gt_dec (2^^n) (u2Z a + u2Z b)); intro.
  inversion_clear H.
  exists (-1).
  generalize (add_u2Z_overflow  _ _ H0); intro.
  rewrite <-H.
  ring.
  exists 0.
  rewrite Zmult_0_l.
  rewrite <-Zplus_0_r_reverse.
  apply add_u2Z.
  omega.
Qed.

Lemma umul_assoc : forall l (a b c:int l), 
  umul (umul a b) (zero_extend l c) = umul (zero_extend l a) (umul b c).
  intros.
  apply (@u2Z_injection (l+l+(l+l))).
  rewrite umul_u2Z.
  rewrite zero_extend_u2Z.
  rewrite umul_u2Z.
  rewrite umul_u2Z.
  rewrite zero_extend_u2Z.
  rewrite umul_u2Z.
  ring.
Qed.

Lemma add_mult_distr : forall l (a b c:int l),
  u2Z b + u2Z c < 2^^l ->
  a (.) (b (+) c) = (a (.) b) (+) (a (.) c).
  intros.
  apply u2Z_injection.
  rewrite umul_u2Z.
  rewrite add_u2Z; auto.
  rewrite add_u2Z.
  rewrite umul_u2Z.
  rewrite umul_u2Z.
  ring.
  rewrite umul_u2Z.
  rewrite umul_u2Z.
  rewrite Zpower_is_exp.
  rewrite <-Zmult_plus_distr_r.
  destruct l.
  simpl.
  simpl in H.
  assert ( u2Z b + u2Z c = 0 ).
  generalize (min_u2Z b); intro.
  generalize (min_u2Z c); intro.
  omega.
  rewrite Zmult_comm; simpl.
  rewrite H0.
  simpl.
  omega.
  assert (u2Z a = 0 \/ u2Z a <> 0).
  omega.
  inversion_clear H0.
  rewrite H1.
  rewrite <-Zpower_is_exp.
  simpl Zmult.
  generalize (Zpower_1 (S l + S l)); omega.
  assert (u2Z b + u2Z c = 0 \/ u2Z b + u2Z c <> 0).
  omega.
  inversion_clear H0.
  rewrite H2.
  rewrite Zmult_0_r.
  rewrite <-Zpower_is_exp.
  generalize (Zpower_1 (S l+S l)); omega.
  apply Zlt_trans with (Zpower 2 (S l) * (u2Z b + u2Z c)); auto.
  apply Zmult_lt_compat_r.
  generalize (min_u2Z b); intro.
  generalize (min_u2Z c); intro.
  omega.
  apply max_u2Z.
  rewrite Zmult_comm.
  apply Zmult_lt_compat_r.
  generalize (Zpower_1 (S l)); omega.
  auto.
Qed.

Lemma add_u2Z_s2Z : forall n (a b:int n), 
  0 <= u2Z a + s2Z b < 2^^n ->
  u2Z (a (+) b) = u2Z a + s2Z b.
  intros.
  generalize (Z_lt_ge_dec (s2Z b) 0); intro X; inversion_clear X.
  generalize (s2Z_u2Z_neg H0); intro.
  assert ( u2Z (add a b) + 2^^n = u2Z a + s2Z b + 2^^n).
  rewrite <-Zplus_assoc.
  rewrite <-H1.
  rewrite add_u2Z_overflow.
  reflexivity.
  omega.
  omega.
  assert (s2Z b = u2Z b).
  apply s2Z_u2Z_pos.
  omega.
  rewrite H1.
  rewrite H1 in H.
  apply add_u2Z.
  omega.
Qed.

Lemma add_le_u2Z : forall n (a b:int n),
  u2Z a <= u2Z (a (+) b) ->
  u2Z a + u2Z b < 2^^n.
  intros n a b H.
  generalize (Z_lt_ge_bool (u2Z a + u2Z b) (2^^n)); intro X; inversion_clear X as [x]; destruct x.
  assumption.
  lapply (add_u2Z_overflow a b).
  intro.
  assert (u2Z (add a b) = u2Z a + u2Z b - 2^^n).
  omega.
  rewrite H2 in H.
  assert ( 2^^n <= u2Z b ).
  omega.
  generalize (max_u2Z b); intro.
  omega.
  omega.
Qed.

Lemma add_lt_u2Z_overflow : forall n (a b: int n),
  u2Z (a (+) b) < u2Z a ->
  2^^n <= u2Z a + u2Z b.
  intros n a0 b0 H.
  generalize (Z_lt_ge_bool (u2Z a0 + u2Z b0) (Zpower 2 n)); intro X; inversion_clear X as [x]; destruct x.
  lapply (add_u2Z a0 b0).
  intro.
  rewrite H1 in H.
  generalize (min_u2Z b0); intro.
  assert (u2Z b0 = 0).
  omega.
  rewrite H3 in H.
  omega.
  auto.
  omega.
Qed.

Definition zero16 := Z2u 16 0.
Definition one16 := Z2u 16 1.
Definition four16 := Z2u 16 4.
Definition mfour16 := Z2s 16 (-4)%Z.
Definition zero32 := Z2u 32 0.
Definition one32 := Z2u 32 1.
Definition four32 := Z2u 32 4.