Preuves impliquant une égalité décidable

Question

J'essaie de prouver des choses simples à propos d'une fonction qui utilise l'égalité décidable. Voici un exemple très simplifié:

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 

Maintenant, je suis en train de prouver quelque chose comme ça où je l'ai déjà montré que les deux côtés de la _≟_ sont identiques. À ce stade, l'objectif actuel est (check ds x x | x ≟ x) ≡ something. Si le x ≟ x était par lui-même, je résous en utilisant quelque chose comme refl, mais dans cette situation, le mieux que je peux venir avec quelque chose comme ceci:

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

En soi, ce n'est pas si mal que ça, mais au milieu d'une plus grande preuve c'est un gâchis. Sûrement il doit y avoir une meilleure façon de le faire?

Answer 1

Depuis ma fonction, comme celle de l'exemple, ne se soucie pas de l'objet de preuve retourné par x ≟ y, j'ai été en mesure de le remplacer par ⌊ x ≟ y ⌋ qui renvoie un booléen.

qui m'a permis d'écrire ce lemme

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

que je pourrais alors utiliser rewrite pour simplifier ma preuve

check-same x rewrite ≟-refl x = refl