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 !!!
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!