Как доказать ¬ 2 <1 в агде?

Question

Я думаю, что я должен что-то упустить, чтобы доказать ¬ 2 < 1.

У меня есть

¬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) 

Если я хочу доказать ¬ 2 < 1, я могу использовать contraposition следующим образом:

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

Но 2<1->1<0 : 2 < 1 → 1 < 0 кажется непросто доказать

Мы можем просто s<s на 1 < 0.

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

Но мы не можем легко сделать то же самое на 2 < 1, потому что у нас есть <

data _<_ : ℕ → ℕ → Set where

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

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

Я знаю

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

маяпомогите доказать 2<1->1<0.Моя интуиция, скажите мне, введите _∸_, чтобы доказать, что эта проблема будет более сложной.В Агде должно быть что-то, чего я не знаю, и это очевидно.

PS:

Я должен сказать, что "решения" не повлияют на людей, которые берут на себя ответственность за себя.Один студент хорош, потому что он хорош.Я прошу помощи здесь, а не потому, что я хочу получить ответ на экзамен.Я больше не студент.Мне просто стало трудно, и мне нужно несколько советов, чтобы продолжить.Требуется 1500 репутация для создания тега likse plfa.Кто-нибудь может помочь?

Answer 1

Чтобы доказать эту конкретную лемму, вам нужно только сопоставить шаблон с аргументом:

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

Все ¬n<m предложения для n, m литералов доказываются при сопоставлении на mчисло s≤s -s, если n на самом деле больше.Например:

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

Смысл в том, чтобы покопаться в случае, когда правая сторона равна zero, а левая равна suc, потому что нет тривиального конструктора _<_ с такой формой.

Answer 2

Многие альтернативные подходы могут быть изобретены.Для вашего подхода к работе вы можете доказать 2<1->1<0, что достаточно просто.

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