Require Import List.
Require Import Minus.
Require Import Gt.
Require Import Plus.
Require Import util.
Require Import ArithRing.

Module ListBit.

  (* 
   * definition of bits 
   *)

  Inductive bit : Set :=
    o : bit
    | i : bit.
  
  Lemma dec_equ_bit : forall (a b:bit),
    { a = b } + {a <> b}.
    decide equality.
  Qed.
  
  Lemma dec_equ_lst_bit : forall (a b:list bit),
    {a = b} + {a <> b}.
    induction a; destruct b; auto.
    right; intro X; discriminate.
    right; intro X; discriminate.
    generalize (dec_equ_bit a b); intro X; inversion_clear X.
    subst b.
    generalize (IHa b0); intro X; inversion_clear X.
    subst b0.
    auto.
    right.
    intro X; apply H.
    injection X; auto.
    generalize (IHa b0); intro X; inversion_clear X.
    subst b0.
    right.
    intro X; apply H.
    injection X; auto.
    right.
    intro X; apply H.
    injection X; auto.
  Qed.

  Lemma dec_equ_lst_bit' : forall (a b:list bit),
    a = b \/ a <> b.
    intros.
    generalize (dec_equ_lst_bit a b); intro X; inversion_clear X.
    auto.
    auto.
  Qed.

  (*
   * lists of zeros and their properties
   *)

  Fixpoint zeros (cnt:nat) : list bit :=
    match cnt with
      O => nil
      | S cnt' => o :: zeros cnt'
    end.
  
  Definition zeros_length : forall n, length (zeros n) = n.
    induction n; auto.
    simpl; rewrite IHn; auto.
  Defined.
  
  Lemma zeros_zero : forall k lst, 
    zeros k ++ o :: lst = zeros (S k) ++ lst.
    induction k; auto.
    intros.
    simpl.
    rewrite IHk.
    simpl.
    auto.
  Qed.
  
  Lemma zeros_app: forall n m,
    zeros n ++ zeros m = zeros (n + m).
    induction n.
    auto.
    simpl.
    intros.
    rewrite IHn.
    auto.
  Qed.

  Lemma del_heads_zeros : forall n k,
    del_heads (zeros k) n = zeros (k-n).
    induction n.
    simpl.
    intros.
    rewrite <-minus_n_O.
    auto.
    intros.
    destruct k.
    simpl.
    auto.
    simpl.
    rewrite IHn.
    auto.
  Qed.
  
  Lemma rev_zeros : forall k, rev (zeros k) = zeros k.
    induction k; auto.
    simpl.
    rewrite IHk.
    rewrite zeros_zero.
    simpl.
    rewrite <-app_nil_end.
    reflexivity.
  Qed.
  
  (*
   * zero extend
   *)

  Definition zero_extend_lst (m:nat) (l:list bit) : list bit :=
    zeros m ++ l.

  Lemma zero_extend_lst_length : forall n lst,
    length lst = n ->
    forall k,
    length (zero_extend_lst k lst) = k + n.
    intros.
    unfold zero_extend_lst.
    rewrite length_app.
    rewrite zeros_length.
    rewrite H.
    reflexivity.
  Qed.
    
  Lemma zero_extend_lst_i : forall k lst,
    zero_extend_lst k (i :: lst) = zeros k ++ i::lst.
    intros.
    unfold zero_extend_lst.
    reflexivity.
  Qed.

  Lemma rev_zero_extend_lst_i' : forall k lst,
    rev (zero_extend_lst k (i :: lst)) = rev lst ++ i::zeros k.
    induction k; auto.
    simpl.
    intro.
    rewrite distr_rev.
    simpl.
    rewrite rev_zeros.
    simpl.
    rewrite app_ass.
    rewrite zeros_zero.
    simpl.
    rewrite <-app_nil_end.
    rewrite app_ass.
    simpl.
    auto.
  Qed.
  
  Lemma rev_zero_extend_lst_i : forall k,
    rev (zero_extend_lst k (i :: nil)) = i :: zeros k.
    intros.
    rewrite (rev_zero_extend_lst_i' k nil).
    simpl.
    auto.
  Qed.

  Fixpoint erase_leading_zeros (lst:list bit) : list bit :=
    match lst with
      o::tl => erase_leading_zeros tl
      | i::tl => lst
      | nil => nil
    end.
  
  Lemma erase_leading_zeros_extend : forall k lst,
    erase_leading_zeros (zero_extend_lst k lst) = erase_leading_zeros lst.
    induction k.
    induction lst.
    simpl.
    auto.
    simpl.
    destruct a.
    auto.
    auto.
    induction lst.
    simpl.
    generalize (IHk nil).
    simpl.
    unfold zero_extend_lst.
    auto.
    simpl.
    destruct a.
    rewrite zeros_zero.
    rewrite <-IHlst.
    unfold zero_extend_lst.
    auto.
    generalize (IHk (i::lst)).
    intros.
    simpl in H.
    unfold zero_extend_lst in H.
    auto.
  Qed.

  Lemma erase_leading_zeros_zeros : forall k,
    erase_leading_zeros (zeros k) = nil.
    induction k; auto.
  Qed.

  Fixpoint is_zeros (a:list bit) {struct a} : bool :=
    match a with
      nil => true
      | o::tl => is_zeros tl
      | i::_ => false
    end.
  
  Lemma is_zeros_zeros : forall b,
    is_zeros b = true -> 
    b = zeros (length b).
    induction b; auto.
    destruct a; intros.
    simpl.
    rewrite IHb.
    rewrite zeros_length.
    auto.
    auto.
    discriminate H.
  Qed.

  Lemma is_zeros_zeros' : forall k,
    is_zeros (zeros k) = true.
    induction k; auto.
  Qed.
  
  (*
   * shift-left and extend 
   *)

  Definition shl_extend_lst (m:nat) (l:list bit) :=
    l ++ zeros m.

  Lemma shl_extend_length: forall n lst,
    length lst = n ->
    forall m, 
    length (shl_extend_lst m lst) = m + n.
    intros.
    unfold shl_extend_lst.
    rewrite length_app.
    rewrite zeros_length.
    rewrite H.
    apply plus_comm.
  Qed.

  (*
   * lists of ones and their properties
   *)

  Fixpoint ones (cnt:nat) : list bit :=
    match cnt with
      O => nil
      | S cnt' => i :: ones cnt'
    end.

  Definition ones_length : forall n, length (ones n) = n.
    induction n; auto.
    simpl; rewrite IHn; auto.
  Defined.
  
  Lemma ones_one : forall k lst, ones k ++ i :: lst = ones (S k) ++ lst.
    induction k; auto.
    intros.
    simpl.
    rewrite IHk.
    simpl.
    auto.
  Qed.

  Lemma rev_ones : forall k,
    rev (ones k) = ones k.
    induction k; auto.
    simpl.
    rewrite IHk.
    rewrite ones_one.
    simpl.
    rewrite <-app_nil_end.
    reflexivity.
  Qed.

  Definition one_extend_n_lst (lst:list bit) (counter:nat) : (list bit) :=
    ones counter ++ lst.
  
  Lemma one_extend_n_lst_i : forall k lst, one_extend_n_lst (i :: lst) k = 
    ones k ++ i::lst.
    auto.
  Qed.

  (*
   * sign-extension for signed list bits
   *)

  Fixpoint sign_extend_lst (m: nat) (l:list bit) {struct m} : list bit :=
    match l with
      nil => zeros m
      | hd::tl => match m with 
                  0 => l
                    | S m' => hd :: sign_extend_lst m' l
                  end
    end.

  Lemma sign_extend_length: forall m n l,
    length l = n ->
    length (sign_extend_lst m l) = n + m.
    induction m.
    simpl.
    destruct l; simpl; intros; subst n; auto.
    simpl.
    destruct l.
    simpl; intros; subst n.
    rewrite zeros_length; auto.
    simpl; intros.
    rewrite (IHm n); auto.
  Qed.
  
  Lemma sign_extend_lst_length: forall m l,
    length (sign_extend_lst m l) = length l + m.
    intros.
    apply sign_extend_length; auto.
  Qed.
  
  Lemma sign_extend_0_lst: forall n l,
    sign_extend_lst n (o::l) = zeros (S n) ++ l.
    induction n.
    auto.
    simpl.
    intros; rewrite IHn; auto.
  Qed.

  (* (zero/sign)-extend or shrink a given list ("adjust" it to some size) *)

  Definition adjust_ulist (lst:list bit) (n:nat) : list bit :=
    if nat_lt (length lst) n then
      zero_extend_lst (n - length lst) lst 
      else
	del_heads lst (length lst - n).
  
  Lemma adjust_ulist_length: forall n lst,
    length (adjust_ulist lst n) = n.
    unfold adjust_ulist.
    intros.
    generalize (nat_lt_classic (length lst) n); intro X; inversion_clear X.
    generalize (nat_lt_true _ _ H); intros.
    rewrite H.
    rewrite (zero_extend_lst_length (length lst)); try reflexivity.
    omega.
    generalize (nat_lt_false _ _ H); intros.
    rewrite H.
    rewrite del_heads_length.
    omega.
  Qed.
  
  Lemma adjust_ulist_nil: forall n,
    adjust_ulist nil n = zeros n.
    induction n.
    trivial.
    simpl.
    unfold adjust_ulist.
    assert (length (@nil bit) < S n).
    simpl; omega.
    rewrite (nat_lt_true' _ _ H).
    simpl.
    unfold zero_extend_lst.
    simpl.
    rewrite <-app_nil_end.
    auto.
  Qed.

  Lemma adjust_ulist_nil': forall lst,
    adjust_ulist lst 0 = nil.
    destruct lst.
    auto.
    unfold adjust_ulist.
    simpl.
    assert (length (del_heads lst (length lst)) = 0).
    rewrite del_heads_length.
    omega.
    destruct (del_heads lst (length lst)); try discriminate||auto.
  Qed.

  Lemma adjust_ulist_id : forall n lst,
    length lst = n ->
    adjust_ulist lst n = lst.
    induction n.
    intro; destruct lst; intro; try discriminate.
    apply adjust_ulist_nil'.
    intros.
    lapply (list_last _ lst); try omega.
    intro X; inversion_clear X.
    inversion_clear H0.
    unfold adjust_ulist.
    rewrite H.
    rewrite nat_lt_irrefl.
    cutrewrite (S n - S n =0).
    auto.
    omega.
  Qed.
  
  Lemma adjust_ulist_S : forall n hds tl l,
    length (hds ++ tl::nil) = l ->
    l >= S n ->
    adjust_ulist (hds ++ tl::nil) (S n) = adjust_ulist hds n ++ (tl::nil).
    induction n.
    
    intros.
    rewrite adjust_ulist_nil'.
    simpl.
    unfold adjust_ulist.
    rewrite nat_lt_false'.
    rewrite del_heads_app.
    auto.
    rewrite length_app.
    simpl.
    omega.
    rewrite length_app.
    simpl.
    omega.
    
    intros.
    destruct hds.
    simpl in H.
    subst l.
    inversion H0.
    inversion H1.
    simpl.
    unfold adjust_ulist.
    simpl.
    rewrite nat_lt_false'.
    rewrite nat_lt_false'.
    rewrite length_app.
    simpl.
    assert ( length hds + 1 - S n = length hds - n).
    omega.
    rewrite H1; clear H1.
    cutrewrite ( b :: hds ++ tl :: nil = (b :: hds) ++ tl :: nil ).
    rewrite (del_heads_app' (length (b::hds))).
    auto.
    auto.
    simpl; omega.
    auto.
    simpl in H.
    rewrite length_app in H.
    simpl in H.
    omega.
    simpl in H.
    rewrite length_app in H.
    simpl in H.
    rewrite length_app.
    simpl.
    omega.
  Qed.
  
  Lemma adjust_ulist_S' : forall n lst l,
    length lst = l ->
    l < n ->
    adjust_ulist lst n = zeros (n - l) ++ lst.
    destruct n.
    simpl.
    destruct l.
    intros.
    destruct lst; try discriminate.
    simpl.
    unfold adjust_ulist.
    simpl.
    unfold zero_extend_lst.
    simpl.
    auto.
    intros.
    inversion H0.
    intros.
    destruct lst.
    destruct l.
    simpl.
    unfold adjust_ulist.
    simpl.
    unfold zero_extend_lst.
    simpl.
    auto.
    discriminate.
    unfold adjust_ulist.
    rewrite nat_lt_true'.
    unfold zero_extend_lst.
    rewrite H.
    auto.
    omega.
  Qed.
  
  Lemma adjust_ulist_S'' : forall n l lst,
    length lst = l ->
    l <= n ->
    adjust_ulist lst n = zeros (n - l) ++ lst.
    intros.
    cut (l=n \/ l<n).
    intro X; inversion_clear X.
    subst n.
    rewrite <-minus_n_n.
    simpl.
    apply adjust_ulist_id; auto.
    apply adjust_ulist_S'; auto.
    omega.
  Qed.
  
  Definition adjust_slist (lst:list bit) (n:nat) : list bit :=
    if nat_lt (length lst) n then
      sign_extend_lst (n - length lst) lst 
      else
	del_heads lst (length lst - n).
  
  Lemma adjust_slist_length : forall n lst,
    length (adjust_slist lst n) = n.
    unfold adjust_slist.
    intros.
    generalize (nat_lt_classic (length lst) n); intro X; inversion_clear X.
    generalize (nat_lt_true _ _ H); intros.
    rewrite H.
    rewrite sign_extend_lst_length.
    omega.
    generalize (nat_lt_false _ _ H); intros.
    rewrite H.
    rewrite del_heads_length.
    omega.
  Qed.

  Lemma adjust_slist_nil : forall n,
    adjust_slist nil n = zeros n.
    induction n; auto.
  Qed.

  (*
   * 1cplt representation and its properties 
   *)

  Definition cplt b :=
    match b with 
      i => o
      | o => i
    end.
  
  Lemma cplt_involutive : forall b, cplt (cplt b) = b.
    destruct b; auto.
  Qed.

  Fixpoint cplt1 (lst:list bit) {struct lst} : list bit := 
    match lst with
      nil => nil
      | hd::tl => cplt hd :: cplt1 tl
    end.

  Lemma cplt1_length : forall a,
    length (cplt1 a) = length a.
    induction a; auto.
    simpl.
    rewrite IHa.
    reflexivity.
  Qed.

  Lemma cplt1_length' : forall n a,
    length a = n ->
    length (cplt1 a) = n.
    intros; rewrite cplt1_length; auto.
  Qed.
  
  Lemma cplt1_app : forall a b, 
    cplt1 (a ++ b) = cplt1 a ++ cplt1 b.
    induction a; auto.
    intros.
    simpl.
    rewrite IHa.
    reflexivity.
  Qed.
  
  Lemma cplt1_zeros : forall k,
    cplt1 (zeros k) = ones k.
    induction k; auto.
    simpl.
    rewrite IHk; reflexivity.
  Qed.
  
  Lemma cplt1_involutive : forall lst,
    cplt1 (cplt1 lst) = lst.
    induction lst; auto.
    simpl.
    rewrite cplt_involutive.
    rewrite IHlst.
    reflexivity.
  Qed.
  
  (*
   * shift left 
   *)
 
  Fixpoint shl_lst  (m: nat) (i: list bit) {struct m} : list bit :=
    match m with
      0 => i
      | S m' => match i with
                  nil => nil
                  | hd::tl => shl_lst m' tl ++ o::nil
                end
    end.

  Lemma shl_length: forall m n i,
    length i = n ->
    length (shl_lst m i) = n.
    induction m.
    auto.
    intros.
    destruct i0.
    auto.
    simpl.
    rewrite length_app.
    simpl.
    destruct n; try discriminate.
    rewrite (IHm n).
    omega.
    simpl in H; omega.
  Qed.

  Lemma shl_lst_zeros_app: forall n l,
    shl_lst n (zeros n ++ l) = l ++ zeros n.
    induction n.
    simpl.
    intuition.
    simpl.
    intros.
    rewrite IHn.
    rewrite <- ass_app.
    rewrite zeros_zero.
    simpl.
    rewrite <-app_nil_end.
    auto.
  Qed.

  Lemma shl_lst_zeros : forall n l lst, 
    length lst = l ->
    n >= l ->
    shl_lst n lst = zeros l.
    induction n; intros.
    destruct l.
    destruct lst; try discriminate.
    auto.
    inversion H0.
    intros.
    destruct l.
    destruct lst; try discriminate.
    auto.
    destruct lst; try discriminate.
    simpl in H; injection H; clear H; intros.
    simpl.
    rewrite (IHn l); auto.
    rewrite zeros_zero.
    rewrite <-app_nil_end.
    auto.
    omega.
  Qed.

  (*
   * shift right
   *)

  (* logical shift (fill the freed bits with 0) *)
  Fixpoint shrl_lst  (m: nat) (i: list bit) {struct m}: list bit :=
    match length i with
      0 => nil
      | S n =>
	match m with
	  0 => i
	  | S m' => o :: shrl_lst m' (del_nth_last i)
	end
    end.

  Lemma shrl_length: forall n m i,
    length i = n ->
    length (shrl_lst m i) = n.
    induction n.
    intros.
    destruct i0; try discriminate.
    destruct m; auto.
    intros.
    lapply (list_last _ i0); intros; try omega.
    inversion_clear H0.
    inversion_clear H1.
    subst i0.
    destruct m; auto.
    simpl.
    rewrite length_app.
    simpl.
    cutrewrite (length x + 1 = S (length x)); auto.
    omega.
    rewrite length_app in H; simpl in H.
    simpl.
    rewrite length_app.
    simpl.
    cutrewrite (length x + 1 = S (length x)); try omega.
    rewrite del_nth_last_exact; try omega.
    simpl.
    rewrite IHn; try omega.
  Qed.

  (* arithmetic shift (fill the freed bits with the bit-sign *)
  Fixpoint shra_lst  (m:nat) (i:list bit) {struct m}: list bit :=
    match length i with
      0 => nil
      | S n =>
	match m with
	  0 => i
	  | S m' => match i with
                      nil => nil
                      | hd::tl => hd :: shra_lst m' (del_nth_last i)
                    end
	end
    end.

  Lemma shra_lst_nil: forall m,
    shra_lst m nil = nil.
    induction m.
    trivial.
    trivial.
  Qed.
  
  Lemma shra_length: forall n m i,
    length i = n ->
    length (shra_lst m i) = n.
    induction n.
    intros.
    destruct i0; try discriminate.
    destruct m; auto.
    intros.
    lapply (list_last _ i0); intros; try omega.
    inversion_clear H0.
    inversion_clear H1.
    subst i0.
    destruct m; auto.
    simpl.
    rewrite length_app.
    simpl.
    cutrewrite (length x + 1 = S (length x)); auto.
    omega.
    rewrite length_app in H; simpl in H.
    simpl.
    repeat rewrite length_app.
    cutrewrite (length x + length (x0::nil) = S (length x)); try omega.
    destruct x.
    simpl.
    rewrite IHn; auto.
    simpl.
    rewrite IHn; auto.
    cutrewrite (length (x ++ x0 :: nil) - 0 = S (length x) ).
    simpl.
    rewrite del_nth_length.
    simpl in H.
    rewrite length_app.
    simpl.
    omega.
    simpl in H.
    rewrite length_app.
    simpl.
    omega.
    simpl in H.
    rewrite length_app.
    simpl.
    omega.
    simpl.
    omega.
  Qed.

  (*
   * shift right and forget about the freed bits
   *)

  Fixpoint shr_shrink_lst (m: nat) (i: list bit) {struct m} : list bit :=
    match m with
      0 => i
      | S m' => shr_shrink_lst m' (del_nth_last i)
    end.
  
  Lemma shr_shrink_length: forall n m i,
    length i = n ->
    length (shr_shrink_lst m i) = n - m.
    induction n.
    intros.
    destruct i0; try discriminate.
    induction m; auto.
    
    intros.
    lapply (list_last _ i0); intros; try omega.
    inversion_clear H0.
    inversion_clear H1.
    subst i0.
    destruct m; auto.
    simpl.
    rewrite length_app in H; simpl in H.
    rewrite del_nth_last_exact; try omega.
    apply IHn; omega.
  Qed.
  
  Lemma shr_shrink_lst_nil : forall n,
    shr_shrink_lst n nil = nil.
    induction n; auto.
  Qed.
  
  Lemma shr_shrink_S : forall k hd tl,
    shr_shrink_lst (S k) (tl++hd::nil) = shr_shrink_lst k tl.
    intros.
    simpl.
    rewrite del_nth_last_exact.
    auto.
  Qed.

  Lemma shr_shrink_lst_prop' : forall n lst,
    length lst <= n ->
    shr_shrink_lst n lst = nil.
    induction n.
    intros.
    destruct lst.
    auto.
    simpl in H.
    inversion H.
    intros.
    inversion H.
    rewrite H1.
    simpl.
    lapply (list_last _ lst).
    intro X; inversion_clear X.
    inversion_clear H0.
    rewrite H2.
    rewrite del_nth_last_exact.
    rewrite IHn.
    auto.
    rewrite H2 in H1.
    rewrite length_app in H1.
    simpl in H1.
    omega.
    omega.
    clear H0 m.
    simpl.
    rewrite IHn.
    auto.
    rewrite (del_nth_last_length (length lst)).
    omega.
    auto.
  Qed.
  
  Lemma shr_shrink_lst_prop : forall l lst n,
    length lst = l ->
    l >= n ->
    (shr_shrink_lst n lst) ++ (adjust_ulist lst n) = lst.
    induction l.
    intros.
    destruct lst; try discriminate.
    destruct n.
    auto.
    inversion H0.
    intros.
    lapply (list_last _ lst); try omega.
    intro X; inversion_clear X.
    inversion_clear H1.
    assert (length x = l).
    assert (length lst = length (x++x0::nil)).
    rewrite H2; auto.
    rewrite length_app in H1.
    simpl in H1.
    omega.
    inversion H0.
    subst n.
    clear H0.
    rewrite adjust_ulist_id.
    rewrite shr_shrink_lst_prop'.
    auto.
    omega.
    auto.
    clear H3 m.
    rewrite H2.
    destruct n.
    simpl.
    rewrite adjust_ulist_nil'.
    rewrite <-app_nil_end.
    auto.
    simpl.
    rewrite del_nth_last_exact.
    rewrite (adjust_ulist_S n x x0 (S l)).
    rewrite <-app_ass.
    rewrite IHl.
    auto.
    auto.
    omega.
    rewrite length_app.
    simpl.
    omega.
    omega.
  Qed.

  (*
   * bitwise-and
   *)

  Definition bit_and (a b : bit) : bit :=
    match (a, b) with
      (i, i) => i
      | (_, _) => o
    end.
  
  Fixpoint and_lst (a b : list bit) {struct a} : list bit :=
    match (a, b) with
      (hd::tl, hd'::tl') => bit_and hd hd' :: and_lst tl tl'
      | (_, _) => nil
    end.
  
  Lemma and_lst_length: forall n i j, 
    length i = n ->
    length j = n ->
    length (and_lst i j) = n.
    induction n.
    intros.
    destruct i0; try discriminate.
    destruct j; try discriminate.
    auto.
    intros.
    destruct i0; try discriminate.
    destruct j; try discriminate.
    simpl.
    simpl in H; simpl in H0.
    rewrite IHn; auto.
  Qed.


  (*
   * bitwise-and
   *)

  Definition bit_or (a b : bit) : bit :=
    match (a, b) with
      (i, _) => i
      | (_,i) => i
      | (_, _) => o
    end.
  
  Fixpoint or_lst (a b : list bit) {struct a} : list bit :=
    match (a, b) with
      (hd::tl, hd'::tl') => bit_or hd hd' :: or_lst tl tl'
      | (_, _) => nil
    end.
  
  Lemma or_lst_length: forall n i j, 
    length i = n ->
    length j = n ->
    length (or_lst i j) = n.
    induction n.
    intros.
    destruct i0; try discriminate.
    destruct j; try discriminate.
    auto.
    intros.
    destruct i0; try discriminate.
    destruct j; try discriminate.
    simpl.
    simpl in H; simpl in H0.
    rewrite IHn; auto.
  Qed.

  Lemma or_lst_zeros: forall n l,
    length l = n ->
    or_lst l (zeros n) = l.
    induction n.
    intros.
    simpl.
    destruct l; try discriminate.
    auto.
    intros.
    destruct l; try discriminate.
    simpl in H.
    simpl.
    rewrite IHn.
    destruct b; auto.
    omega.
  Qed.

  (* 
   * addition of listbits
   *)

  (* add two lists, propagating carry, ignoring last carry *)
  Fixpoint add_lst' (a b:list bit) (carry:bit) {struct a} : list bit :=
    match (a, b) with
      (o :: tla, o :: tlb) => 
      carry :: add_lst' tla tlb o
      | (i :: tla, i :: tlb) => 
	carry :: add_lst' tla tlb i
      | (_ :: tla, _ :: tlb) => 
	match carry with
	  o => i :: add_lst' tla tlb o
	  | i => o :: add_lst' tla tlb i
	end
      | _ => nil
    end.

  Lemma add_lst'_length : forall (a b:list bit), length a = length b -> 
    forall carry, length (add_lst' a b carry) = length a.
    induction a; auto.
    intros.
    destruct b; try discriminate.
    simpl in H; injection H; clear H; intro.
    destruct a; destruct b; destruct carry; simpl;
    rewrite IHa; auto.
  Qed.

  Lemma add_lst'_neutral : forall lst list_of_zeros,
    list_of_zeros = zeros (length lst) ->
    add_lst' lst list_of_zeros o = lst.
    induction lst; auto.
    intros.
    rewrite H.
    simpl.
    rewrite IHlst; auto.
    destruct a; auto.
  Qed.
  
  (* commutativity *)
  Lemma add_lst'_com : forall a b,
    add_lst' a b o = add_lst' b a o /\ add_lst' a b i = add_lst' b a i.
    induction a; induction b; auto.
    destruct a; auto.
    destruct a; auto.
    destruct a; destruct a1; auto.
    simpl.
    rewrite (proj1 (IHa b)).
    auto.
    simpl.
    rewrite (proj1 (IHa b)).
    rewrite (proj2 (IHa b)).
    auto.
    simpl.
    rewrite (proj1 (IHa b)).
    rewrite (proj2 (IHa b)).
    auto.
    simpl.
    rewrite (proj2 (IHa b)).
    auto.
  Qed.

  Definition add_lst (a b:list bit) (carry:bit) : list bit :=
    rev (add_lst' (rev a) (rev b) carry).
  
  Lemma add_lst_length : forall n (a b:list bit), 
    length a = n -> 
    length b = n -> 
    forall carry, length (add_lst a b carry) = n.
    intros.
    unfold add_lst.
    rewrite length_rev.
    rewrite add_lst'_length.
    rewrite length_rev.
    assumption.
    do 2 rewrite length_rev.
    rewrite H0.
    exact H.
  Qed.

  Lemma add_lst_com : forall a b carry,
    add_lst a b carry = add_lst b a carry.
    unfold add_lst.
    intros.
    generalize (add_lst'_com (rev a) (rev b)); intro.
    inversion_clear H.
    destruct carry.
    rewrite H0; auto.
    rewrite H1; auto.
  Qed.

  Lemma add_lst_neutral : forall lst list_of_zeros,
    list_of_zeros = zeros (length lst) ->
    add_lst lst list_of_zeros o = lst.
    intros.
    unfold add_lst.
    rewrite H.
    rewrite rev_zeros.
    rewrite <-H.
    rewrite (add_lst'_neutral (rev lst)).
    apply rev_involutive.
    rewrite length_rev.
    assumption.
  Qed.
  
  Lemma carry_add : forall lst k list_of_zeros, 
    S k = length lst ->
    list_of_zeros = zeros (length lst) ->
    add_lst lst list_of_zeros i = 
    add_lst lst (zero_extend_lst k (i::nil)) o.
    intros.
    unfold add_lst.
    cutrewrite (rev (zero_extend_lst k (i :: nil)) = i :: zeros k).
    cutrewrite (rev list_of_zeros = o :: zeros k).
    assert (exists hd, exists tl, lst = hd++tl::nil).
    apply list_last.
    omega.
    inversion_clear H1 as [hd].
    inversion_clear H2 as [tl].
    rewrite H1; clear H1.
    rewrite distr_rev.
    simpl.
    auto.
    rewrite H0.
    rewrite rev_zeros.
    rewrite <-H.
    reflexivity.
    rewrite rev_zero_extend_lst_i.
    reflexivity.
  Qed.

  Lemma carry_add' : forall lst k list_of_zeros, 
    S k = length lst ->
    list_of_zeros = zeros (length lst) ->
    rev (add_lst' lst list_of_zeros i) = 
    rev (add_lst' lst (rev (zero_extend_lst k (i::nil))) o).
    intros.
    generalize (carry_add (rev lst) k (rev list_of_zeros)); intro.
    unfold add_lst in H1.
    repeat rewrite rev_involutive in H1.
    apply H1.
    rewrite length_rev.
    assumption.
    rewrite length_rev.
    rewrite H0.
    rewrite rev_zeros.
    reflexivity.
  Qed.
  
  Lemma add_lst'_no_overflow : forall n l1 l2 carry,
    length l1 = S n ->
    length l2 = S n ->
    add_lst' (l1 ++ o::o::nil) (l2 ++ o::o::nil) carry = 
    (add_lst' (l1 ++ o::nil) (l2 ++ o::nil) carry) ++ o::nil.
    induction n.
    intros.
    destruct l1; try discriminate.
    destruct l2; try discriminate.
    simpl in H; simpl in H0; injection H; injection H0; clear H H0; intros.
    destruct l2; try discriminate.
    destruct l1; try discriminate.
    simpl.
    destruct b; destruct b0; destruct carry; auto.
    intros.
    destruct l1; try discriminate.
    destruct l2; try discriminate.
    simpl in H; simpl in H0; injection H; injection H0; clear H H0; intros.
    destruct b; destruct b0; destruct carry; simpl; rewrite IHn; auto.
  Qed.

  Lemma add_lst_no_overflow : forall n l1 l2,
    length l1 = n ->
    length l2 = n ->
    add_lst (o::o::l1) (o::o::l2) o = o :: add_lst (o::l1) (o::l2) o.
    intros.
    unfold add_lst.
    cutrewrite (rev (o :: o :: l1) = rev l1 ++ (o::o::nil)).
    cutrewrite (rev (o :: o :: l2) = rev l2 ++ (o::o::nil)).
    simpl.
    destruct n.
    destruct l1; try discriminate.
    destruct l2; try discriminate.
    auto.
    rewrite (add_lst'_no_overflow n).
    rewrite distr_rev; auto.
    rewrite length_rev ;auto.
    rewrite length_rev; auto.
    simpl.
    rewrite app_ass; reflexivity.
    simpl.
    rewrite app_ass; reflexivity.
  Qed.

  Lemma add_lst'_leading_bit : forall n l1 l2 carry,
    length l1 = n ->
    length l2 = n ->
    add_lst' (l1 ++ i::o::nil) (l2 ++ o::o:: nil) carry =
    add_lst' (l1 ++ o::o::nil) (l2 ++ i::o::nil) carry.
    induction n.
    intros.
    destruct l1; try discriminate.
    destruct l2; try discriminate.
    auto.
    intros.
    destruct l1.
    discriminate H.
    destruct l2.
    discriminate H0.
    simpl.
    destruct b; destruct b0; destruct carry; rewrite IHn; intuition.
  Qed.
  
  Lemma add_lst_leading_bit : forall n l1 l2 carry,
    length l1 = n ->
    length l2 = n ->
    add_lst (o::i::l1) (o::o::l2) carry = 
    add_lst (o::o::l1) (o::i::l2) carry.
    intros.
    unfold add_lst.
    simpl.
    repeat rewrite app_ass.
    simpl.
    rewrite (add_lst'_leading_bit n).
    auto.
    rewrite length_rev; auto.
    rewrite length_rev; auto.
  Qed.

  Ltac List2hdtl l :=
    assert (A1: length l > 0); [ omega |
      generalize (list_last _ l A1); intro; clear A1].
  
  Lemma add_carry_xchg: forall n l1 l2 l3 c1 c2,
    length l1 = n ->
    length l2 = n ->
    length l3 = n ->
    add_lst (add_lst l1 l2 c1) l3 c2 =  add_lst (add_lst l1 l2 c2) l3 c1.
    induction n.
    intros.
    destruct l1; try discriminate.
    destruct l2; try discriminate.
    destruct l3; try discriminate.
    intuition.
    intros.
    List2hdtl l1.
    inversion_clear H2 as [hd1].
    inversion_clear H3 as [tl1].
    subst l1.
    List2hdtl l2.
    inversion_clear H2 as [hd2].
    inversion_clear H3 as [tl2].
    subst l2.
    List2hdtl l3.
    inversion_clear H2 as [hd3].
    inversion_clear H3 as [tl3].
    subst l3.
    simpl.

    unfold add_lst in IHn.
    unfold add_lst.
    
    rewrite length_app in H; simpl in H.
    rewrite length_app in H0; simpl in H0.
    rewrite length_app in H1; simpl in H1.
    
    destruct c1.
    destruct c2.
    
    auto.
    
    destruct tl1.
    destruct tl2.
    destruct tl3.
    
    simpl.
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    auto.
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    auto.
    
    destruct tl3.
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    rewrite IHn; [auto | omega | omega | omega].
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    rewrite IHn; [auto | omega | omega | omega].
    
    destruct tl2.
    destruct tl3.
    
    simpl.
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    rewrite IHn; [auto | omega | omega | omega].
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    rewrite IHn; [auto | omega | omega | omega].
    
    destruct tl3.
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    rewrite IHn; [auto | omega | omega | omega].
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    auto.
    
    destruct c2.
    
    auto.
    
    destruct tl1.
    destruct tl2.
    destruct tl3.
    
    simpl.
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    auto.
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    auto.
    
    destruct tl3.
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    rewrite IHn; [auto | omega | omega | omega].
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    rewrite IHn; [auto | omega | omega | omega].
    
    destruct tl2.
    destruct tl3.
    
    simpl.
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    rewrite IHn; [auto | omega | omega | omega].
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    rewrite IHn; [auto | omega | omega | omega].
    
    destruct tl3.
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    rewrite IHn; [auto | omega | omega | omega].
    
    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    simpl.
    auto.
    
    auto.
  Qed.
  
  Lemma rev_unit'': forall (A:Set) (l:list A) a, rev (a::l) = (rev l) ++ a :: nil.
    auto.
  Qed.
  
  (* associativity *)
  Lemma add_lst_assoc: forall n l1 l2 l3 c1 c2,
    length l1 = n ->
    length l2 = n ->
    length l3 = n ->
    add_lst (add_lst l1 l2 c1) l3 c2 =  add_lst l1 (add_lst l2 l3 c1) c2.
    unfold add_lst.
    induction n.
    intros.
    destruct l1; try discriminate.
    destruct l2; try discriminate.
    destruct l3; try discriminate.
    intuition.
    intros.
    List2hdtl l1.
    inversion_clear H2 as [hd1].
    inversion_clear H3 as [tl1].
    subst l1.
    List2hdtl l2.
    inversion_clear H2 as [hd2].
    inversion_clear H3 as [tl2].
    subst l2.
    List2hdtl l3.
    inversion_clear H2 as [hd3].
    inversion_clear H3 as [tl3].
    subst l3.
    simpl.

    rewrite length_app in H; simpl in H.
    rewrite length_app in H0; simpl in H0.
    rewrite length_app in H1; simpl in H1.

    destruct c1.
    destruct c2.

    destruct tl1.
    destruct tl2.
    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    generalize (add_carry_xchg); intro A; unfold add_lst in A.
    rewrite (A n); [auto | omega | omega | omega].

    destruct tl2.
    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.
    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    generalize (add_carry_xchg); intro A; unfold add_lst in A.
    rewrite (A n); [auto | omega | omega | omega].


    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    destruct tl1.
    destruct tl2.
    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    generalize (add_carry_xchg); intro A; unfold add_lst in A.
    rewrite (A n); [auto | omega | omega | omega].

    destruct tl2.
    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    generalize (add_carry_xchg); intro A; unfold add_lst in A.
    rewrite (A n); [auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    destruct c2.

    destruct tl1.
    destruct tl2.
    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    generalize (add_carry_xchg); intro A; unfold add_lst in A.
    rewrite (A n); [auto | omega | omega | omega].

    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    destruct tl2.
    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    generalize (add_carry_xchg); intro A; unfold add_lst in A.
    rewrite (A n); [auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    destruct tl1.
    destruct tl2.
    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    generalize (add_carry_xchg); intro A; unfold add_lst in A.
    rewrite (A n); [auto | omega | omega | omega].

    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) o)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    destruct tl2.
    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) o))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    generalize (add_carry_xchg); intro A; unfold add_lst in A.
    rewrite (A n); [auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    destruct tl3.

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (o :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].

    repeat rewrite rev_unit.
    simpl.
    repeat rewrite rev_unit.

    pattern (rev
      (i :: add_lst' (rev hd1) (rev (rev (add_lst' (rev hd2) (rev hd3) i))) i)).
    rewrite rev_unit''.
    rewrite <- IHn; [simpl; auto | omega | omega | omega].
  Qed.

  Lemma add_zero_queue: forall m n l1 l2 ,
    length l1 = n ->
    length l2 = n ->
    add_lst l1 l2 o ++ zeros m = add_lst (l1 ++ zeros m) (l2 ++ zeros m) o.
    induction m.
    simpl; intros.
    repeat rewrite <- app_nil_end.
    auto.
    cutrewrite ( zeros (S m) = zeros m ++ o::nil).
    unfold add_lst.
    intros.
    repeat rewrite distr_rev.
    simpl.
    unfold add_lst in IHm.
    repeat rewrite <- distr_rev.
    rewrite <- (IHm n); auto.
    rewrite app_ass.
    auto.
    rewrite zeros_zero.
    rewrite <-app_nil_end; auto.
  Qed.
  
  Lemma isolated_i_helper: forall l m top,
    length l = m ->
    top::l = add_lst' (top::zeros m) (o::l) o.
    induction l.
    intros.
    destruct top; auto.
    rewrite add_lst'_neutral.
    destruct m; auto.
    discriminate H.
    destruct m; auto.
    discriminate H.
    rewrite add_lst'_neutral.
    destruct m; auto.
    discriminate H.
    destruct m; auto.
    discriminate H.
    intros.
    destruct top; simpl.
    rewrite (proj1 (add_lst'_com (zeros m) (a :: l))).
    rewrite add_lst'_neutral.
    auto.
    rewrite H; auto.
    rewrite (proj1 (add_lst'_com (zeros m) (a :: l))).
    rewrite add_lst'_neutral.
    auto.
    rewrite H; auto.
  Qed.
  
  Lemma isolated_i_helper2: forall k n m l top,
    length k = n ->
    length l = m ->
    k ++ top::l = add_lst' (zeros n ++ top::zeros m) (k ++ o::l) o.
    induction k.
    intros.
    simpl.
    rewrite (isolated_i_helper l m top); auto.
    destruct n.
    auto.
    discriminate H.
    intros.
    simpl.
    destruct n.
    discriminate H.
    simpl.
    rewrite (IHk n m l top); auto.
    destruct a; auto.
  Qed.

  Lemma isolated_i_add_lst': forall l1 l2,
    l1 ++ i::l2 = add_lst' (zeros (length l1) ++ i::zeros (length l2)) (l1 ++ o::l2) o.
    intros.
    rewrite (isolated_i_helper2 l1 (length l1) (length l2) l2); auto.
  Qed.
  
  Lemma isolated_i_add_lst: forall l1 l2,
    l1 ++ i::l2 = add_lst (zeros (length l1) ++i::zeros (length l2)) (l1 ++ o::l2) o.
    intros.
    unfold add_lst.
    do 2 rewrite distr_rev.
    simpl.
    do 2 rewrite rev_zeros.
    generalize (isolated_i_add_lst' (rev l2) (rev l1)); intro.
    do 2 rewrite length_rev in H.
    do 2 rewrite app_ass.
    simpl.
    rewrite <-H.
    rewrite distr_rev.
    simpl.
    do 2 rewrite rev_involutive.
    rewrite app_ass.
    auto.
  Qed.
  
  Lemma add_lst'_app : forall n lst l lst',
    length lst = n ->
    length lst' = l ->
    add_lst' (lst ++ zeros l) (zeros n ++ lst') o = lst ++ lst'.
    induction n.
    intros.
    destruct lst; try discriminate.
    simpl.
    rewrite (proj1 (add_lst'_com (zeros l) lst')).
    rewrite add_lst'_neutral.
    auto.
    rewrite H0; auto.
    intros.
    simpl.
    destruct lst; try discriminate.
    simpl in H; injection H; clear H; intro.
    destruct b.
    simpl.
    rewrite IHn; auto.
    simpl.
    rewrite IHn; auto.
  Qed.
  
  Lemma add_lst_app : forall n lst l lst',
    length lst = l ->
    length lst' = n ->
    add_lst (zeros l ++ lst') (lst ++ zeros n) o = lst ++ lst'.
    intros.
    unfold add_lst.
    do 2 rewrite distr_rev.
    do 2 rewrite rev_zeros.
    rewrite add_lst'_app.
    rewrite distr_rev.
    do 2 rewrite rev_involutive; auto.
    rewrite length_rev; auto.
    rewrite length_rev; auto.
  Qed.

  (*
   * subtraction
   *)

  Fixpoint sub_lst' (a b:list bit) (borrow:bit) {struct a} : list bit := 
    match (a, b) with
      (o :: tla, o :: tlb) => 
      match borrow with
	o => o :: sub_lst' tla tlb o
	| i => i :: sub_lst' tla tlb i
      end
      | (i :: tla, o :: tlb) =>
	match borrow with
	  o => i :: sub_lst' tla tlb o
	  | i => o :: sub_lst' tla tlb o
	end
      | (i :: tla, i :: tlb) =>
	match borrow with
	  o => o :: sub_lst' tla tlb o
	  | i => i :: sub_lst' tla tlb i
	end
      | (o :: tla, i :: tlb) =>
	match borrow with
	  o => i :: sub_lst' tla tlb i
	  | i => o :: sub_lst' tla tlb i
	end
      | _ => nil
    end.

  Definition sub_lst (a b:list bit) (borrow:bit) : list bit :=
    rev (sub_lst' (rev a) (rev b) borrow).

  Lemma sub_lst_length : forall n lsta lstb borrow,
    length lsta = n ->
    length lstb = n ->
    length (sub_lst lsta lstb borrow) = n.
    induction n.
    intros.
    destruct lsta; try discriminate.
    destruct lstb; try discriminate.
    auto.
    intros.
    lapply (list_last _ lsta).
    intro X; inversion_clear X as [tla Y]; inversion_clear Y as [hda].
    lapply (list_last _ lstb).
    intro X; inversion_clear X as [tlb Y]; inversion_clear Y as [hdb].
    rewrite H1.
    rewrite H2.
    unfold sub_lst.
    rewrite rev_unit.
    rewrite rev_unit.
    unfold sub_lst in IHn.
    rewrite H1 in H.
    rewrite H2 in H0.
    rewrite length_app in H.
    rewrite length_app in H0.
    simpl in H.
    simpl in H0.
    destruct hda; destruct hdb; destruct borrow; simpl; rewrite length_app; rewrite IHn; try (simpl; omega).
    omega.
    omega.
  Qed.
    
  (*
   * 2cplt and its properties
   *)

  Definition cplt2 lst :=
    add_lst (cplt1 lst) (zero_extend_lst (length lst - 1) (i::nil)) o.
  
  Definition cplt2_length : forall lst,
    length (cplt2 lst) = length lst.
    intro.
    destruct lst as [_ | hd tl].
    reflexivity.
    unfold cplt2.
    rewrite (add_lst_length (length (hd::tl))).
    reflexivity.
    rewrite cplt1_length; reflexivity.
    rewrite (zero_extend_lst_length 1).
    simpl.
    rewrite <-minus_n_O.
    rewrite S_to_plus_one.
    ring.
    reflexivity.
  Qed.

  Definition cplt2_length' : forall n lst,
    length lst = n ->
    length (cplt2 lst) = n.
    intros; rewrite cplt2_length; auto.
  Qed.

  
  Lemma cplt2_nil : forall lst,
    lst <> nil -> cplt2 lst <> nil.
    intros.
    intro.
    apply H; clear H.
    destruct lst; auto.
    assert (length (cplt2 (b::lst)) = O).
    rewrite H0; auto.
    rewrite cplt2_length in H; discriminate.
  Qed.

  Lemma cplt2_zeros : forall k,
    cplt2 (zeros k) = zeros k.
    induction k.
    unfold cplt2.
    unfold add_lst.
    simpl.
    reflexivity.
    simpl.
    unfold cplt2.
    unfold add_lst.
    simpl.
    rewrite zeros_length.
    rewrite <-minus_n_O.
    cutrewrite ( o :: zeros k = zeros (S k) ).
    rewrite cplt1_zeros.
    simpl.
    unfold cplt2 in IHk.
    cutrewrite ( rev (ones k) ++ i :: nil = i :: (rev (ones k)) ).
    unfold zero_extend_lst.
    rewrite distr_rev.
    simpl.
    rewrite <-cplt1_zeros.
    destruct k; auto.
    rewrite (carry_add' (rev (cplt1 (zeros (S k)))) k).
    rewrite zeros_length in IHk.
    simpl minus in IHk.
    rewrite <-minus_n_O in IHk.
    unfold add_lst in IHk.
    rewrite IHk.
    simpl.
    rewrite zeros_zero.
    rewrite <-app_nil_end.
    reflexivity.
    rewrite length_rev.
    rewrite cplt1_length.
    rewrite zeros_length.
    reflexivity.
    rewrite length_rev.
    rewrite cplt1_length.
    rewrite zeros_length.
    rewrite rev_zeros.
    reflexivity.
    rewrite rev_ones.
    rewrite ones_one.
    rewrite <-app_nil_end.
    reflexivity.
    reflexivity.
  Qed.

  (* the two complement of the weird number is itself *)
  Lemma cplt2_weird : forall k, 
    cplt2 (i :: zeros k) = i :: zeros k.
    induction k.
    simpl.
    unfold cplt2.
    unfold add_lst.
    simpl.
    reflexivity.
    simpl.
    unfold cplt2.
    unfold add_lst.
    simpl.
    unfold cplt2 in IHk.
    unfold add_lst in IHk.
    unfold zero_extend_lst in IHk.
    simpl in IHk.
    rewrite <-minus_n_O in IHk.
    rewrite zeros_length in IHk.
    rewrite zeros_length.
    assert ( (rev (cplt1 (zeros k)) ++ i :: nil) ++ o :: nil =
      i :: rev (cplt1 (zeros k)) ++ o::nil ).
    rewrite cplt1_zeros.
    rewrite rev_ones.
    rewrite ones_one.
    rewrite <-app_nil_end.
    reflexivity.
    rewrite H; clear H.
    assert ( (rev (zeros k ++ i :: nil) ++ o :: nil) =
      (i :: zeros k ++ o :: nil) ).
    rewrite distr_rev.
    simpl.
    rewrite rev_zeros.
    reflexivity.
    rewrite H; clear H.
    simpl.
    rewrite (carry_add' (rev (cplt1 (zeros k)) ++ o :: nil) k).
    unfold zero_extend_lst.
    rewrite IHk.
    simpl.
    rewrite zeros_zero.
    rewrite <-app_nil_end.
    reflexivity.
    rewrite length_app.
    rewrite length_rev.
    rewrite cplt1_length.
    rewrite zeros_length.
    simpl.
    ring.
    rewrite length_app.
    rewrite length_rev.
    rewrite cplt1_length.
    rewrite zeros_length.
    simpl.
    rewrite zeros_zero.
    rewrite <-app_nil_end.
    rewrite S_to_plus_one.
    rewrite plus_comm.
    reflexivity.
  Qed.

  Lemma two2one : forall lst, length lst > O ->
    cplt2 (lst ++ o::nil) = 
    add_lst
    (cplt1 lst ++ i::nil)
    (zero_extend_lst (length lst) (i::nil)) o.
    intros.
    destruct lst.
    simpl in H; inversion H.
    unfold cplt2.
    simpl.
    rewrite length_app.
    simpl.
    rewrite <-minus_n_O.
    rewrite cplt1_app.
    simpl.
    rewrite (S_to_plus_one (length lst)).
    rewrite (plus_comm 1).
    reflexivity.
  Qed.

 Lemma one2two : forall lst, length lst > 0 ->
    add_lst 
      (cplt1 lst ++ i :: nil)
      (zero_extend_lst (length lst) (i :: nil)) o = 
    cplt2 lst ++ o :: nil.
    destruct lst.
    intro X; inversion X.
    intros.
    unfold cplt2.
    simpl.
    rewrite <-minus_n_O.
    unfold add_lst.
    simpl.
    assert ( rev (cplt1 lst ++ i :: nil) ++ cplt b :: nil =
      i :: rev (cplt1 lst) ++ cplt b :: nil ).
    rewrite distr_rev.
    simpl.
    reflexivity.
    rewrite H0; clear H0.
    assert ( rev (zeros (length lst) ++ i :: nil) ++ o :: nil =
      i :: rev (zeros (length lst)) ++ o :: nil ).
    rewrite distr_rev.
    simpl.
    reflexivity.
    rewrite H0; clear H0.
    simpl.
    rewrite (carry_add' (rev (cplt1 lst) ++ cplt b :: nil) (length lst)).
    reflexivity.
    rewrite length_app.
    rewrite length_rev.
    rewrite cplt1_length.
    ring.
    rewrite length_app.
    rewrite length_rev.
    rewrite cplt1_length.
    rewrite rev_zeros.
    simpl.
    rewrite zeros_zero.
    rewrite <-app_nil_end.
    rewrite S_to_plus_one.
    rewrite plus_comm.
    reflexivity.
  Qed.

  Lemma cplt2_involutive_o : forall lst, lst <> nil ->
    ~ (exists k, lst = zeros k) ->
    cplt2 (lst ++ o::nil) = cplt2 lst ++ o::nil.
    destruct lst.
    tauto.
    intros.
    rewrite two2one.
    rewrite one2two.
    reflexivity.
    simpl; omega.
    simpl; omega.
  Qed.
  
  Lemma cplt2_involutive_i : forall lst, lst <> nil ->
    cplt2 (lst ++ i::nil) = cplt1 lst ++ i::nil.
    destruct lst.
    tauto.
    intro X; clear X.
    unfold cplt2.
    simpl.
    rewrite <-minus_n_O.
    rewrite length_app.
    simpl.
    unfold add_lst.
    simpl.
    assert ( rev (cplt1 (lst ++ i :: nil)) ++ cplt b :: nil =
      o :: rev (cplt1 lst) ++ cplt b :: nil ).
    rewrite cplt1_app.
    simpl.
    rewrite distr_rev.
    simpl.
    reflexivity.
    rewrite H; clear H.
    assert ( rev (zero_extend_lst (length lst + 1) (i :: nil)) =
      i :: zeros (length lst + 1) ).
    unfold zero_extend_lst.
    rewrite distr_rev.
    simpl.
    rewrite rev_zeros.
    reflexivity.
    rewrite H; clear H.
    simpl.
    rewrite add_lst'_neutral.
    rewrite distr_rev.
    rewrite rev_involutive.
    simpl.
    reflexivity.
    rewrite length_app.
    rewrite length_rev.
    rewrite cplt1_length.
    simpl.
    reflexivity.
  Qed.

  (* two-complement is involutive *)
  Lemma cplt2_involutive : forall lst,
    cplt2 (cplt2 lst) = lst.
    intro.
    assert (exists k, length lst = k).
    exists (length lst); auto.
    inversion_clear H as [k].
    generalize lst H0; clear lst H0.
    induction k; intros.
    destruct lst; try discriminate.
    auto.
    generalize (dec_equ_lst_bit' lst (zeros (length lst))); 
      intro X; inversion_clear X.
    rewrite H.
    rewrite cplt2_zeros.
    rewrite cplt2_zeros.
    reflexivity.
    cut (exists lst', lst = lst' ++ (o::nil) \/ lst = lst' ++ (i::nil)).
    intro.
    inversion_clear H1 as [lst'].
    inversion_clear H2.
    rewrite H1.
    destruct lst'.
    unfold cplt2; unfold add_lst; reflexivity.
    rewrite cplt2_involutive_o.
    rewrite cplt2_involutive_o.
    rewrite IHk.
    reflexivity.
    rewrite H1 in H0; rewrite length_app in H0; simpl in H0.
    simpl; omega.
    intro.
    generalize (cplt2_length (b::lst')); intro.
    rewrite H2 in H3; discriminate.
    intro.
    inversion_clear H2.
    assert ( length (b::lst') = k ).
    rewrite H1 in H0; rewrite length_app in H0; simpl in H0; injection H0; intro.
    rewrite <-H2.
    simpl.
    ring.
    generalize (IHk _ H2); intro.
    rewrite H3 in H4.
    rewrite cplt2_zeros in H4.
    destruct b.
    apply H.
    rewrite H1.
    rewrite <-H4.
    simpl.
    rewrite zeros_zero.
    simpl.
    rewrite <-app_nil_end.
    rewrite zeros_length.
    reflexivity.
    destruct x; discriminate H4.
    intro; discriminate.
    intro.
    apply H.
    inversion_clear H2.
    destruct x; try discriminate.
    simpl in H3; injection H3; intros.
    subst b.
    rewrite H1.
    simpl.
    rewrite H2.
    rewrite zeros_zero.
    simpl; rewrite <-app_nil_end; auto.
    rewrite zeros_length.
    reflexivity.
    rewrite H1.
    destruct lst'.
    unfold cplt2; unfold add_lst; simpl.
    auto.
    rewrite cplt2_involutive_i.
    rewrite cplt2_involutive_i.
    rewrite cplt1_involutive.
    auto.
    intro.
    simpl in H2.
    destruct b; discriminate H2.
    intro.
    discriminate H2.
    assert (length lst > 0).
    omega.
    generalize (list_last _ lst H1); intro X; inversion_clear X.
    inversion_clear H2.
    destruct x0; exists x; auto.
  Qed.

  Lemma cplt2_prop : forall tl,
    ~(exists k, tl = zeros k) ->
    forall hd,
      ~(exists k, hd::tl = i::zeros k) ->
      cplt2 (hd::tl) = cplt hd :: cplt2 tl.
    intro.
    assert (exists l, length tl = l).
    exists (length tl); auto.
    inversion_clear H as [k].
    generalize tl H0; clear tl H0.
    induction k.
    intros.
    assert (exists k, tl = zeros k).
    exists O; auto.
    simpl.
    destruct tl.
    auto.
    discriminate H0.
    contradiction.
    intros.
    destruct k.
    destruct tl.
    discriminate H0.
    simpl in H0.
    injection H0; intro.
    destruct tl.
    unfold cplt2.
    destruct hd; destruct b; simpl; auto.
    assert (exists k, o :: nil = zeros k).
    exists (S O).
    auto.
    contradiction.
    assert (exists k : nat, i :: o :: nil = i :: zeros k). 
    exists (S O).
    auto.
    contradiction.
    simpl in H2.
    discriminate H2.
    cut (exists tl', exists b, tl = tl' ++ (b::nil)).
    intro.
    inversion_clear H2.
    inversion_clear H3 as [c].
    rewrite H2.
    assert ( hd :: x ++ c :: nil = (hd :: x) ++ c :: nil ).
    auto.
    rewrite H3; clear H3.
    destruct c.
    rewrite cplt2_involutive_o.
    rewrite IHk.
    rewrite cplt2_involutive_o.
    auto.
    intro.
    rewrite H3 in H2; rewrite H2 in H0.
    simpl in H0.
    discriminate H0.
    intro.
    apply H.
    inversion_clear H3.
    rewrite H2.
    exists (S x0).
    simpl.
    rewrite H4.
    rewrite zeros_zero.
    simpl.
    rewrite <-app_nil_end.
    auto.
    rewrite H2 in H0.
    rewrite length_app in H0.
    simpl in H0.
    assert ( length x + 1 = S (length x) ).
    omega.
    rewrite H3 in H0.
    injection H0; auto.
    intro.
    inversion_clear H3.
    apply H.
    exists (S x0).
    rewrite H2.
    rewrite H4.
    rewrite zeros_zero.
    simpl.
    rewrite <-app_nil_end.
    auto.
    intro.
    apply H.
    inversion_clear H3.
    injection H4; intros.
    subst hd.
    rewrite H2; rewrite H3.
    exists (S x0).
    simpl.
    rewrite zeros_zero.
    simpl.
    rewrite <-app_nil_end.
    auto.
    intro.
    discriminate H3.
    intro.
    apply H1.
    inversion_clear H3.
    assert (exists k, tl = zeros k).
    rewrite H2.
    exists x0.
    destruct x0.
    discriminate H4.
    simpl in H4.
    injection H4; intros.
    rewrite H3.
    simpl.
    rewrite zeros_zero.
    simpl.
    rewrite <-app_nil_end.
    auto.
    contradiction.
    rewrite cplt2_involutive_i.
    rewrite cplt2_involutive_i.
    destruct hd; simpl; auto.
    intro.
    rewrite H3 in H2; rewrite H2 in H0.
    simpl in H0.
    discriminate H0.
    intro.
    discriminate H3.
    apply list_last.
    rewrite H0.
    omega.
  Qed.

  (*
   * unsigned multiplication (result on 2*n bits)
   *)

  Fixpoint umul_lst (a b:list bit) {struct b} : list bit :=
    match b with
      nil => zeros (length a)
      | io::tl => match io with
                    o => o::(umul_lst a tl)
                    | i => add_lst
                      (o :: a ++ zeros (length tl))
                      (o :: umul_lst a tl) 
		      o
                  end
    end.

  Lemma umul_lst_length : forall (a b:list bit),
    length (umul_lst a b) = length a + length b.
    intros a b; generalize a; clear a; induction b as [_ | hd tl]; intros.
    simpl.
    rewrite zeros_length.
    rewrite <-plus_n_O.
    reflexivity.
    destruct hd.
    simpl.
    rewrite IHtl.
    apply plus_n_Sm.
    simpl.
    rewrite (add_lst_length (length (o::a) + length tl)); simpl.
    apply plus_n_Sm.
    rewrite length_app.
    rewrite zeros_length.
    reflexivity.
    rewrite IHtl.
    reflexivity.
  Qed.
  
  Lemma umul_lst_nil: forall l,
    umul_lst nil l = zeros (length l).
    induction l; auto.
    destruct a.
    simpl.
    rewrite IHl.
    auto.
    simpl.
    rewrite IHl.
    rewrite add_lst_neutral; auto.
    simpl.
    rewrite zeros_length; auto.
  Qed.

  Lemma umul_lst_zeros : forall b, is_zeros b = true ->
    forall a, 
      umul_lst a b = zeros (length a + length b).
    induction b.
    intros.
    simpl.
    rewrite <-plus_n_O; auto.
    intros.
    destruct a.
    simpl.
    rewrite IHb.
    cutrewrite (length a0 + S (length b) = S (length a0 + length b)).
    auto.
    omega.
    auto.
    simpl in H.
    discriminate H.
  Qed.
  
  Lemma umul_lst_leading_o: forall l1 l2,
    l1 <> nil -> l2 <> nil ->
    umul_lst (o::l1) l2 = o :: umul_lst l1 l2.
    induction l1.
    destruct l2; tauto.
    intros.
    clear H; generalize l2 H0; clear l2 H0.
    induction l2; try tauto.
    intros.
    destruct a0.
    simpl.
    destruct l2; auto.
    rewrite IHl2; auto.
    intro X; discriminate.
    simpl.
    destruct l2.
    simpl.
    rewrite (add_lst_no_overflow (S (length l1))).
    auto.
    simpl.
    rewrite length_app; auto.
    simpl.
    rewrite zeros_length; auto.
    rewrite IHl2.
    rewrite (add_lst_no_overflow (S (S (length l1 + length l2)))).
    auto.
    simpl.
    rewrite length_app.
    simpl.
    rewrite zeros_length.
    auto.
    rewrite umul_lst_length.
    simpl; auto.
    intro X; discriminate.
  Qed.
  
  Lemma umul_lst_leading_o': forall l1 l2,
    l1 <> nil -> l2 <> nil ->
    umul_lst l1 (o::l2) = o :: umul_lst l1 l2.
    induction l1.
    destruct l2; tauto.
    intros.
    clear H; generalize l2 H0; clear l2 H0.
    induction l2; try tauto.
  Qed.
  
  Lemma umul_lst_leading_i: forall l2 l1,
    umul_lst (i :: l1) l2 = 
    add_lst (o :: l2 ++ zeros (length l1)) (o :: umul_lst l1 l2) o.
    induction l2.
    induction l1; auto.
    simpl.
    rewrite add_lst_neutral.
    auto.
    simpl.
    rewrite zeros_length; auto.
    intros.
    destruct a.
    simpl.
    rewrite IHl2.
    rewrite (add_lst_no_overflow (length l1 + length l2)).
    auto.
    rewrite length_app.
    rewrite zeros_length.
    ring.
    rewrite umul_lst_length; auto.
    simpl.
    rewrite IHl2.
    
    rewrite <- (add_lst_no_overflow (length l1 + length l2)).
    rewrite <- (add_lst_assoc (length l1 + length l2 + 2)).
    rewrite (add_lst_leading_bit (length l1 + length l2)).
    rewrite <-(add_lst_no_overflow (length l1 + length l2)).
    rewrite <- (add_lst_assoc (length l1 + length l2 + 2)).
    rewrite (add_lst_com (o :: o :: l1 ++ zeros (length l2)) (o :: i :: l2 ++ zeros (length l1)) o).
    auto.
    simpl; rewrite length_app; rewrite zeros_length; omega.
    simpl; rewrite length_app; rewrite zeros_length; omega.
    simpl; rewrite umul_lst_length; omega.
    simpl; rewrite length_app; rewrite zeros_length; omega.
    simpl; rewrite umul_lst_length; omega.
    simpl; rewrite length_app; rewrite zeros_length; omega.
    simpl; rewrite length_app; rewrite zeros_length; omega.
    simpl; rewrite length_app; rewrite zeros_length; omega.
    simpl; rewrite length_app; rewrite zeros_length; omega.
    simpl; rewrite umul_lst_length; omega.
    simpl; rewrite length_app; rewrite zeros_length; omega.
    simpl; rewrite umul_lst_length; omega.
  Qed.
  
  (* commutativity *)
  Lemma umul_lst_com: forall  n l2 l1,
    length l1 = n ->
    length l2 = n ->
    n > 0 ->
    umul_lst l1 l2 = umul_lst l2 l1.
    induction n.
    intros.
    inversion H1.
    intros.
    destruct l1.
    discriminate H.
    destruct l2.
    discriminate H0.
    simpl in H; simpl in H0; injection H; injection H0; clear H H0; intros.
    rename b into hd1.
    rename b0 into hd2.
    destruct n.
    destruct l1; try discriminate.
    destruct l2; try discriminate.
    simpl.
    destruct hd2; destruct hd1; auto.
    destruct hd2.
    destruct hd1.
    simpl.
    rewrite umul_lst_leading_o; auto.
    rewrite umul_lst_leading_o; auto.
    rewrite  IHn; auto.
    omega.
    intro; subst l2; discriminate H.
    intro; subst l1; discriminate H0.
    intro; subst l1; discriminate H0.
    intro; subst l2; discriminate H.
    simpl.
    rewrite umul_lst_leading_o; auto.
    rewrite (add_lst_no_overflow (S n + S n)).
    rewrite umul_lst_leading_i; auto.
    rewrite IHn; auto.
    omega.
    rewrite length_app.
    rewrite zeros_length.
    auto.
    rewrite umul_lst_length.
    auto.
    intro; subst l2; discriminate H.
    intro; subst l1; discriminate H0.
    destruct hd1.
    simpl.
    rewrite umul_lst_leading_o.
    rewrite umul_lst_leading_i.
    rewrite (add_lst_no_overflow (S n + S n)).
    rewrite IHn; auto.
    omega.
    rewrite length_app.
    rewrite zeros_length.
    auto.
    rewrite umul_lst_length.
    auto.
    intro; subst l1; discriminate H0.
    intro; subst l2; discriminate H.
    simpl.
    rewrite umul_lst_leading_i.
    rewrite umul_lst_leading_i.
    rewrite <-(add_lst_no_overflow (S n + S n)).
    rewrite <-(add_lst_no_overflow (S n + S n)).
    rewrite <- (add_lst_assoc (length l1 + length l2 + 2)).
    rewrite (add_lst_leading_bit (S n + S n)).
    rewrite <- (add_lst_assoc (length l1 + length l2 + 2)).
    rewrite (add_lst_com (o :: o :: l1 ++ zeros (length l2)) (o :: i :: l2 ++ zeros (length l1)) o).
    rewrite IHn; auto.
    omega.
    simpl.
    rewrite length_app.
    rewrite zeros_length.
    omega.
    simpl.
    rewrite length_app.
    rewrite zeros_length.
    omega.
    simpl.
    rewrite umul_lst_length.
    omega.
    simpl.
    rewrite length_app.
    rewrite zeros_length.
    omega.
    simpl.
    rewrite length_app.
    rewrite zeros_length.
    omega.
    simpl.
    rewrite length_app.
    rewrite zeros_length.
    omega.
    simpl.
    rewrite length_app.
    rewrite zeros_length.
    omega.
    simpl.
    rewrite umul_lst_length.
    omega.
    simpl.
    rewrite length_app.
    rewrite zeros_length.
    omega.
    simpl.
    rewrite umul_lst_length.
    omega.
    simpl.
    rewrite length_app.
    rewrite zeros_length.
    omega.
    simpl.
    rewrite umul_lst_length.
    omega.
  Qed.

  Lemma umul_lst_zero : forall  l2 l1,
    umul_lst l1 (l2 ++ o::nil) = umul_lst l1 l2 ++ o::nil.
    induction l2.
    simpl.
    intros.
    rewrite zeros_zero.
    rewrite <-app_nil_end; auto.
    destruct a.
    simpl.
    intros; rewrite IHl2.
    auto.
    simpl.
    intros.
    rewrite IHl2.
    unfold add_lst.
    simpl.
    assert (length (l2 ++ o::nil) = S (length l2)).
    rewrite length_app; simpl; ring.
    rewrite H; clear H.
    simpl.
    repeat rewrite distr_rev.
    simpl.
    rewrite rev_zeros.
    rewrite (zeros_zero (length l2) nil).
    simpl.
    rewrite <-app_nil_end.
    auto.
  Qed.
  
  Lemma umul_lst_1 : forall l lst,
    length lst = S l ->
    umul_lst lst (zeros l ++ i::nil) = zeros (S l) ++ lst.
    induction l.
    
    intros.
    destruct lst; try discriminate.
    destruct lst; try discriminate.
    simpl.
    destruct b; auto.
    
    intros.
    simpl.
    destruct lst; try discriminate.
    destruct b.
    
    rewrite umul_lst_leading_o.
    rewrite IHl.
    rewrite zeros_zero.
    auto.
    simpl in H; omega.
    intro; subst lst; discriminate.
    intro.
    destruct l; discriminate.
    
    simpl in H; injection H; clear H; intro.
    rewrite umul_lst_leading_i.
    rewrite IHl; auto.
    cutrewrite ( 
      o :: (zeros l ++ i :: nil) ++ zeros (length lst) =
      (zeros (length (zeros (S l)))) ++ i::zeros (length lst)
    ).
    cutrewrite (o :: zeros (S l) ++ lst = zeros (S l) ++ o::lst).
    rewrite <-isolated_i_add_lst.
    simpl.
    auto.
    rewrite zeros_zero.
    auto.
    simpl.
    rewrite zeros_length.
    rewrite app_ass.
    simpl.
    auto.
  Qed.

  Lemma umul_lst_zero_list: forall n l1 l2,
    umul_lst l1 (l2 ++ zeros n) = umul_lst l1 l2 ++ zeros n.
    induction n.
    simpl.
    intros.
    repeat rewrite <- app_nil_end.
    auto.
    cutrewrite ( zeros (S n) = zeros n ++ o::nil ).
    intros.
    rewrite ass_app.
    rewrite ass_app.
    rewrite (umul_lst_zero (l2 ++ zeros n) l1).
    rewrite IHn.
    auto.
    rewrite zeros_zero.
    rewrite <-app_nil_end; auto.
  Qed.

  Lemma umul_lst_weird : forall l, 
    umul_lst (i::zeros l) (i::zeros l) = o :: i :: zeros (l+l).
    induction l.
    simpl.
    rewrite add_lst_neutral; auto.
    simpl.
    rewrite zeros_length.
    rewrite umul_lst_zeros.
    rewrite add_lst_neutral.
    rewrite <-zeros_app.
    auto.
    simpl.
    rewrite length_app.
    simpl.
    rewrite zeros_length.
    rewrite <-plus_Snm_nSm.
    auto.
    apply is_zeros_zeros'.
  Qed.

  Lemma umul_lst_weird' : forall n l k, 
    length k = n ->
    umul_lst k (i::zeros l) = o :: k ++ zeros l.
    induction n.
    induction l.
    intros.
    simpl.
    rewrite <-app_nil_end.
    rewrite add_lst_neutral.
    auto.
    auto.
    intros.
    destruct k; try discriminate.
    rewrite umul_lst_nil.
    simpl.
    rewrite zeros_length.
    auto.
    induction l.
    intros.
    simpl.
    rewrite add_lst_neutral.
    auto.
    simpl.
    rewrite <-app_nil_end.
    auto.
    intros.
    destruct k; try discriminate.
    destruct b.
    
    destruct k.
    simpl.
    rewrite umul_lst_zeros.
    simpl.
    rewrite add_lst_neutral.
    rewrite zeros_length; auto.
    rewrite zeros_length.
    simpl.
    rewrite zeros_length.
    auto.
    apply is_zeros_zeros'.
    rewrite umul_lst_leading_o.
    cutrewrite (i::zeros (S l) = (i::zeros l) ++ o::nil).
    rewrite umul_lst_zero.
    rewrite IHn.
    simpl.
    rewrite app_ass.
    rewrite zeros_zero.
    rewrite <-app_nil_end.
    auto.
    simpl in H; auto.
    simpl.
    rewrite zeros_zero.
    rewrite <-app_nil_end.
    auto.
    intro; discriminate.
    intro; discriminate.
    
    rewrite umul_lst_leading_i.
    cutrewrite (i::zeros (S l) = (i::zeros l) ++ o::nil).
    rewrite umul_lst_zero.
    rewrite IHn.
    simpl.
    
    rewrite app_ass.
    rewrite app_ass.
    simpl.
    generalize (isolated_i_add_lst (o::nil) (k++o::zeros l)); intro.
    simpl in H0.
    rewrite H0.
    match goal with
      | |- add_lst ?L ?K _ = add_lst ?M ?N _ => assert (L=M /\ K=N)
    end.
    rewrite length_app.
    simpl.
    rewrite zeros_length.
    rewrite plus_comm.
    rewrite plus_Snm_nSm.
    rewrite <-zeros_app.
    split; auto.
    rewrite zeros_zero.
    rewrite <-app_nil_end; auto.
    rewrite (proj1 H1); rewrite (proj2 H1); auto.
    simpl in H; auto.
    simpl.
    rewrite zeros_zero.
    rewrite <-app_nil_end; auto.
  Qed.

  (*
   * signed multiplication
   *)
  
  Definition is_pos (a:list bit) : bool :=
    match a with
      i::_ => false
      | _ => true
    end.
  
  Definition smul_lst (a b:list bit) :=
    match (is_pos a), (is_pos b) with
      true, true => umul_lst a b
      | false, false => umul_lst (cplt2 a) (cplt2 b)
      | true, false => cplt2 (umul_lst a (cplt2 b))
      | false, true => cplt2 (umul_lst (cplt2 a) b)
    end.
  
  Lemma smul_lst_length : forall n (a b: list bit),
    length a = n -> length b = n ->
    length (smul_lst a b) = 2 * n.
    intros.
    destruct a; destruct b; auto.
    destruct n; try discriminate || auto.
    destruct n; try discriminate || auto.
    destruct n; try discriminate || auto.
    simpl in H; simpl in H0.
    destruct b0; destruct b.
    simpl.
    rewrite umul_lst_length.
    simpl; omega.
    unfold smul_lst.
    simpl.
    rewrite cplt2_length.
    rewrite umul_lst_length.
    rewrite cplt2_length.
    simpl; omega.
    unfold smul_lst.
    simpl.
    rewrite cplt2_length.
    simpl.
    rewrite umul_lst_length.
    rewrite cplt2_length.
    simpl.
    omega.
    unfold smul_lst.
    simpl.
    rewrite umul_lst_length.
    rewrite cplt2_length.
    rewrite cplt2_length.
    simpl.
    omega.
  Qed.

  Lemma smul_lst_com : forall n a b,
    length a = S (S n) ->
    length b = S (S n) ->
    smul_lst a b = smul_lst b a.
    intros.
    destruct a; destruct b; try (discriminate || auto).
    destruct b; destruct b0; unfold smul_lst.
    rewrite (umul_lst_com (S (S n))); auto.
    omega.
    rewrite (umul_lst_com (S (S n)) (cplt2 (i :: a)) (o::b1)); auto.
    rewrite cplt2_length; auto.
    omega.
    rewrite (umul_lst_com (S (S n)) (o::a) (cplt2 (i :: b1))); auto.
    rewrite cplt2_length; auto.
    omega.
    rewrite (umul_lst_com (S (S n)) (cplt2 (i :: a)) (cplt2 (i :: b1))); auto.
    rewrite cplt2_length; auto.
    rewrite cplt2_length; auto.
    omega.
  Qed.
  
  (*
   * Booth algorithm (definition only!) 
   *)

  Definition shift_right_1 := shrl_lst 1.

  Fixpoint booth_mul_lst' (a s p:list bit) (n:nat) {struct n} : list bit :=
    match n with 
      O => p
      | S m => 
	match rev p with
	  o::o::_ => booth_mul_lst' a s (shift_right_1 p) m
	  | i::i::_ => booth_mul_lst' a s (shift_right_1 p) m
	  | i::o::_ => booth_mul_lst' a s 
	    (shift_right_1 (add_lst p a o)) m (* ignore overflow *)
	  | o::i::_ => booth_mul_lst' a s 
	    (shift_right_1 (add_lst p s o)) m (* ignore overflow *)
	  | _ => nil
	end
    end.
  
  (* works only with s =/= weird number! *)
  Definition booth_mul_lst (a s:list bit) :=
    del_nth_last (booth_mul_lst' 
      (shl_extend_lst (length s + 1) a)
      (shl_extend_lst (length s + 1) (cplt2 a))
      (zero_extend_lst (length a) (shl_extend_lst 1 a)) 
      (length s)).
  
  Lemma booth_mul_lst'_length : forall (k:nat) (a s p:list bit),  
    length p = length s -> 
    length p = length a -> 
    length p > 1 ->
    length (booth_mul_lst' a s p k) = length p.
    induction k.
    auto.
    intros.
    assert (exists x, exists y, exists p', p = p' ++ (x::y::nil)).
    assert (length p > 0).
    red.
    red in H1.
    apply lt_trans with 1; auto.
    generalize (list_last _ p H2); intro.
    inversion_clear H3 as [p'].
    inversion_clear H4 as [x].
    rewrite H3; clear H2.
    assert (length p' > 0).
    rewrite H3 in H1.
    rewrite length_app in H1.
    simpl in H1.
    omega.
    generalize (list_last _ p' H2); intro.
    inversion_clear H4 as [p''].
    inversion_clear H5 as [y].
    rewrite H4.
    exists y; exists x; exists p''; auto.
    rewrite app_ass.
    simpl.
    reflexivity.
    inversion_clear H2.
    inversion_clear H3.
    inversion_clear H2.
    rewrite H3.
    simpl.
    rewrite distr_rev.
    simpl.
    rewrite <-H3.
    destruct x0; destruct x.
    
    assert ( length (shift_right_1 p) = length p ).
    unfold shift_right_1.
    rewrite (shrl_length (length p)); auto.
    rewrite IHk; auto.
    rewrite <-H; assumption.
    rewrite <-H0; assumption.
    rewrite H2; assumption.
    
    assert ( length (shift_right_1 (add_lst p s o)) = length p ).
    unfold shift_right_1.
    rewrite (shrl_length (length p)).
    auto.
    rewrite (add_lst_length (length p)); auto.
    rewrite IHk; trivial.
    rewrite <-H; assumption.
    rewrite <-H0; assumption.
    rewrite H2; assumption.
    
    assert ( length (shift_right_1 (add_lst p a o)) = length p ).
    unfold shift_right_1.
    rewrite (shrl_length (length p)).
    reflexivity.
    rewrite (add_lst_length (length p)); auto.
    rewrite IHk; auto.
    rewrite <-H; assumption.
    rewrite <-H0; assumption.
    rewrite H2; assumption.
    
    assert ( length (shift_right_1 p) = length p ).
    unfold shift_right_1.
    rewrite (shrl_length (length p)); auto.
    rewrite IHk; auto.
    rewrite <-H; assumption.
    rewrite <-H0; assumption.
    rewrite H2; assumption.
  Qed.
  
  Lemma del_nth_last_length' : forall (lst:list bit), 
    length lst > 0 -> length (del_nth_last lst) = length lst - 1.
    intros.
    rewrite (del_nth_last_length  (length lst) _ lst); auto.
  Qed.
  
  Definition booth_mul_lst_length : forall (a b:list bit), 
    length a = length b -> 0 < length b ->
    length (booth_mul_lst a b) = 2 * length a.
    intros.
    unfold booth_mul_lst.
    rewrite del_nth_last_length'.
    rewrite booth_mul_lst'_length.
    rewrite (zero_extend_lst_length (S (length a))).
    omega.
    rewrite (shl_extend_length (length a)); try reflexivity.
    rewrite (zero_extend_lst_length (S (length a))).
    rewrite (shl_extend_length (length a)).
    omega.
    rewrite cplt2_length.
    omega.
    rewrite (shl_extend_length (length a)); try reflexivity.
    rewrite (zero_extend_lst_length (S (length a))).
    rewrite (shl_extend_length (length a)); try reflexivity.
    omega.
    rewrite (shl_extend_length (length a)); try reflexivity.
    rewrite (zero_extend_lst_length (S (length a))).
    omega.
    rewrite (shl_extend_length (length a)); try reflexivity.
    rewrite booth_mul_lst'_length.
    rewrite (zero_extend_lst_length (S (length a))).
    omega.
    rewrite (shl_extend_length (length a)); try reflexivity.
    rewrite (zero_extend_lst_length (S (length a))).
    rewrite (shl_extend_length (length a)); try reflexivity.
    omega.
    rewrite cplt2_length.
    reflexivity.
    rewrite (shl_extend_length (length a)); try reflexivity.
    rewrite (zero_extend_lst_length (S (length a))).
    rewrite (shl_extend_length (length a)); try reflexivity.
    omega.
    rewrite (shl_extend_length (length a)); try reflexivity.
    rewrite (zero_extend_lst_length (S (length a))).
    omega.
    rewrite (shl_extend_length (length a)); try reflexivity.
  Qed.

 (*
  * comparisons
  *)

Fixpoint listbit_lt (a b:list bit) {struct a} : bool :=
  match a with
    o::tla => match b with
                o::tlb => listbit_lt tla tlb
              | i::_ => true
              | _ => false (* could not happen with lists of the same length *)
              end
  | i::tla => match b with
                o::_ => false
              | i::tlb => listbit_lt tla tlb
              | _ => false (* could not happen with lists of the same length *)
	      end
  | _ => false 
  end.

Lemma listbit_lt_zeros : forall l,
  listbit_lt l (zeros (length l)) = false.
  induction l; auto.
  destruct a; auto.
Qed.


End ListBit.