types - 在 coq 中类型转换可转换类型

Question

在以下内容中:

Lemma test:
  forall n j  (jn : j < n)  (ln : j + 0 < n) (P:  forall {x} {y}, (x<y) -> nat),
    P ln = P jn.

类型 ln 和 jn 似乎可以相互转换(从算术的角度来看)。我怎样才能用这个事实来证明上面的引理呢？我可以很容易地证明 assert(JL: j < n -> j + 0 < n) by auto.但我看不出如何将其应用于类型。

Answer 1

这些类型不能相互转换，因为在 Coq 中定义了自然数加法的方式(即，通过对第一个参数的递归)。事实上，你的引理可以在 Coq 中输入的唯一原因是 P 的第一个隐式参数被实例化为右侧的 j + 0 -手边。

不幸的是，即使这些类型是可转换的，如果没有额外的假设也无法证明这个引理，因为它需要命题外延性公理(见here ，例如)。