How to prove ¬ 2 < 1 in agda?

Question

I think I must missing something to prove ¬ 2 < 1.

I have

¬1<0 : ¬ (1 < 0)
¬1<0 = λ()

¬0<0 : ¬ (0 < 0)
¬0<0 = λ()

¬2<0 : ¬ (2 < 0)
¬2<0 = λ()


contraposition : ∀ {A B : Set}
→ (A → B)
    -----------
→ (¬ B → ¬ A)
contraposition f ¬y x = ¬y (f x) 

If I want to prove ¬ 2 < 1 I can use contraposition like this:

¬2<1 : ¬ (2 < 1)
¬2<1 =  contraposition 2<1->1<0 ¬1<0

But 2<1->1<0 : 2 < 1 → 1 < 0 seem not simple to prove

We can simple s<s on 1 < 0.

1<0->2<1 : 1 < 0 → 2 < 1
1<0->2<1  x =  s<s x

But we can't easy do same thing on 2 < 1 Because we have <

data _<_ : ℕ → ℕ → Set where

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

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

I know the

_∸_ : ℕ → ℕ → ℕ  -
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

may have help to prove 2<1->1<0. My intuition tell me, introduce _∸_ to prove this problem will be more complicate. There must something I don't know in Agda and it is obvious.

PS:

I must say "The solutions" will don't effect the people who take responsibility for themself. One student is good because he is good. I ask help here not because I want to get some answer to do exam. I am not a student anymore. I just got difficult and need some tips to go on. It need 1500 reputation to create tag likse plfa. Can anyone help it?

Answer 1

Many alternative approaches can be contrived. For your approach to work, you can prove 2<1->1<0, which is simple enough.

sm<sn->m<n : {m n : ℕ} -> suc m < suc n -> m < n
sm<sn->m<n (s<s m<n) = m<n

¬2<1 : ¬ (2 < 1)
¬2<1 = contraposition sm<sn->m<n ¬1<0

Answer 2

To prove this particular lemma, you only need to pattern match on the argument:

¬2<1 : ¬ 2 < 1
¬2<1 (s≤s ())

All ¬n<m propositions for n, m literals are provable by matching on m number of s≤s-s, if n is actually greater. For example:

¬5<3 : ¬ 5 < 3
¬5<3 (s≤s (s≤s (s≤s ())))

The point is to dig down into the case where the right side is zero and the left is suc, because there is trivially no _<_ constructor with that shape.

Answer 3

Chapter Decidable of PLFA shows you how Agda can compute either m < n or ¬ (m < n) for any given m and n. In particular, it defines a function ¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n) that does exactly what you want.