在Coq中实现向量加法 [英] Implementing vector addition in Coq

问题描述

在某些依赖类型的语言（例如Idris）中实现向量加法非常简单。按照 Wikipedia上的示例：

Implementing vector addition in some of the dependently typed languages (such as Idris) is fairly straightforward. As per the 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 向量在逻辑上是不可能的。）

(Note how Idris' totality checker automatically infers that addition of Nil and non-Nil vectors is a logical impossibility.)

我正在尝试使用自定义向量实现在Coq中实现等效功能，尽管与官方 Coq库中提供的类似：

I am trying to implement the equivalent functionality in Coq, using a custom vector implementation, albeit very similar to the one provided in the official 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 时，产生以下错误：

When Coq attempts to check vpadd, it yields the following error:

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 统一。

Note that, I use False_rect to specify the impossible case, otherwise the totality check wouldn't pass. However, for some reason the type checker doesn't manage to unify n0 with n1.

我在做什么错了？

推荐答案

在普通的Coq中轻松实现此功能：您需要使用 convoy模式重写函数。不久前，发布了一个类似问题。这个想法是，您需要使 match 返回一个函数，以便传播索引之间的关系：

It's not possible to implement this function so easily in plain Coq: you need to rewrite your function using the convoy pattern. There was a similar question posted a while ago about this. The idea is that you need to make your match return a function in order to propagate the relation between the indices:

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中实现向量加法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！