Require Import Bool Arith Div2 List.
Require Import BellantoniCook.Lib.

Notation bs := (list bool).

Definition unary (v : bs) := forallb id v.

(** * Boolean interpretation of bitstrings *)

Definition bs2bool (v:bs) : bool := hd false v.

Definition bool2bs (b:bool) : bs :=
  if b then true::nil else nil.

Lemma bs_nat2bool_true : forall v,
  bs2bool v = true -> length v <> 0.
Proof.
(* Goal: forall (v : list bool) (_ : @eq bool (bs2bool v) true), not (@eq nat (@length bool v) O) *)
 intro v; case v; simpl; auto; intros; discriminate.
Qed.

Lemma bs_nat2bool_true_conv : forall v,
  unary v = true ->
  length v <> 0 -> bs2bool v = true.
Proof.
(* Goal: forall (v : list bool) (_ : @eq bool (unary v) true) (_ : not (@eq nat (@length bool v) O)), @eq bool (bs2bool v) true *)
 intro v; case v; simpl; intros.
(* Goal: @eq bool false true *)
(* Goal: @eq bool b true *)
 elim H0; trivial.
(* Goal: @eq nat (S (@length bool v)) O *)
 rewrite andb_true_iff in H.
(* Goal: @eq bool b true *)
 decompose [and] H; destruct b; trivial.
Qed.

Lemma bs_nat2bool_false v :
  unary v = true ->
  bs2bool v = false -> length v = 0.
Proof.
(* Goal: forall _ : @eq nat (@length bool v) O, @eq bool (bs2bool v) false *)
 destruct v; simpl; trivial; intros.
(* Goal: @eq nat (S (@length bool v)) O *)
 rewrite andb_true_iff in H.
(* Goal: @eq nat (S (@length bool v)) O *)
 decompose [and] H; destruct b; discriminate.
Qed.

Lemma bs_nat2bool_false_conv v :
  length v = 0 ->
  bs2bool v = false.
Proof.
(* Goal: forall _ : @eq nat (@length bool v) O, @eq bool (bs2bool v) false *)
 destruct v; simpl; trivial; intros.
(* Goal: @eq bool b false *)
 discriminate.
Qed.

(** * Binary interpretation of bitstrings *)

Fixpoint bs2nat (v:bs) : nat :=
  match v with
  | nil => 0
  | false :: v' => 2 * bs2nat v'
  | true  :: v' => S (2 * bs2nat v')
  end.

Fixpoint succ_bs (v : bs) : bs :=
  match v with
    | nil => [true]
    | false :: v' => true :: v'
    | true :: v' => false :: succ_bs v'
  end.

Lemma succ_bs_correct v : bs2nat (succ_bs v) = bs2nat v + 1.
Proof.
(* Goal: @eq nat (bs2nat (succ_bs v)) (Init.Nat.add (bs2nat v) (S O)) *)
 induction v; simpl; trivial; case a; simpl; ring [IHv].
Qed.

Fixpoint nat2bs (n:nat) : bs :=
  match n with
  | 0 => nil
  | S n' => succ_bs (nat2bs n')
  end.

Lemma bs2nat_nil :
  bs2nat nil = 0.
Proof. trivial. Qed.

Lemma bs2nat_false v :
  bs2nat (false :: v) = 2 * bs2nat v.
Proof. trivial. Qed.

Lemma bs2nat_true v :
  bs2nat (true :: v) = 1 + 2 * bs2nat v.
Proof. trivial. Qed.

Lemma bs2nat_tl : forall v, bs2nat (tl v) = div2 (bs2nat v).
Proof.
(* Goal: forall v : list bool, @eq nat (bs2nat (@tl bool v)) (Nat.div2 (bs2nat v)) *)
 destruct v; simpl; [ trivial | ].
(* Goal: @eq nat (bs2nat v) (Nat.div2 (if b then S (Init.Nat.add (bs2nat v) (Init.Nat.add (bs2nat v) O)) else Init.Nat.add (bs2nat v) (Init.Nat.add (bs2nat v) O))) *)
 replace (bs2nat v + (bs2nat v + 0)) with (2 * bs2nat v) by omega.
(* Goal: @eq nat (bs2nat (@cons bool true v)) (Init.Nat.add (S O) (Init.Nat.mul (S (S O)) (bs2nat v))) *)
 case b;[ rewrite div2_double_plus_one | rewrite div2_double]; trivial.
Qed.

Lemma bs2nat_nat2bs : forall n, bs2nat (nat2bs n) = n.
Proof.
(* Goal: forall n : nat, @eq nat (bs2nat (nat2bs n)) n *)
 induction n as [ | n' IHn]; simpl; auto.
(* Goal: @eq nat (bs2nat (succ_bs (nat2bs n'))) (S n') *)
 rewrite succ_bs_correct; ring [IHn].
Qed.
