我对Prop
Coq 中的证据等感到困惑。我们如何证明这一点(n = n) = (m = m)
?
我的意图是表明这是某种方式True=True
。但这甚至是正确的表述?
到目前为止我尝试的是:
Theorem test: forall m n:nat, (n = n) = (m = m).
Proof. intros. simpl.
但simpl.
什么都不做,reflexivity
也不做。X
这只是一个例子,一般来说,如果可能的话,我需要为任何类型证明这一点。
我对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
andm = m
都是propsitions,所以它们是 sortProp
而不是 sort Set
。这基本上意味着这n = n
就像一个陈述(必须证明)而不是类似的东西true : boolean
。
相反,您可以尝试证明类似:n-n = m-m
,或者,您可以定义一个函数nat_equal : nat -> bool
,给定一个自然值,将其映射到 bool,然后证明nat_equal n = nat_equal m
。
如果你真的想断言陈述是平等的,你需要命题外延。
如果不假设其他公理,就不可能证明您的要求;参看。这个答案。