gpt4 book ai didi

vector - 依赖模式匹配 - 压缩两个向量

转载 作者:行者123 更新时间:2023-12-05 02:09:59 26 4
gpt4 key购买 nike

如何在 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.

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

最佳答案

您可以使用护航模式(另请参阅类似的 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.

关于vector - 依赖模式匹配 - 压缩两个向量,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/59290356/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com