# 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) ; _≟_ = _∼?_ }```

}