Require Import Bool Arith Div2.
Require Import BellantoniCook.Lib BellantoniCook.Bitstring BellantoniCook.BC.

(** * Zero

  - with any arities (n, s)
*)

Definition zero_e (n s:nat) : BC :=
  comp n s zero nil nil.

Lemma zero_correct n s l1 l2: 
 bs2nat (sem (zero_e n s) l1 l2) = 0.
(* Goal: @eq nat (bs2nat (sem (zero_e n s) l1 l2)) O *)
Proof. intros; simpl; trivial. Qed.

(** * One

  - with any arities (n, s)
*)

Definition one_e n s :=
  comp n s (comp 0 0 (succ true) nil [zero]) nil nil.

(** * Successor

  - arities: (1, 0)
*)

Definition succ_e : BC :=
  rec (one_e 0 0)
      (comp 1 1 (succ true) nil [proj 1 1 0])
      (comp 1 1 (succ false) nil [proj 1 1 1]).

Lemma succ_correct :
  forall n, bs2nat (sem succ_e [n] nil) = S (bs2nat n).
Proof.
(* Goal: forall n : list bool, @eq nat (bs2nat (sem succ_e (@cons (list bool) n (@nil (list bool))) (@nil (list bool)))) (S (bs2nat n)) *)
 induction n; simpl in *; trivial.
(* Goal: @eq nat (bs2nat (if a then @cons bool false (sem_rec (fun _ _ : list (list bool) => @cons bool true (@nil bool)) (fun vnl _ : list (list bool) => @cons bool true (@List.nth (list bool) O vnl (@nil bool))) (fun _ vsl : list (list bool) => @cons bool false (@List.nth (list bool) O vsl (@nil bool))) n (@nil (list bool)) (@nil (list bool))) else @cons bool true n)) (S (if a then S (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) else Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
 case a; simpl; [rewrite IHn | ]; ring.
Qed.

Global Opaque succ_e.

(** * Zero predicate

  - arities: (1,0)
*)

Definition is_zero_e : BC :=
  rec (one_e 0 0) (proj 1 1 1) (zero_e 1 1).

Lemma is_zero_correct v :
  bs2bool (sem is_zero_e [v] nil) = true <->
  bs2nat v = 0.
Proof.
(* Goal: iff (@eq bool (bs2bool (sem is_zero_e (@cons (list bool) v (@nil (list bool))) (@nil (list bool)))) true) (@eq nat (bs2nat v) O) *)
 intros; split; induction v; simpl; trivial.
(* Goal: forall _ : @eq nat (if a 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)) O, @eq bool (bs2bool (if a then @nil bool else sem_rec (fun _ _ : list (list bool) => @cons bool true (@nil bool)) (fun _ vsl : list (list bool) => @List.nth (list bool) O vsl (@nil bool)) (fun _ _ : list (list bool) => @nil bool) v (@nil (list bool)) (@nil (list bool)))) true *)
 case a; intros; simpl in *.
(* Goal: @eq nat (S (Init.Nat.add (bs2nat v) (Init.Nat.add (bs2nat v) O))) O *)
(* Goal: @eq nat (Init.Nat.add (bs2nat v) (Init.Nat.add (bs2nat v) O)) O *)
(* Goal: forall _ : @eq nat (if a 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)) O, @eq bool (bs2bool (if a then @nil bool else sem_rec (fun _ _ : list (list bool) => @cons bool true (@nil bool)) (fun _ vsl : list (list bool) => @List.nth (list bool) O vsl (@nil bool)) (fun _ _ : list (list bool) => @nil bool) v (@nil (list bool)) (@nil (list bool)))) true *)
 discriminate.
(* Goal: @eq nat (Init.Nat.add (bs2nat v) (Init.Nat.add (bs2nat v) O)) O *)
(* Goal: forall _ : @eq nat (if a 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)) O, @eq bool (bs2bool (if a then @nil bool else sem_rec (fun _ _ : list (list bool) => @cons bool true (@nil bool)) (fun _ vsl : list (list bool) => @List.nth (list bool) O vsl (@nil bool)) (fun _ _ : list (list bool) => @nil bool) v (@nil (list bool)) (@nil (list bool)))) true *)
 rewrite IHv; trivial.
