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

Question

我开始使用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长度的列表k.串联定义的问题natappend是以下错误:

Error:
In environment
natappend : forall n : nat,
            natlist n ->
            forall m : nat,
            natlist m -> natlist (n + m)
n : nat
l1 : natlist n
m : nat
l2 : natlist m
The term "l2" has type "natlist m"
while it is expected to have type
 "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中编译的没有错误,所以我有点困惑.

是否有一些设置我必须设置为启用更多类型推断并允许上述类型的代码？或者:如何编写不依赖于类型推断的依赖类型代码？

Answer 1

问题是你的第二个分支中有一个类型错误.这是一个有效的版本:

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建议的语句中添加注释在尝试诊断出错时很有用.