Decidable setoid in Agda

If you have known setoid in Agda, the decidable setoid may be quite easy to understand. We first explain (I hope so …) what is decidable relation. A decidable relation is defined as follows in Agda,

data Dec (P : Set) : Set where

yes : ( p : P) → Dec P
no : (¬p : ¬ P) → Dec P

It defines a type which has two element: yes if the given proposition is not empty(which means we could give the proof term!) , and no otherwise. Next, a function which translates a relation to a decidable one,

Decidable : {a : Set} → Rel a → Set
Decidable _∼_ = ∀ x y → Dec (x ∼ y)

By combining these two, we could define a decidable judgement of relations. Consider the example given in Data.Nat as follows,

_≤?_ : Decidable _≤_
zero ≤? _ = yes z≤n
suc m ≤? zero = no λ()
suc m ≤? suc n with m ≤? n
... | yes m≤n = yes (s≤s m≤n)
... | no m≰n = no (m≰n ∘ ≤-pred)

We define a relation _≤_, and a function decide whether two element are related to each other. Moreover, the function returns the proof together.

Then, the decidable setoid is just a setoid with a decidable equality. That is,

record IsDecEquivalence {a : Set} (_≈_ : Rel a) : Set where

field

isEquivalence : IsEquivalence _≈_
_≟_ : Decidable _≈_

record DecSetoid : Set1 where

field

carrier : Set
_≈_ : Rel carrier
isDecEquivalence : IsDecEquivalence _≈_

There is no magic. Back to the earlier example ListLen, we could define a judgement about that relation. But we first modify the relation without using any other datatype.

data _∼_ {a : Set} : (List a) → (List a) → Set where

[]-eq : [] ∼ []
∷-eq : ∀ {xs ys x y} → (xs∼ys : xs ∼ ys) → (x ∷ xs) ∼ (y ∷ ys)

The corresponding function is defined as follows,

_∼?_ : ∀ {a} → Decidable (_∼_ {a})
_∼?_ [] [] = yes []-eq
_∼?_ [] (y ∷ ys) = no (λ ())
_∼?_ (x ∷ xs) [] = no (λ ())
_∼?_ (x ∷ xs) (y ∷ ys) with xs ∼? ys
... | yes eq = yes (∷-eq eq)
... | no neq = no (neq ∘ ∼-pre)

where

∼-pre : ∀ {a} → {x y : a}{xs ys : List a} → (x ∷ xs) ∼ (y ∷ ys) → xs ∼ ys
∼-pre (∷-eq xs∼ys) = xs∼ys

It’s almost the same as Data.Nat._≟_. We have the decidable version of ListLen immediately.

decListLen : (a : Set) → DecSetoid
decListLen a = record

{ carrier = Setoid.carrier (ListLen a)
; _≈_ = _∼_
; isDecEquivalence = record

{ isEquivalence = Setoid.isEquivalence (ListLen a)
; _≟_ = _∼?_
}

}

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s