为什么 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 无法在类型级别解析任意表达式以避免非终止计算，但我觉得很奇怪，即使是这种简单的情况也没有处理。

我是运行 CoqIDE linux，版本是：

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

您需要 match ... as ... in ... return ... 来做更复杂的类型注释。参见 Adam Chlipala's chapter "Library MoreDep" in his Book "Certified Programming with Dependent Types" or "Chapter 17: Extended pattern-matching" in the Coq manual。两者都有您正在处理的 concat 示例。

您也可以将依赖类型位延迟到最后：

Definition natlist n := { x : list nat & n = length x }.

然后证明非依赖类型 concat 保留长度和。

Answer 2

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

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 抱怨第一个分支，但实际上问题出在第二个分支。正如@jbapple 所建议的那样，在 match 语句中添加注释在尝试诊断问题所在时很有用。

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

Why can't coq infer the that 0+n=n in this dependently typed program?

type-inference

list

coq

dependent-type