在 Coq 中实现向量加法

Question

在某些依赖类型的语言（例如 Idris）中实现向量加法非常简单。根据 example on Wikipedia:

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 libraries:

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 与 n1 统一起来。

我做错了什么？

Answer 1

在普通 Coq 中不可能如此轻松地实现此函数：您需要使用 convoy 模式 重写您的函数。不久前有一个 similar question 发布了关于这个的帖子。这个想法是你需要让你的 match return 成为一个函数来传播索引之间的关系：

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.

在 Coq 中实现向量加法

Implementing vector addition in Coq

vector

coq

idris

convoy-pattern