Section Zip.

Inductive Vec (A : Set) : nat -> Set :=
| vnil : Vec A 0
| vcons : forall n, A -> Vec A n -> Vec A (S n).

Definition v1 := vcons _ _ 2 (vcons _ _ 3 (vnil _)).
Definition v2 := vcons _ _ true (vcons _ _ false (vnil _)).

(* Implement zipping of vectors, either as term or via the interactive 
proof interface.
*)

Definition head (A : Set) (n : nat) (v : Vec A (S n)) : A.
intros A n v.
inversion v; assumption.
Defined.

Definition tail (A : Set) (n : nat) (v : Vec A (S n)) : Vec A n.
intros A n v.
inversion v; assumption.
Defined.

(* :=
match v in Vec _ (S x) return Vec A x with
| vcons _ x xs => xs
| vnil => vnil _
end.
*)

(*
Fixpoint zip (A B : Set) (n : nat) (v1 : Vec A n) :
  forall (v2 : Vec B n), Vec (A * B) n :=
match v1 in Vec _ m return Vec B m -> Vec (A * B) m with
| vnil => fun _ => vnil _
| vcons n' x xs => fun v2 => 
    match v2 in Vec _ m' return Vec (A * B) m' with
    | vcons _ y ys => vcons _ _ (x,y) (zip _ _ _ xs ys)
    | vnil => vnil _
    end
end.
*)

Fixpoint zip (A B : Set) (n : nat) (v1 : Vec A n) :
  forall (v2 : Vec B n), Vec (A * B) n :=
match v1 in Vec _ m return Vec B m -> Vec (A * B) m with
| vnil => fun _ => vnil _
| vcons n' x xs => fun v2 => 
    vcons _ _ (x , head _ _ v2) (zip _ _ _ xs (tail _ _ v2))
end.

Eval compute in (zip  _ _ _ v1 v2).

Definition zip' (A B : Set) (n : nat) (v1 : Vec A n) (v2 : Vec B n)
  : Vec (A * B) n.
intros A B n v.
induction v.
constructor.
intro v'.
inversion_clear v' as [ | m b bs ].
constructor.
exact (a,b).
exact (IHv bs).
Defined.

Eval compute in (zip' _ _ _ v1 v2).

End Zip.