删除Coq中大小列表的最后一个元素

Question

考虑以下大小列表的类型定义：

Inductive listn: nat -> Type -> Type :=
| nil: forall {A: Set}, listn 0 A
| cons: forall {n: nat} {A: Set}, A -> listn n A -> listn (S n) A.

这本质上是Idris中的Vect类型。

我正在尝试为listn定义init函数，它删除了最后一个元素。

我尝试的实现实际上与Idris中init的定义完全相同。这是在伊德里斯：

init : Vect (S len) elem -> Vect len elem
init (x::[])    = []
init (x::y::ys) = x :: init (y::ys)

转录到Coq:

Fixpoint init {n: nat} {A: Set} (l: listn (S n) A): listn n A :=
match l with
| cons x nil => nil
| cons x (cons y ys) => cons x (init (cons y ys))
end.

…但这失败了：

The term "nil" has type "listn 0 ?A"
while it is expected to have type "listn ?n ?S@{a0:=S}"
(cannot unify "?n" and "0").

我认为Coq不能看到这种情况必然意味着n为零。这是我一直遇到的一个问题——Coq无法看到n和列表本身之间的关系。

因此，我提出了以下问题：

• 如何在Coq中实现init
• 为什么Idris定义在Idris中有效，而在Coq中无效？Idris在幕后做什么，而Coq不是

Answer 1

就其本身而言，Coq不太适合编写此类代码，但您可以使用Equations插件使其更简单。尽管如此，让我们看看如何在没有外部依赖的情况下做到这一点：

Require Import Coq.Vectors.Vector.
(* Vector.t is equivalent to your listn type *)
Arguments nil {A}.
Arguments cons {A} _ {n}.
Fixpoint init {n: nat} {A: Set} (xs: Vector.t A (S n)): Vector.t A n :=
match xs in Vector.t _ m return Vector.t A (pred m) with
| nil => nil
| cons x xs =>
match xs in Vector.t _ m return Vector.t A m -> Vector.t A m with
| nil      => fun _  => nil
| cons _ _ => fun xs => cons x (init xs)
end xs
end.

这个定义与您的定义有几个不同之处。首先，我们需要对match的返回类型进行注释，以解释它如何取决于向量的长度。in Vector.t _ m部分说，返回类型是向量长度上的泛型——我们不能假设长度的形式为S n。

其次，我们必须列举数据类型的所有情况：match在Coq中总是穷举的，即使某些分支由于键入信息而无法访问。因此，我在第一个匹配中包含了nil的情况。

第三，Coq无法识别init (cons y ys)是有效的递归调用。我们通过在销毁cons y ys之前给它一个名称xs并使用init xs来修复此问题。然而，有一个微妙之处。在cons x xs中，对于某些m，xs的类型是Vector.t A m，它可能是也可能不是后继，所以我们不能直接调用init。相反，我们首先销毁xs，并仅对cons分支执行递归调用。但是，由于match的长度参数是通用的，Coq看不到xs在match内外的长度之间的联系。解决方案是执行Adam Chlipala所称的保护模式：我们使match返回一个函数而不是一个普通向量，并将xs作为match之外的参数传递。这样，两个长度之间的连接就不会丢失。

我对Idris了解不多，但我猜测它的类型检查算法比Coq的更复杂，这就是为什么它可以判断类似的定义是有效的。老实说，库克的规则非常简单(而且是有限的(。