在某些依赖类型语言(例如 Idris)中实现向量加法相当简单。根据维基百科上的例子:
import Data.Vect
%default total
pairAdd : Num a => Vect n a -> Vect n a -> Vect n a
pairAdd Nil Nil = Nil
pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys
(注意 Idris 的完整性检查器如何自动推断添加Nil
和非Nil
向量在逻辑上是不可能的。)
我正在尝试使用自定义向量实现在 Coq 中实现等效功能,尽管与官方提供的非常相似Coq 库:
Set Implicit Arguments.
Inductive vector (X : Type) : nat -> Type :=
| vnul : vector X 0
| vcons {n : nat} (h : X) (v : vector X n) : vector X (S n).
Arguments vnul [X].
Fixpoint vpadd {n : nat} (v1 v2 : vector nat n) : vector nat n :=
match v1 with
| vnul => vnul
| vcons _ x1 v1' =>
match v2 with
| vnul => False_rect _ _
| vcons _ x2 v2' => vcons (x1 + x2) (vpadd v1' v2')
end
end.
当 Coq 尝试检查时vpadd
,它会产生以下错误:
Error:
In environment
vpadd : forall n : nat, vector nat n -> vector nat n -> vector nat n
[... other types]
n0 : nat
v1' : vector nat n0
n1 : nat
v2' : vector nat n1
The term "v2'" has type "vector nat n1" while it is expected to have type "vector nat n0".
请注意,我使用False_rect
指定不可能的情况,否则完整性检查将无法通过。然而,由于某种原因,类型检查器无法统一n0
with n1
.
我究竟做错了什么?
在普通 Coq 中不可能如此轻松地实现这个函数:您需要使用以下代码重写您的函数车队模式。有一个类似的问题不久前发布了关于此的内容。这个想法是你需要让你的match
返回一个函数以传播索引之间的关系:
Set Implicit Arguments.
Inductive vector (X : Type) : nat -> Type :=
| vnul : vector X 0
| vcons {n : nat} (h : X) (v : vector X n) : vector X (S n).
Arguments vnul [X].
Definition vhd (X : Type) n (v : vector X (S n)) : X :=
match v with
| vcons _ h _ => h
end.
Definition vtl (X : Type) n (v : vector X (S n)) : vector X n :=
match v with
| vcons _ _ tl => tl
end.
Fixpoint vpadd {n : nat} (v1 v2 : vector nat n) : vector nat n :=
match v1 in vector _ n return vector nat n -> vector nat n with
| vnul => fun _ => vnul
| vcons _ x1 v1' => fun v2 => vcons (x1 + vhd v2) (vpadd v1' (vtl v2))
end v2.
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)