Evidence with Solvable Equality

Question

I am trying to prove some simple things about a function that uses decidable equality. Here is a 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 xy with x ≟ y ... | yes _ = something ... | no _ = something-else 

Now I am trying to prove something like this when I have already shown that both sides _≟_ identical.

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

At this point, the current target (check ds xx | x ≟ x) ≡ something . If x ≟ x was on its own, I would solve it 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) ... | () 

This in itself is not so bad, but in the middle of the larger evidence is a mess. Surely there should be a better way to do this?

Answer 1

Since my function, as in the example, does not care about the proof object returned by x ≟ y , I was able to replace it with ⌊ x ≟ y ⌋ , which returns a boolean value.

This allowed me to 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 use with rewrite to simplify my proof to

 check-same x rewrite ≟-refl x = refl