Skip to content

Instantly share code, notes, and snippets.

@louisswarren

louisswarren/Discrete.agda

Last active Dec 18, 2019
Embed
What would you like to do?
Instance resolution for decidable equality of discrete types
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 }
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 ∈ 01234 ∷ [])
eg₁ n = is n ∈ (01234 ∷ [])
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.