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

由于我的函数(如示例中的函数)不关心 x ≟ y 返回的证明对象，因此我能够用返回 bool 值的 ⌊ x ≟ y ⌋ 替换它。

这允许我写这个引理

≟-refl : ∀ x → ⌊ x ≟ x ⌋ ≡ true
≟-refl x with x ≟ x 
... | yes p = refl
... | no ¬p = ⊥-elim (¬p (DecSetoid.refl ds))

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

check-same x rewrite ≟-refl x = refl