How to prove strict inequality holds for no in Agda

Question

I am currently working on one of the recommended question from the chapter Negation in plfa

Here is the question description:

Using negation, show that strict inequality is irreflexive, that is, n < n holds for no n.

From my understanding, I think in strict inequality, it will take two natural numbers as the argument and output a set right? :

data _<_ : ℕ → ℕ → Set where

    z<s : ∀ {n : ℕ}
        ------------
      → zero < suc n

    s<s : ∀ {m n : ℕ}
      → m < n
        -------------
      → suc m < suc n

And here is my definition of irreflexive:

<-irreflexive : ∀ {n : ℕ} → n < n → ⊥
<-irreflexive n<n = ?

I know that I need to achieve a "⊥" in the RHS. And since "n<n" is a set, I try to use ¬, but the complier says "n<n" :(n < n) !=< Set. So, what is the type of "n<n" in this case? And am I approaching right in this question? Could anybody give me a hint on that? Thanks in advance !!!

Answer 1

You're on the right track! The trick is now to use the argument n<n for which there can be no real element to produce something of type ⊥. We do this by pattern matching on n<n. Agda can already see that the constructor z<s can't possibly apply (this is morally equivalent of producing something of type ⊥) so all that's left to do is to handle the s<s case:

<-irreflexive : ∀ {n : ℕ} → n < n → ⊥
<-irreflexive (s<s n<n) = ?

However, we can now use recursion to produce the required element of type ⊥

<-irreflexive : ∀ {n : ℕ} → n < n → ⊥
<-irreflexive (s<s n<n) = <-irreflexive n<n

Tada, done!