能否用Agda标准库的Nat求解器实现反证法证明？

完全可以借助Agda标准库的自然数求解器配合反证法完成你给出的证明。核心思路是先通过求解器化简等式两边的复杂表达式，再利用自然数的模运算性质导出矛盾，最终证明原等式不可能成立。

步骤说明 #

1. 导入必要依赖
   需要导入标准库中处理自然数、等式性质、矛盾证明的模块，以及自动化简代数表达式的+-*-Solver。

2. 化简等式两边
   原等式的左右两边可以通过求解器自动化简：

   • 左边化简后为(n + 3)²（即(n + 3) * (n + 3)）
   • 右边化简后为3m + 5
     原等式等价于(n + 3)² ≡ 3m + 5。

3. 找矛盾点
   对等式两边取模3：

   • 左边(n+3)² mod 3等价于n² mod 3，而自然数的平方模3只能是0或1（0²=0，1²=1，2²=4≡1 mod3）
   • 右边3m+5 mod3等于5 mod3=2
     显然左边不可能等于2，由此导出矛盾。

完整Agda代码示例 #

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import ≡-Reasoning

-- 用求解器化简左边表达式
simplify-left : ∀ n → 3 + (n + (3 + (n + (3 + (n + n * (3 + n)))))) ≡ (n + 3) * (n + 3)
simplify-left n = +-*-Solver.solve 1
  (λ n → con 3 :+ (n :+ (con 3 :+ (n :+ (con 3 :+ (n :+ (n :* (con 3 :+ n))))))))
  ((n :+ con 3) :* (n :+ con 3))
  refl

-- 用求解器化简右边表达式
simplify-right : ∀ m → 1 + m + (1 + m + (1 + m + 0)) + 2 ≡ 3 * m + 5
simplify-right m = +-*-Solver.solve 1
  (λ m → con 1 :+ m :+ (con 1 :+ m :+ (con 1 :+ m :+ con 0)) :+ con 2)
  (con 3 :* m :+ con 5)
  refl

-- 证明自然数平方模3只能是0或1
square-mod3 : ∀ n → n * n mod 3 ≡ 0 ∨ n * n mod 3 ≡ 1
square-mod3 n with n mod 3
... | 0 = inj₁ (cong (_mod 3) (0*n n))
... | 1 = inj₂ (cong (_mod 3) (1*n n))
... | 2 = inj₂ (begin
  2 * 2 mod 3 ≡⟨ refl ⟩
  4 mod 3 ≡⟨ refl ⟩
  1 ∎)

-- 主证明：从原等式导出矛盾
proof : ∀ {n m : ℕ} → 3 + (n + (3 + (n + (3 + (n + n * (3 + n)))))) ≡ 1 + m + (1 + m + (1 + m + 0)) + 2 → ⊥
proof eq = contra eq'
  where
    -- 化简后的等式
    eq₁ : (n + 3) * (n + 3) ≡ 3 * m + 5
    eq₁ = trans (sym (simplify-left _)) (trans eq (simplify-right _))

    -- 等式两边取模3
    eq₂ : ((n + 3) * (n + 3)) mod 3 ≡ (3 * m + 5) mod 3
    eq₂ = cong (_mod 3) eq₁

    -- 左边模3等价于n²模3
    lhs-equiv : ((n + 3) * (n + 3)) mod 3 ≡ n * n mod 3
    lhs-equiv = begin
      ((n + 3) * (n + 3)) mod 3 ≡⟨ cong (_mod 3) (+-distrib-* (n + 3) n 3) ⟩
      (n * (n + 3) + 3 * (n + 3)) mod 3 ≡⟨ cong (_mod 3) (+-comm _ _) ⟩
      (3 * (n + 3) + n * (n + 3)) mod 3 ≡⟨ mod-+-multiple-right _ _ ⟩
      (n * (n + 3)) mod 3 ≡⟨ cong (_mod 3) (*-distrib-right n 3 n) ⟩
      (n * 3 + n * n) mod 3 ≡⟨ cong (_mod 3) (+-comm _ _) ⟩
      (n * n + n * 3) mod 3 ≡⟨ mod-+-multiple-right _ _ ⟩
      n * n mod 3 ∎
      where
        -- 辅助引理：a + 3*b 模3等于a模3
        mod-+-multiple-right : ∀ a b → (a + 3 * b) mod 3 ≡ a mod 3
        mod-+-multiple-right a b = begin
          (a + 3 * b) mod 3 ≡⟨ mod-+ a (3 * b) ⟩
          (a mod 3 + (3 * b) mod 3) mod 3 ≡⟨ cong (λ x → (a mod 3 + x) mod 3) (mod-mult₁ 3 b) ⟩
          (a mod 3 + 0) mod 3 ≡⟨ refl ⟩
          a mod 3 ∎
        -- 辅助引理：3*b模3等于0
        mod-mult₁ : ∀ a b → (a * b) mod a ≡ 0
        mod-mult₁ a b = mod-* a b 0 refl

    -- 右边模3等于2
    rhs-res : (3 * m + 5) mod 3 ≡ 2
    rhs-res = begin
      (3 * m + 5) mod 3 ≡⟨ mod-+ (3 * m) 5 ⟩
      ((3 * m) mod 3 + 5 mod 3) mod 3 ≡⟨ cong (λ x → (x + 2) mod 3) (mod-mult₁ 3 m) ⟩
      (0 + 2) mod 3 ≡⟨ refl ⟩
      2 ∎

    -- 导出n²模3等于2的矛盾式
    eq' : n * n mod 3 ≡ 2
    eq' = trans (sym lhs-equiv) (trans eq₂ rhs-res)

    -- 结合square-mod3的结论，证明该矛盾式不可能成立
    contra : n * n mod 3 ≡ 2 → ⊥
    contra p with square-mod3 n
    ... | inj₁ q = contradiction p (λ ())
    ... | inj₂ q = contradiction p (λ ())

关键说明 #

• +-*-Solver自动处理了复杂的代数展开和化简，避免了手动推导的繁琐和出错。
• 通过模运算找到的矛盾是自然数的固有性质，确保了证明的严谨性。
• 最终利用contradiction函数完成反证法，从原等式导出⊥（矛盾）。

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