依赖模式匹配 - zip 两个向量

Question

如何在 Coq 中压缩两个向量？我尝试了下面的代码，但遇到了问题：

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.

那么如何让类型检查器假设两个向量的长度相等呢？

Answer 1

您可以使用护航模式（另请参阅类似的问题）：

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.