Coq 无法推断`match` 中的类型参数

问题描述

考虑以下 Coq 程序：

Inductive foo : nat -> Type :=
| nil : foo 0
| succ{n:nat} : foo n -> foo n.

Fixpoint bar {n:nat}(A:foo n)(B:foo n) : Prop :=
  match B with
  | nil => False
  | succ C => bar A C
  end.

Coq 抱怨 bar 的定义：

In environment
bar : forall n : nat,foo n -> foo n -> Prop
n : nat
A : foo n
B : foo n
n0 : nat
C : foo n0
The term "C" has type "foo n0" while it is expected to have type "foo n".

但要使 B : foo n 成为 succ C，C 也必须是 foo n。为什么 Coq 不能推断出这一点，我该如何修正 bar 的定义？

解决方法

当您匹配 B 时，类型系统“忘记”B 类型中的新 n' 与 n 相同。有一个技巧可以将该信息添加到上下文中（有很多方法、插件等，但最好知道如何“手动”完成）。它被称为 "The convoy pattern" by Adam Chlipala，每个 coq 用户都必须在他/她的生活中发布一次关于它的问题（你的真的包括在内）。

您使主体不仅仅是一个值，而是一个函数，它接受类型为 n=n' 的附加输入并在末尾添加一个 eq_refl 项。这与 Coq 的类型系统如何分解术语非常吻合。

您可以使用策略重写 A 类型以将其类型从 foo n 更改为 foo n'，如下所示：


Fixpoint bar (n:nat) (A:foo n) (B:foo n) : Prop.
  refine (
  match B in (foo m) return  (n=m -> _) with
  | nil => fun _ =>  False
  | @succ n' B' => fun (E : n = n') => bar n' _ B'
  end  eq_refl).
  rewrite E in A.
  apply A.
Defined.

或直接使用eq_rect

Fixpoint bar {n:nat} (A:foo n) (B:foo n) : Prop :=
  match B in (foo m) return  (n=m -> _) with
  | nil => fun _ =>  False
  | succ B' => fun E => bar (eq_rect _ _ A _ E) B'
  end  eq_refl.

coq math proof