浇铸COQ转换类型

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.，但我没有看到如何将此应用于类型。

2015-11-05 krokodil

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

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

2015-11-05 05:34:10

感谢。我知道这是不可证明的，但我能够证明它对于特别的P. – krokodil

我很抱歉，但我仍然不明白。即使我让'x'和'y'非隐式，'P'也是自然数，所以'j'和'j + 0'是'nat'类型，我可以证明它们是等价的。从常理上来说，从证明'j + 0 krokodil

并非所有“m gallais

引理不可证明。尝试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 s为平等的，不知道什么对他们...

编辑：

其实我是有点太快......函数的值P不能由于它们是Prop s，因此取决于ln和jn。但为了证明这一点，你需要proof irrelevance。

如果你Require Import ProofIrrelevance.你得到的公理

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

这不是勒柯克的逻辑的结果，但它符合它（而且往往正是我们的意思用一个证明 - 两个形式上正确的参数即使他们的细节有所不同，也是一样的）。

现在你只是做

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

2015-11-05 19:32:11 larsr

谢谢！这有助于 – krokodil

我添加了一些关于使用*证明不相关*来完成证明的评论。 – larsr

回答