I'm currently exploring Euclidean geometry with Agda, and sometimes, I need to provide an **evidence** for relations like:

$$ 1 + 1 > 1 $$

(This one is used in proving that there must be two different intersection points for two circles with a radius of 1 when proving Proposition 1 in Στοιχεῖα)

In fact, when I first encountered this problem, I found it difficult to prove this "obvious" proposition^{1}, especially when these `1`

s are actually `1ℚ`

. I tried hard to find a tool to do this in the stdlib and finally discovered those `Decidable`

related concepts.

## How to prove 2 ≤ 3

Let's start small, how can we provide *evidence* that `2 ≤ 3`

, when `2`

and `3`

are `ℕ`

s in Agda?

Examine the definition of `≤`

in `Data.Nat.Base`

:

```
data _≤_ : Rel ℕ 0ℓ where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
```

So `z≤n`

is the evidence for `0 ≤ n`

, and `s≤s`

is the evidence for `m ≤ n`

when `m ≤ n`

is given. We can prove `2 ≤ 3`

by using `s≤s`

twice on `z≤n`

:

```
2≤3 : 2 ≤ 3
2≤3 = s≤s (s≤s z≤n)
```

## Push it further

This seems easy, right? But what if we want to prove, say `99 ≤ 100`

? It's insane to use `s≤s`

99 times, right?

We can also find another version of `≤`

, which returns `Bool`

s in `Data.Nat`

:

```
_≤ᵇ_ : (m n : ℕ) → Bool
zero ≤ᵇ n = true
suc m ≤ᵇ n = m <ᵇ n
```

where

```
_<ᵇ_ : Nat → Nat → Bool
_ <ᵇ zero = false
zero <ᵇ suc _ = true
suc n <ᵇ suc m = n < m
```

So we know the value of the term `99 ≤ᵇ 100`

is (`≡`

) `true`

. The *computation* process of `≤ᵇ`

seems somewhat like, or at least related to, an *evidence* of `99 ≤ 100`

.

And this is where `Decidable`

things can help.

The proof of `99 ≤ 100`

can be written as:

```
99≤100 : 99 ≤ 100
99≤100 = ≤ᵇ⇒≤ 99 100 tt
```

So, what is `≤ᵇ⇒≤`

? Why do we need to pass a `tt`

here? Let's examine the definition of `≤ᵇ⇒≤`

.

```
≤ᵇ⇒≤ : ∀ m n → T (m ≤ᵇ n) → m ≤ n
≤ᵇ⇒≤ zero n m≤n = z≤n
≤ᵇ⇒≤ (suc m) n m≤n = <ᵇ⇒< m n m≤n
```

where

```
<⇒<ᵇ : ∀ {m n} → m < n → T (m <ᵇ n)
<⇒<ᵇ (s≤s z≤n) = tt
<⇒<ᵇ (s≤s (s≤s m<n)) = <⇒<ᵇ (s≤s m<n)
```

and

```
T : Bool → Set
T true = ⊤
T false = ⊥
```

So, for `≤ᵇ⇒≤`

, we input the numbers we want to compare and then provide a `tt`

to the type checker, which checks whether `T (m ≤ᵇ n)`

is `tt`

. If it is, we obtain the evidence of `m ≤ n`

; otherwise, the type checker will complain.

All other details in `≤ᵇ⇒≤`

are trivial, just naive pattern matching.

### Decidable

You might have noticed another kind of `≤`

: `≤?`

. What's that for? Let's examine its definition.

```
_≤?_ : Decidable _≤_
m ≤? n = map′ (≤ᵇ⇒≤ m n) ≤⇒≤ᵇ (T? (m ≤ᵇ n))
```

There are several unfamiliar things in this definition, so let's examine them one by one.

`Decidable`

```
Decidable : REL A B ℓ → Set _
Decidable _∼_ = ∀ x y → Dec (x ∼ y)
```

`REL`

here represents an abstraction of binary relations between two types (in other words, heterogeneous binary relations). So `Decidable`

means that for each `x`

and `y`

in `A`

and `B`

, we have `Dec (x op y)`

.

The really interesting part is `Dec`

, which is a record type:

```
record Dec {p} (P : Set p) : Set p where
constructor _because_
field
does : Bool
proof : Reflects P does
```

```
data Reflects {p} (P : Set p) : Bool → Set p where
ofʸ : ( p : P) → Reflects P true
ofⁿ : (¬p : ¬ P) → Reflects P false
```

The `Reflects`

type indicates that the truth value of the proposition `P`

is reflected (or, in other words, determined) by the `Bool`

value. It has two constructors: `ofʸ`

, which means `P`

is true, and `ofⁿ`

, which means `P`

is false.

`Reflects P b`

