Coq 无法在 `match` 中推断类型参数答案

【问题标题】：Coq can't infer type parameter in `match`Coq 无法在 `match` 中推断类型参数
【发布时间】：2021-03-31 03:31:43
【问题描述】：

考虑以下 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 的定义？

【问题讨论】：

标签： math coq proof

【解决方案1】：

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

你让body不仅仅是一个值，而是一个函数，它接受一个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.

【讨论】：