How to prove 2 ≤ 3 in Agda

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¹, 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 ℕ 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 Bools 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