(* Goal: forall _ : @eq nat (if a 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)) O, @eq bool (bs2bool (if a then @nil bool else sem_rec (fun _ _ : list (list bool) => @cons bool true (@nil bool)) (fun _ vsl : list (list bool) => @List.nth (list bool) O vsl (@nil bool)) (fun _ _ : list (list bool) => @nil bool) v (@nil (list bool)) (@nil (list bool)))) true *)
 case a; intros; simpl in *.
(* Goal: @eq bool false true *)
(* Goal: @eq bool (bs2bool (sem_rec (fun _ _ : list (list bool) => @cons bool true (@nil bool)) (fun _ vsl : list (list bool) => @List.nth (list bool) O vsl (@nil bool)) (fun _ _ : list (list bool) => @nil bool) v (@nil (list bool)) (@nil (list bool)))) true *)
 contradict H; omega.
(* Goal: @eq bool (bs2bool (sem_rec (fun _ _ : list (list bool) => @cons bool true (@nil bool)) (fun _ vsl : list (list bool) => @List.nth (list bool) O vsl (@nil bool)) (fun _ _ : list (list bool) => @nil bool) v (@nil (list bool)) (@nil (list bool)))) true *)
 apply IHv; omega.
Qed.

Lemma is_zero_correct_conv v :
  bs2bool (sem is_zero_e [v] nil) = false <->
  bs2nat v <> 0.
Proof.
(* Goal: iff (@eq bool (bs2bool (sem is_zero_e (@cons (list bool) v (@nil (list bool))) (@nil (list bool)))) false) (not (@eq nat (bs2nat v) O)) *)
 intros; split; intros. intro.
(* Goal: @eq nat (bs2nat (@nil bool)) (Init.Nat.pred (bs2nat n)) *)
(* Goal: @eq nat (bs2nat (sem pred_pos_e (@cons (list bool) n (@nil (list bool))) (@nil (list bool)))) (Init.Nat.pred (bs2nat n)) *)
 apply is_zero_correct in H0.
(* Goal: @eq nat (S (Init.Nat.add (bs2nat v) (Init.Nat.add (bs2nat v) O))) O *)
(* Goal: @eq nat (Init.Nat.add (bs2nat v) (Init.Nat.add (bs2nat v) O)) O *)
(* Goal: forall _ : @eq nat (if a 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)) O, @eq bool (bs2bool (if a then @nil bool else sem_rec (fun _ _ : list (list bool) => @cons bool true (@nil bool)) (fun _ vsl : list (list bool) => @List.nth (list bool) O vsl (@nil bool)) (fun _ _ : list (list bool) => @nil bool) v (@nil (list bool)) (@nil (list bool)))) true *)
 rewrite H in H0; discriminate.
(* Goal: @eq bool (bs2bool (sem is_zero_e (@cons (list bool) v (@nil (list bool))) (@nil (list bool)))) false *)
 apply not_true_is_false.
(* Goal: @eq nat (bs2nat (@nil bool)) (Init.Nat.pred (bs2nat n)) *)
(* Goal: @eq nat (bs2nat (sem pred_pos_e (@cons (list bool) n (@nil (list bool))) (@nil (list bool)))) (Init.Nat.pred (bs2nat n)) *)
 intro; apply is_zero_correct in H0.
(* Goal: False *)
 rewrite H0 in H; auto.
Qed.

Global Opaque is_zero_e.

(** * Predecessor

  - arities: (1,0)
*)

Definition pred_pos_e : BC :=
  rec (zero_e 0 0)
      (comp 1 1 (succ true) nil [proj 1 1 1])
      (comp 1 1 (succ false) nil [proj 1 1 0]).

Lemma pred_pos_correct n :
  bs2nat n <> 0 ->  
  bs2nat (sem pred_pos_e [n] nil) = Peano.pred (bs2nat n).
