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

Question

我对 Coq 中的证据和 Prop 等感到困惑。我们如何证明 (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 = n 和 m = m 都是 propsitions，所以它们属于 Prop 而不是比排序 Set。这基本上意味着 n = n 就像一个陈述(必须证明)而不是像 true : boolean 这样的东西。

相反，您可以尝试证明如下内容:n-n = m-m，或者，您可以定义一个函数 nat_equal : nat -> bool 给定一个自然映射它变成 bool，然后证明 nat_equal n = nat_equal m。

如果您真的想断言陈述 是相等的，您将需要命题外延性。