dhlp.v

Require Import Coq.Init.Nat.


Inductive bit : Set := I | O.

Inductive bits : nat -> Set :=
  | bnil  : bits 0
  | bcons : forall (n : nat), bit -> bits n -> bits (S n).
Arguments bcons [n] _ _.

Require Import List.
Import ListNotations.

Fixpoint from_list (l : list bit) : bits (length l) :=
  match l with
  | [] => bnil
  | b :: l' => bcons b (from_list l')
  end.

Fixpoint to_list {n : nat} (bs : bits n) : list bit :=
  match bs with
  | bnil => []
  | bcons b bs' => b :: (to_list bs')
  end.

Fixpoint bits_list (l : list nat) : bits (length l) :=
  match l with
  | [] => bnil
  | 0 :: l' => bcons O (bits_list l')
  | _ :: l' => bcons I (bits_list l')
  end.

Fixpoint list_bits {n : nat} (bs : bits n) : list nat :=
  match bs with
  | bnil => []
  | bcons O bs' => 0 :: (list_bits bs')
  | bcons I bs' => 1 :: (list_bits bs')
  end.

Definition my_bs := bits_list [1; 1; 0; 1; 1].
Compute my_bs.

Definition bits_length {n : nat} (bs : bits n) := n.


Definition bits_head {n : nat} (bs : bits (S n)) : bit :=
  match bs with
  | bcons b _ => b
  end.


Definition bits_tail {n : nat} (bs : bits (S n)) : bits n :=
  match bs with
  | bcons _ bs' => bs'
  end.

Definition bits_uncons {n : nat} (bs : bits (S n)) : bit * bits n := (bits_head bs, bits_tail bs).

Fixpoint bits_app {n m : nat} (b1 : bits n) (b2 : bits m) : bits (n + m) :=
  match b1 (*in (bits n) return (bits (n + m))*) with
  | bnil => b2
  | bcons b b1' => bcons b (bits_app b1' b2)
  end.



Definition bit_bin_op : Type := bit -> bit -> bit.

Definition bits_uncons2 {n : nat} (bs cs : bits (S n)) : (bit * bits n) * (bit * bits n) :=
  match bs,cs with
  | bcons b bs',bcons c cs' => ((b,bs'),(c,cs'))
  end.

Check bits_uncons2.

Fixpoint bits_map {n : nat} (f : bit -> bit) (bs : bits n) : bits n :=
  match bs with
  | bnil => bnil
  | bcons b bs' => bcons (f b) (bits_map f bs')
  end.


Fixpoint zip_with {A B C : Type} (f : A -> B -> C)
  (l1 : list A) (l2 : list B) : list C :=
  match l1, l2 with
  | [], _ => []
  | _, [] => []
  | x :: xs, y :: ys => f x y :: zip_with f xs ys
  end.

Fixpoint zipWith {n : nat} (f : bit -> bit -> bit)
  (v1 : bits n) (v2 : bits n) : bits n.
  induction n.
  - exact bnil.
  - inversion v1. inversion v2.
    rewrite <- H in * |- .
    rewrite H in * |- .
    apply bcons.
    exact (f H0 H3).
    exact (IHn H1 H4).
Defined.
Print zipWith.

(*I couldn't figure this one out. Just learned about proof mode for functions. This is great. But I suspect it will be impossible to prove things about this function. *)