如何在 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证明起来似乎并不简单

我们可以在 1 < 0 上简化 s<s。

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 中肯定有一些我不知道的东西，而且很明显。

PS:

我必须说 "The solutions" 不会影响那些对自己负责的人。一个学生好，因为他好。我在这里寻求帮助不是因为我想得到一些答案来做考试。我不再是学生了。我只是遇到了困难，需要一些提示才能继续。它需要 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

Answer 3

PLFA 的可判定章节向您展示了 Agda 如何为任何给定的 m 和 n 计算 m < n 或 ¬ (m < n)。特别是，它定义了一个函数 ¬s≤s : ∀ {m n : ℕ} → ¬ (m ≤ n) → ¬ (suc m ≤ suc n) 完全符合您的要求。

如何在 agda 中证明 ¬ 2 < 1？

How to prove ¬ 2 < 1 in agda?

agda

plfa