Proof.
(* Goal: forall n : list bool, @eq nat (bs2nat (sem succ_e (@cons (list bool) n (@nil (list bool))) (@nil (list bool)))) (S (bs2nat n)) *)
 intros; induction n; simpl in *; trivial.
(* Goal: @eq nat (bs2nat (if a then @cons bool false n else @cons bool true (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool))))) (Init.Nat.pred (if a then S (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) else Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
 destruct a; simpl.
(* Goal: @eq nat (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) *)
(* Goal: @eq nat (S (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) O))) (Init.Nat.pred (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
 trivial.
(* Goal: @eq nat (S (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) O))) (Init.Nat.pred (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
 rewrite IHn.
(* Goal: @eq nat (S (Init.Nat.add (Init.Nat.pred (bs2nat n)) (Init.Nat.add (Init.Nat.pred (bs2nat n)) O))) (Init.Nat.pred (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
(* Goal: not (@eq nat (bs2nat n) O) *)
 destruct (bs2nat n).
(* Goal: @eq nat (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) *)
(* Goal: @eq nat (S (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) O))) (Init.Nat.pred (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
 elim H; trivial.
(* Goal: @eq nat (S (Init.Nat.add (Init.Nat.pred (S n0)) (Init.Nat.add (Init.Nat.pred (S n0)) O))) (Init.Nat.pred (Init.Nat.add (S n0) (Init.Nat.add (S n0) O))) *)
(* Goal: not (@eq nat (bs2nat n) O) *)
 simpl.
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (bs2nat l)) (Init.Nat.add (bs2nat l) (Init.Nat.add (bs2nat l) O)) *)
(* Goal: @eq nat (bs2nat l) (Nat.div2 (Init.Nat.add (bs2nat l) (Init.Nat.add (bs2nat l) O))) *)
 ring.
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (bs2nat l)) (Init.Nat.add (bs2nat l) (Init.Nat.add (bs2nat l) O)) *)
 omega.
Qed.

Global Opaque pred_pos_e.

Definition pred_e : BC :=
  comp 1 0 cond 
       nil [is_zero_e; pred_pos_e; zero_e 1 0; pred_pos_e].

Lemma pred_correct n :
  bs2nat (sem pred_e [n] nil) = Peano.pred (bs2nat n).
Proof.
(* Goal: @eq nat (bs2nat (sem pred_e (@cons (list bool) n (@nil (list bool))) (@nil (list bool)))) (Init.Nat.pred (bs2nat n)) *)
 simpl; intros.
(* Goal: @eq nat (bs2nat match sem is_zero_e (@cons (list bool) n (@nil (list bool))) (@nil (list bool)) with | nil => sem pred_pos_e (@cons (list bool) n (@nil (list bool))) (@nil (list bool)) | cons (true as b) l => @nil bool | cons (false as b) l => sem pred_pos_e (@cons (list bool) n (@nil (list bool))) (@nil (list bool)) end) (Init.Nat.pred (bs2nat n)) *)
 case_eq (sem is_zero_e [n] nil); intros.
(* Goal: @eq nat (bs2nat (sem pred_pos_e (@cons (list bool) n (@nil (list bool))) (@nil (list bool)))) (Init.Nat.pred (bs2nat n)) *)
 assert (bs2bool (sem is_zero_e [n] nil) = false).
(* Goal: @eq nat (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) *)
(* Goal: @eq nat (S (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) O))) (Init.Nat.pred (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
 rewrite H; simpl; trivial.
 apply is_zero_correct_conv  in H0.
(* Goal: @eq nat (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) *)
(* Goal: @eq nat (S (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) O))) (Init.Nat.pred (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
 apply pred_pos_correct; trivial.
(* Goal: @eq nat (bs2nat (if b then @nil bool else sem pred_pos_e (@cons (list bool) n (@nil (list bool))) (@nil (list bool)))) (Init.Nat.pred (bs2nat n)) *)
 destruct b.
(* Goal: @eq nat (bs2nat (@nil bool)) (Init.Nat.pred (bs2nat n)) *)
(* Goal: @eq nat (bs2nat (sem pred_pos_e (@cons (list bool) n (@nil (list bool))) (@nil (list bool)))) (Init.Nat.pred (bs2nat n)) *)
 assert (bs2bool (sem is_zero_e [n] nil) = true).
(* Goal: @eq nat (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) *)
(* Goal: @eq nat (S (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) O))) (Init.Nat.pred (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
 rewrite H; simpl; trivial.
 apply is_zero_correct  in H0.
(* Goal: @eq nat (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) *)
(* Goal: @eq nat (S (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) O))) (Init.Nat.pred (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
 rewrite H0; simpl; trivial.
(* Goal: @eq nat (bs2nat (sem pred_pos_e (@cons (list bool) n (@nil (list bool))) (@nil (list bool)))) (Init.Nat.pred (bs2nat n)) *)
 assert (bs2bool (sem is_zero_e [n] nil) = false).
(* Goal: @eq nat (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) *)
(* Goal: @eq nat (S (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) O))) (Init.Nat.pred (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
 rewrite H; simpl; trivial.
 apply is_zero_correct_conv  in H0.
(* Goal: @eq nat (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) *)
(* Goal: @eq nat (S (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) O))) (Init.Nat.pred (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
 apply pred_pos_correct; trivial.
Qed.

Global Opaque pred_e.

(** * Division by 2

  - arities: (1,0)
*)

Notation div2_e := pred.

Lemma div2_correct : forall v,
  bs2nat (sem pred nil [v]) = div2 (bs2nat v).
Proof.
(* Goal: forall v : list bool, @eq nat (bs2nat (sem pred (@nil (list bool)) (@cons (list bool) v (@nil (list bool))))) (Nat.div2 (bs2nat v)) *)
 intros v; case v; simpl; trivial; intros.
(* Goal: @eq nat (bs2nat l) (Nat.div2 (if b then S (Init.Nat.add (bs2nat l) (Init.Nat.add (bs2nat l) O)) else Init.Nat.add (bs2nat l) (Init.Nat.add (bs2nat l) O))) *)
 case b.
(* Goal: @eq nat (bs2nat l) (Nat.div2 (Init.Nat.add (bs2nat l) (Init.Nat.add (bs2nat l) O))) *)
 replace (bs2nat l + (bs2nat l + 0)) with (2 * (bs2nat l)).
(* Goal: @eq nat (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) *)
(* Goal: @eq nat (S (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) O))) (Init.Nat.pred (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
 rewrite div2_double_plus_one; trivial.
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (bs2nat l)) (Init.Nat.add (bs2nat l) (Init.Nat.add (bs2nat l) O)) *)
(* Goal: @eq nat (bs2nat l) (Nat.div2 (Init.Nat.add (bs2nat l) (Init.Nat.add (bs2nat l) O))) *)
 ring.
(* Goal: @eq nat (bs2nat l) (Nat.div2 (Init.Nat.add (bs2nat l) (Init.Nat.add (bs2nat l) O))) *)
 replace (bs2nat l + (bs2nat l + 0)) with (2 * (bs2nat l)).
(* Goal: @eq nat (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O)) *)
(* Goal: @eq nat (S (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) (Init.Nat.add (bs2nat (sem_rec (fun _ _ : list (list bool) => @nil bool) (fun _ vsl : list (list bool) => @cons bool true (@List.nth (list bool) O vsl (@nil bool))) (fun vnl _ : list (list bool) => @cons bool false (@List.nth (list bool) O vnl (@nil bool))) n (@nil (list bool)) (@nil (list bool)))) O))) (Init.Nat.pred (Init.Nat.add (bs2nat n) (Init.Nat.add (bs2nat n) O))) *)
 rewrite div2_double; trivial.
(* Goal: @eq nat (Init.Nat.mul (S (S O)) (bs2nat l)) (Init.Nat.add (bs2nat l) (Init.Nat.add (bs2nat l) O)) *)
 omega.
Qed.
