我Prop
对Coq中的证据等感到困惑。我们如何证明这一点(n = n) = (m = m)
?
我的意图是证明这是某种方式True=True
。但这甚至是正确的表述吗?
到目前为止,我尝试过的是:
Theorem test: forall m n:nat, (n = n) = (m = m).
Proof. intros. simpl.
但是simpl.
什么也没做,也reflexivity
没有。这仅是示例,通常,我需要针对任何类型证明这一点X
。
n = n
而且m = m
都是命题,所以它们是排序Prop
而非排序Set
。这基本上意味着它n = n
就像一个语句(必须被证明),而不是类似true : boolean
。
取而代之的是,您可以尝试证明类似:的方法n-n = m-m
,或者可以定义一个nat_equal : nat -> bool
给定自然的函数,将其映射到bool,然后证明nat_equal n = nat_equal m
。
如果您真的想断言语句是相等的,则需要命题可扩展性。
本文收集自互联网,转载请注明来源。
如有侵权,请联系[email protected] 删除。
我来说两句