涉及可判定相等性的证明

Question

我试图证明关于使用可判定相等的函数的一些简单的事情。这是一个非常简化的示例：

\n\n

open import Relation.Nullary\nopen import Relation.Binary\nopen import Relation.Binary.PropositionalEquality\n\nmodule Foo {c} {\xe2\x84\x93} (ds : DecSetoid c \xe2\x84\x93) where\n\nopen DecSetoid ds hiding (refl)\n\ndata Result : Set where\n  something something-else : Result\n\ncheck : Carrier \xe2\x86\x92 Carrier \xe2\x86\x92 Result\ncheck x y with x \xe2\x89\x9f y\n... | yes _ = something\n... | no  _ = something-else\n

\n\n

现在，我正在尝试证明这样的事情，我已经证明了两边_\xe2\x89\x9f_是相同的。

\n\n

check-same : \xe2\x88\x80 x \xe2\x86\x92 check x x \xe2\x89\xa1 something\ncheck-same x = {!!}\n

\n\n

至此，当前的目标是(check ds x x | x \xe2\x89\x9f x) \xe2\x89\xa1 something。如果x \xe2\x89\x9f x是单独的，我会使用类似的方法来解决它refl，但在这种情况下，我能想到的最好的办法是这样的：

\n\n

check-same x with x \xe2\x89\x9f x\n... | yes p = refl\n... | no \xc2\xacp with \xc2\xacp (DecSetoid.refl ds) \n... | ()\n

\n\n

就其本身而言，这并没有那么糟糕，但在更大的证明中，这就很混乱了。当然一定有更好的方法来做到这一点吗？

\n

Answer 1

由于我的函数（如示例中的函数）不关心 所返回的证明对象x \xe2\x89\x9f y，因此我能够将其替换为\xe2\x8c\x8a x \xe2\x89\x9f y \xe2\x8c\x8b返回布尔值的函数。

\n\n

这让我可以写出这个引理

\n\n

\xe2\x89\x9f-refl : \xe2\x88\x80 x \xe2\x86\x92 \xe2\x8c\x8a x \xe2\x89\x9f x \xe2\x8c\x8b \xe2\x89\xa1 true\n\xe2\x89\x9f-refl x with x \xe2\x89\x9f x \n... | yes p = refl\n... | no \xc2\xacp = \xe2\x8a\xa5-elim (\xc2\xacp (DecSetoid.refl ds))\n

\n\n

然后我可以用它来rewrite简化我的证明

\n\n

check-same x rewrite \xe2\x89\x9f-refl x = refl\n

\n