在 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.

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

Answer 1

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

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

Answer 2

引理无法证明。尝试 intros. remember (j+0) as Q. rewrite <- plus_n_O in HeqQ. subst Q. 它将摆脱 + 0。你现在的目标是

P j n ln = P j n jn

两边都是nat类型。但是现在你需要证明这两个 nat 是相等的，而不知道关于它们的任何其他信息......

编辑：

实际上我有点太快了...函数 P 的值不能依赖于 ln 和 jn 因为它们是 Props, 。但要证明这一点，你需要 proof irrelevance。

如果你这样做 Require Import ProofIrrelevance. 你就会得到公理

Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.

这不是 Coq 逻辑的结果，但与它是一致的（而且通常正是我们所说的证明 - 两个形式上正确的论点同样正确，即使它们在细节上有所不同）。

现在你就做

rewrite (proof_irrelevance _ ln jn). reflexivity. Qed.

casting convertible types in coq