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