Dependent pattern matching - zip two vectors

Question

How to zip two vectors in Coq? I tried the code below, but stuck into a problem:

Require Import Vectors.Vector.
Import VectorNotations.

(* Non exhaustive pattern-matching: no clause found for patterns [], _ :: _ *)
Fail Fixpoint zip {A B : Type} {n : nat} (a : t A n) (b : t B n) : t (A * B) n :=
match a, b with
| ha :: ta, hb :: tb => (ha, hb) :: zip ta tb
| [], [] => []
end.

(* The term "tb" has type "t B n1" while it is expected to have type "t B n0"
   (cannot unify "n1" and "n0"). *)
Fail Fixpoint zip {A B : Type} {n : nat} (a : t A n) (b : t B n) : t (A * B) n :=
match a, b with
| ha :: ta, hb :: tb => (ha, hb) :: zip ta tb
| _, _ => []
end.

(* The term "a" has type "t A n" while it is expected to have type "t A (S k)". *)
Fail Fixpoint zip {A B : Type} {n : nat} (a : t A n) (b : t B n) : t (A * B) n :=
match n with
| (S k) => ((fst (uncons (a : t A (S k)))), (fst (uncons b))) ::
           zip (snd (uncons a)) (snd (uncons b))
| O => []
end.

So how to make the typechecker to assume the lengths of the two vectors are equal?

Answer 1

You can use the convoy pattern (see also a similar question):

From Coq Require Vector.
Import Vector.VectorNotations.

Fixpoint zip {A B : Type} {n : nat} (a : Vector.t A n) (b : Vector.t B n) : Vector.t (A * B) n :=
match a in Vector.t _ n return Vector.t B n -> Vector.t (A * B) n  with
| ha :: ta => fun b => (ha, Vector.hd b) :: zip ta (Vector.tl b)
| [] => fun _ => []
end b.