Section Vectors.

  Definition data : Set := bool.

  Inductive vector: nat -> Set :=
    | vnil : vector O
    | vcons: forall n, data -> vector n -> vector (S n).

  Eval compute in vnil.
  Eval compute in (vcons 0 true vnil).
  Eval compute in (vcons 1 false (vcons 0 true vnil)).
  Eval compute in (vcons 2 true (vcons 1 false (vcons 0 true vnil))).
  Eval compute in (vcons _ true (vcons _ false (vcons _ true vnil))).

  Fixpoint init (n: nat) (t: data): vector n :=
    match n with
        | O => vnil
        | S m => vcons m t (init m t)
    end.

  Eval compute in (init 10 true).

  Definition first (n: nat) (v: vector (S n)): data :=
    match v with
      | vcons _ d v' => d
    end.

  Eval compute in (first _ (vcons _ false (vcons _ true vnil))).
  Eval compute in (first _ (vcons _ true (vcons _ false (vcons _ true vnil)))).
  (* Eval compute in (first _ vnil). *)
  Eval compute in (first _ (init 10 true)).
  (* Eval compute in (first _ (init 0 true)). *)

  Eval compute in (first _ (init (1 + 1) true)).

  Fixpoint append (n m: nat) (v1: vector n) (v2: vector m): vector (n+m) :=
    match v1 with
        | vnil => v2
        | vcons _ d v1' => vcons _ d (append _ _ v1' v2)
    end.
  (* Print append. *)
  Eval simpl in (append _ _ (init 2 true) (init 3 false)).
  
  
  Theorem append2: forall (n m:nat) (v1: vector n) (v2: vector m),
                     vector (n+m).
    Proof.
      intros. induction v1.
      SearchPattern (_ + _ = _).
      rewrite plus_O_n. assumption.
      Check vcons.
      rewrite plus_Sn_m. apply vcons. assumption. assumption.
    Defined. (* Qed. *)
    Print append2.
    Eval simpl in (append2 _ _ (init 2 true) (init 3 false)).



  Check append _ _ (init 0 true) (init 1 false).
  Check append _ _ (init 0 true) (init 1 false) : vector 1.

  Eval compute in (first _ (append _ _ (init 0 true) (init 1 false))).

  
  
  Fixpoint inject (ls : list data) : vector (length ls) :=
    match ls with
      | nil => vnil
      | cons h t => vcons _ h (inject t)
    end.

  Fixpoint unject n (v: vector n) : list data :=
    match v with
      | vnil => nil
      | vcons _ h t => cons h (unject _ t)
    end.

  Theorem inject_inverse : forall ls, unject _ (inject ls) = ls.
  Proof.
    induction ls. auto.
    unfold unject. simpl. fold unject.
    rewrite IHls. auto.
  Qed.

  Print inject_inverse.

End Vectors.