在Agda中证明自然数平方模3不为2的技术问询

问题描述 #

需要在Agda中证明命题：(n : ℕ) → ∃[ m ] n * n ≡ 3 * m + 2 → ⊥，即不存在自然数n和m使得n² = 3m + 2。

方法一：直接归纳+分情况推导 #

无需自定义模算术结构，直接基于自然数归纳原理，将n分为3k、3k+1、3k+2三类展开计算，通过等式推理导出矛盾。

完整可运行代码 #

open Data.Nat.Base
open Relation.Binary.PropositionalEquality
open Data.Empty
open Data.Product using (Σ; _,_; ∃; ∃-syntax)
open Relation.Binary.PropositionalEquality.≡-Reasoning

-- 辅助引理：证明(3k+1)² = 3*(3k²+2k)+1
sq₁ : ∀ k → (3 * k + 1) * (3 * k + 1) ≡ 3 * (3 * k * k + 2 * k) + 1
sq₁ k =
  begin
    (3 * k + 1) * (3 * k + 1)
  ≡⟨ *-distrib-+ (3 * k) 1 (3 * k + 1) ⟩
    (3 * k) * (3 * k + 1) + 1 * (3 * k + 1)
  ≡⟨ cong₂ _+_ (*-distrib-+ (3 * k) (3 * k) 1) refl ⟩
    (3 * k) * (3 * k) + (3 * k) * 1 + (3 * k + 1)
  ≡⟨ cong₂ _+_ (cong (λ x → x * (3 * k)) (*-comm 3 k)) refl ⟩
    3 * (k * 3 * k) + 3 * k + 3 * k + 1
  ≡⟨ cong₂ _+_ (cong (λ x → 3 * x) (*-assoc k 3 k)) refl ⟩
    3 * (3 * k * k) + 3 * (k + k) + 1
  ≡⟨ cong (λ x → x + 1) (+-comm (3 * (3 * k * k)) (3 * (k + k))) ⟩
    3 * (3 * k * k + 2 * k) + 1
  ∎

-- 辅助引理：证明(3k+2)² = 3*(3k²+4k+1)+1
sq₂ : ∀ k → (3 * k + 2) * (3 * k + 2) ≡ 3 * (3 * k * k + 4 * k + 1) + 1
sq₂ k =
  begin
    (3 * k + 2) * (3 * k + 2)
  ≡⟨ *-distrib-+ (3 * k) 2 (3 * k + 2) ⟩
    (3 * k) * (3 * k + 2) + 2 * (3 * k + 2)
  ≡⟨ cong₂ _+_ (*-distrib-+ (3 * k) (3 * k) 2) (*-distrib-+ 2 (3 * k) 2) ⟩
    (3 * k) * (3 * k) + (3 * k) * 2 + 2 * 3 * k + 4
  ≡⟨ cong₂ _+_ (cong (λ x → x * (3 * k)) (*-comm 3 k)) (cong₂ _+_ (*-comm 2 (3 * k)) refl) ⟩
    3 * (k * 3 * k) + 3 * (2 * k) + 3 * (2 * k) + 4
  ≡⟨ cong₂ _+_ (cong (λ x → 3 * x) (*-assoc k 3 k)) (cong₂ _+_ refl refl) ⟩
    3 * (3 * k * k) + 3 * (2 * k + 2 * k) + 3 + 1
  ≡⟨ cong (λ x → x + 1) (+-comm (3 * (3 * k * k)) (3 * (4 * k)) +-cong refl) ⟩
    3 * (3 * k * k + 4 * k + 1) + 1
  ∎

-- 核心证明：平方不可能模3余2
no-sq-mod3≡2 : (n : ℕ) → ∃[ m ] n * n ≡ 3 * m + 2 → ⊥
no-sq-mod3≡2 zero (m , eq) =
  -- 0²=0，0≡3m+2 → 3m+2=0，矛盾
  case eq of λ ()
no-sq-mod3≡2 (suc n) hyp with n divMod 3
-- 情况1：n = 3k → suc n = 3k+1
... | k , 0 , refl =
  let (m , eq) = hyp
      eq' = trans (sq₁ k) eq
  in case eq' of λ ()
-- 情况2：n = 3k+1 → suc n = 3k+2
... | k , 1 , refl =
  let (m , eq) = hyp
      eq' = trans (sq₂ k) eq
  in case eq' of λ ()
-- 情况3：n = 3k+2 → suc n = 3(k+1)
... | k , 2 , refl =
  let (m , eq) = hyp
      eq' = trans (cong (λ x → x * x) (sym (+-assoc (3 * k) 2 1))) eq
  in case eq' of λ ()

方法二：自定义模3同余系统 #

先定义自然数模3的余数类型，证明所有自然数都属于三类余数之一，再推导每类数平方后的余数，最终导出矛盾。

完整可运行代码 #

open Data.Nat.Base
open Relation.Binary.PropositionalEquality
open Data.Empty
open Data.Product using (Σ; _,_; ∃; ∃-syntax; _×_)
open Relation.Binary.PropositionalEquality.≡-Reasoning

-- 定义模3的余数类型
data Mod3 : ℕ → Set where
  mod0 : ∀ k → Mod3 (3 * k)
  mod1 : ∀ k → Mod3 (3 * k + 1)
  mod2 : ∀ k → Mod3 (3 * k + 2)

-- 引理：所有自然数都属于Mod3的某一类
all-mod3 : ∀ n → Σ[ r ∈ ℕ ] Mod3 n
all-mod3 zero = 0 , mod0 0
all-mod3 (suc n) with all-mod3 n
... | 0 , mod0 k = 1 , mod1 k
... | 1 , mod1 k = 2 , mod2 k
... | 2 , mod2 k = 0 , mod0 (suc k)

-- 引理：平方后的余数情况
sq-mod3 : ∀ n → Mod3 n → Mod3 (n * n)
sq-mod3 (3 * k) (mod0 .k) = mod0 (3 * k * k)
sq-mod3 (3 * k + 1) (mod1 .k) = mod1 (3 * k * k + 2 * k)
sq-mod3 (3 * k + 2) (mod2 .k) = mod1 (3 * k * k + 4 * k + 1)

-- 核心证明：平方不可能模3余2
no-sq-mod3≡2' : (n : ℕ) → ∃[ m ] n * n ≡ 3 * m + 2 → ⊥
no-sq-mod3≡2' n (m , eq) with all-mod3 n
... | _ , mod3-n =
  let mod3-sq = sq-mod3 n mod3-n
  in case mod3-sq of
    -- 平方后只能是mod0或mod1，不可能是mod2
    λ { (mod0 k) → case eq of λ ()
      ; (mod1 k) → case eq of λ ()
      ; (mod2 k) → ⊥-elim (λ ()) }

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