Proofs involving decidable equality
agda
Solution
Since my function, like the one in the example, doesn't care about the proof object returned by `x ≟ y`, I was able to replace it with `⌊ x ≟ y ⌋` which returns a boolean.
That allowed me write this lemma
≟-refl : ∀ x → ⌊ x ≟ x ⌋ ≡ true
≟-refl x with x ≟ x
... | yes p = refl
... | no ¬p = ⊥-elim (¬p (DecSetoid.refl ds))
which I could then use with `rewrite` to simplify my proof to
check-same x rewrite ≟-refl x = refl
Problem
I'm trying to prove some simple things about a function which uses decidable equality. Here is a much simplified example: ``` 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 ``` Now, I'm trying to prove something like this where I've already shown that both sides of the `_≟_` are identical. ``` check-same : ∀ x → check x x ≡ something check-same x = {!!} ``` At this point, the current goal is `(check ds x x | x ≟ x) ≡ something`. If the `x ≟ x` was by itself, I would solve it by using something like `refl`, but in this situation the best I can come up with is something like this: ``` check-same x with x ≟ x ... | yes p = refl ... | no ¬p with ¬p (DecSetoid.refl ds) ... | () ``` By itself this isn't that bad, but in the middle of a larger proof it's a mess. Surely there must be a better way to do this?