Library listbit
Require Import Arith_ext.
Require Import ssreflect ssrnat ssrbool eqtype.
Require Import Lists_ext.
Require Import ssreflect ssrnat ssrbool eqtype.
Require Import Lists_ext.
Definition of lists of bits, of various operations
on lists of bits, along with their algebraic properties.
This is for the implementation of finite-size integers.
This is for the implementation of finite-size integers.
Module ListBit.
Notation "'o'" := false : listbit_scope.
Notation "'i'" := true : listbit_scope.
Local Open Scope listbit_scope.
Lemma dec_equ_bit : forall (a b : bool), { a = b } + { a <> b }.
Lemma dec_equ_lst_bit : forall (a b : list bool), { a = b } + { a <> b }.
Lemma dec_equ_lst_bit' : forall (a b : list bool), a = b \/ a <> b.
lists of zeros
Definition zeros (n : nat) := rep o n.
Definition len_zeros : forall n, length (zeros n) = n.
Lemma zeros_dec : forall l, {l = zeros (length l)} + {l <> zeros (length l)}.
Lemma zeros_zero : forall n l, zeros n ++ o :: l = zeros (S n) ++ l.
Lemma zeros_app: forall n m, zeros n ++ zeros m = zeros (n + m).
Lemma zeros_app2 : forall m n, (n <= m)%coq_nat -> zeros m = zeros n ++ zeros (m - n).
Lemma skipn_zeros : forall n m, skipn n (zeros m) = zeros (m - n).
Lemma rev_zeros : forall n, rev (zeros n) = zeros n.
Definition len_zeros : forall n, length (zeros n) = n.
Lemma zeros_dec : forall l, {l = zeros (length l)} + {l <> zeros (length l)}.
Lemma zeros_zero : forall n l, zeros n ++ o :: l = zeros (S n) ++ l.
Lemma zeros_app: forall n m, zeros n ++ zeros m = zeros (n + m).
Lemma zeros_app2 : forall m n, (n <= m)%coq_nat -> zeros m = zeros n ++ zeros (m - n).
Lemma skipn_zeros : forall n m, skipn n (zeros m) = zeros (m - n).
Lemma rev_zeros : forall n, rev (zeros n) = zeros n.
zero-extend
Definition zext_lst m l := zeros m ++ l.
Lemma len_zext_lst : forall n lst, length lst = n ->
forall k, length (zext_lst k lst) = k + n.
Lemma zext_lst_i : forall k l, zext_lst k (i :: l) = zeros k ++ i :: l.
Lemma rev_zext_lst_i' : forall k l, rev (zext_lst k (i :: l)) = rev l ++ i :: zeros k.
Lemma rev_zext_lst_i : forall n, rev (zext_lst n (i :: nil)) = i :: zeros n.
Fixpoint erase_leading_zeros (l : list bool) : list bool :=
match l with
| o :: t => erase_leading_zeros t
| i :: t => l
| _ => nil
end.
Lemma len_erase_leading_zeros : forall n l, length l = n ->
(length (erase_leading_zeros l) <= n)%coq_nat.
Lemma erase_leading_zeros_prop : forall n l, length l = n ->
zeros (n - length (erase_leading_zeros l)) ++ (erase_leading_zeros l) = l.
Lemma erase_leading_zeros_app : forall l, erase_leading_zeros l ++ true :: nil =
erase_leading_zeros (l ++ true :: nil).
Lemma erase_leading_zeros_app' : forall l, l <> zeros (length l) ->
erase_leading_zeros l ++ false :: nil = erase_leading_zeros (l ++ false :: nil).
Lemma erase_leading_zeros_zeros : forall n, erase_leading_zeros (zeros n) = nil.
Lemma tail_zeros : forall n, (0 < n)%coq_nat -> tail (zeros n) = zeros (n - 1).
Lemma heads_zeros : forall m n, (m <= n)%coq_nat -> firstn m (zeros n) = zeros m.
Lemma nth_zeros : forall k n def, (k < n)%coq_nat -> nth k (zeros n) def = o.
Lemma len_zext_lst : forall n lst, length lst = n ->
forall k, length (zext_lst k lst) = k + n.
Lemma zext_lst_i : forall k l, zext_lst k (i :: l) = zeros k ++ i :: l.
Lemma rev_zext_lst_i' : forall k l, rev (zext_lst k (i :: l)) = rev l ++ i :: zeros k.
Lemma rev_zext_lst_i : forall n, rev (zext_lst n (i :: nil)) = i :: zeros n.
Fixpoint erase_leading_zeros (l : list bool) : list bool :=
match l with
| o :: t => erase_leading_zeros t
| i :: t => l
| _ => nil
end.
Lemma len_erase_leading_zeros : forall n l, length l = n ->
(length (erase_leading_zeros l) <= n)%coq_nat.
Lemma erase_leading_zeros_prop : forall n l, length l = n ->
zeros (n - length (erase_leading_zeros l)) ++ (erase_leading_zeros l) = l.
Lemma erase_leading_zeros_app : forall l, erase_leading_zeros l ++ true :: nil =
erase_leading_zeros (l ++ true :: nil).
Lemma erase_leading_zeros_app' : forall l, l <> zeros (length l) ->
erase_leading_zeros l ++ false :: nil = erase_leading_zeros (l ++ false :: nil).
Lemma erase_leading_zeros_zeros : forall n, erase_leading_zeros (zeros n) = nil.
Lemma tail_zeros : forall n, (0 < n)%coq_nat -> tail (zeros n) = zeros (n - 1).
Lemma heads_zeros : forall m n, (m <= n)%coq_nat -> firstn m (zeros n) = zeros m.
Lemma nth_zeros : forall k n def, (k < n)%coq_nat -> nth k (zeros n) def = o.
shift-left and extend
Definition shl_extend_lst n (l : list bool) := l ++ zeros n.
Lemma len_shl_extend_lst : forall n lst, length lst = n ->
forall m, length (shl_extend_lst m lst) = m + n.
Lemma len_shl_extend_lst : forall n lst, length lst = n ->
forall m, length (shl_extend_lst m lst) = m + n.
lists of ones
Definition ones (n : nat) := rep i n.
Definition len_ones : forall n, length (ones n) = n.
Lemma ones_one : forall n l, ones n ++ i :: l = ones (S n) ++ l.
Lemma rev_ones : forall n, rev (ones n) = ones n.
Definition one_extend_n_lst lst cnt := ones cnt ++ lst.
Lemma one_extend_n_lst_i : forall k lst, one_extend_n_lst (i :: lst) k = ones k ++ i :: lst.
Definition len_ones : forall n, length (ones n) = n.
Lemma ones_one : forall n l, ones n ++ i :: l = ones (S n) ++ l.
Lemma rev_ones : forall n, rev (ones n) = ones n.
Definition one_extend_n_lst lst cnt := ones cnt ++ lst.
Lemma one_extend_n_lst_i : forall k lst, one_extend_n_lst (i :: lst) k = ones k ++ i :: lst.
sign-extension for signed list-bits
Fixpoint sext_lst (m : nat) (l : list bool) : list bool :=
match l with
| nil => zeros m
| hd :: _ => match m with
| 0 => l
| S m' => hd :: sext_lst m' l
end
end.
Lemma len_sext_lst' : forall m n l, length l = n -> length (sext_lst m l) = n + m.
Lemma len_sext_lst : forall m l, length (sext_lst m l) = length l + m.
Lemma sext_0_lst : forall n l, sext_lst n (o :: l) = zeros (S n) ++ l.
match l with
| nil => zeros m
| hd :: _ => match m with
| 0 => l
| S m' => hd :: sext_lst m' l
end
end.
Lemma len_sext_lst' : forall m n l, length l = n -> length (sext_lst m l) = n + m.
Lemma len_sext_lst : forall m l, length (sext_lst m l) = length l + m.
Lemma sext_0_lst : forall n l, sext_lst n (o :: l) = zeros (S n) ++ l.
zero-extend or shrink a given list ("adjust" it to some size)
Definition adjust_ulist l n :=
if length l < n then
zext_lst (n - length l) l
else
skipn (length l - n) l.
Lemma len_adjust_ulist : forall n l, length (adjust_ulist l n) = n.
Lemma adjust_ulist_nil: forall n, adjust_ulist nil n = zeros n.
Lemma adjust_ulist_0 : forall lst, adjust_ulist lst 0 = nil.
Lemma adjust_ulist_id : forall n lst, length lst = n -> adjust_ulist lst n = lst.
Lemma adjust_ulist_S : forall n h t l,
length (h ++ t :: nil) = l -> l >= S n ->
adjust_ulist (h ++ t :: nil) (S n) = adjust_ulist h n ++ (t :: nil).
Lemma adjust_ulist_S' : forall n lst l, length lst = l -> l < n ->
adjust_ulist lst n = zeros (n - l)%coq_nat ++ lst.
Lemma adjust_ulist_S'' : forall n l lst, length lst = l -> l <= n ->
adjust_ulist lst n = zeros (n - l)%coq_nat ++ lst.
Lemma adjust_ulist_zeros : forall k n, adjust_ulist (zeros n) k = zeros k.
if length l < n then
zext_lst (n - length l) l
else
skipn (length l - n) l.
Lemma len_adjust_ulist : forall n l, length (adjust_ulist l n) = n.
Lemma adjust_ulist_nil: forall n, adjust_ulist nil n = zeros n.
Lemma adjust_ulist_0 : forall lst, adjust_ulist lst 0 = nil.
Lemma adjust_ulist_id : forall n lst, length lst = n -> adjust_ulist lst n = lst.
Lemma adjust_ulist_S : forall n h t l,
length (h ++ t :: nil) = l -> l >= S n ->
adjust_ulist (h ++ t :: nil) (S n) = adjust_ulist h n ++ (t :: nil).
Lemma adjust_ulist_S' : forall n lst l, length lst = l -> l < n ->
adjust_ulist lst n = zeros (n - l)%coq_nat ++ lst.
Lemma adjust_ulist_S'' : forall n l lst, length lst = l -> l <= n ->
adjust_ulist lst n = zeros (n - l)%coq_nat ++ lst.
Lemma adjust_ulist_zeros : forall k n, adjust_ulist (zeros n) k = zeros k.
sign-extend or shrink a given list
Definition adjust_slist lst n :=
if length lst < n then
sext_lst (n - length lst) lst
else
skipn (length lst - n) lst.
Lemma len_adjust_slist : forall n lst, length (adjust_slist lst n) = n.
Lemma adjust_slist_nil : forall n, adjust_slist nil n = zeros n.
if length lst < n then
sext_lst (n - length lst) lst
else
skipn (length lst - n) lst.
Lemma len_adjust_slist : forall n lst, length (adjust_slist lst n) = n.
Lemma adjust_slist_nil : forall n, adjust_slist nil n = zeros n.
bit complement
Definition cplt b := match b with i => o | o => i end.
Lemma cplt_involutive : forall b, cplt (cplt b) = b.
Lemma cplt_involutive : forall b, cplt (cplt b) = b.
ones' complement
Fixpoint cplt1 lst := if lst is hd :: tl then cplt hd :: cplt1 tl else nil.
Lemma len_cplt1 : forall a, length (cplt1 a) = length a.
Lemma len_cplt1' : forall n a, length a = n -> length (cplt1 a) = n.
Lemma cplt1_app : forall a b, cplt1 (a ++ b) = cplt1 a ++ cplt1 b.
Lemma cplt1_zeros : forall k, cplt1 (zeros k) = ones k.
Lemma rev_cplt1_zeros : forall n, rev (cplt1 (zeros n)) = ones n.
Lemma cplt1_involutive : forall lst, cplt1 (cplt1 lst) = lst.
Lemma len_cplt1 : forall a, length (cplt1 a) = length a.
Lemma len_cplt1' : forall n a, length a = n -> length (cplt1 a) = n.
Lemma cplt1_app : forall a b, cplt1 (a ++ b) = cplt1 a ++ cplt1 b.
Lemma cplt1_zeros : forall k, cplt1 (zeros k) = ones k.
Lemma rev_cplt1_zeros : forall n, rev (cplt1 (zeros n)) = ones n.
Lemma cplt1_involutive : forall lst, cplt1 (cplt1 lst) = lst.
shift left
Fixpoint shl_lst m (l : list bool) {struct m} : list bool :=
match m with
| 0 => l
| S m' => match l with
| nil => nil
| hd :: tl => shl_lst m' tl ++ o :: nil
end
end.
Lemma len_shl_lst : forall m n l, length l = n -> length (shl_lst m l) = n.
Lemma shl_lst_zeros : forall m n, shl_lst m (zeros n) = zeros n.
Lemma shl_lst_app : forall m l k, length l = m -> shl_lst m (l ++ k) = k ++ zeros m.
Lemma shl_lst_zeros_app: forall n l, shl_lst n (zeros n ++ l) = l ++ zeros n.
Lemma shl_lst_overflow : forall n l lst, length lst = l -> (n >= l)%coq_nat ->
shl_lst n lst = zeros l.
Lemma shl_lst_app' : forall m n l k, length l = n -> (m <= n)%nat ->
shl_lst m (l ++ k) = skipn m l ++ k ++ zeros m.
match m with
| 0 => l
| S m' => match l with
| nil => nil
| hd :: tl => shl_lst m' tl ++ o :: nil
end
end.
Lemma len_shl_lst : forall m n l, length l = n -> length (shl_lst m l) = n.
Lemma shl_lst_zeros : forall m n, shl_lst m (zeros n) = zeros n.
Lemma shl_lst_app : forall m l k, length l = m -> shl_lst m (l ++ k) = k ++ zeros m.
Lemma shl_lst_zeros_app: forall n l, shl_lst n (zeros n ++ l) = l ++ zeros n.
Lemma shl_lst_overflow : forall n l lst, length lst = l -> (n >= l)%coq_nat ->
shl_lst n lst = zeros l.
Lemma shl_lst_app' : forall m n l k, length l = n -> (m <= n)%nat ->
shl_lst m (l ++ k) = skipn m l ++ k ++ zeros m.
logical shift right (fill the freed bits with 0)
Fixpoint shrl_lst (m : nat) (l : list bool) : list bool :=
match length l with
| 0 => nil
| S n => match m with
| 0 => l
| S m' => o :: shrl_lst m' (idel_last l)
end
end.
Lemma shrl_lst_nil : forall k, shrl_lst k nil = nil.
Lemma shrl_lst_0 : forall l, shrl_lst 0 l = l.
Lemma shrl_lst_S : forall k hd tl, shrl_lst (S k) (hd ++ tl :: nil) = o :: shrl_lst k hd.
Lemma len_shrl_lst : forall n m l, length l = n -> length (shrl_lst m l) = n.
Lemma shrl_lst_o : forall n l, shrl_lst n (o :: l) = o :: shrl_lst n l.
Lemma shrl_lst_comp : forall l m n, shrl_lst m (shrl_lst n l) = shrl_lst (m + n) l.
Lemma shrl_lst_zeros : forall n m, shrl_lst m (zeros n) = zeros n.
Lemma shrl_lst_unfold : forall n l, n <> O -> l <> nil -> shrl_lst n l = o :: shrl_lst (n.-1) (idel_last l).
Lemma shrl_lst_app_zeros : forall k n l, length l = n ->
shrl_lst k (l ++ zeros k) = zeros k ++ l.
Lemma shrl_lst_tail : forall n l m, length l = n -> (m <= n)%coq_nat ->
shrl_lst m l = zeros m ++ del_last_n m l.
Lemma shrl_lst_overflow: forall n lst k, length lst = n -> (n <= k)%nat -> shrl_lst k lst = zeros n.
Lemma shl_lst_shrl_lst : forall n l k, length l = n -> (k <= n)%coq_nat ->
shl_lst k (shrl_lst k l) = firstn (n - k) l ++ zeros k.
match length l with
| 0 => nil
| S n => match m with
| 0 => l
| S m' => o :: shrl_lst m' (idel_last l)
end
end.
Lemma shrl_lst_nil : forall k, shrl_lst k nil = nil.
Lemma shrl_lst_0 : forall l, shrl_lst 0 l = l.
Lemma shrl_lst_S : forall k hd tl, shrl_lst (S k) (hd ++ tl :: nil) = o :: shrl_lst k hd.
Lemma len_shrl_lst : forall n m l, length l = n -> length (shrl_lst m l) = n.
Lemma shrl_lst_o : forall n l, shrl_lst n (o :: l) = o :: shrl_lst n l.
Lemma shrl_lst_comp : forall l m n, shrl_lst m (shrl_lst n l) = shrl_lst (m + n) l.
Lemma shrl_lst_zeros : forall n m, shrl_lst m (zeros n) = zeros n.
Lemma shrl_lst_unfold : forall n l, n <> O -> l <> nil -> shrl_lst n l = o :: shrl_lst (n.-1) (idel_last l).
Lemma shrl_lst_app_zeros : forall k n l, length l = n ->
shrl_lst k (l ++ zeros k) = zeros k ++ l.
Lemma shrl_lst_tail : forall n l m, length l = n -> (m <= n)%coq_nat ->
shrl_lst m l = zeros m ++ del_last_n m l.
Lemma shrl_lst_overflow: forall n lst k, length lst = n -> (n <= k)%nat -> shrl_lst k lst = zeros n.
Lemma shl_lst_shrl_lst : forall n l k, length l = n -> (k <= n)%coq_nat ->
shl_lst k (shrl_lst k l) = firstn (n - k) l ++ zeros k.
arithmetic right shift (fill the freed bits with the bit-sign)
Definition shra_lst (m : nat) (l : list bool) :=
match l with
| nil => nil
| h :: t => h :: rep h (Min.min m (length t)) ++ firstn (length t - m)%coq_nat t
end.
Lemma shra_lst_nil : forall m, shra_lst m nil = nil.
Lemma len_shra_lst : forall n m l, length l = n -> length (shra_lst m l) = n.
shift right and forget about the freed bits
Fixpoint shr_shrink_lst n (l : list bool) : list bool :=
match n with
| 0 => l
| S n' => shr_shrink_lst n' (idel_last l)
end.
Lemma shr_shrink_lst_nil : forall n, shr_shrink_lst n nil = nil.
Lemma shr_shrink_lst_S : forall n h t, shr_shrink_lst (S n) (t ++ h :: nil) = shr_shrink_lst n t.
Lemma len_shr_shrink_lst : forall n m l, length l = n ->
length (shr_shrink_lst m l) = (n - m)%coq_nat.
Lemma shr_shrink_lst_overflow : forall n lst, (length lst <= n)%coq_nat ->
shr_shrink_lst n lst = nil.
Lemma shr_shrink_lst_adjust_ulist : forall l lst n, length lst = l -> (l >= n)%coq_nat ->
shr_shrink_lst n lst ++ adjust_ulist lst n = lst.
Lemma shr_shrink_lst_shrl : forall n l, length l = n -> forall k, k <= n ->
zeros k ++ shr_shrink_lst k l = shrl_lst k l.
Lemma shr_shrink_lst_app : forall k l' l, length l' = k ->
shr_shrink_lst k (l ++ l') = l.
match n with
| 0 => l
| S n' => shr_shrink_lst n' (idel_last l)
end.
Lemma shr_shrink_lst_nil : forall n, shr_shrink_lst n nil = nil.
Lemma shr_shrink_lst_S : forall n h t, shr_shrink_lst (S n) (t ++ h :: nil) = shr_shrink_lst n t.
Lemma len_shr_shrink_lst : forall n m l, length l = n ->
length (shr_shrink_lst m l) = (n - m)%coq_nat.
Lemma shr_shrink_lst_overflow : forall n lst, (length lst <= n)%coq_nat ->
shr_shrink_lst n lst = nil.
Lemma shr_shrink_lst_adjust_ulist : forall l lst n, length lst = l -> (l >= n)%coq_nat ->
shr_shrink_lst n lst ++ adjust_ulist lst n = lst.
Lemma shr_shrink_lst_shrl : forall n l, length l = n -> forall k, k <= n ->
zeros k ++ shr_shrink_lst k l = shrl_lst k l.
Lemma shr_shrink_lst_app : forall k l' l, length l' = k ->
shr_shrink_lst k (l ++ l') = l.
bitwise-and
Definition bit_and a b := if (a, b) is (i, i) then i else o.
Fixpoint and_lst a b :=
if (a, b) is (h :: t, h' :: t') then bit_and h h' :: and_lst t t' else nil.
Lemma len_and_lst : forall n a b, length a = n -> length b = n ->
length (and_lst a b) = n.
Lemma and_lst_zeros : forall n l, length l = n -> and_lst l (zeros n) = zeros n.
Lemma and_lst_ones : forall n l, length l = n -> and_lst l (ones n) = l.
Lemma and_lst_app : forall n a a' b b', length a = n -> length a' = n ->
and_lst (a ++ b) (a' ++ b') = and_lst a a' ++ and_lst b b'.
Lemma and_lst_idempotent : forall n a, length a = n -> and_lst a a = a.
Lemma and_lst_comm: forall n l k, length l = n -> length k = n ->
and_lst l k = and_lst k l.
Fixpoint and_lst a b :=
if (a, b) is (h :: t, h' :: t') then bit_and h h' :: and_lst t t' else nil.
Lemma len_and_lst : forall n a b, length a = n -> length b = n ->
length (and_lst a b) = n.
Lemma and_lst_zeros : forall n l, length l = n -> and_lst l (zeros n) = zeros n.
Lemma and_lst_ones : forall n l, length l = n -> and_lst l (ones n) = l.
Lemma and_lst_app : forall n a a' b b', length a = n -> length a' = n ->
and_lst (a ++ b) (a' ++ b') = and_lst a a' ++ and_lst b b'.
Lemma and_lst_idempotent : forall n a, length a = n -> and_lst a a = a.
Lemma and_lst_comm: forall n l k, length l = n -> length k = n ->
and_lst l k = and_lst k l.
bitwise-or
Definition bit_or a b :=
match (a, b) with | (i, _) => i | (_, i) => i | _ => o end.
Lemma bit_or_o : forall b, bit_or b o = b.
Fixpoint or_lst a b {struct a} :=
if (a, b) is (h :: t, h' :: t') then bit_or h h' :: or_lst t t' else nil.
Lemma len_or_lst : forall n a b, length a = n -> length b = n -> length (or_lst a b) = n.
Lemma or_lst_zeros: forall n l, length l = n -> or_lst l (zeros n) = l.
Lemma or_lst_comm: forall n l k, length l = n -> length k = n ->
or_lst l k = or_lst k l.
Lemma or_lst_idempotent : forall n a, length a = n -> or_lst a a = a.
Lemma nth_or_lst : forall len n l k, length l = len -> length k = len ->
nth n (or_lst l k) i = bit_or (nth n l i) (nth n k i).
Lemma heads_or_lst : forall len n a b, length a = len -> length b = len ->
firstn n (or_lst a b) = or_lst (firstn n a) (firstn n b).
Lemma skipn_or_lst : forall len n a b, length a = len -> length b = len ->
skipn n (or_lst a b) = or_lst (skipn n a) (skipn n b).
Lemma or_lst_app : forall n m a b a' b',
length a = n -> length b = m -> length a' = n -> length b' = m ->
or_lst (a ++ b) (a' ++ b') = or_lst a a' ++ or_lst b b'.
Lemma rev_or_lst : forall len a b, length a = len -> length b = len ->
rev (or_lst a b) = or_lst (rev a) (rev b).
Lemma cplt1_or_lst : forall n a b, length a = n -> length b = n ->
cplt1 (or_lst a b) = and_lst (cplt1 a) (cplt1 b).
Lemma shr_lst_or_lst : forall (n : nat)
(a : list bool) (Ha: length a = n)
(b : list bool) (Hb : length b = n) (m : nat),
shl_lst m (or_lst a b) = or_lst (shl_lst m a) (shl_lst m b).
Lemma shrl_lst_or_lst : forall (n : nat)
(a : list bool) (Ha: length a = n)
(b : list bool) (Hb : length b = n) (m : nat),
shrl_lst m (or_lst a b) = or_lst (shrl_lst m a) (shrl_lst m b).
Lemma adjust_ulist_or_lst : forall n a (Ha : length a = n) b (Hb : length b = n) m,
adjust_ulist (or_lst a b) m = or_lst (adjust_ulist a m) (adjust_ulist b m).
match (a, b) with | (i, _) => i | (_, i) => i | _ => o end.
Lemma bit_or_o : forall b, bit_or b o = b.
Fixpoint or_lst a b {struct a} :=
if (a, b) is (h :: t, h' :: t') then bit_or h h' :: or_lst t t' else nil.
Lemma len_or_lst : forall n a b, length a = n -> length b = n -> length (or_lst a b) = n.
Lemma or_lst_zeros: forall n l, length l = n -> or_lst l (zeros n) = l.
Lemma or_lst_comm: forall n l k, length l = n -> length k = n ->
or_lst l k = or_lst k l.
Lemma or_lst_idempotent : forall n a, length a = n -> or_lst a a = a.
Lemma nth_or_lst : forall len n l k, length l = len -> length k = len ->
nth n (or_lst l k) i = bit_or (nth n l i) (nth n k i).
Lemma heads_or_lst : forall len n a b, length a = len -> length b = len ->
firstn n (or_lst a b) = or_lst (firstn n a) (firstn n b).
Lemma skipn_or_lst : forall len n a b, length a = len -> length b = len ->
skipn n (or_lst a b) = or_lst (skipn n a) (skipn n b).
Lemma or_lst_app : forall n m a b a' b',
length a = n -> length b = m -> length a' = n -> length b' = m ->
or_lst (a ++ b) (a' ++ b') = or_lst a a' ++ or_lst b b'.
Lemma rev_or_lst : forall len a b, length a = len -> length b = len ->
rev (or_lst a b) = or_lst (rev a) (rev b).
Lemma cplt1_or_lst : forall n a b, length a = n -> length b = n ->
cplt1 (or_lst a b) = and_lst (cplt1 a) (cplt1 b).
Lemma shr_lst_or_lst : forall (n : nat)
(a : list bool) (Ha: length a = n)
(b : list bool) (Hb : length b = n) (m : nat),
shl_lst m (or_lst a b) = or_lst (shl_lst m a) (shl_lst m b).
Lemma shrl_lst_or_lst : forall (n : nat)
(a : list bool) (Ha: length a = n)
(b : list bool) (Hb : length b = n) (m : nat),
shrl_lst m (or_lst a b) = or_lst (shrl_lst m a) (shrl_lst m b).
Lemma adjust_ulist_or_lst : forall n a (Ha : length a = n) b (Hb : length b = n) m,
adjust_ulist (or_lst a b) m = or_lst (adjust_ulist a m) (adjust_ulist b m).
bitwise-xor
Lemma bit_xor_tri_ine : forall a b c, xorb a b <= xorb a c + xorb c b.
Fixpoint xor_lst a b :=
if (a, b) is (h :: t, h' :: t') then xorb h h' :: xor_lst t t' else nil.
Lemma len_xor_lst : forall n a b, length a = n -> length b = n -> length (xor_lst a b) = n.
Lemma xor_lst_app : forall a b c d, length a = length c ->
xor_lst (a ++ b) (c ++ d) = xor_lst a c ++ xor_lst b d.
Lemma xor_lst_zeros: forall n l, length l = n -> xor_lst l (zeros n) = l.
Lemma xor_lst_comm : forall n a b, length a = n -> length b = n ->
xor_lst a b = xor_lst b a.
Lemma xor_lst_assoc : forall n a b c, length a = n -> length b = n -> length c = n ->
xor_lst a (xor_lst b c) = xor_lst (xor_lst a b) c.
Lemma xor_lst_self : forall n a, length a = n -> xor_lst a a = zeros n.
Lemma xor_lst_map : forall n {A:Type} (a:list A) f g, length a = n ->
xor_lst (map f a) (map g a) = map (fun x => xorb (f x) (g x)) a.
We model the hardware addition as a recursive function that does
bitwise comparisons and carry propagation. The last carry is ignored.
The least significant bit (LSb) is first.
Fixpoint add_lst' a b c :=
match (a, b) with
| (o :: a', o :: b') => c :: add_lst' a' b' o
| (i :: a', i :: b') => c :: add_lst' a' b' i
| (_ :: a', _ :: b') => match c with o => i :: add_lst' a' b' o | i => o :: add_lst' a' b' i end
| _ => nil
end.
Lemma len_add_lst' : forall a b, length a = length b ->
forall carry, length (add_lst' a b carry) = length a.
Lemma add_lst'_neutral : forall lst list_of_zeros, list_of_zeros = zeros (length lst) ->
add_lst' lst list_of_zeros o = lst.
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.
match (a, b) with
| (o :: a', o :: b') => c :: add_lst' a' b' o
| (i :: a', i :: b') => c :: add_lst' a' b' i
| (_ :: a', _ :: b') => match c with o => i :: add_lst' a' b' o | i => o :: add_lst' a' b' i end
| _ => nil
end.
Lemma len_add_lst' : forall a b, length a = length b ->
forall carry, length (add_lst' a b carry) = length a.
Lemma add_lst'_neutral : forall lst list_of_zeros, list_of_zeros = zeros (length lst) ->
add_lst' lst list_of_zeros o = lst.
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.
Hardware addition with MSb first.
Definition add_lst a b carry := rev (add_lst' (rev a) (rev b) carry).
Lemma len_add_lst : forall n (a b : list bool), length a = n -> length b = n ->
forall carry, length (add_lst a b carry) = n.
Lemma add_lst_com : forall a b carry, add_lst a b carry = add_lst b a carry.
Lemma add_lst_neutral : forall lst list_of_zeros, list_of_zeros = zeros (length lst) ->
add_lst lst list_of_zeros o = lst.
Lemma carry_add : forall l k zs,
S k = length l -> zs = zeros (length l) ->
add_lst l zs i = add_lst l (zext_lst k (i :: nil)) o.
Lemma carry_add' : forall l k, S k = length l ->
rev (add_lst' l (zeros (S k)) i) = rev (add_lst' l (rev (zext_lst k (i :: nil))) o).
Lemma add_lst'_no_overflow : forall n l1 l2 c, length l1 = S n ->
length l2 = S n ->
add_lst' (l1 ++ o :: o :: nil) (l2 ++ o :: o :: nil) c =
(add_lst' (l1 ++ o :: nil) (l2 ++ o :: nil) c) ++ o :: nil.
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.
Lemma add_lst'_leading_bit : forall n l1 l2 c, length l1 = n -> length l2 = n ->
add_lst' (l1 ++ i :: o :: nil) (l2 ++ o :: o :: nil) c =
add_lst' (l1 ++ o :: o :: nil) (l2 ++ i :: o :: nil) c.
Lemma add_lst_leading_bit : forall n l1 l2 c, length l1 = n -> length l2 = n ->
add_lst (o :: i :: l1) (o :: o :: l2) c =
add_lst (o :: o :: l1) (o :: i :: l2) c.
Open Local Scope coq_nat_scope.
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.
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.
Close Local Scope coq_nat_scope.
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.
Lemma isolated_i_helper : forall l m top, length l = m ->
top :: l = add_lst' (top :: zeros m) (o :: l) o.
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.
Lemma isolated_i_add_lst': forall l1 l2,
l1 ++ i :: l2 = add_lst' (zeros (length l1) ++ i :: zeros (length l2)) (l1 ++ o :: l2) o.
Lemma isolated_i_add_lst: forall l1 l2,
l1 ++ i :: l2 = add_lst (zeros (length l1) ++ i :: zeros (length l2)) (l1 ++ o :: l2) o.
Lemma add_lst'_app : forall n l m l', length l = n -> length l' = m ->
add_lst' (l ++ zeros m) (zeros n ++ l') o = l ++ l'.
Lemma add_lst_app : forall n l m l', length l = m -> length l' = n ->
add_lst (zeros m ++ l') (l ++ zeros n) o = l ++ l'.
Lemma len_add_lst : forall n (a b : list bool), length a = n -> length b = n ->
forall carry, length (add_lst a b carry) = n.
Lemma add_lst_com : forall a b carry, add_lst a b carry = add_lst b a carry.
Lemma add_lst_neutral : forall lst list_of_zeros, list_of_zeros = zeros (length lst) ->
add_lst lst list_of_zeros o = lst.
Lemma carry_add : forall l k zs,
S k = length l -> zs = zeros (length l) ->
add_lst l zs i = add_lst l (zext_lst k (i :: nil)) o.
Lemma carry_add' : forall l k, S k = length l ->
rev (add_lst' l (zeros (S k)) i) = rev (add_lst' l (rev (zext_lst k (i :: nil))) o).
Lemma add_lst'_no_overflow : forall n l1 l2 c, length l1 = S n ->
length l2 = S n ->
add_lst' (l1 ++ o :: o :: nil) (l2 ++ o :: o :: nil) c =
(add_lst' (l1 ++ o :: nil) (l2 ++ o :: nil) c) ++ o :: nil.
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.
Lemma add_lst'_leading_bit : forall n l1 l2 c, length l1 = n -> length l2 = n ->
add_lst' (l1 ++ i :: o :: nil) (l2 ++ o :: o :: nil) c =
add_lst' (l1 ++ o :: o :: nil) (l2 ++ i :: o :: nil) c.
Lemma add_lst_leading_bit : forall n l1 l2 c, length l1 = n -> length l2 = n ->
add_lst (o :: i :: l1) (o :: o :: l2) c =
add_lst (o :: o :: l1) (o :: i :: l2) c.
Open Local Scope coq_nat_scope.
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.
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.
Close Local Scope coq_nat_scope.
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.
Lemma isolated_i_helper : forall l m top, length l = m ->
top :: l = add_lst' (top :: zeros m) (o :: l) o.
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.
Lemma isolated_i_add_lst': forall l1 l2,
l1 ++ i :: l2 = add_lst' (zeros (length l1) ++ i :: zeros (length l2)) (l1 ++ o :: l2) o.
Lemma isolated_i_add_lst: forall l1 l2,
l1 ++ i :: l2 = add_lst (zeros (length l1) ++ i :: zeros (length l2)) (l1 ++ o :: l2) o.
Lemma add_lst'_app : forall n l m l', length l = n -> length l' = m ->
add_lst' (l ++ zeros m) (zeros n ++ l') o = l ++ l'.
Lemma add_lst_app : forall n l m l', length l = m -> length l' = n ->
add_lst (zeros m ++ l') (l ++ zeros n) o = l ++ l'.
subtraction
Fixpoint sub_lst' (a b : list bool) (borrow : bool) {struct a} : list bool :=
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, i :: 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
| (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 bool) (bor : bool) : list bool :=
rev (sub_lst' (rev a) (rev b) bor).
Lemma len_sub_lst : forall n a b bor, length a = n -> length b = n ->
length (sub_lst a b bor) = n.
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, i :: 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
| (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 bool) (bor : bool) : list bool :=
rev (sub_lst' (rev a) (rev b) bor).
Lemma len_sub_lst : forall n a b bor, length a = n -> length b = n ->
length (sub_lst a b bor) = n.
two's complement
Definition cplt2_lst lst := add_lst (cplt1 lst) (zext_lst (length lst - 1) (i :: nil)) o.
Definition len_cplt2_lst : forall lst, length (cplt2_lst lst) = length lst.
Definition len_cplt2_lst' : forall n l, length l = n -> length (cplt2_lst l) = n.
Lemma cplt2_lst_nil : forall l, l <> nil -> cplt2_lst l <> nil.
Lemma cplt2_lst_zeros : forall k, cplt2_lst (zeros k) = zeros k.
Definition len_cplt2_lst : forall lst, length (cplt2_lst lst) = length lst.
Definition len_cplt2_lst' : forall n l, length l = n -> length (cplt2_lst l) = n.
Lemma cplt2_lst_nil : forall l, l <> nil -> cplt2_lst l <> nil.
Lemma cplt2_lst_zeros : forall k, cplt2_lst (zeros k) = zeros k.
the two's complement of the weird number is itself
Lemma cplt2_lst_weird : forall k, cplt2_lst (i :: zeros k) = i :: zeros k.
Lemma two2one : forall lst, length lst > O ->
cplt2_lst (lst ++ o :: nil) = add_lst (cplt1 lst ++ i::nil) (zext_lst (length lst) (i :: nil)) o.
Lemma one2two : forall lst, length lst > 0 ->
add_lst (cplt1 lst ++ i :: nil) (zext_lst (length lst) (i :: nil)) o =
cplt2_lst lst ++ o :: nil.
Lemma cplt2_lst_involutive_o : forall lst, lst <> nil -> ~ (exists k, lst = zeros k) ->
cplt2_lst (lst ++ o :: nil) = cplt2_lst lst ++ o :: nil.
Lemma cplt2_lst_involutive_i : forall lst, lst <> nil -> cplt2_lst (lst ++ i :: nil) = cplt1 lst ++ i :: nil.
Lemma two2one : forall lst, length lst > O ->
cplt2_lst (lst ++ o :: nil) = add_lst (cplt1 lst ++ i::nil) (zext_lst (length lst) (i :: nil)) o.
Lemma one2two : forall lst, length lst > 0 ->
add_lst (cplt1 lst ++ i :: nil) (zext_lst (length lst) (i :: nil)) o =
cplt2_lst lst ++ o :: nil.
Lemma cplt2_lst_involutive_o : forall lst, lst <> nil -> ~ (exists k, lst = zeros k) ->
cplt2_lst (lst ++ o :: nil) = cplt2_lst lst ++ o :: nil.
Lemma cplt2_lst_involutive_i : forall lst, lst <> nil -> cplt2_lst (lst ++ i :: nil) = cplt1 lst ++ i :: nil.
two-complement is involutive
Lemma cplt2_lst_involutive : forall lst, cplt2_lst (cplt2_lst lst) = lst.
Lemma cplt2_lst_prop : forall tl, ~ (exists k, tl = zeros k) ->
forall hd, ~ (exists k, hd::tl = i::zeros k) ->
cplt2_lst (hd::tl) = cplt hd :: cplt2_lst tl.
Lemma cplt2_lst_prop : forall tl, ~ (exists k, tl = zeros k) ->
forall hd, ~ (exists k, hd::tl = i::zeros k) ->
cplt2_lst (hd::tl) = cplt hd :: cplt2_lst tl.
unsigned multiplication (result on 2*n bits)
Fixpoint umul_lst (a b:list bool) {struct b} : list bool :=
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 len_umul_lst : forall (a b:list bool), length (umul_lst a b) = length a + length b.
Lemma umul_lst_nil: forall l, umul_lst nil l = zeros (length l).
Lemma umul_lst_zeros : forall n a, umul_lst a (zeros n) = zeros (length a + n).
Lemma umul_lst_leading_o: forall l1 l2, l1 <> nil -> l2 <> nil ->
umul_lst (o :: l1) l2 = o :: umul_lst l1 l2.
Lemma umul_lst_leading_o' : forall l1 l2, l1 <> nil -> l2 <> nil ->
umul_lst l1 (o :: l2) = o :: umul_lst l1 l2.
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.
Lemma umul_lst_com: forall n l2 l1, length l1 = n -> length l2 = n -> n > 0 ->
umul_lst l1 l2 = umul_lst l2 l1.
Lemma umul_lst_zero : forall b a, umul_lst a (b ++ o :: nil) = umul_lst a b ++ o::nil.
Lemma umul_lst_1 : forall l lst, length lst = S l ->
umul_lst lst (zeros l ++ i::nil) = zeros (S l) ++ lst.
Lemma umul_lst_zero_list: forall n l1 l2, umul_lst l1 (l2 ++ zeros n) = umul_lst l1 l2 ++ zeros n.
Lemma umul_lst_weird : forall l, umul_lst (i :: zeros l) (i :: zeros l) = o :: i :: zeros (l + l).
Lemma umul_lst_weird' : forall n l k, length k = n ->
umul_lst k (i :: zeros l) = o :: k ++ zeros l.
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 len_umul_lst : forall (a b:list bool), length (umul_lst a b) = length a + length b.
Lemma umul_lst_nil: forall l, umul_lst nil l = zeros (length l).
Lemma umul_lst_zeros : forall n a, umul_lst a (zeros n) = zeros (length a + n).
Lemma umul_lst_leading_o: forall l1 l2, l1 <> nil -> l2 <> nil ->
umul_lst (o :: l1) l2 = o :: umul_lst l1 l2.
Lemma umul_lst_leading_o' : forall l1 l2, l1 <> nil -> l2 <> nil ->
umul_lst l1 (o :: l2) = o :: umul_lst l1 l2.
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.
Lemma umul_lst_com: forall n l2 l1, length l1 = n -> length l2 = n -> n > 0 ->
umul_lst l1 l2 = umul_lst l2 l1.
Lemma umul_lst_zero : forall b a, umul_lst a (b ++ o :: nil) = umul_lst a b ++ o::nil.
Lemma umul_lst_1 : forall l lst, length lst = S l ->
umul_lst lst (zeros l ++ i::nil) = zeros (S l) ++ lst.
Lemma umul_lst_zero_list: forall n l1 l2, umul_lst l1 (l2 ++ zeros n) = umul_lst l1 l2 ++ zeros n.
Lemma umul_lst_weird : forall l, umul_lst (i :: zeros l) (i :: zeros l) = o :: i :: zeros (l + l).
Lemma umul_lst_weird' : forall n l k, length k = n ->
umul_lst k (i :: zeros l) = o :: k ++ zeros l.
signed multiplication
Definition is_pos (a : list bool) : bool := if a is i :: _ then false else true.
Definition smul_lst (a b:list bool) :=
match is_pos a, is_pos b with
| true, true => umul_lst a b
| false, false => umul_lst (cplt2_lst a) (cplt2_lst b)
| true, false => cplt2_lst (umul_lst a (cplt2_lst b))
| false, true => cplt2_lst (umul_lst (cplt2_lst a) b)
end.
Lemma len_smul_lst : forall n (a b : list bool),
length a = n -> length b = n -> length (smul_lst a b) = 2 * n.
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.
Definition smul_lst (a b:list bool) :=
match is_pos a, is_pos b with
| true, true => umul_lst a b
| false, false => umul_lst (cplt2_lst a) (cplt2_lst b)
| true, false => cplt2_lst (umul_lst a (cplt2_lst b))
| false, true => cplt2_lst (umul_lst (cplt2_lst a) b)
end.
Lemma len_smul_lst : forall n (a b : list bool),
length a = n -> length b = n -> length (smul_lst a b) = 2 * n.
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.
Booth algorithm (definition only)
Definition shift_right_1 := shrl_lst 1.
Fixpoint booth_mul_lst' (a s p : list bool) (n : nat) : list bool :=
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
| o :: i :: _ => booth_mul_lst' a s
(shift_right_1 (add_lst p s o)) m
| _ => nil
end
end.
Fixpoint booth_mul_lst' (a s p : list bool) (n : nat) : list bool :=
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
| o :: i :: _ => booth_mul_lst' a s
(shift_right_1 (add_lst p s o)) m
| _ => nil
end
end.
works only with s =/= weird number
Definition booth_mul_lst (a s : list bool) := idel_last (booth_mul_lst'
(shl_extend_lst (length s + 1) a)
(shl_extend_lst (length s + 1) (cplt2_lst a))
(zext_lst (length a) (shl_extend_lst 1 a))
(length s)).
Lemma len_booth_mul_lst' : forall (k : nat) (a s p : list bool),
length p = length s -> length p = length a -> (1 < length p)%coq_nat ->
length (booth_mul_lst' a s p k) = length p.
Definition len_booth_mul_lst : forall a b, length a = length b ->
0 < length b -> length (booth_mul_lst a b) = 2 * length a.
(shl_extend_lst (length s + 1) a)
(shl_extend_lst (length s + 1) (cplt2_lst a))
(zext_lst (length a) (shl_extend_lst 1 a))
(length s)).
Lemma len_booth_mul_lst' : forall (k : nat) (a s p : list bool),
length p = length s -> length p = length a -> (1 < length p)%coq_nat ->
length (booth_mul_lst' a s p k) = length p.
Definition len_booth_mul_lst : forall a b, length a = length b ->
0 < length b -> length (booth_mul_lst a b) = 2 * length a.
comparisons
Fixpoint listbit_eq a b :=
match (a, b) with
| (hd :: tl, hd' :: tl') => if eqb hd hd' then listbit_eq tl tl' else false
| (nil, nil) => true
| _ => false
end.
Lemma listbit_eq_refl : forall l, listbit_eq l l.
Lemma listbit_eq_eq : forall a b, listbit_eq a b -> a = b.
Fixpoint listbit_lt (a b : list bool) {struct a} : bool :=
match a with
| o :: tla =>
match b with
| o :: tlb => listbit_lt tla tlb
| i :: _ => true
| _ => false
end
| i :: tla =>
match b with
| o :: _ => false
| i :: tlb => listbit_lt tla tlb
| _ => false
end
| _ => false
end.
Lemma listbit_lt_zeros : forall l, listbit_lt l (zeros (length l)) = false.
Definition listbit_le a b := listbit_lt a b || listbit_eq a b.
Lemma listbit_le_0 : forall n lst, length lst = n ->
listbit_le (zeros n) lst.
Lemma listbit_lt_tail : forall n h h' t t', length h = n -> length h' = n ->
listbit_lt (h ++ t :: nil) (h' ++ t' :: nil) ->
listbit_le h h'.
Lemma listbit_lt_min : forall l n, ~ listbit_lt l (zeros n).
Lemma listbit_lt_tail' : forall n hd hd' tl, length hd = n -> length hd' = n ->
listbit_lt (hd ++ tl :: nil) (hd' ++ false :: nil) ->
listbit_lt hd hd'.
End ListBit.
match (a, b) with
| (hd :: tl, hd' :: tl') => if eqb hd hd' then listbit_eq tl tl' else false
| (nil, nil) => true
| _ => false
end.
Lemma listbit_eq_refl : forall l, listbit_eq l l.
Lemma listbit_eq_eq : forall a b, listbit_eq a b -> a = b.
Fixpoint listbit_lt (a b : list bool) {struct a} : bool :=
match a with
| o :: tla =>
match b with
| o :: tlb => listbit_lt tla tlb
| i :: _ => true
| _ => false
end
| i :: tla =>
match b with
| o :: _ => false
| i :: tlb => listbit_lt tla tlb
| _ => false
end
| _ => false
end.
Lemma listbit_lt_zeros : forall l, listbit_lt l (zeros (length l)) = false.
Definition listbit_le a b := listbit_lt a b || listbit_eq a b.
Lemma listbit_le_0 : forall n lst, length lst = n ->
listbit_le (zeros n) lst.
Lemma listbit_lt_tail : forall n h h' t t', length h = n -> length h' = n ->
listbit_lt (h ++ t :: nil) (h' ++ t' :: nil) ->
listbit_le h h'.
Lemma listbit_lt_min : forall l n, ~ listbit_lt l (zeros n).
Lemma listbit_lt_tail' : forall n hd hd' tl, length hd = n -> length hd' = n ->
listbit_lt (hd ++ tl :: nil) (hd' ++ false :: nil) ->
listbit_lt hd hd'.
End ListBit.