agda - 涉及可判定相等性的证明

Question

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

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module Foo {c} {ℓ} (ds : DecSetoid c ℓ) where

open DecSetoid ds hiding (refl)

data Result : Set where
  something something-else : Result

check : Carrier → Carrier → Result
check x y with x ≟ y
... | yes _ = something
... | no  _ = something-else

现在，我试图证明这样的事情，我已经证明了两边_≟_是相同的。

check-same : ∀ x → check x x ≡ something
check-same x = {!!}

此时，当前的目标是(check ds x x | x ≟ x) ≡ something。如果x ≟ x它本身是，我会使用类似的东西来解决它refl，但在这种情况下，我能想到的最好的东西是这样的：

check-same x with x ≟ x
... | yes p = refl
... | no ¬p with ¬p (DecSetoid.refl ds) 
... | ()

就其本身而言，这并没有那么糟糕，但是在一个更大的证明中它是一团糟。当然必须有更好的方法来做到这一点？

Answer 1