coq - 如何在 Coq 中证明 (n = n) = (m = m)？

Question

我对PropCoq 中的证据等感到困惑。我们如何证明这一点(n = n) = (m = m)？

我的意图是表明这是某种方式True=True。但这甚至是正确的表述？

到目前为止我尝试的是：

Theorem test: forall m n:nat, (n = n) = (m = m).
Proof. intros. simpl.

但simpl.什么都不做，reflexivity也不做。X这只是一个例子，一般来说，如果可能的话，我需要为任何类型证明这一点。

Answer 1

n = nandm = m都是propsitions，所以它们是 sortProp而不是 sort Set。这基本上意味着这n = n就像一个陈述（必须证明）而不是类似的东西true : boolean。

相反，您可以尝试证明类似：n-n = m-m，或者，您可以定义一个函数nat_equal : nat -> bool，给定一个自然值，将其映射到 bool，然后证明nat_equal n = nat_equal m。

如果你真的想断言陈述是平等的，你需要命题外延。

Answer 2

如果不假设其他公理，就不可能证明您的要求；参看。这个答案。