is equivalent to `if b then P else ¬ P`

, and these two forms can be converted back and forth using the following two functions:

```
of : ∀ {b} → if b then P else ¬ P → Reflects P b
of {b = false} ¬p = ofⁿ ¬p
of {b = true } p = ofʸ p
invert : ∀ {b} → Reflects P b → if b then P else ¬ P
invert (ofʸ p) = p
invert (ofⁿ ¬p) = ¬p
```

And `Dec`

is simply a combination of a `Bool`

and the proof that a proposition `P`

's truth value is reflected by the `Bool`

.

There are also two patterns:

```
pattern yes p = true because ofʸ p
pattern no ¬p = false because ofⁿ ¬p
```

which can be understand from their literal meaning.

Now we know that `Decidable`

means for each `x`

and `y`

in `A`

and `B`

, there is a `Bool`

that reflects the relationship `x op y`

.

`T?`

```
T? : Relation.Unary.Decidable T
does (T? b) = b
proof (T? true ) = ofʸ _
proof (T? false) = ofⁿ λ()
```

`Relation.Unary.Decidable`

is the unary version of `Decidable`

we mentioned earlier (`Decidable P = ∀ x → Dec (P x)`

).

So, `T?`

is a function that takes a `Bool`

and returns an instance of `Decidable`

, which is a term that demonstrates a certain proposition's truth value is reflected by that `Bool`

.

`≤⇒≤ᵇ`

This is just the reverse of `≤ᵇ⇒≤`

.

```
≤⇒≤ᵇ : ∀ {m n} → m ≤ n → T (m ≤ᵇ n)
≤⇒≤ᵇ z≤n = tt
≤⇒≤ᵇ m≤n@(s≤s _) = <⇒<ᵇ m≤n
```

`map′`

```
map′ : (P → Q) → (Q → P) → Dec P → Dec Q
does (map′ P→Q Q→P p?) = does p?
proof (map′ P→Q Q→P (true because [p])) = ofʸ (P→Q (invert [p]))
proof (map′ P→Q Q→P (false because [¬p])) = ofⁿ (invert [¬p] ∘ Q→P)
```

So `map′`

means that if two propositions are in an "iff" relation, and one of them is `Dec`

, then the other is also `Dec`

.

Now we can return to `≤?`

and understand what it is:

```
_≤?_ : Decidable _≤_
m ≤? n = map′ (≤ᵇ⇒≤ m n) ≤⇒≤ᵇ (T? (m ≤ᵇ n))
```

Since `≤ᵇ⇒≤`

and `≤⇒≤ᵇ`

are inverse functions of each other, and `T? (m ≤ᵇ n)`

is a `Dec`

instance for `m ≤ᵇ n`

, we can obtain a `Dec`

instance for `m ≤ n`

.

So, what are the benefits of using `≤?`

?

Well, we can extract both `Bool`

values from a `Dec`

:

```
Dec.does (2 ≤? 1)
-- or
isYes (2 ≤? 1)
-- or
⌊ 2 ≤? 1 ⌋
```

The advantage of `isYes`

and the `⌊⌋`

operator is that they can retain the typing information, whereas `Dec.does`

is a naive `Bool`

.

We can also extract the evidence using a function called `toWitness`

:

```
99≤100' : 99 ≤ 100
99≤100' = toWitness {Q = 99 ≤? 100} tt
```

where:

```
toWitness : {Q : Dec P} → True Q → P
toWitness {Q = true because [p]} _ = invert [p]
toWitness {Q = false because _ } ()
```

where

```
True : Dec P → Set
True Q = T (isYes Q)
```

We can see that `Decidable`

can be used in places where either a `Bool`

or evidence is needed.
Therefore, it is always preferable to use `Decidable`

instead of `Bool`

when possible.

## Use cases

Consider the following constructor of `ℚ`

as an example:

```
_/_ : (n : ℤ) (d : ℕ) → {d≢0 : d ≢0} → ℚ
(+ n / d) {d≢0} = normalize n d {d≢0}
(-[1+ n ] / d) {d≢0} = - normalize (suc n) d {d≢0}
```

Here, `{d≢0 : d ≢0}`

requires that the denominator of a rational number should not be zero.

`≢0`

is defined as

```
n ≢0 = False (n ℕ.≟ 0)
```

And `ℕ.≟`

is very similar with `≤?`

:

```
_≟_ : Decidable {A = ℕ} _≡_
m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
```

By requiring an `≢0`

instance (instead of requiring a "real" evidence of `n ≢ 0`

), we can omit the proof when using number literals:

```
half : ℚ
half = 1ℤ / 2
```

^{1}

I can write an Agda representation of Common Notion 5 in Στοιχεῖα, but I always try to use, and more importantly, understand the stdlib when possible.