为什么不能在这个依赖类型的程序中求和推断0 + n = n？

Bakuriu 发表于 Dev

巴库留

我开始使用Coq，我想定义一些依赖类型的程序。考虑以下：

Inductive natlist : nat -> Type :=
  | natnil : natlist 0
  | natcons : forall k, nat -> natlist k -> natlist (S k).

Fixpoint natappend (n:nat) (l1: natlist n) (m:nat) (l2: natlist m) : natlist (n+m) :=
  match l1 with
    | natnil => l2
    | natcons _ x rest => natcons (n+m) x (natappend rest l2)
  end.

因此，natlist k将是一个nat长度为s的列表k。串联定义的问题natappend是以下错误：

错误：
在环境中
natappend：全部n：nat，
            natlist n->
            forall m：nat，
            natlist m-> natlist（n + m）
n：自然
l1：纳豆
m：纳特
l2：纳豆
术语“ l2”的类型为“ natlist m”
虽然应该有类型
 “ natlist（？n @ {n1：= 0} + m）”。

如您所见，该子句存在问题：

| natnil => l2

因为它声称的类型为l2，natlist m而结果类型必须为natlist (n+m) = natlist (0+m)。

我知道Coq不能在类型级别解析任意表达式以避免非终止计算，但是我感到奇怪的是，即使这种简单的情况也无法解决。

我在Linux上运行CoqIDE，版本为：

The Coq Proof Assistant, version 8.5 (February 2016)
  compiled on Feb 22 2016 18:19:5 with OCaml 4.02.2

我已经看到了使用MacOSX版本的实时类，其代码类似于上面在IDE中编译的代码，并且没有该错误，所以我有些困惑。

我必须设置一些设置以启用更多类型推断并允许上述类型的代码吗？或者：如何编写不依赖类型推断的依赖类型代码？

亚瑟·阿兹维多·德·阿莫林

问题是您在第二个分支中有类型错误。这是一个有效的版本：

Fixpoint natappend {n m:nat} (l1 : natlist n) (l2 : natlist m) : natlist (n + m) :=
  match l1 with
  | natnil => l2
  | natcons n' x rest => natcons (n' + m) x (natappend rest l2)
  end.

此版本与原始版本之间的关键区别是传递给的参数natcons：此处为n' + m，而之前为n + m。

此示例很好地说明了Coq中错误消息的非本地性的一个普遍问题，尤其是在编写依赖类型的程序时。即使Coq抱怨第一分支，问题实际上出在第二分支。match如@jbapple所建议，在语句中添加注释在尝试诊断出问题时会很有用。

本文收集自互联网，转载请注明来源。

如有侵权，请联系[email protected] 删除。