Agda中空模式匹配失败，如何证明2不整除5及5是素数？

为什么你的空模式匹配没生效 #

Agda无法自动识别k ≤5 × k*2≡5是一个空类型——它不会主动枚举k ≤5的所有构造子并验证每个子情况都和k*2≡5矛盾。你必须手动展开k ≤5的所有可能实例，让Agda看到每个分支里的等式都不可能成立，才能用空模式完成证明。

证明2不整除5的具体步骤 #

首先导入必要的基础模块：

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Product

我们的目标是证明¬ (∃ λ k → k * 2 ≡ 5)（即不存在自然数k使得2k=5），结合k ≤5的约束（因为k>5时2k必然大于5，不可能等于5），可以写出如下证明：

方法1：枚举k的所有可能值 #

2-not-divides-5 : ¬ (∃ λ k → k * 2 ≡ 5)
2-not-divides-5 (k , eq) = helper k eq
  where
    -- 先推导k必然≤5（因为k*2=5 → k≤5）
    k≤5 : k ≤ 5
    k≤5 = ≤-trans (m*2≡n⇒m≤n eq) (m≤n+m k 5)

    helper : ∀ k → k * 2 ≡ 5 → ⊥
    helper zero ()       -- 0*2=0≠5，直接空模式
    helper (suc zero) () -- 1*2=2≠5
    helper (suc (suc zero)) () -- 2*2=4≠5
    helper (suc (suc (suc zero))) eq = 
      let eq' = sym eq in rewrite eq' in () -- 3*2=6≡5，构造子矛盾
    helper (suc (suc (suc (suc zero)))) eq =
      let eq' = sym eq in rewrite eq' in () -- 4*2=8≡5，同理矛盾
    helper (suc (suc (suc (suc (suc zero))))) eq =
      let eq' = sym eq in rewrite eq' in () -- 5*2=10≡5，同理矛盾

方法2：展开k ≤5的构造子 #

直接通过with语句拆分k ≤5的证明结构，每个分支对应k的具体值：

2-not-divides-5' : ∀ k → k ≤ 5 → ¬ (k * 2 ≡ 5)
2-not-divides-5' k p with p
... | z≤n = λ ()          -- k=0，0*2≠5
... | s≤s z≤n = λ ()      -- k=1，2≠5
... | s≤s (s≤s z≤n) = λ () -- k=2，4≠5
... | s≤s (s≤s (s≤s z≤n)) = λ eq → let _ = sym eq in () -- k=3，6≠5
... | s≤s (s≤s (s≤s (s≤s z≤n))) = λ eq → let _ = sym eq in () -- k=4，8≠5
... | s≤s (s≤s (s≤s (s≤s (s≤s z≤n)))) = λ eq → let _ = sym eq in () -- k=5，10≠5

一般情况下证明5是素数 #

素数的标准定义是：大于1的自然数，仅能被1和自身整除。在Agda中可以表述为：

Prime : ℕ → Set
Prime n = n > 1 × (∀ m → m ∣ n → m ≡ 1 ∨ m ≡ n)

其中m ∣ n表示m整除n，定义为∃ λ k → m * k ≡ n。

要证明5是素数，需完成两点：

1. 证明5>1（直接用s≤s构造子即可）；
2. 对所有自然数m，若m整除5，则m≡1或m≡5。

具体证明思路：

• 缩小m的范围：若m>5，则m*1=m>5，不可能等于5，所以只需考虑m≤5的情况；
• 逐个验证m=0到m=5：
  • m=0：0*k=0≠5，不可能整除5；
  • m=1：1*5=5，满足m≡1；
  • m=2：用上面的2-not-divides-5证明不整除5；
  • m=3：枚举k的可能值（31=3≠5，32=6>5），导出矛盾；
  • m=4：41=4≠5，42=8>5，矛盾；
  • m=5：5*1=5，满足m≡5。

完整的素数证明代码框架：

5-is-prime : Prime 5
5-is-prime = 5>1 , divides-5-implies-1-or-5
  where
    5>1 : 5 > 1
    5>1 = s≤s (s≤s (s≤s (s≤s z≤n)))

    divides-5-implies-1-or-5 : ∀ m → m ∣ 5 → m ≡ 1 ∨ m ≡ 5
    divides-5-implies-1-or-5 m (k , eq) = helper m k eq
      where
        m≤5 : m ≤5
        m≤5 = ≤-trans (m*k≡n⇒m≤n eq) (m≤n+m m 5)

        helper : ∀ m k → m *k ≡5 → m ≡1 ∨ m≡5
        helper 0 k ()
        helper 1 k eq = inj₁ refl
        helper 2 k eq = ⊥-elim (2-not-divides-5 (k , sym eq))
        helper 3 k eq = let _ = sym eq in () -- 3*k=5无自然数解
        helper 4 k eq = let _ = sym eq in () -- 4*k=5无自然数解
        helper 5 k eq = inj₂ refl
        helper (suc (suc (suc (suc (suc (suc m)))))) k eq =
          ⊥-elim (≤-irrefl (s≤s m≤5)) -- m>5时m≤5不成立，导出矛盾

内容的提问来源于stack exchange，提问作者zaabson