3

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

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

到目前为止我尝试的是:

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

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

4

2 回答 2

2

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

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

于 2015-12-09T03:15:50.060 回答
1

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

于 2015-12-09T03:07:55.223 回答