Require Import List.
Require Import Minus.
Require Import Gt.
Require Import Plus.
Require Import ArithRing.
Require Import ZArith.
Require Import util.
Require Import listbit.
Import ListBit.
Require Import Max.
Require Import presburgerZ.

Open Local Scope Z_scope.

  (*
   * interpretation of listbits as unsigned integers, and properties
   *)

  Fixpoint ulst2Z (l:list bit) {struct l} : Z :=
    match l with
      nil => 0 
      | hd::tl => 
	match hd with
          i => 2^^(length tl) + ulst2Z tl
          | o => ulst2Z tl
	end
    end.

  Notation "'[[' lst ']]u'" := (ulst2Z lst) (at level 30).

  Lemma ulst2Z_zeros : forall n, [[ zeros n ]]u = 0.
    induction n; auto.
  Qed.
  
  Lemma ulst2Z_app : forall lst lst',
    [[ lst ++ lst' ]]u =  [[ lst ++ zeros (length lst') ]]u + ulst2Z lst'.
    induction lst; intros.
    simpl.
    rewrite ulst2Z_zeros.
    ring.
    destruct a; simpl.
    apply IHlst.
    rewrite IHlst.
    do 2 rewrite length_app.
    rewrite zeros_length.
    ring.
  Qed.

  Lemma ulst2Z_o : forall tl, [[ o::tl ]]u = [[ tl ]]u.
    auto.
  Qed.
  
  Lemma ulst2Z_i : forall tl, [[ i::tl ]]u = 2^^(length tl) + [[ tl ]]u.
    auto.
  Qed.

  Lemma ulst2Z_app_zeros : forall l n,
     [[ l ++ zeros n ]]u = [[ l ]]u * 2^^n.
    induction l; intro.
    simpl.
    rewrite ulst2Z_zeros.
    reflexivity.
    destruct a; simpl.
    apply IHl.
    rewrite IHl.
    rewrite length_app.
    rewrite zeros_length.
    rewrite Zpower_is_exp.
    ring.
  Qed.

  Lemma max_ulst2Z : forall n l,
    (length l <= n)%nat ->
    [[ l ]]u < 2^^n.
    induction n; intros.
    destruct l.
    simpl.
    repeat constructor.
    simpl in H; inversion H.
    rewrite Zpower_S.
    destruct l.
    simpl ulst2Z.
    generalize (Zpower_1 n); omega.
    simpl in H.
    destruct b.
    simpl ulst2Z.
    apply Zlt_trans with (Zpower 2 n).
    apply IHn; omega.
    generalize (Zpower_1 n); omega.
    apply Zle_lt_trans with (Zpower 2 n + ulst2Z l).
    simpl ulst2Z.
    apply Zplus_le_compat_r.
    apply Zpower_2_le.
    omega.
    cutrewrite (2* Zpower 2 n= Zpower 2 n+Zpower 2 n).
    apply Zplus_lt_compat_l.
    apply IHn; omega.
    ring.
  Qed.

  Lemma ulst2Z_pos : forall lst,
    0 <= [[ lst ]]u.
    induction lst.
    simpl.
    apply Zle_refl.
    destruct a; auto.
    simpl.
    generalize (Zpower_1 (length lst)); intro.
    omega.
  Qed.

  Lemma ulst2Z_injection : forall l (v w: list bit), 
    length v = l ->
    length w = l ->
    [[ v ]]u = [[ w ]]u -> v = w.
    induction l.
    intros.
    destruct v; try discriminate.
    destruct w; try discriminate.
    auto.
    intros.
    destruct v; try discriminate.
    destruct w; try discriminate.
    simpl in H; injection H; clear H; intro.
    simpl in H0; injection H0; clear H0; intro.
    generalize (IHl _ _ H H0); intro.
    destruct b; destruct b0.
    simpl in H1.
    rewrite H2; auto.
    simpl in H1.
    assert (length v <= l)%nat.
    omega.
    generalize (max_ulst2Z _ _ H3); intros.
    assert (ulst2Z v >= Zpower 2 l).
    rewrite H0 in H1.
    generalize (ulst2Z_pos w); intro.
    omega.
    red in H4.
    red in H5.
    tauto.
    simpl in H1.
    assert (length w <= l)%nat.
    omega.
    generalize (max_ulst2Z _ _ H3); intros.
    assert (ulst2Z w >= Zpower 2 l).
    rewrite H in H1.
    generalize (ulst2Z_pos v); intro.
    omega.
    red in H4.
    red in H5.
    tauto.
    simpl in H1.
    rewrite H2.
    auto.
    rewrite H0 in H1.
    rewrite H in H1.
    omega.
  Qed.

  Lemma ulst2Z_power': forall n lst m,
    (m <= n)%nat ->
    (length lst = n)%nat ->
    [[ lst ]]u < 2^^m ->
    exists lst', lst = zeros (n - m) ++ lst'.
    induction n; intros.
    destruct lst; try discriminate.
    exists (@nil bit); auto.
    destruct lst; try discriminate.
    simpl in H0; injection H0; clear H0; intro.
    destruct b.
    assert (m = S n \/ m < S n)%nat.
    omega.
    inversion_clear H2.
    subst m.
    rewrite <-minus_n_n.
    exists (o::lst); auto.
    assert (m<=n)%nat.
    omega.
    rewrite ulst2Z_o in H1.
    generalize (IHn _ _ H2 H0 H1); intros.
    inversion_clear H4.
    exists x.
    cutrewrite (S n - m = S (n-m))%nat.
    simpl.
    rewrite H5; auto.
    omega.
    rewrite ulst2Z_i in H1.
    assert (m = S n \/ m < S n)%nat.
    omega.
    inversion_clear H2.
    subst m.
    rewrite <-minus_n_n.
    exists (i::lst); auto.
    assert (m<=n)%nat.
    omega.
    assert (m = n \/ m < n)%nat.
    omega.
    inversion_clear H4.
    subst m.
    rewrite H0 in H1.
    assert (forall x y, 0 <= y -> ~ (x + y < x)).
    intros; omega.
    generalize (H4 (Zpower 2 n) (ulst2Z lst) (ulst2Z_pos lst)); intros.
    tauto.
    rewrite H0 in H1.
    generalize (Zpower_2_lt _ _ H5); intro.
    assert (Zpower 2 n < Zpower 2 m).
    generalize (ulst2Z_pos lst); intro.
    omega.
    assert (forall x y, ~ (x < y /\ y < x)).
    intros; omega.
    generalize (H7 (Zpower 2 n) (Zpower 2 m)); tauto.
  Qed.

  Lemma ulst2Z_zeros' : forall l v,
    length v = l ->
    [[ v ]]u = 0 -> 
    v = zeros l.
    induction l.
    intros.
    destruct v; try discriminate; auto.
    intros.
    simpl.
    destruct v; try discriminate.
    simpl in H; injection H; clear H; intros.
    destruct b.
    rewrite <-(IHl v); auto.
    simpl in H.
    simpl in H0.
    assert (Zpower 2 (length v) = 0).
    generalize (ulst2Z_pos v); intros.
    generalize (Zpower_1 (length v)); intros.
    omega.
    generalize (Zpower_1 (length v)); intro.
    assert (Zpower 2 (length v) <> 0).
    omega.
    tauto.
  Qed.

  Lemma ulst2Z_last : forall l e,
    [[ l ++ e::nil ]]u = 2 * [[ l ]]u + [[ e::nil ]]u.
    induction l; intros; auto.
    destruct a.
    simpl.
    rewrite IHl.
    auto.
    simpl (ulst2Z ((i :: l) ++ e :: nil)).
    simpl (ulst2Z (i :: l)).
    rewrite IHl.
    rewrite length_app.
    simpl length.
    rewrite Zpower_is_exp.
    ring.
  Qed.

  Lemma ulst2Z_erase_leading_zeros: forall l,
    [[ erase_leading_zeros l ]]u = [[ l ]]u.
    induction l; intros; auto.
    destruct a; auto.
  Qed.

  (*
   * correctness of zero_extend_lst
   *)

  Lemma zero_extend_lst_correct : forall p l,
    [[ zero_extend_lst p l ]]u = [[ l ]]u.
    induction p; intros.
    unfold zero_extend_lst.
    reflexivity.
    simpl.
    rewrite ulst2Z_app.
    rewrite zeros_app.
    rewrite ulst2Z_zeros.
    auto.
  Qed.

  (*
   * subtraction
   *)

  Lemma sub_lst'_nat : forall (n:nat) (a b:list bit) borrow,
    length a = n ->
    length b = n ->
    (n > 0)%nat ->
    [[ a ]]u >= [[ b ]]u + [[ borrow::nil ]]u ->
    [[ rev (sub_lst' (rev a) (rev b) borrow) ]]u + [[borrow::nil]]u + [[b]]u = [[a]]u.
    induction n.
    intros.
    inversion H1.
    intros.
    lapply (list_last _ a).
    intro X; inversion_clear X as [tla Y]; inversion_clear Y as [hda].
    lapply (list_last _ b).
    intro X; inversion_clear X as [tlb Y]; inversion_clear Y as [hdb].
    pattern a at 1.
    rewrite H3.
    pattern b at 1.
    rewrite H4.
    rewrite rev_unit.
    rewrite rev_unit.

    destruct n.
    destruct a; try discriminate.
    destruct a; try discriminate.
    destruct b; try discriminate.
    destruct b1; try discriminate.
    destruct tla; destruct tlb.
    simpl in H3; simpl in H4.
    injection H3; clear H3; intro.
    injection H4; clear H4; intro.
    subst b0; subst b.
    destruct hda; destruct hdb; destruct borrow; auto.
    simpl in H2.
    omega.
    simpl in H2.
    omega.
    simpl in H2.
    omega.
    simpl in H2.
    omega.
    destruct tlb; discriminate.
    simpl in H3.
    destruct tla; discriminate.
    simpl in H3.
    destruct tla; discriminate.

    rewrite H3 in H.
    rewrite length_app in H.
    simpl in H.
    rewrite H4 in H0.
    rewrite length_app in H0.
    simpl in H0.
    assert (length tla = S n).
    omega.
    clear H.
    assert (length tlb = S n).
    omega.
    clear H0.
    
    destruct hda; destruct hdb; destruct borrow.
    
    Ltac local_simpl :=
      repeat ( rewrite ulst2Z_app; rewrite ulst2Z_app_zeros); simpl ulst2Z; simpl length; simpl (Zpower 2 1).

    local_simpl.
    assert (ulst2Z tla >= ulst2Z tlb + ulst2Z (o::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ o H5 H (gt_Sn_O n) H0); intro.
    generalize H6; clear H6.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    intro.
    omega.

    local_simpl.
    assert (ulst2Z tla >= ulst2Z tlb + ulst2Z (i::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ i H5 H (gt_Sn_O n) H0); intro.
    generalize H6; clear H6.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    intro.
    omega.

    local_simpl.
    assert (ulst2Z tla >= ulst2Z tlb + ulst2Z (i::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ i H5 H (gt_Sn_O n) H0); intro.
    generalize H6; clear H6.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    intro.
    omega.

    local_simpl.
    assert (ulst2Z tla >= ulst2Z tlb + ulst2Z (i::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ i H5 H (gt_Sn_O n) H0); intro.
    generalize H6; clear H6.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    intro.
    omega.

    local_simpl.
    assert (ulst2Z tla >= ulst2Z tlb + ulst2Z (o::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ o H5 H (gt_Sn_O n) H0); intro.
    generalize H6; clear H6.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    intro.
    omega.

    local_simpl.
    assert (ulst2Z tla >= ulst2Z tlb + ulst2Z (o::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ o H5 H (gt_Sn_O n) H0); intro.
    generalize H6; clear H6.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    intro.
    omega.

    local_simpl.
    assert (ulst2Z tla >= ulst2Z tlb + ulst2Z (o::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ o H5 H (gt_Sn_O n) H0); intro.
    generalize H6; clear H6.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    intro.
    omega.

    local_simpl.
    assert (ulst2Z tla >= ulst2Z tlb + ulst2Z (i::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ i H5 H (gt_Sn_O n) H0); intro.
    generalize H6; clear H6.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    intro.
    omega.
    
    omega.
    omega.
  Qed.

  Lemma sub_lst_nat : forall n a b borrow,
    length a = n ->
    length b = n ->
    (n > 0)%nat ->
    [[ a ]]u >= [[ b ]]u + [[ borrow::nil ]]u ->
    [[ sub_lst a b borrow ]]u + [[ borrow::nil ]]u + [[ b ]]u = [[ a ]]u.
    intros.
    unfold sub_lst.
    eapply sub_lst'_nat.
    apply H.
    auto.
    auto.
    auto.
  Qed.

  Lemma sub_lst'_nat_overflow : forall (n:nat) (a b:list bit) borrow,
    length a = n ->
    length b = n ->
    (n > 0)%nat ->
    [[ a ]]u < [[ b ]]u + [[ borrow::nil ]]u ->
    [[ rev (sub_lst' (rev a) (rev b) borrow) ]]u + [[ borrow::nil ]]u = [[ a ]]u + 2^^n - [[ b ]]u.
    induction n.
    intros.
    inversion H1.
    intros.
    lapply (list_last _ a).
    intro X; inversion_clear X as [tla Y]; inversion_clear Y as [hda].
    lapply (list_last _ b).
    intro X; inversion_clear X as [tlb Y]; inversion_clear Y as [hdb].
    pattern a at 1.
    rewrite H3.
    pattern b at 1.
    rewrite H4.
    rewrite rev_unit.
    rewrite rev_unit.

    destruct n.
    destruct a; try discriminate.
    destruct a; try discriminate.
    destruct b; try discriminate.
    destruct b1; try discriminate.
    destruct tla; destruct tlb.
    simpl in H3; simpl in H4.
    injection H3; clear H3; intro.
    injection H4; clear H4; intro.
    subst b0; subst b.
    destruct hda; destruct hdb; destruct borrow; auto.
    simpl in H2.
    inversion H2.
    simpl in H2.
    omega.
    simpl in H2.
    inversion H2.
    simpl in H2.
    inversion H2.
    destruct tlb; discriminate.
    simpl in H3.
    destruct tla; discriminate.
    simpl in H3.
    destruct tla; discriminate.

    rewrite H3 in H.
    rewrite length_app in H.
    simpl in H.
    rewrite H4 in H0.
    rewrite length_app in H0.
    simpl in H0.
    assert (length tla = S n).
    omega.
    clear H.
    assert (length tlb = S n).
    omega.
    clear H0.
    
    destruct hda; destruct hdb; destruct borrow.

    local_simpl.
    assert (ulst2Z tla < ulst2Z tlb + ulst2Z (o::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    simpl in H2.
    omega.
    generalize (IHn _ _ o H5 H (gt_Sn_O n) H0); intro.
    generalize H6; clear H6.
    rewrite H3; rewrite H4.
    local_simpl.
    rewrite (Zpower_S 2 (S n)).
    local_simpl.
    intro.
    omega.

    local_simpl.
    assert (ulst2Z tla < ulst2Z tlb + ulst2Z (i::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ i H5 H (gt_Sn_O n) H0); intro.
    generalize H6 H0; clear H6 H0.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    rewrite (Zpower_S 2 (S n)).
    intros.
    omega.

    local_simpl.
    assert (ulst2Z tla < ulst2Z tlb + ulst2Z (i::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ i H5 H (gt_Sn_O n) H0); intro.
    generalize H6 H0; clear H6 H0.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    rewrite (Zpower_S 2 (S n)).
    intros.
    omega.

    local_simpl.
    assert (ulst2Z tla < ulst2Z tlb + ulst2Z (i::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ i H5 H (gt_Sn_O n) H0); intro.
    generalize H6 H0; clear H6 H0.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    rewrite (Zpower_S 2 (S n)).
    intros.
    omega.

    local_simpl.
    assert (ulst2Z tla < ulst2Z tlb + ulst2Z (o::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ o H5 H (gt_Sn_O n) H0); intro.
    generalize H6 H0; clear H6 H0.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    rewrite (Zpower_S 2 (S n)).
    intros.
    omega.

    local_simpl.
    assert (ulst2Z tla < ulst2Z tlb + ulst2Z (o::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ o H5 H (gt_Sn_O n) H0); intro.
    generalize H6 H0; clear H6 H0.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    rewrite (Zpower_S 2 (S n)).
    intros.
    omega.
    
    local_simpl.
    assert (ulst2Z tla < ulst2Z tlb + ulst2Z (o::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ o H5 H (gt_Sn_O n) H0); intro.
    generalize H6 H0; clear H6 H0.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    rewrite (Zpower_S 2 (S n)).
    intros.
    omega.

   local_simpl.
    assert (ulst2Z tla < ulst2Z tlb + ulst2Z (i::nil)).
    generalize H2; clear H2.
    rewrite H3; rewrite H4.
    local_simpl.
    intros.
    omega.
    generalize (IHn _ _ i H5 H (gt_Sn_O n) H0); intro.
    generalize H6 H0; clear H6 H0.
    local_simpl.
    rewrite H3; rewrite H4.
    local_simpl.
    rewrite (Zpower_S 2 (S n)).
    intros.
    omega.
    
    omega.
    omega.
  Qed.

  Lemma sub_lst_nat_overflow : forall n a b borrow,
    length a = n ->
    length b = n ->
    (n > 0)%nat ->
    [[ a ]]u < [[ b ]]u + [[ borrow::nil ]]u ->
    [[ sub_lst a b borrow ]]u + [[ borrow::nil ]]u = [[ a ]]u + 2^^n - [[ b ]]u.
    intros.
    unfold sub_lst.
    eapply sub_lst'_nat_overflow; auto.
  Qed.
    
  (*
   * nat2lst
   *)
  
  (* NB:
     positive is a type that represents strictly positive number
     xH is the leading 1
     xO (resp. xH) represents the bit 0 (resp. 1)
     binary numbers are represented in signed-magnitude notation, with the LSB first
  *)

  Fixpoint pos2lst (p:positive) : list bit :=
    match p with
      xI p' => i :: pos2lst p'
      | xO p' => o :: pos2lst p'
      | xH => i :: nil
    end.

  Lemma pos2lst_len : forall p,
    (length (pos2lst p) > O)%nat.
    induction p; simpl; omega.
  Qed.

  Lemma pos2lst_O : forall p,
    ~ pos2lst p = zeros (length (pos2lst p)).
    intros.
    induction p.
    simpl.
    intro.
    discriminate.
    simpl.
    intro.
    injection H.
    intro.
    tauto.
    simpl.
    intro.
    discriminate.
  Qed.
  
  Lemma pos2lst_length: forall p m,
    (m > 0)%nat ->
    Zpos p < 2^^m ->
    (length (pos2lst p) <= m)%nat.
    unfold nat_of_P.
    induction p.
    intros.
    simpl.
    simpl in H0.
    destruct m.
    inversion_clear H.
    rewrite Zpos_xI in H0.
    destruct m.
    simpl in H0.
    rewrite Zpos_xI in H0.
    generalize (Zgt_pos_0 p); intro.
    omega.
    rewrite Zpower_S in H0.
    apply le_n_S.
    apply IHp.
    omega.
    omega.
    intros.
    simpl.
    destruct m.
    inversion_clear H.
    rewrite Zpos_xO in H0.
    destruct m.
    simpl in H0.
    rewrite Zpos_xO in H0.
    generalize (Zgt_pos_0 p); intro.
    omega.
    rewrite Zpower_S in H0.
    apply le_n_S.
    apply IHp.
    omega.
    omega.
    intros.
    simpl.
    omega.
  Qed.

  Lemma Zneg_two_power_nat : forall m p,
    Zneg p = - two_power_nat m ->
    rev (pos2lst p) = i :: zeros m.
    induction m.
    intros.
    simpl in H.
    unfold shift_nat in H.
    simpl in H.
    injection H; intro X; rewrite X.
    simpl.
    auto.
    intros.
    rewrite two_power_nat_S in H.
    injection H; intro.
    rewrite H0.
    simpl.
    lapply (IHm (shift_nat m 1)).
    intro.
    rewrite H1.
    simpl.
    rewrite zeros_zero.
    simpl.
    rewrite <-app_nil_end.
    auto.
    simpl.
    auto.
  Qed.
  
  Lemma Zneg_Zpower : forall m p,
    Zneg p = - 2^^m ->
    rev (pos2lst p) = i :: zeros m.
    induction m.
    intros.
    simpl in H.
    simpl.
    assert (p = xH).
    destruct p.
    rewrite Zneg_xI in H.
    assert (Zneg p = 0).
    omega.
    assert (Zneg p < 0).
    apply Zlt_neg_0.
    assert (Zneg p <> 0).
    omega.
    tauto.
    rewrite Zneg_xO in H.
    assert (Zneg p < 0).
    apply Zlt_neg_0.
    assert ( 2 * Zneg p <= - 2 ).
    omega.
    rewrite H in H1.
    assert (~(-1<=-2)).
    omega.
    tauto.
    auto.
    rewrite H0.
    simpl.
    auto.
    intros.
    rewrite Zpower_S in H.
    destruct p.
    assert (Zodd (Zneg (xI p))).
    simpl.
    auto.
    assert (Zeven ( - (2 * Zpower 2 m))).
    cutrewrite (- (2*Zpower 2 m) = 2 * (-Zpower 2 m)).
    apply Zeven_2.
    ring.    
    rewrite H in H0.
    generalize (Zeven_not_Zodd _ H1); intro.
    tauto.
    rewrite Zneg_xO in H.
    simpl.
    rewrite IHm.
    simpl.
    rewrite zeros_zero.
    simpl.
    rewrite <-app_nil_end.
    auto.
    omega.
    generalize (Zpower_1 m); intro.
    assert ( - (2 * Zpower 2 m) <= - 2).
    omega.
    rewrite <-H in H1.
    assert (~(-1<=-2)).
    omega.
    tauto.
  Qed.

  Lemma pos2lst_inj : forall p q, pos2lst p = pos2lst q -> p = q.
    induction p.
    destruct q; simpl; intros.
    rewrite (IHp q).
    reflexivity.
    injection H; auto.
    discriminate.
    destruct p; try discriminate.
    destruct q; simpl; intros.
    discriminate.
    rewrite (IHp q).
    reflexivity.
    injection H; auto.
    destruct p; try discriminate.
    destruct q; simpl; intros.
    destruct q; try discriminate.
    discriminate.
    reflexivity.
  Qed.
  
  Lemma pos2lst_nil : forall p, pos2lst p <> nil.
    destruct p; intros H; simpl in H; discriminate.
  Qed.
  
  Definition Z2ulst (n:Z) : list bit :=
    match n with
      Z0 => nil
      | Zpos p => let l := pos2lst p in rev l
      | _ => nil
    end.

  Lemma Z2ulst_inj : forall a b, 
    0 <= a -> 0 <= b ->
    Z2ulst a = Z2ulst b -> a = b.
    intros.
    destruct a; destruct b; auto.
    simpl in H1.
    assert (pos2lst p = rev nil).
    rewrite H1.
    rewrite rev_involutive.
    reflexivity.
    simpl in H2.
    generalize (pos2lst_nil p); intro.
    tauto.
    generalize (Zlt_neg_0 p); intro.
    omega.
    simpl in H1.
    assert (pos2lst p = rev nil).
    rewrite <-H1.
    rewrite rev_involutive.
    reflexivity.
    simpl in H2.
    generalize (pos2lst_nil p); intro.
    tauto.
    simpl in H1.
    generalize (rev_inj _ _ _ H1); intro.
    generalize (pos2lst_inj _ _ H2); intro.
    rewrite H3; reflexivity.
    generalize (Zlt_neg_0 p0); intro.
    omega.
    generalize (Zlt_neg_0 p); intro.
    omega.
    generalize (Zlt_neg_0 p); intro.
    omega.
    generalize (Zlt_neg_0 p0); intro.
    omega.
  Qed.      

  Lemma ulst2Z_rev_poslst: forall p,
    ulst2Z (rev (pos2lst p)) = Zpos p.
    induction p.
    simpl.
    rewrite ulst2Z_app.
    rewrite ulst2Z_app_zeros.
    simpl.
    rewrite IHp.
    rewrite Zpos_xI.
    ring.
    simpl.
    rewrite ulst2Z_app.
    rewrite ulst2Z_app_zeros.
    simpl.
    rewrite IHp.
    symmetry.
    rewrite Zpos_xO.
    ring.
    auto.
  Qed.

  Lemma ulst2Z2ulst : forall n, n >= 0 -> [[ Z2ulst n ]]u = n.
    intros.
    assert (n = 0 \/ n > 0).
    omega.
    inversion_clear H0.
    subst n; auto.
    destruct n.
    inversion H1.
    simpl.
    apply ulst2Z_rev_poslst.
    inversion H1.
  Qed.

  Lemma Z2ulst_length: forall n m,
    (m > 0)%nat ->
    n < 2^^m ->
    (length (Z2ulst n) <= m)%nat.
    intros.
    assert (n = 0 \/ n > 0 \/ n < 0).
    omega.
    inversion_clear H1.
    subst n.
    simpl.
    intuition.
    inversion_clear H2.
    destruct n.
    inversion H1.
    simpl.
    rewrite length_rev.
    apply pos2lst_length.
    auto.
    auto.
    simpl.
    omega.
    destruct n.
    inversion H1.
    inversion H1.
    simpl.
    omega.
  Qed.

  (*
   * properties of add_lst'/add_lst w.r.t. lst2nat
   *)

  Lemma add_lst'_nat : forall n a b carry,
    length a = n ->
    length b = n ->
    [[ rev a ]]u + [[ rev b ]]u + [[ carry::nil ]]u < 2^^n -> 
    [[ rev (add_lst' a b carry) ]]u = 
    [[ rev a ]]u + [[ rev b ]]u + [[ carry::nil ]]u.
    induction n; intros.
    destruct a; try discriminate.
    destruct b; try discriminate.
    destruct carry.
    auto.
    simpl in H1.
    inversion H1.

    destruct a; try discriminate.
    destruct b; try discriminate.
    simpl in H; injection H; clear H; intro.
    simpl in H0; injection H0; clear H0; intro.

    destruct b0; destruct b; destruct carry; (
    simpl;
    rewrite Zpower_S in H1;
    simpl rev in H1;
    repeat rewrite ulst2Z_last;
    repeat rewrite ulst2Z_last in H1;
    simpl ulst2Z;
    simpl ulst2Z in H1).

    assert ( ulst2Z (rev a) + ulst2Z (rev b1) + (ulst2Z (o::nil)) < Zpower 2 n).
    simpl.
    omega.
    generalize (IHn _ _ o H H0 H2); intro.
    simpl in H3.
    omega.

    assert (ulst2Z (rev a) + ulst2Z (rev b1) + (ulst2Z (o::nil)) < Zpower 2 n).
    simpl.
    omega.
    generalize (IHn _ _ o H H0 H2); intro.
    simpl in H3.
    omega.

    assert ( ulst2Z (rev a) + ulst2Z (rev b1) + (ulst2Z (o::nil)) < Zpower 2 n).
    simpl.
    omega.
    generalize (IHn _ _ o H H0 H2); intro.
    simpl in H3.
    omega.

    assert ( ulst2Z (rev a) + ulst2Z (rev b1) + ulst2Z (i::nil) < Zpower 2 n).
    simpl.
    omega.
    generalize (IHn _ _ i H H0 H2); intro.
    simpl in H3.
    omega.

    assert (ulst2Z (rev a) + ulst2Z (rev b1) + ulst2Z (o::nil) < Zpower 2 n).
    simpl.
    omega.
    generalize (IHn _ _ o H H0 H2); intro.
    simpl in H3.
    omega.

    assert ( ulst2Z (rev a) + ulst2Z (rev b1) + ulst2Z (i::nil) < Zpower 2 n).
    simpl.
    omega.
    generalize (IHn _ _ i H H0 H2); intro.
    simpl in H3.
    omega.

    assert (ulst2Z (rev a) + ulst2Z (rev b1) + ulst2Z (i::nil) < Zpower 2 n).
    simpl.
    omega.
    generalize (IHn _ _ i H H0 H2); intro.
    simpl in H3.
    omega.

    assert (ulst2Z (rev a) + ulst2Z (rev b1) + ulst2Z (i::nil) < Zpower 2 n).
    simpl.
    omega.
    generalize (IHn _ _ i H H0 H2); intro.
    simpl in H3.
    omega.
  Qed.

  Lemma add_lst_nat : forall n a b,
    length a = n ->
    length b = n ->
    [[ a ]]u + [[ b ]]u < 2^^n -> 
    [[ add_lst a b o ]]u = [[ a ]]u + [[ b ]]u.
    unfold add_lst.
    intros.
    rewrite (add_lst'_nat n).
    repeat rewrite rev_involutive; simpl; ring.
    rewrite length_rev; auto.
    rewrite length_rev; auto.
    repeat rewrite rev_involutive; simpl; omega.
  Qed.

  Lemma ulst2Z_add_lst' : forall n l k carry,
    length l = n ->
    length k = n ->
    [[ rev (add_lst' (l++(o::nil)) (k++(o::nil)) carry) ]]u = 
    [[ rev l ]]u + [[ rev k ]]u + [[ carry::nil ]]u.
    induction n.
    destruct l.
    destruct k.
    destruct carry; auto.
    intros.
    discriminate H0.
    intros.
    discriminate H.
    intros.
    destruct l.
    discriminate H.
    destruct k.
    discriminate H0.
    destruct b; destruct b0; destruct carry; (
    simpl;
    repeat rewrite ulst2Z_last;
    rewrite IHn; auto;
    simpl ulst2Z;
    ring).
  Qed.
  
  Lemma ulst2Z_add_lst : forall n l k carry,
    length l = n ->
    length k = n ->
    [[ add_lst (o::l) (o::k) carry ]]u = 
    [[ l ]]u + [[ k ]]u + [[ carry::nil ]]u.
    intros.
    unfold add_lst.
    simpl.
    rewrite (ulst2Z_add_lst' n).
    repeat rewrite rev_involutive.
    destruct carry; auto.
    rewrite length_rev; auto.
    rewrite length_rev; auto.
  Qed.

  Lemma add_lst'_nat_overflow : forall (n:nat) (a b:list bit) carry,
    length a = n ->
    length b = n ->
    2^^n <= [[ rev a ]]u + [[ rev b ]]u  + [[ carry::nil ]]u -> 
    [[ rev (add_lst' a b carry) ]]u + 2^^n = 
    [[ rev a ]]u + [[ rev b ]]u + [[ carry::nil ]]u.
    induction n; intros.
    destruct a; try discriminate.
    destruct b; try discriminate.
    destruct carry.
    simpl in H1.
    assert (~(1<=0)).
    omega.
    tauto.
    simpl.
    auto.

    destruct a; try discriminate.
    destruct b; try discriminate.
    simpl in H; injection H; clear H; intro.
    simpl in H0; injection H0; clear H0; intro.
    
    destruct b0; destruct b; destruct carry; (
    simpl add_lst';
    simpl ulst2Z in H1;
    simpl rev;
    repeat rewrite ulst2Z_last;
    repeat rewrite ulst2Z_last in H1;
    simpl ulst2Z in H1;
    simpl ulst2Z;
    rewrite Zpower_S in H1).

    assert ( Zpower 2 n <= ulst2Z (rev a) + ulst2Z (rev b1) + (ulst2Z (o::nil))).
    simpl.
    omega.
    generalize (IHn _ _ o H H0 H2); intro.
    simpl in H3.
    rewrite Zpower_S.
    omega.

    assert ( Zpower 2 n <= ulst2Z (rev a) + ulst2Z (rev b1) + (ulst2Z (o::nil))).
    simpl.
    omega.
    generalize (IHn _ _ o H H0 H2); intro.
    simpl in H3.
    rewrite Zpower_S.
    omega.

    assert ( Zpower 2 n <= ulst2Z (rev a) + ulst2Z (rev b1) + (ulst2Z (o::nil)) ).
    simpl.
    omega.
    generalize (IHn _ _ o H H0 H2); intro.
    simpl in H3.
    rewrite Zpower_S.
    omega.

    assert ( Zpower 2 n <= ulst2Z (rev a) + ulst2Z (rev b1) + ulst2Z (i::nil)).
    simpl.
    omega.
    generalize (IHn _ _ i H H0 H2); intro.
    simpl in H3.
    rewrite Zpower_S.
    omega.

    assert ( Zpower 2 n <= ulst2Z (rev a) + ulst2Z (rev b1) + ulst2Z (o::nil)).
    simpl.
    omega.
    generalize (IHn _ _ o H H0 H2); intro.
    simpl in H3.
    rewrite Zpower_S.
    omega.

    assert ( Zpower 2 n <= ulst2Z (rev a) + ulst2Z (rev b1) + ulst2Z (i::nil)).
    simpl.
    omega.
    generalize (IHn _ _ i H H0 H2); intro.
    simpl in H3.
    rewrite Zpower_S.
    omega.

    assert ( Zpower 2 n <= ulst2Z (rev a) + ulst2Z (rev b1) + ulst2Z (i::nil)).
    simpl.
    omega.
    generalize (IHn _ _ i H H0 H2); intro.
    simpl in H3.
    rewrite Zpower_S.
    omega.

    assert ( Zpower 2 n <= ulst2Z (rev a) + ulst2Z (rev b1) + ulst2Z (i::nil)).
    simpl.
    omega.
    generalize (IHn _ _ i H H0 H2); intro.
    simpl in H3.
    rewrite Zpower_S.
    omega.
  Qed.

  Lemma add_lst_nat_overflow : forall n a b,
    length a = n ->
    length b = n ->
    2^^n <= [[ a ]]u + [[ b ]]u -> 
    [[ add_lst a b o ]]u + 2^^n = [[ a ]]u + [[ b ]]u.
    unfold add_lst.
    intros.
    rewrite (add_lst'_nat_overflow n).
    repeat rewrite rev_involutive; simpl; ring.
    rewrite length_rev; auto.
    rewrite length_rev; auto.
    repeat rewrite rev_involutive; auto.
    simpl.
    omega.
  Qed.

  (*
   * correctness of adjust
   *)

  Lemma adjust_ulst2Z: forall n lst,
    [[ lst ]]u < 2^^n ->
    [[ adjust_ulist lst n ]]u = [[ lst ]]u. 
    intros.
    assert (length lst >= n \/ length lst < n)%nat.
    omega.
    inversion_clear H0.
    generalize (ulst2Z_power' (length lst) lst n H1); intros.
    intuition.
    inversion_clear H0.
    unfold adjust_ulist.
    rewrite (nat_lt_false' _ _ H1).
    rewrite H2.
    rewrite del_heads_app.
    rewrite ulst2Z_app.
    rewrite zeros_app.
    rewrite ulst2Z_zeros.
    omega.
    assert (length lst = length (zeros (length lst - n) ++ x)).
    rewrite <- H2; auto.
    rewrite length_app in H0.
    rewrite zeros_length in H0.
    assert (length x = n).
    omega.
    rewrite length_app.
    rewrite zeros_length.
    omega.
    unfold adjust_ulist.
    rewrite (nat_lt_true' _ _ H1).
    unfold zero_extend_lst.
    rewrite ulst2Z_app.
    rewrite zeros_app.
    rewrite ulst2Z_zeros.
    omega.
  Qed.

  (*
   * properties of cplt2 w.r.t. lst2nat
   *)

  Lemma ulst2Z_cplt2_O : forall a,
    length a = O ->
    a <> zeros O ->
    [[ cplt2 a ]]u = 2^^O - [[ a ]]u.
    intros.
    destruct a; try discriminate.
    simpl in H0; tauto.
  Qed.

  Lemma ulst2Z_cplt2_1 : forall a,
    length a = 1%nat ->
    a <> zeros 1 ->
    [[ cplt2 a ]]u = 2^^1 - [[ a ]]u.
    intros.
    destruct a; try discriminate.
    destruct a; try discriminate.
    destruct b.
    simpl in H0.
    tauto.
    simpl.
    auto.
  Qed.

  Lemma ulst2Z_cplt2' : forall n a,
    length a = S (S n) ->
    a <> zeros (S (S n)) ->
    [[ cplt2 a ]]u = 2^^(S (S n)) - [[ a ]]u.
    induction n; intros.
    destruct a; try discriminate.
    destruct a; try discriminate.
    destruct a; try discriminate.
    destruct b; destruct b0; auto.
    simpl in H0; tauto.
    destruct a; try discriminate.
    destruct b.
    simpl in H; injection H; clear H; intro.

    rewrite cplt2_prop.
    rewrite ulst2Z_i.
    rewrite cplt2_length.
    rewrite IHn; auto.
    rewrite H; auto.
    rewrite ulst2Z_o.
    lapply (max_ulst2Z (S (S n)) a).
    intro.
    rewrite <- (Zpower_plus (S (S n))).
    omega.
    rewrite H; constructor.
    intro X; apply H0; rewrite X; auto.
    intro X; inversion_clear X.
    rewrite H1 in H.
    rewrite zeros_length in H.
    subst x.
    apply H0; rewrite H1; auto.
    intro X; inversion X; discriminate.

    simpl in H; injection H; clear H; intro.
    cut (a <> zeros (S (S n)) \/ a = zeros (S (S n))).
    intro X; inversion_clear X.

    rewrite cplt2_prop.
    rewrite ulst2Z_o.
    rewrite ulst2Z_i.
    rewrite IHn; auto.
    rewrite H; auto.
    lapply (max_ulst2Z (S (S n)) a).
    intro.
    rewrite <-(Zpower_plus (S (S n))).
    omega.
    omega.
    intro X; inversion_clear X.
    rewrite H2 in H.
    rewrite zeros_length in H.
    subst x.
    tauto.
    intro.
    inversion_clear H2.
    injection H3; clear H3; intro.
    rewrite H2 in H.
    rewrite zeros_length in H.
    subst x.
    tauto.

    rewrite H1.
    rewrite cplt2_weird.
    rewrite ulst2Z_i.
    rewrite ulst2Z_zeros.
    rewrite zeros_length.
    rewrite <-(Zpower_plus (S (S n))).
    ring.
    generalize (dec_equ_lst_bit' a (zeros (S (S n)))); tauto.
  Qed.

  Lemma ulst2Z_cplt2 : forall n lst,
    length lst = n ->
    lst <> zeros n ->
    [[ cplt2 lst ]]u = 2^^n - [[ lst ]]u.
    destruct n.
    apply ulst2Z_cplt2_O.
    destruct n.
    apply ulst2Z_cplt2_1.
    apply ulst2Z_cplt2'.
  Qed.
  
  (*
   * correctness of 2k-multiplication (given k-long inputs, the result fits in 2k)
   *)

  Lemma umul_lst_nat: forall n l k,
    length l = S n ->
    length k = S n ->
    [[ umul_lst l k ]]u = [[ l ]]u * [[ k ]]u.
    induction n.
    destruct l; destruct k; intros; try discriminate.
    destruct l; destruct k; intros; try discriminate.
    destruct b; destruct b0; auto.
    intros.
    destruct l; try discriminate.
    destruct k; try discriminate.
    destruct b; destruct b0.
    rewrite umul_lst_leading_o.
    simpl.
    rewrite IHn; auto.
    intro; subst l; discriminate.
    intro X; discriminate.
    rewrite umul_lst_leading_o.
    simpl.
    rewrite (ulst2Z_add_lst (S n + S n)).
    rewrite ulst2Z_app_zeros.
    simpl; do 2 ring.
    rewrite IHn; auto.
    rewrite length_app.
    rewrite zeros_length.
    simpl in H; injection H; intro.
    simpl in H0; injection H0; intro.
    auto.
    rewrite umul_lst_length; auto.
    intro; subst l; discriminate.
    intro; discriminate.
    rewrite umul_lst_leading_i.
    simpl.
    rewrite (ulst2Z_add_lst (S (S n + S n))).
    simpl.
    rewrite ulst2Z_app_zeros.
    rewrite IHn; auto.
    ring.
    simpl.
    rewrite length_app.
    rewrite zeros_length.
    simpl in H; injection H; intro.
    simpl in H0; injection H0; intro.
    auto.
    omega.
    simpl; rewrite umul_lst_length.
    simpl in H; simpl in H0; omega.
    rewrite umul_lst_leading_i.
    simpl.
    rewrite (ulst2Z_add_lst (S (S n + S n))).
    simpl.
    rewrite (ulst2Z_add_lst (S n + S n)).
    simpl.
    rewrite IHn; auto.
    rewrite ulst2Z_app_zeros.
    rewrite ulst2Z_app_zeros.
    rewrite length_app.
    rewrite zeros_length.
    rewrite Zpower_is_exp.
    ring.
    rewrite length_app.
    rewrite zeros_length.
    simpl in H; injection H; intro.
    simpl in H0; injection H0; intro.
    auto.
    rewrite umul_lst_length; auto.
    simpl; rewrite length_app; rewrite zeros_length.
    simpl in H; injection H; intro.
    simpl in H0; injection H0; intro.
    omega.
    rewrite (add_lst_length (S (S n) + length k)).
    simpl in H; injection H; intro.
    simpl in H0; injection H0; intro.
    omega.
    simpl; rewrite length_app; rewrite zeros_length.
    simpl in H0; simpl in H; omega.
    simpl.
    simpl in H; injection H; intro.
    simpl in H0; injection H0; intro.
    rewrite umul_lst_length; omega.
  Qed.
  
  (*
   * correctness of k-multiplication (given k-long inputs, returns a result in k)
   *) 

  Lemma mul_lst_nat: forall n a b,
    length a = n ->
    length b = n ->
    [[ a ]]u * [[ b ]]u < 2^^n ->
    [[ adjust_ulist (umul_lst a b) n ]]u = [[ a ]]u * [[ b ]]u.
    destruct n.
    intros.
    destruct a; try discriminate.
    destruct b; try discriminate.
    auto.
    intros.
    rewrite <- (umul_lst_nat n) in H1; auto.
    rewrite <- (umul_lst_nat n); auto.
    rewrite adjust_ulst2Z; auto.
  Qed.

  (*
   * properties of shift-left w.r.t. lst2nat 
   *)
  
  Lemma shl_lst_ulst2Z: forall k n (lst : list bit),
    length lst = n ->
    forall l,
      (k + l <= n)%nat ->
      [[ lst ]]u < 2^^l ->
      [[ shl_lst k lst ]]u = [[ lst ]]u * 2^^k.
    intros.
    assert (n >= l)%nat; try omega.
    generalize (ulst2Z_power' n lst l H2 H H1); clear H2; intros.
    inversion_clear H2 as [lst'].
    rewrite H3.
    generalize (plus_lt_exists l k n H0); intros.
    inversion_clear H2.
    assert (n - l = k + x)%nat.
    intuition.
    rewrite H2.
    rewrite <- zeros_app.
    rewrite <- ass_app.
    rewrite shl_lst_zeros_app.
    rewrite <- ulst2Z_app_zeros.
    repeat rewrite <- ass_app.
    rewrite ulst2Z_app.
    rewrite zeros_app.
    rewrite ulst2Z_zeros.
    symmetry.
    rewrite ass_app.
    rewrite zeros_app.
    rewrite ulst2Z_app.
    rewrite zeros_app.
    rewrite ulst2Z_zeros.
    auto.
  Qed.

  Lemma shl_ulst2Z' : forall n lst,
    length lst = n ->
    forall l, ulst2Z lst < Zpower 2 l ->
      forall k, (k+l <= n)%nat ->
	ulst2Z (shl_lst k lst) <= Zpower 2 (l+k) - Zpower 2 k.
    induction k.
    simpl.
    rewrite <-plus_n_O.
    omega.
    intros.
    assert (k + l <= n)%nat.
    omega.
    generalize (IHk H2); clear IHk H2; intro.
    rewrite (shl_lst_ulst2Z k n lst H l) in H2.
    rewrite (shl_lst_ulst2Z (S k) n lst H l).
    cutrewrite ( Zpower 2 (l + S k) - Zpower 2 (S k) = 2 * (Zpower 2 (l + k) - Zpower 2 k)).
    rewrite Zpower_S.
    rewrite Zmult_comm.
    rewrite <-Zmult_assoc.
    rewrite (Zmult_comm (Zpower 2 k)).
    omega.
    cutrewrite (l+S k = S(l+k))%nat.
    cutrewrite (Zpower 2 (S (l + k)) = 2 * Zpower 2 (l + k)).
    cutrewrite (Zpower 2 (S k) = 2 * Zpower 2 k).
    omega.
    rewrite Zpower_S.
    reflexivity.
    rewrite Zpower_S.
    reflexivity.
    omega.
    omega.
    auto.
    omega.
    auto.
  Qed.

  (*
   * properties of shift-left-extend w.r.t. lst2nat 
   *)

  Lemma shl_extend_ulst2Z : forall k n lst,
    length lst = n ->
    [[ shl_extend_lst k lst ]]u = [[ lst ]]u * 2^^k.
    destruct k; intros.
    unfold shl_extend_lst.
    simpl.
    rewrite <-app_nil_end.
    ring.
    unfold shl_extend_lst.
    rewrite ulst2Z_app_zeros.
    reflexivity.
  Qed.

  Lemma shl_extend_ulst2Z' : forall n lst,
    length lst = n ->
    forall l, [[ lst ]]u < 2^^l ->
      forall k, 
	[[ shl_extend_lst k lst ]]u <= 2^^(l+k) - 2^^k.
    unfold shl_extend_lst.
    induction k.
    simpl.
    rewrite <-app_nil_end.
    rewrite <-plus_n_O.
    omega.
    cutrewrite (lst ++ zeros (S k) = (lst ++ zeros k) ++ zeros 1).
    rewrite ulst2Z_app_zeros.
    cutrewrite (l + S k = S (l+k))%nat.
    rewrite Zpower_S.
    rewrite Zpower_S.
    simpl (Zpower 2 0).
    rewrite Zpower_S.
    omega.
    omega.
    simpl.
    rewrite app_ass.
    rewrite zeros_zero.
    rewrite <-app_nil_end.
    auto.
  Qed.

  (*
   * properties of sign_extend w.r.t. lst2nat/nat2lst
   *)

  Lemma sign_extend_ulst2Z : forall n lst l,
    length lst = l ->
    0 <= ulst2Z lst < Zpower 2 (pred l) ->
    ulst2Z (sign_extend_lst n lst) = ulst2Z lst.
    intros.
    destruct lst.
    simpl in H.
    subst l.
    destruct n.
    simpl.
    auto.
    simpl.
    rewrite ulst2Z_zeros.
    auto.
    destruct b.
    simpl.
    rewrite sign_extend_0_lst.
    rewrite ulst2Z_app.
    rewrite zeros_app.
    rewrite ulst2Z_zeros.
    omega.
    simpl in H0.
    destruct l; try discriminate.
    simpl in H; injection H; clear H; intro.
    rewrite H in H0.
    simpl in H0.
    assert (~(Zpower 2 l + ulst2Z lst < Zpower 2 l)).
    generalize (ulst2Z_pos lst); omega.
    tauto.
  Qed.

  Lemma sign_extend_lst_s2nat_o : forall l n,
    ulst2Z (sign_extend_lst n (o::l)) = ulst2Z l.
    induction n; auto.
  Qed.
  
  Lemma sign_extend_lst_s2nat_i : forall n l,
    ulst2Z (sign_extend_lst n (i::l)) = 
    Zpower 2 (length l) * (Zpower 2 (S n) - 1) + ulst2Z l.
    induction n; intros.
    simpl (Zpower 2 1).
    ring.
    simpl sign_extend_lst.
    simpl ulst2Z.
    ring.
    simpl sign_extend_lst.
    simpl ulst2Z.
    rewrite (sign_extend_length n (S (length l))); auto.
    rewrite <-Zpower_plus.
    rewrite <-Zpower_plus.
    simpl (S (length l) + n)%nat.
    rewrite Zpower_S.
    rewrite IHn; clear IHn.
    rewrite Zpower_S.
    rewrite Zpower_is_exp.
    ring.
  Qed.

  Lemma sign_extend_lst_Z2ulst:
    forall n m m',
      (m > 0)%nat ->
      n < Zpower 2 m ->
      sign_extend_lst m' (adjust_ulist (Z2ulst n) (S m)) =
      adjust_ulist (Z2ulst n) (S (m + m')).
    intros.
    generalize (Z2ulst_length _ _ H H0); intros.
    assert (length (Z2ulst n) < S m)%nat.
    omega.
    unfold adjust_ulist.
    rewrite (nat_lt_true' _ _ H2); simpl.
    assert (length (Z2ulst n) < S (m + m'))%nat.
    omega.
    rewrite (nat_lt_true' _ _ H3); simpl.
    unfold zero_extend_lst.
    destruct (length (Z2ulst n)).
    simpl.
    rewrite sign_extend_0_lst.
    rewrite ass_app.
    rewrite zeros_app.
    simpl.
    cutrewrite (m + m' = m' + m)%nat; try (omega || auto).
    cutrewrite (m - n0 = S(m - S n0))%nat; try omega.
    simpl.
    rewrite sign_extend_0_lst.
    rewrite ass_app.
    rewrite zeros_app.
    cutrewrite (S m' + (m - S n0) = m + m' - n0)%nat; try (omega || auto).
  Qed.

  (* 
   * interpretation of list bits as signed integers in 2cplt notation
   *)

  Definition slst2Z (l:list bit) : Z :=
    match l with
      nil => 0
      | o::tl => ulst2Z tl
      | i::tl => - 2^^(length tl) + ulst2Z tl
    end.

  Notation "'[[' lst ']]s'" := (slst2Z lst) (at level 30).

  Lemma slst2Z_o : forall tl, [[ o::tl ]]s = [[ tl ]]u.
    auto.
  Qed.

  Lemma slst2Z_i : forall tl, [[ i::tl ]]s = - 2^^(length tl) + [[ tl ]]u.
    auto.
  Qed.
  
  Lemma slst2Z_injection : forall n (a b: list bit), 
    length a = n ->
    length b = n ->
    [[ a ]]s = [[ b ]]s -> a = b.
    induction n; intros.
    destruct a; try discriminate.
    destruct b; try discriminate.
    reflexivity.
    destruct a as [_ | a0 a]; try discriminate.
    simpl in H; injection H; clear H; intro.
    destruct b as [_ | b0 b]; try discriminate.
    simpl in H0; injection H0; clear H0; intro.
    destruct a0; destruct b0.
    do 2 rewrite slst2Z_o in H1.
    rewrite (ulst2Z_injection n a b); auto.
    rewrite slst2Z_o in H1.
    rewrite slst2Z_i in H1.
    rewrite H0 in H1.
    assert ( [[ b ]]u < 2^^n ).
    apply max_ulst2Z.
    rewrite H0.
    constructor.
    assert ( [[ a ]]u < 0 ).
    omega.
    generalize (ulst2Z_pos a);intro.
    assert (~([[ a ]]u < 0)).
    omega.
    tauto.
    rewrite slst2Z_o in H1.
    rewrite slst2Z_i in H1.
    rewrite H in H1.
    assert ( [[ a ]]u < 2^^n).
    apply max_ulst2Z.
    rewrite H.
    constructor.
    assert ( [[ b ]]u < 0).
    omega.
    generalize (ulst2Z_pos b); intro.
    assert (~( [[ b ]]u < 0)).
    omega.
    tauto.
    do 2 rewrite slst2Z_i in H1.
    rewrite H in H1; rewrite H0 in H1.
    assert ([[ a ]]u = [[ b ]]u).
    omega.
    rewrite (ulst2Z_injection n a b); auto.
  Qed.

  Lemma slst2Z_ulst2Z_pos : forall n lst,
    length lst = n ->
    0 <= [[ lst ]]s ->
    [[ lst ]]s = [[ lst ]]u.
    destruct lst; intros; auto.
    destruct b; auto.
    simpl in H.
    destruct n; try discriminate.
    injection H; clear H; intro.
    simpl in H0.
    rewrite H in H0.
    assert ( 0 <= [[ lst ]]u < 2^^n).
    split.
    apply ulst2Z_pos.
    apply max_ulst2Z.
    rewrite H.
    constructor.
    omega.
  Qed.

  Lemma slst2Z_ulst2Z_pos_equiv : forall n lst,
    length lst = n ->
    (0 <= [[ lst ]]s <-> [[ lst ]]u < 2^^pred n).
    induction n.
    intros.
    destruct lst; try discriminate.
    simpl.
    firstorder.
    intros.
    destruct lst; try discriminate.
    simpl in H; injection H; clear H; intro.
    generalize (IHn _ H); intro.
    inversion_clear H0.
    destruct b; simpl.
    split; intros.
    apply max_ulst2Z.
    rewrite H.
    constructor.
    apply ulst2Z_pos.
    split; intros.
    rewrite H in H0.
    rewrite H.
    assert (2^^n <= [[lst ]]u).
    omega.
    lapply (max_ulst2Z n lst).
    intro.
    assert (~(2^^n <= [[lst ]]u)).
    omega.
    contradiction.
    rewrite H; constructor.
    rewrite H in H0.
    rewrite H.
    assert ([[lst ]]u < 0).
    omega.
    generalize (ulst2Z_pos lst); intro.
    omega.
  Qed.

  Lemma slst2Z_ulst2Z_neg : forall n lst,
    length lst = n ->
    [[ lst ]]s < 0 ->
    [[ lst ]]s = [[ lst ]]u - 2^^n.
    intros.
    destruct n.
    destruct lst; try discriminate.
    destruct lst; try discriminate.
    destruct b.
    simpl in H0.
    generalize (ulst2Z_pos lst); omega.
    rewrite ulst2Z_i.
    rewrite slst2Z_i.
    rewrite Zpower_S.
    simpl in H; injection H; clear H; intro.
    rewrite H.
    ring.
  Qed.
  
  Lemma slst2Z_zeros : forall n, [[ zeros n ]]s = 0.
    induction n; auto.
    simpl.
    destruct n; auto.
  Qed.

(*  Lemma slst2Z_i_lt0: forall tl,
    slst2Z (i :: tl) < 0.
    intros.
    rewrite slst2Z_i.
    generalize tl.
    clear tl.
    induction tl.
    simpl.
    omega.
    destruct a.
    simpl ulst2Z.
    simpl length.
    rewrite Zpower_S.
    generalize (Zpower_1 (length tl)); omega.
    simpl ulst2Z.
    simpl length.
    rewrite Zpower_S.
    generalize (Zpower_1 (length tl)); omega.
  Qed.*)

  Lemma max_slst2Z : forall n lst,
    length lst = S n ->
    [[ lst ]]s < 2^^n.
    induction n; intros.
    destruct lst; try discriminate.
    destruct lst; try discriminate.
    destruct b; simpl; omega.
    destruct lst; try discriminate.
    simpl in H; injection H; clear H; intro.
    destruct b.
    rewrite slst2Z_o.
    lapply (max_ulst2Z (length lst) lst).
    rewrite H.
    auto.
    constructor.
    generalize (IHn _ H); intro.
    rewrite slst2Z_i.
    lapply (max_ulst2Z (S n) lst).
    intro.
    rewrite H.
    apply Zlt_trans with 0.
    omega.
    apply Zpower_0.
    rewrite H.
    constructor.
  Qed.

  Lemma slst2Z_app : forall lst elt, 
    (length lst > O)%nat ->
    [[ lst ++ (elt::nil) ]]s = 2 * [[ lst ]]s + [[ elt::nil ]]u.
    induction lst.
    intros.
    inversion H.
    intros.
    assert ((a :: lst) ++ elt :: nil = (a :: lst++elt::nil) ++ nil).
    simpl.
    rewrite app_ass.
    auto.
    rewrite H0; clear H0.
    rewrite <-app_nil_end.
    destruct a.
    rewrite slst2Z_o.
    rewrite slst2Z_o.
    rewrite ulst2Z_last.
    auto.
    rewrite slst2Z_i.
    rewrite slst2Z_i.
    rewrite ulst2Z_last.
    ring.
    rewrite length_app.
    simpl length.
    rewrite Zpower_is_exp.
    simpl (Zpower 2 1).
    ring.
  Qed.

  Lemma slst2Z_neg_ones : forall n lst,
    length lst = n ->
    forall l',
      (l' < n)%nat ->
      - 2^^l' <= [[ lst ]]s < 0 ->
      exists lst', lst = ones (n - l') ++ lst'.
    induction n.
    intros.
    inversion H0.
    intros.
    destruct lst; try discriminate.
    simpl in H; injection H; clear H; intro.
    destruct b.
    rewrite slst2Z_o in H1.
    inversion_clear H1.
    generalize (ulst2Z_pos lst); intro.
    assert (~(ulst2Z lst < 0)).
    omega.
    tauto.
    rewrite slst2Z_i in H1.
    rewrite H in H1.
    assert (l' = n \/ l' < n)%nat.
    omega.
    inversion_clear H2.
    subst l'.
    cutrewrite (S n - n = 1)%nat.
    exists lst; auto.
    omega.
    generalize (IHn _ H _ H3); intro.
    destruct lst.
    simpl in H; subst n; inversion H3.
    destruct b.
    simpl ulst2Z in H1.
    rewrite slst2Z_o in H2.

    destruct n; try discriminate.
    simpl in H; injection H; clear H; intro.
    destruct n.
    destruct lst; try discriminate.
    clear H.
    destruct l'.
    simpl in H1.
    assert (~(-1<=-2)).
    omega.
    tauto.
    inversion H3.
    inversion H4.
    assert (ulst2Z lst < Zpower 2 (S n)).
    apply max_ulst2Z.
    omega.
    assert ( - Zpower 2 (S (S n)) + ulst2Z lst < - Zpower 2 (S n)).
    rewrite Zpower_S.
    omega.
    assert ( - Zpower 2 l' <  - Zpower 2 (S n)).
    omega.
    assert ( Zpower 2 l' > Zpower 2 (S n)).
    omega.
    assert (l' <= S n)%nat.  
    omega.
    generalize (Zpower_2_le _ _ H8); intro.
    assert ( ~ (Zpower 2 l' <= Zpower 2 (S n)) ).
    omega.
    tauto.
    rewrite slst2Z_i in H2.
    rewrite ulst2Z_i in H1.
    destruct n; try discriminate.
    simpl in H; injection H; clear H; intro.
    rewrite H in H2.
    rewrite H in H1.
    rewrite Zpower_S in H1.
    assert ( - Zpower 2 l' <= - Zpower 2 n + ulst2Z lst < 0 ).
    omega.
    generalize (H2 H4); intro.
    inversion_clear H5.
    cutrewrite (S n - l' = S (n-l'))%nat in H6.
    simpl in H6.
    injection H6; intro.
    exists x.
    cutrewrite (S (S n) - l' = S (S (n-l')))%nat.
    simpl.
    rewrite H5; auto.
    omega.
    omega.
  Qed.

  Lemma slst2Z_ulst2Z_pos_zeros : forall n lst,
    length lst = n ->
    forall l',
      (l' < n)%nat ->
      0 <= [[ lst ]]s < 2^^l' ->
      exists lst', lst = zeros (n - l') ++ lst'.
    intros.
    destruct lst.
    simpl in H.
    subst n.
    inversion H0.
    destruct n; try discriminate.
    simpl in H; injection H; clear H; intro.
    destruct b.
    rewrite slst2Z_o in H1.
    assert (n >= l')%nat.
    omega.
    assert ( ulst2Z lst < Zpower 2 l').
    omega.
    generalize (ulst2Z_power' _ _ _ H2 H H3); intro X; inversion_clear X.
    exists x.
    rewrite H4.
    cutrewrite (S n - l' = S (n-l') )%nat.
    auto.
    omega.
    rewrite slst2Z_i in H1.
    rewrite H in H1.
    assert ( ulst2Z lst < Zpower 2 n).
    apply max_ulst2Z.
    omega.
    assert ( - Zpower 2 n + ulst2Z lst < 0).
    omega.
    assert ( ~( - Zpower 2 n + ulst2Z lst < 0) ).
    omega.
    tauto.
  Qed.

  Lemma slst2Z_shl_lst : forall l lst,
    length lst = l ->
    forall k l',
      (l' > k)%nat ->
      forall lst',
	lst = ones l' ++ lst' \/ lst = zeros l' ++ lst' ->
	[[ shl_lst k lst ]]s = [[ lst ]]s * 2^^k.
    induction l.
    intros.
    destruct lst; try discriminate.
    destruct k; auto.
    intros.
    destruct lst; try discriminate.
    simpl in H; injection H; clear H; intro.
    destruct l'.
    inversion H0.
    simpl in H1.
    destruct b.
    inversion_clear H1; try discriminate.
    injection H2; clear H2; intro.
    destruct k.
    simpl.
    ring.
    simpl shl_lst.
    rewrite slst2Z_o.
    assert (l' > k)%nat.
    omega.
    lapply (IHl _ H _ _ H2 lst').
    intro.
    destruct l.
    destruct lst; try discriminate.
    simpl.
    destruct k; auto.
    rewrite slst2Z_app.
    simpl ulst2Z.
    rewrite H3.
    destruct l'.
    inversion H2.
    simpl in H1.
    rewrite H1.
    rewrite slst2Z_o.
    rewrite ulst2Z_o.
    rewrite Zpower_S.
    ring.
    rewrite (shl_length k (S l)).
    omega.
    auto.
    auto.
    destruct k.
    simpl shl_lst.
    
    simpl Zpower.
    ring.
    assert (l' > k)%nat.
    omega.
    lapply (IHl _ H _ _ H2 lst').
    intro.
    simpl shl_lst.
    rewrite slst2Z_i.
    rewrite H.
    destruct l.
    destruct lst; try discriminate.
    inversion_clear H1.
    destruct l'; try discriminate.
    destruct lst'; try discriminate.
    destruct k.
    inversion H2.
    inversion H2.
    discriminate.
    rewrite slst2Z_app.
    simpl ulst2Z.
    rewrite H3.
    destruct l'.
    inversion H2.
    inversion_clear H1.
    simpl in H4.
    injection H4; clear H4; intro.
    rewrite H1.
    rewrite slst2Z_i .
    rewrite ulst2Z_i.
    rewrite length_app.
    rewrite ones_length.
    assert (length lst' = l - l')%nat.
    
    rewrite H1 in H.
    simpl in H.
    rewrite length_app in H.
    rewrite ones_length in H.
    omega.
    rewrite H4.
    
    cutrewrite (l' + (l-l') = l )%nat.

    do 2 rewrite Zpower_S.
    ring.

    rewrite H1 in H.
    simpl in H.
    rewrite length_app in H.
    rewrite ones_length in H.
    omega.
    discriminate.
    rewrite (shl_length k (S l)).
    omega.
    auto.
    inversion_clear H1.
    injection H3; auto.
    discriminate.
  Qed.

  (*
   * correctness of cplt2
   *)

  Lemma cplt2_correct : forall n a,
    length a = S n ->
    ~(exists k, a = i :: zeros k) ->
    [[ cplt2 a ]]s = - [[ a ]]s .
    induction n.
    destruct a.
    intro.
    discriminate H.
    destruct a.
    intros.
    destruct b.
    auto.
    assert (exists k : nat, i :: nil = i :: zeros k).
    exists O; auto.
    tauto.
    intros.
    discriminate H.
    intros.
    destruct a.
    discriminate H.
    destruct a.
    discriminate H.
    simpl in H.
    injection H; clear H; intro.
    destruct b; destruct b0.
    
    generalize (dec_equ_lst_bit' a (zeros n)); intro X; inversion_clear X.
    subst a.
    assert ( o :: o :: zeros n = zeros (S (S n)) ).
    auto.
    rewrite H1.
    rewrite cplt2_zeros.
    rewrite slst2Z_zeros.
    auto.
    rewrite cplt2_prop.
    rewrite slst2Z_i.
    rewrite cplt2_length.
    simpl length.
    rewrite slst2Z_o.
    rewrite ulst2Z_o.
    rewrite cplt2_prop.
    rewrite ulst2Z_i.
    rewrite cplt2_length.
    rewrite H.
    assert ( length (o::a) = S n).
    simpl in H; simpl; omega.
    assert (~(exists k : nat, o::a = i :: zeros k)).
    intro.
    inversion_clear H3.
    discriminate H4.
    generalize (IHn (o::a) H2 H3); intro.
    rewrite cplt2_prop in H4; auto.
    rewrite slst2Z_i in H4.
    rewrite slst2Z_o in H4.
    rewrite cplt2_length in H4.
    rewrite H in H4.
    rewrite <-H4.
    rewrite <-(Zpower_plus n).
    ring.
    intro X; inversion_clear X.
    rewrite H5 in H2; simpl in H2; injection H2; intros.
    rewrite zeros_length in H6; subst x; tauto.
    intro X; inversion_clear X.
    rewrite H2 in H; rewrite zeros_length in H; subst x; tauto.
    intro X; inversion_clear X.
    discriminate.
    intro X; inversion_clear X.
    destruct x; try discriminate.
    simpl in H2; injection H2; intro.
    rewrite H3 in H; rewrite zeros_length in H; subst x; tauto.
    intro X; inversion_clear X.
    discriminate.
    
    rewrite cplt2_prop.

    generalize (dec_equ_lst_bit' a (zeros n)); intro X; inversion_clear X.
    rewrite H1.
    rewrite cplt2_weird.
    rewrite slst2Z_i.
    rewrite slst2Z_o.
    rewrite ulst2Z_i.
    simpl length.
    rewrite zeros_length.
    rewrite ulst2Z_zeros.
    rewrite <-(Zpower_plus n).
    ring.
    auto.
    assert ( length (i::a) = S n ).
    simpl; auto.
    assert ( ~ (exists k : nat, i::a = i :: zeros k) ).
    intro.
    inversion_clear H3.
    injection H4; intro.
    rewrite H3 in H; rewrite zeros_length in H; subst x.
    tauto.
    generalize (IHn _ H2 H3); intro.
    rewrite cplt2_prop in H4; auto.
    rewrite slst2Z_o in H4.
    rewrite slst2Z_i in H4.
    rewrite slst2Z_i.
    rewrite slst2Z_o.
    rewrite ulst2Z_i.
    rewrite cplt2_prop; auto.
    assert ( (length (cplt i :: cplt2 a) = S (length (cplt2 a)))).
    auto.
    rewrite H5; clear H5.
    rewrite cplt2_length.
    rewrite Zpower_S.
    rewrite ulst2Z_o.
    rewrite H4.
    ring.
    intro.
    inversion_clear H5.
    rewrite H6 in H; rewrite zeros_length in H; subst x; tauto.
    intro X; inversion_clear X.
    rewrite H5 in H; rewrite zeros_length in H; subst x; tauto.
    intro X; inversion_clear X.
    destruct x; discriminate.
    intro X; inversion_clear X; discriminate.

    generalize (dec_equ_lst_bit' a (zeros n)); intro X; inversion_clear X.
    assert (exists k : nat, i :: o :: a = i :: zeros k).
    exists (S n).
    rewrite H1; auto.
    tauto.
    rewrite cplt2_prop.
    assert ( length (o::a) = S n).
    simpl; auto.
    assert  (~ (exists k : nat, o::a = i :: zeros k)).
    intro X; inversion_clear X.
    discriminate.
    generalize (IHn _ H2 H3); intro.
    rewrite slst2Z_o in H4.
    rewrite cplt2_prop in H4; auto.
    rewrite cplt2_prop; auto.
    rewrite slst2Z_i in H4.
    rewrite slst2Z_i.
    rewrite slst2Z_o.
    rewrite ulst2Z_i.
    rewrite ulst2Z_o.
    rewrite cplt2_length.
    rewrite cplt2_length in H4.
    assert (length (o::a) = S (length a)).
    auto.
    rewrite H5; clear H5.
    rewrite Zpower_S.
    omega.
    intro.
    inversion_clear H2.
    inversion_clear H5.
    rewrite H2 in H; rewrite zeros_length in H; subst x; tauto.
    intro X; inversion_clear X.
    rewrite H5 in H; rewrite zeros_length in H; subst x; tauto.
    intro X; inversion_clear X.
    destruct x; try discriminate.
    simpl in H2; injection H2; intro.
    rewrite H3 in H; rewrite zeros_length in H; subst x; tauto.
    intro X; inversion_clear X.
    destruct x; try discriminate.
    simpl in H2; injection H2; intro.
    rewrite H3 in H; rewrite zeros_length in H; subst x; tauto.
    
    rewrite cplt2_prop.
    generalize (dec_equ_lst_bit' a (zeros n)); intro X; inversion_clear X.
    rewrite H1.
    rewrite cplt2_weird.
    rewrite slst2Z_o.
    rewrite slst2Z_i.
    rewrite ulst2Z_i.
    rewrite ulst2Z_zeros.
    simpl length.
    rewrite Zpower_S.
    rewrite zeros_length.
    ring.
    assert ( length (i::a) = S n).
    simpl; auto.
    assert (  ~ (exists k : nat, i::a = i :: zeros k) ).
    intro X; inversion_clear X.
    injection H3; intro.
    rewrite H4 in H; rewrite zeros_length in H; subst x; tauto.
    generalize (IHn _ H2 H3); intro.
    rewrite cplt2_prop in H4; auto.
    rewrite cplt2_prop; auto.
    rewrite slst2Z_o in H4.
    rewrite slst2Z_i in H4.
    rewrite slst2Z_o.
    rewrite slst2Z_i.
    rewrite ulst2Z_i.
    rewrite ulst2Z_o.
    simpl length.
    rewrite H4; clear H4.
    rewrite Zpower_S.
    omega.
    intro X; inversion_clear X.
    rewrite H5 in H; rewrite zeros_length in H; subst x; tauto.
    intro X; inversion_clear X.
    rewrite H5 in H; rewrite zeros_length in H; subst x; tauto.
    intro X; inversion_clear X.
    destruct x; try discriminate.
    intro X; inversion_clear X.
    destruct x; discriminate.
  Qed.

  (*
   * from Coq integers to integers in two's complement notation
   *)

  Definition Z2slst (z:Z) : list bit :=
    match z with
      Z0 => o::o::nil
      | Zpos p => o :: Z2ulst z 
      | Zneg p => cplt2  (o :: Z2ulst (Zpos p))
    end.

  Lemma Z2slst2Z: forall n,
    [[ Z2slst n ]]s = n.
    induction n.
    auto.
    simpl.
    rewrite ulst2Z_rev_poslst.
    auto.
    simpl.
    rewrite (cplt2_correct (length (pos2lst p))).
    simpl.
    rewrite ulst2Z_rev_poslst.
    auto.
    simpl.
    rewrite length_rev.
    auto.
    intro.
    inversion_clear H.
    discriminate.
  Qed.

  Lemma Z2slst_Zpower: forall m (z:Z), 
    z = - 2^^m ->
    Z2slst z = i :: i :: zeros m.
    destruct z; intros; try discriminate.
    generalize (Zpower_1 m); intro.
    assert (Zpower 2 m <> 0).
    omega.
    assert (Zpower 2 m = 0).
    omega.
    tauto.
    generalize (Zpower_1 m); intro.
    assert (- (Zpower 2 m) > 0).
    rewrite <-H.
    apply Zgt_pos_0.
    assert (- (Zpower 2 m) < 0).
    omega.
    red in H1.
    red in H2.
    rewrite H2 in H1.
    discriminate.
    simpl.
    rewrite cplt2_prop.
    simpl.
    generalize (Zneg_Zpower _ _ H); intro.
    rewrite H0.
    rewrite cplt2_weird.
    auto.
    intro.
    inversion_clear H0.
    rewrite (Zneg_Zpower _ _ H) in H1.
    destruct x; discriminate.
    intro X; inversion_clear X; discriminate.
  Qed.

  (*
   * correctness of the addition for signed numbers
   *)

  Lemma slst2Z_last : forall l e,
    l <> nil ->
    [[ l ++ e::nil ]]s = 2 * [[ l ]]s + [[ e::nil ]]u.
    induction l; intros.
    tauto.
    destruct a.
    rewrite slst2Z_o.
    simpl app.
    rewrite slst2Z_o.
    apply ulst2Z_last.
    rewrite slst2Z_i.
    simpl app.
    rewrite slst2Z_i.
    rewrite length_app.
    simpl length.
    rewrite Zpower_is_exp.
    rewrite ulst2Z_last.
    ring.
    simpl (Zpower 2 1).
    ring.
  Qed.
  
  Lemma length_not_nil : forall (A:Set) (lst:list A),
    length lst <> O -> lst <> nil.
    intros.
    intro.
    apply H.
    rewrite H0; auto.
  Qed.

  Lemma add_lst'_Z_oo: forall n l k carry,
    length l = n ->
    length k = n ->
    (n > 0)%nat ->
    [[ rev l ]]u + [[ rev k ]]u + [[ carry::nil ]]u < 2^^n ->
    [[ rev (add_lst' (l ++ o::nil)  (k ++ o::nil) carry) ]]s = 
    [[ rev l ]]u + [[ rev k ]]u + [[ carry::nil ]]u.
    induction n.
    intros.
    inversion_clear H1.
    intros.
    destruct l as [_ | l0 l]; try discriminate.
    destruct k as [_ | k0 k]; try discriminate.
    simpl in H; injection H; clear H; intro H.
    simpl in H0; injection H0; clear H0; intro H0.
    assert ( n = 0 \/ n > 0 )%nat.
    omega.
    inversion_clear H3.
    subst n.
    destruct l; try discriminate.
    destruct k; try discriminate.
    destruct l0; destruct k0; destruct carry; simpl; auto.
    simpl in H2.
    inversion H2.
    simpl in H2.
    inversion H2.
    simpl in H2.
    inversion H2.
    simpl in H2.
    inversion H2.
    destruct l0; destruct k0; destruct carry; simpl.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    ring.
    simpl rev in H2.
    do 2 rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    rewrite Zpower_S in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    ring.
    simpl rev in H2.
    do 2 rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    rewrite Zpower_S in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    ring.
    simpl rev in H2.
    do 2 rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    rewrite Zpower_S in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    ring.
    simpl rev in H2.
    do 2 rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    rewrite Zpower_S in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    ring.
    simpl rev in H2.
    do 2 rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    rewrite Zpower_S in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    ring.
    simpl rev in H2.
    do 2 rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    rewrite Zpower_S in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    ring.
    simpl rev in H2.
    do 2 rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    rewrite Zpower_S in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    ring.
    simpl rev in H2.
    do 2 rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    rewrite Zpower_S in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.
  Qed.

  Lemma add_lst_Z_oo : forall n l k carry,
    length l = n ->
    length k = n ->
    (n > 0)%nat ->
    [[ l ]]u + [[ k ]]u + [[ carry::nil ]]u < 2^^n ->
    [[ add_lst (o::l) (o::k) carry ]]s = 
    [[ l ]]u + [[ k ]]u + [[ carry::nil ]]u.
    intros.
    unfold add_lst.
    do 2 rewrite rev_unit''.
    rewrite (add_lst'_Z_oo n).
    do 2 rewrite rev_involutive.
    auto.
    rewrite length_rev; auto.
    rewrite length_rev; auto.
    auto.
    do 2 rewrite rev_involutive.
    auto.
  Qed.

  Lemma add_lst'_Z_oi : forall n l k carry,
    length l = n ->
    length k = n ->
    (n > 0)%nat ->
    [[ rev (add_lst' (l++(o::nil)) (k++(i::nil)) carry) ]]s = 
    [[ rev l ]]u + [[ rev k ]]u + [[ carry::nil ]]u - 2^^n.
    induction n.
    intros.
    inversion H1.
    intros.
    destruct l; try discriminate.
    destruct k; try discriminate.
    simpl in H; injection H; clear H; intro.
    simpl in H0; injection H0; clear H0; intro.
    assert ( n = 0 \/ n > 0 )%nat.
    omega.
    inversion_clear H2.
    subst n.
    destruct l; try discriminate.
    destruct k; try discriminate.
    destruct b; destruct b0; destruct carry; simpl; auto.
    
    destruct b; destruct b0; destruct carry; simpl rev.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite Zpower_S.
    ring.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite Zpower_S.
    ring.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite Zpower_S.
    ring.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite Zpower_S.
    ring.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite Zpower_S.
    ring.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite Zpower_S.
    ring.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite Zpower_S.
    ring.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite Zpower_S.
    ring.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.
  Qed.

  Lemma add_lst_Z_oi : forall n l k carry,
    length l = n ->
    length k = n ->
    (n > 0)%nat ->
    [[ add_lst (o::l) (i::k) carry ]]s = 
    [[ l ]]u + [[ k ]]u + [[ carry::nil ]]u - 2^^n.
    intros.
    unfold add_lst.
    do 2 rewrite rev_unit''.
    rewrite (add_lst'_Z_oi n); auto.
    do 2 rewrite rev_involutive.
    auto.
    rewrite length_rev; auto.
    rewrite length_rev; auto.
  Qed.

  Lemma add_lst'_Z_ii : forall n l k carry,
    length l = n ->
    length k = n ->
    (n > 0)%nat ->
    2^^n <= [[ rev l ]]u + [[ rev k ]]u + [[ carry::nil ]]u ->
    [[ rev (add_lst' (l++(i::nil)) (k++(i::nil)) carry) ]]s = 
    [[ rev l ]]u + [[ rev k ]]u + [[ carry::nil ]]u - 2^^(S n).
    induction n.
    intros.
    inversion H1.
    intros.
    destruct l; try discriminate.
    destruct k; try discriminate.
    simpl in H; injection H; clear H; intro.
    simpl in H0; injection H0; clear H0; intro.
    destruct n.
    destruct l; try discriminate.
    destruct k; try discriminate.
    destruct b; destruct b0; destruct carry; auto.
    simpl in H2.
    omega.
    simpl in H2.
    omega.
    simpl in H2.
    omega.
    simpl in H2.
    omega.
    destruct b; destruct b0; destruct carry; simpl rev.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite (Zpower_S 2 (S (S n))).
    ring.
    omega.
    rewrite Zpower_S in H2.
    simpl rev in H2.
    repeat rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite (Zpower_S 2 (S (S n))).
    ring.
    omega.
    rewrite Zpower_S in H2.
    simpl rev in H2.
    repeat rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite (Zpower_S 2 (S (S n))).
    ring.
    omega.
    rewrite Zpower_S in H2.
    simpl rev in H2.
    repeat rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite (Zpower_S 2 (S (S n))).
    ring.
    omega.
    rewrite Zpower_S in H2.
    simpl rev in H2.
    repeat rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite (Zpower_S 2 (S (S n))).
    ring.
    omega.
    rewrite Zpower_S in H2.
    simpl rev in H2.
    repeat rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite (Zpower_S 2 (S (S n))).
    ring.
    omega.
    rewrite Zpower_S in H2.
    simpl rev in H2.
    repeat rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite (Zpower_S 2 (S (S n))).
    ring.
    omega.
    rewrite Zpower_S in H2.
    simpl rev in H2.
    repeat rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.

    rewrite slst2Z_last.
    rewrite ulst2Z_last.
    rewrite ulst2Z_last.
    rewrite IHn; auto.
    simpl ulst2Z.
    rewrite (Zpower_S 2 (S (S n))).
    ring.
    omega.
    rewrite Zpower_S in H2.
    simpl rev in H2.
    repeat rewrite ulst2Z_last in H2.
    simpl ulst2Z in H2.
    simpl ulst2Z.
    omega.
    apply length_not_nil.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_app.
    simpl.
    omega.
    do 2 rewrite length_app.
    rewrite H; rewrite H0; simpl; reflexivity.
  Qed.

  Lemma add_lst_Z_ii : forall n l k carry,
    length l = n ->
    length k = n ->
    (n > 0)%nat ->
    2^^n <= [[ l ]]u + [[ k ]]u + [[ carry::nil ]]u ->
    [[ add_lst (i::l) (i::k) carry ]]s = 
    [[ l ]]u + [[ k ]]u + [[ carry::nil ]]u - 2^^(S n).
    intros.
    unfold add_lst.
    do 2 rewrite rev_unit''.
    rewrite (add_lst'_Z_ii n); auto.
    do 2 rewrite rev_involutive.
    auto.
    rewrite length_rev; auto.
    rewrite length_rev; auto.
    do 2 rewrite rev_involutive.
    auto.
  Qed.

  Lemma add_lst_Z : forall (n:nat) (a b:list bit),
    length a = S n ->
    length b = S n ->
    - 2^^n <= [[ a ]]s + [[ b ]]s < 2^^n -> 
    [[ add_lst a b o ]]s = [[ a ]]s + [[ b ]]s.
    destruct n.
    destruct a.
    intros.
    discriminate H.
    destruct b0.
    intros.
    discriminate H0.
    intros.
    destruct a.
    destruct b1.
    destruct b; destruct b0; try (simpl; firstorder).
    discriminate H0.
    discriminate H.
    intros.
    destruct a.
    discriminate H.
    rename b0 into a0.
    destruct b.
    discriminate H0.
    rename b0 into btmp.
    rename b into b0.
    rename btmp into b.
    simpl in H; injection H; clear H; intro.
    simpl in H0; injection H0; clear H0; intro.
    
    destruct a0; destruct b0.
    
    (* we add two positive numbers *)
    
    do 2 rewrite slst2Z_o.
    do 2 rewrite slst2Z_o in H1.
    rewrite (add_lst_Z_oo (S n)); auto.
    ring.
    omega.
    simpl ulst2Z.
    omega.
    
    (* we add a positive number with a negative number (never overflows) *)

    rewrite slst2Z_o in H1.
    rewrite slst2Z_i in H1.
    rewrite H0 in H1.
    rewrite slst2Z_o.
    rewrite slst2Z_i.
    rewrite H0.
    rewrite (add_lst_Z_oi (S n)); auto.
    ring.
    omega.
    
    rewrite (add_lst_com (i::a) (o::b) o).
    rewrite (add_lst_Z_oi (S n)); auto.
    rewrite ulst2Z_o.
    rewrite slst2Z_i.
    rewrite slst2Z_o.
    ring.
    rewrite H.
    ring.
    omega.
    
    (* we add two negative numbers *)
    
    do 2 rewrite slst2Z_i.
    rewrite H.
    rewrite H0.
    do 2 rewrite slst2Z_i in H1.
    rewrite H in H1.
    rewrite H0 in H1.
    rewrite (add_lst_Z_ii (S n)); auto.
    ring.
    rewrite Zpower_S.
    ring.
    omega.
    simpl ulst2Z.
    omega.
  Qed.

  Lemma sign_extend_lst_s2Z : forall l n,
    [[ sign_extend_lst n l ]]s = [[ l ]]s.
    induction n.
    destruct l; auto.
    destruct l.
    simpl.
    rewrite ulst2Z_zeros.
    auto.
    destruct b.
    simpl.
    rewrite sign_extend_lst_s2nat_o.
    auto.
    simpl (sign_extend_lst (S n) (i::l)).
    rewrite slst2Z_i.
    rewrite (sign_extend_length n (S (length l))); auto.
    rewrite slst2Z_i.
    rewrite sign_extend_lst_s2nat_i.
    rewrite Zpower_is_exp.
    rewrite <-Zpower_plus.
    rewrite <-Zpower_plus.
    ring.
  Qed.

  (*
   * correctness of the signed multiplication
   *)

  Ltac rew_len :=
    simpl; 
      rewrite length_app ||
	rewrite zeros_length || 
	    (*rewrite add_lst_length || *)
	    rewrite cplt2_length ||
	      rewrite umul_lst_length ||
		idtac.
  
  Lemma smul_lst_Z1 : forall n a b,
    length a = S (S n) ->
    length b = S (S n) ->
    ~ (is_pos a = true) ->
    is_pos b = true ->
    [[ smul_lst a b ]]s = [[ a ]]s * [[ b ]]s.
    intros.
    destruct b; try discriminate.
    destruct b0; try discriminate.
    destruct a; try discriminate.
    destruct a; try discriminate.
    rename a into a1.
    rename b2 into a.
    rename b3 into a0.
    destruct a.
    simpl in H1; tauto.
    destruct b; try discriminate.
    destruct n.
    destruct a1; try discriminate.
    destruct b1; try discriminate.
    destruct a0; destruct b0; auto.
    unfold smul_lst.
    match goal with
      | |- slst2Z ?X = ?Y => simpl X
    end.
    simpl in H; injection H; clear H; intros.
    simpl in H0; injection H0; clear H0; intros.
    rewrite (cplt2_correct (S (S (S (S n+S n))))).
    rewrite slst2Z_o.
    rewrite slst2Z_i.
    rewrite slst2Z_o.
    simpl length.
    rewrite H.
    rewrite H0.
    destruct b0.
    rewrite ulst2Z_o.
    rewrite ulst2Z_o.
    destruct a0.
    rewrite ulst2Z_o.
    cut (is_zeros a1 = true \/ is_zeros a1 = false).
    intro X; inversion_clear X.
    generalize (is_zeros_zeros _ H3); clear H3; intro.
    rewrite H3.
    cutrewrite ( o :: zeros (length a1) = zeros (S (S n)) ).
    rewrite cplt2_weird.
    rewrite umul_lst_leading_i.
    simpl zeros.
    rewrite umul_lst_leading_o.
    rewrite (umul_lst_com (S n)).
    rewrite umul_lst_zeros.
    simpl length.
    rewrite zeros_length.
    rewrite add_lst_neutral.
    rewrite ulst2Z_o.
    rewrite ulst2Z_zeros.
    cutrewrite (o::o::zeros n = zeros (S (S n))).
    rewrite ulst2Z_app_zeros.
    ring.
    auto.
    rew_len.
    rew_len.
    rewrite <-(plus_Snm_nSm (length b1) (S n)).
    auto.
    simpl.
    apply is_zeros_zeros'.
    rew_len.
    auto.
    auto.
    omega.
    intro; discriminate.
    intro; subst b1; discriminate.
    rewrite H; auto.
    rewrite cplt2_prop.
    rewrite umul_lst_leading_o.
    rewrite cplt2_prop.
    rewrite umul_lst_leading_i.
    rewrite ulst2Z_o.
    rewrite (ulst2Z_add_lst (S (S (n+n)))).
    rewrite ulst2Z_app_zeros.
    rewrite cplt2_length.
    rewrite ulst2Z_o.
    rewrite (umul_lst_nat n).

    destruct n; try discriminate.
    destruct a1; try discriminate.
    destruct a1; try discriminate.
    destruct b1; try discriminate.
    destruct b1; try discriminate.
    destruct b; destruct b0; try discriminate.
    simpl.
    auto.
    simpl.
    auto.

    rewrite (ulst2Z_cplt2' n).
    rewrite H.
    rewrite <-(Zpower_plus (S (S n))).
    simpl ulst2Z.
    ring.
    auto.
    intro X; rewrite X in H3.
    rewrite is_zeros_zeros' in H3; discriminate.
    rew_len.
    auto.
    auto.
    rew_len.
    rew_len.
    rew_len.
    omega.
    rew_len.
    rew_len.
    rew_len.
    omega.
    intro X; inversion_clear X.
    rewrite H4 in H3.
    rewrite is_zeros_zeros' in H3; discriminate.
    intro X; inversion_clear X; discriminate.
    apply cplt2_nil.
    intro X; discriminate.
    intro X; subst b1; discriminate.
    intro X; inversion_clear X.
    destruct x.
    simpl in H4.
    discriminate.
    injection H4; intro X; rewrite X in H3; rewrite is_zeros_zeros' in H3; discriminate.
    intro X; inversion_clear X.
    destruct x.
    simpl in H4; discriminate.
    injection H4; intro X; rewrite X in H3; rewrite is_zeros_zeros' in H3; discriminate.
    case (is_zeros a1); auto.
    rewrite ulst2Z_i.
    rewrite H.
    rewrite cplt2_prop.
    rewrite umul_lst_leading_o.

    cut (is_zeros a1 = true \/ is_zeros a1 = false).
    intro X; inversion_clear X.
    generalize (is_zeros_zeros _ H3); clear H3; intro.
    rewrite H3.
    rewrite ulst2Z_zeros.
    rewrite cplt2_weird.
    rewrite umul_lst_leading_i.
    rewrite (umul_lst_com (S n)).
    rewrite umul_lst_zeros.
    rewrite add_lst_neutral.
    rewrite ulst2Z_o.
    rewrite ulst2Z_o.
    rewrite ulst2Z_app_zeros.
    rewrite zeros_length.
    rewrite H.
    rewrite <-(Zpower_plus (S n)).
    ring.
    rew_len.
    rew_len.
    rew_len.
    auto.
    apply is_zeros_zeros'.
    rew_len.
    auto.
    auto.
    omega.
    rewrite cplt2_prop.
    rewrite umul_lst_leading_o.
    rewrite ulst2Z_o.
    rewrite ulst2Z_o.
    rewrite (umul_lst_nat n).

    destruct n; try discriminate.
    destruct a1; try discriminate.
    destruct a1; try discriminate.
    destruct b1; try discriminate.
    destruct b1; try discriminate.
    destruct b; destruct b0; try discriminate.
    simpl.
    auto.
    simpl.
    auto.

    rewrite (ulst2Z_cplt2' n).
    rewrite <-(Zpower_plus (S (S n))).
    ring.
    auto.
    intro X; rewrite X in H3; rewrite is_zeros_zeros' in H3; discriminate.
    rew_len.
    auto.
    auto.
    apply cplt2_nil.
    intro X; subst a1; discriminate.
    intro X; subst b1; discriminate.
    intro X; inversion_clear X.
    rewrite H4 in H3;  rewrite is_zeros_zeros' in H3; discriminate.
    intro X; inversion_clear X.
    injection H4; clear H4; intro.
    rewrite H4 in H3; rewrite is_zeros_zeros' in H3; discriminate.
    case (is_zeros a1); auto.
    apply cplt2_nil.
    intro X; discriminate.
    intro X; subst b1; discriminate.

    intro X; inversion_clear X as [k]; destruct k; discriminate.
    intro X; inversion_clear X as [k]; destruct k; discriminate.

    rewrite ulst2Z_i.
    rewrite H0.
    rewrite (ulst2Z_add_lst (S (S (S (S (n + n)))))).
    rewrite ulst2Z_o.
    simpl (ulst2Z nil).
    rewrite ulst2Z_app_zeros.
    destruct a0.
    rewrite ulst2Z_o.
    cut (is_zeros a1 = true \/ is_zeros a1 = false).
    intro X; inversion_clear X.
    generalize (is_zeros_zeros _ H3); clear H3; intro.
    rewrite H3.
    cutrewrite ( o :: zeros (length a1) = zeros (S (S n)) ).
    rewrite cplt2_weird.
    rewrite ulst2Z_zeros.
    rewrite ulst2Z_i.
    rewrite zeros_length.
    rewrite ulst2Z_zeros.
    rewrite umul_lst_leading_i.
    rewrite zeros_length.
    rewrite (ulst2Z_add_lst (S (S (S ((n + n)))))).
    rewrite ulst2Z_o.
    simpl (ulst2Z nil).
    rewrite ulst2Z_app_zeros.
    simpl zeros.
    rewrite umul_lst_leading_o.
    rewrite ulst2Z_o.

    rewrite (umul_lst_com (S n)).
    rewrite umul_lst_zeros.
    rewrite ulst2Z_zeros.
    rewrite <-(Zpower_plus (S n)).
    ring.
    simpl.
    apply is_zeros_zeros'.
    simpl.
    rew_len.
    auto.
    auto.
    omega.
    intro X; discriminate X.
    intro; subst b1; discriminate.
    rew_len.
    rew_len.
    rew_len.
    rew_len.
    rew_len.
    rew_len.
    rew_len.
    omega.
    rew_len.
    rew_len.
    omega.
    rew_len.
    rewrite H; auto.

    rewrite (ulst2Z_cplt2' (S n)).
    rewrite ulst2Z_i.
    rewrite ulst2Z_o.
    simpl length.
    rewrite H.
    rewrite cplt2_prop.
    rewrite umul_lst_leading_o.
    rewrite ulst2Z_o.
    rewrite cplt2_prop.
    rewrite umul_lst_leading_i.
    rewrite (ulst2Z_add_lst (S (S (n+n)))).
    rewrite ulst2Z_o.
    simpl (ulst2Z nil).
    rewrite cplt2_length.
    rewrite ulst2Z_app_zeros.
    rewrite (umul_lst_nat n).

    destruct n; try discriminate.
    destruct a1; try discriminate.
    destruct a1; try discriminate.
    destruct b1; try discriminate.
    destruct b1; try discriminate.
    destruct b; destruct b0; try discriminate.
    simpl.
    auto.
    simpl.
    auto.

    rewrite (ulst2Z_cplt2' n).
    rewrite H.
    rewrite <-(Zpower_plus (S (S (S n)))).
    rewrite <-(Zpower_plus (S (S n))).
    ring.
    auto.
    intro X; rewrite X in H3; rewrite is_zeros_zeros' in H3; discriminate.
    rew_len; auto.
    auto.
    rew_len.
    rew_len.
    rew_len.
    omega.
    rew_len.
    rew_len.
    omega.
    intro X; inversion_clear X.
    rewrite H4 in H3; rewrite is_zeros_zeros' in H3; discriminate.
    intro X; inversion_clear X; discriminate.
    apply cplt2_nil.
    intro; discriminate.
    intro; subst b1; discriminate.
    intro X; inversion_clear X.
    destruct x; try discriminate.
    simpl in H4; injection H4; clear H4; intro.
    rewrite H4 in H3; rewrite is_zeros_zeros' in H3; discriminate.
    intro X; inversion_clear X.
    destruct x; try discriminate.
    simpl in H4; injection H4; clear H4; intro.
    rewrite H4 in H3; rewrite is_zeros_zeros' in H3; discriminate.
    simpl; auto.
    simpl; intro; discriminate.
    case (is_zeros a1); auto.
    rewrite ulst2Z_i.
    rewrite H.
    rewrite (ulst2Z_cplt2' (S n)).
    rewrite ulst2Z_i.
    rewrite ulst2Z_i.
    simpl length.
    rewrite H.
    rewrite cplt2_prop.
    rewrite umul_lst_leading_o.
    rewrite ulst2Z_o.
    cut (is_zeros a1 = true \/ is_zeros a1 = false).
    intro X; inversion_clear X.
    rewrite (is_zeros_zeros _ H3).
    rewrite cplt2_weird.
    rewrite ulst2Z_zeros.
    rewrite umul_lst_leading_i.
    rewrite (umul_lst_com (S n)).
    rewrite umul_lst_zeros.
    rewrite add_lst_neutral.
    rewrite ulst2Z_o.
    rewrite ulst2Z_app_zeros.
    rewrite zeros_length.
    rewrite H.
    rewrite <-(Zpower_plus (S (S n))).
    rewrite <-(Zpower_plus (S n)).
    ring.
    rew_len.
    rew_len.
    rew_len.
    auto.
    apply is_zeros_zeros'.
    rew_len.
    auto.
    auto.
    omega.
    rewrite cplt2_prop.
    rewrite umul_lst_leading_o.
    rewrite ulst2Z_o.
    rewrite (umul_lst_nat n).

    destruct n; try discriminate.
    destruct a1; try discriminate.
    destruct a1; try discriminate.
    destruct b1; try discriminate.
    destruct b1; try discriminate.
    destruct b; destruct b0; try discriminate.
    simpl.
    auto.
    simpl.
    auto.

    rewrite (ulst2Z_cplt2' n); auto.
    rewrite <-(Zpower_plus (S (S (S n)))).
    rewrite <-(Zpower_plus (S (S n))).
    ring.
    intro X; subst a1.
    rewrite is_zeros_zeros' in H3; discriminate.
    auto.
    rew_len; auto.
    auto.
    apply cplt2_nil.
    intro X; subst a1; discriminate.
    intro; subst b1; discriminate.
    intro X; inversion_clear X.
    rewrite H4 in H3.
    rewrite is_zeros_zeros' in H3; discriminate.
    intro X; inversion_clear X.
    injection H4; intro.
    rewrite H5 in H3.
    rewrite is_zeros_zeros' in H3; discriminate.
    case (is_zeros a1); auto.
    apply cplt2_nil.
    intro; discriminate.
    intro; subst b1; discriminate.
    intro X; inversion_clear X.
    destruct x; discriminate.
    intro X; inversion_clear X.
    destruct x; discriminate.
    simpl; auto.
    simpl; intro; discriminate.
    rew_len.
    rew_len.
    rew_len.
    rew_len.
    omega.
    rew_len.
    rew_len.
    rew_len.
    omega.

    simpl.
    destruct b0; rew_len; rew_len; rew_len.
    omega.
    rewrite (add_lst_length ((S (S n))+(S (S (S n))))).
    rew_len.
    rew_len.
    rew_len.
    rew_len.
    omega.
    rew_len.
    rew_len.
    rew_len.
    rew_len.
    omega.
    rew_len.
    rew_len.
    rew_len.
    rew_len.
    omega.
    auto.
    intro X; inversion_clear X.
    discriminate.
  Qed.

  Lemma smul_lst_Z : forall n a b,
    length a = n ->
    length b = n ->
    [[ smul_lst a b ]]s = [[ a ]]s * [[ b ]]s.
    intros.
    destruct a; destruct b; auto.
    simpl in H; subst n; discriminate H0.
    simpl in H0; subst n.
    discriminate H0.
    destruct b0; destruct b.
    simpl.
    destruct n; try discriminate.
    destruct n; try discriminate.
    destruct a; try discriminate.
    destruct b1; try discriminate.
    auto.
    rewrite umul_lst_leading_o.
    rewrite ulst2Z_o.
    rewrite (umul_lst_nat n).
    auto.
    simpl in H; auto.
    simpl in H0; auto.
    intro; subst a; discriminate.
    intro; subst b1; discriminate.

    destruct n; try discriminate.
    destruct a; try discriminate.
    destruct b1; try discriminate.
    auto.
    simpl in H; injection H; intro; subst n; discriminate.
    destruct b1; try discriminate.
    simpl in H0; injection H0; intro; subst n; discriminate.
    destruct n; try discriminate.
    rewrite (smul_lst_com n); auto.
    rewrite (smul_lst_Z1 n); auto.
    ring.

    destruct n; try discriminate.
    destruct a; try discriminate.
    destruct b1; try discriminate.
    auto.
    simpl in H; injection H; intro; subst n; discriminate.
    destruct b1; try discriminate.
    simpl in H0; injection H0; intro; subst n; discriminate.
    destruct n; try discriminate.
    rewrite (smul_lst_Z1 n); auto.
    ring.

    destruct n; try discriminate.
    unfold smul_lst.
    match goal with
      | |- slst2Z ?X = ?Y => simpl X
    end.
    destruct n; try discriminate.
    destruct a; try discriminate.
    destruct b1; try discriminate.
    auto.
    simpl in H; injection H; clear H; intro.
    simpl in H0; injection H0; clear H0; intro.
    cut (is_zeros a = true \/ is_zeros a = false).
    intro X; inversion_clear X.
    rewrite (is_zeros_zeros _ H1).
    cut (is_zeros b1 = true \/ is_zeros b1 = false).
    intro X; inversion_clear X.
    rewrite (is_zeros_zeros _ H2).
    rewrite cplt2_weird.
    rewrite cplt2_weird.
    rewrite H; rewrite H0.
    rewrite umul_lst_weird.
    rewrite slst2Z_o.
    rewrite slst2Z_i.
    rewrite ulst2Z_i.
    rewrite zeros_length.
    rewrite ulst2Z_zeros.
    rewrite zeros_length.
    rewrite ulst2Z_zeros.
    rewrite Zpower_is_exp.
    ring.

    rewrite (umul_lst_com (S (S n))).
    rewrite cplt2_prop.
    rewrite umul_lst_leading_o.
    rewrite slst2Z_o.
    rewrite cplt2_weird.

    rewrite (umul_lst_weird' (length (cplt2 b1))); auto.
    rewrite ulst2Z_o.
    rewrite ulst2Z_app_zeros.

    destruct n; try discriminate.
    destruct a; try discriminate.
    destruct b1; try discriminate.
    destruct a; try discriminate.
    destruct b1; try discriminate.
    destruct b; destruct b0; auto.
    discriminate.
    discriminate.

    rewrite (ulst2Z_cplt2' n).
    rewrite slst2Z_i.
    rewrite slst2Z_i.
    rewrite zeros_length.
    rewrite ulst2Z_zeros.
    rewrite H; rewrite H0.
    ring.
    auto.
    intro X; rewrite X in H2; rewrite is_zeros_zeros' in H2; discriminate.
    apply cplt2_nil.
    intro; subst b1; discriminate.
    apply cplt2_nil.
    intro; discriminate.
    intro X; inversion_clear X.
    rewrite H3 in H2; rewrite is_zeros_zeros' in H2; discriminate.
    intro X; inversion_clear X.
    injection H3; intro X; rewrite X in H2; rewrite is_zeros_zeros' in H2; discriminate.
    rew_len.
    rew_len.
    auto.
    rew_len.
    simpl; auto.
    omega.
    case (is_zeros b1); auto.

    rewrite cplt2_prop.
    rewrite umul_lst_leading_o.
    rewrite slst2Z_o.
    cut (is_zeros b1 = true \/ is_zeros b1 = false).
    intro X; inversion_clear X.
    rewrite (is_zeros_zeros _ H2).
    rewrite cplt2_weird.
    rewrite (umul_lst_weird' (S n)).
    rewrite ulst2Z_o.
    rewrite ulst2Z_app_zeros.
    rewrite H0.

    destruct n; try discriminate.
    destruct a; try discriminate.
    destruct b1; try discriminate.
    destruct a; try discriminate.
    destruct b1; try discriminate.
    destruct b; destruct b0; auto.
    discriminate.
    discriminate.

    rewrite (ulst2Z_cplt2' n); auto.
    rewrite slst2Z_i.
    rewrite slst2Z_i.
    rewrite zeros_length.
    rewrite ulst2Z_zeros.
    rewrite H.
    ring.
    intro X; rewrite X in H1; rewrite is_zeros_zeros' in H1; discriminate.
    rew_len; auto.

    rewrite cplt2_prop.

    rewrite umul_lst_leading_o'.
    rewrite ulst2Z_o.
    rewrite (umul_lst_nat n).

    destruct n; try discriminate.
    destruct a; try discriminate.
    destruct b1; try discriminate.
    destruct a; try discriminate.
    destruct b1; try discriminate.
    destruct b; destruct b0; auto.
    discriminate.
    discriminate.
    discriminate.

    rewrite (ulst2Z_cplt2' n); auto.
    rewrite (ulst2Z_cplt2' n); auto.
    rewrite slst2Z_i.
    rewrite slst2Z_i.
    rewrite H0.
    rewrite H.
    ring.
    intro X; rewrite X in H2; rewrite is_zeros_zeros' in H2; discriminate.
    intro X; rewrite X in H1; rewrite is_zeros_zeros' in H1; discriminate.
    rew_len; auto.
    rew_len; auto.
    apply cplt2_nil.
    intro; subst a; discriminate.
    apply cplt2_nil.
    intro; subst b1; discriminate.
    intro X; inversion_clear X.
    rewrite H3 in H2; rewrite is_zeros_zeros' in H2; discriminate.
    intro X; inversion_clear X.
    injection H3; clear H3; intro X; rewrite X in H2; rewrite is_zeros_zeros' in H2; discriminate.
    case (is_zeros b1); auto.
    apply cplt2_nil.
    intro; subst a; discriminate.
    apply cplt2_nil.
    intro; discriminate.
    intro X; inversion_clear X.
    rewrite H2 in H1; rewrite is_zeros_zeros' in H1; discriminate.
    intro X; inversion_clear X.
    injection H2; intro.
    rewrite H3 in H1; rewrite is_zeros_zeros' in H1; discriminate.
    case (is_zeros a); auto.
  Qed.

  (*
   * correctness of comparisons
   *)

  Lemma listbit_lt_correct : forall n a b,
    length a = n ->
    length b = n ->
    listbit_lt a b = true -> [[ a ]]u < [[ b ]]u.
    induction n.
    intros.
    destruct a; try discriminate.
    intros.
    destruct a; try discriminate.
    destruct b; try discriminate.
    simpl in H; injection H; clear H; intros.
    simpl in H0; injection H0; clear H0; intros.
    destruct b0; destruct b.
    simpl.
    apply IHn; auto.
    simpl.
    rewrite H0.
    assert (ulst2Z a < Zpower 2 n).
    apply max_ulst2Z.
    rewrite H.
    constructor.
    generalize (ulst2Z_pos b1); intro.
    omega.
    simpl in H1.
    discriminate.
    simpl.
    rewrite H; rewrite H0.
    simpl in H1.
    generalize (IHn _ _ H H0 H1); omega.
  Qed.

  Lemma listbit_lt_correct' : forall n m a b,
    length a = n ->
    length b = m ->
    forall p, p = max n m ->
      listbit_lt (zero_extend_lst (p-n) a) (zero_extend_lst (p-m) b) = true -> 
      [[ zero_extend_lst (p-n) a ]]u < [[ zero_extend_lst (p-m) b ]]u.
    intros.
    apply listbit_lt_correct with p.
    rewrite (zero_extend_lst_length n).
    apply minus_plus_comm.
    rewrite H1.
    apply le_max_l.
    omega.
    assumption.
    rewrite (zero_extend_lst_length m).
    ring.
    rewrite le_plus_minus_r.
    reflexivity.
    rewrite H1.
    apply le_max_r.
    assumption.
    auto.
  Qed.

Eval compute in ([[ i::i::i::i::nil ]]u).

Eval compute in ([[ i::i::i::i::nil ]]u).

Eval compute in ([[ o::o::o::i::nil ]]s).
Eval compute in (listbit_lt (i::i::i::i::nil) (o::o::o::i::nil)).


Eval compute in ([[ i::o::i::i::nil ]]s).
Eval compute in ([[ adjust_slist (i::o::i::i::nil) 3 ]]s).
Eval compute in ([[ adjust_slist (i::o::i::i::nil) 2 ]]s).


 Close Local Scope Z_scope.