Instance resolution for decidable equality of discrete types

Discrete.agda

module Discrete where

open import Agda.Builtin.Equality public

data ⊥ : Set where

¬_ : ∀{a} → Set a → Set a
¬ A = A → ⊥

data Dec {a} (A : Set a) : Set a where
  yes :   A → Dec A
  no  : ¬ A → Dec A

record Discrete {a} (A : Set a) : Set a where
  field
    _⟨_≟_⟩ : (x y : A) → Dec (x ≡ y)
open Discrete public

_≟_ : ∀{a} {A : Set a} ⦃ _ : Discrete A ⦄ → (x y : A) → Dec (x ≡ y)
_≟_ ⦃ discreteA ⦄ x y = discreteA ⟨ x ≟ y ⟩


-- We now give instances for the (safe) built-in types (other than unit)

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Int
open import Agda.Builtin.List

instance DiscreteBool : Discrete Bool
DiscreteBool ⟨ false ≟ false ⟩ = yes refl
DiscreteBool ⟨ false ≟ true  ⟩ = no λ ()
DiscreteBool ⟨ true  ≟ false ⟩ = no λ ()
DiscreteBool ⟨ true  ≟ true  ⟩ = yes refl

instance Discreteℕ : Discrete ℕ
Discreteℕ ⟨ zero  ≟ zero  ⟩ = yes refl
Discreteℕ ⟨ zero  ≟ suc _ ⟩ = no λ ()
Discreteℕ ⟨ suc _ ≟ zero  ⟩ = no λ ()
Discreteℕ ⟨ suc n ≟ suc m ⟩ with n ≟ m
...                         | yes refl = yes refl
...                         | no  n≢m  = no λ { refl → n≢m refl }

instance DiscreteInt : Discrete Int
DiscreteInt ⟨ pos n    ≟ pos m    ⟩ with n ≟ m
...                                 | yes refl = yes refl
...                                 | no  n≢m  = no λ { refl → n≢m refl }
DiscreteInt ⟨ pos _    ≟ negsuc _ ⟩ = no λ ()
DiscreteInt ⟨ negsuc _ ≟ pos _    ⟩ = no λ ()
DiscreteInt ⟨ negsuc n ≟ negsuc m ⟩ with n ≟ m
...                                 | yes refl = yes refl
...                                 | no  n≢m  = no λ { refl → n≢m refl }

instance DiscreteList : ∀{a} {A : Set a} ⦃ _ : Discrete A ⦄ → Discrete (List A)
DiscreteList ⟨ []     ≟ []     ⟩ = yes refl
DiscreteList ⟨ []     ≟ _ ∷ _  ⟩ = no λ ()
DiscreteList ⟨ x ∷ xs ≟ []     ⟩ = no λ ()
DiscreteList ⟨ x ∷ xs ≟ y ∷ ys ⟩ with x ≟ y
...                              | no  x≢y  = no λ { refl → x≢y refl }
...                              | yes refl with xs ≟ ys
...                                         | yes refl  = yes refl
...                                         | no  xs≢ys = no λ { refl
                                                                 → xs≢ys refl }

example.agda

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.List

open import Discrete

infix 4 _∈_
data _∈_ {A : Set} (x : A) : List A → Set where
  head : ∀{xs}            → x ∈ x ∷ xs
  tail : ∀{y xs} → x ∈ xs → x ∈ y ∷ xs

is_∈_ : {A : Set} ⦃ _ : Discrete A ⦄ → (x : A) → (xs : List A) → Dec (x ∈ xs)
is x ∈ [] = no λ ()
is x ∈ (y ∷ xs) with x ≟ y
...             | yes refl = yes head
...             | no  x≢y  with is x ∈ xs
...                        | yes x∈xs = yes (tail x∈xs)
...                        | no  x∉xs = no λ { head        → x≢y refl
                                             ; (tail x∈xs) → x∉xs x∈xs }

-- Because the Discrete module proves ℕ discrete, we can do the following
eg₁ : ∀ n → Dec (n ∈ 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
eg₁ n = is n ∈ (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])