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" proposition1, especially when these 1s 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 ℕ 0where
  zn : {n}                 → zero  n
  ss : {m n} (mn : 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:

23 : 2 3
23 = ss (ss zn)

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 Bools in Data.Nat:

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


_<ᵇ_ : 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:

99100 : 99 100
99100 = ≤ᵇ⇒≤ 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 mn = zn
≤ᵇ⇒≤ (suc m) n mn = <ᵇ⇒< m n mn


<⇒<ᵇ : {m n} → m < n T (m <ᵇ n)
<⇒<ᵇ (ss zn)       = tt
<⇒<ᵇ (ss (ss m<n)) = <⇒<ᵇ (ss m<n)


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.


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 : 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_
    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? : 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)
≤⇒≤ᵇ zn         = tt
≤⇒≤ᵇ mn@(ss _) = <⇒<ᵇ mn


map′ : (P Q) → (Q P) → Dec P Dec Q
does  (mapPQ QP p?)                   = does p?
proof (mapPQ QP (true  because  [p])) = ofʸ (PQ (invert [p]))
proof (mapPQ QP (false becausep])) = ofⁿ (invertp] ∘ QP)

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:

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


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


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 : ) → {d0 : d 0} → (+ n      / d) {d0} =   normalize n       d {d0}
(-[1+ n ] / d) {d0} = - normalize (suc n) d {d0}

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

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.