agda - 如何在 agda 中证明 ¬ 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 .直觉告诉我，介绍一下_∸_证明这个问题会更复杂。 Agda 中肯定有一些我不知道的东西，这是显而易见的。

附言:

我必须说“解决方案”不会影响那些为自己负责的人。一个学生好，因为他好。我在这里寻求帮助不是因为我想得到一些答案来做考试。我不再是学生了。我只是遇到了困难，需要一些提示才能继续。它需要 1500创建标签的声誉 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 ，因为根本没有 _<_具有该形状的构造函数。