11.3 數學家的編程新體驗：讓編譯器幫你檢查邏輯漏洞#

theorem sqrt_two_irrational : ∀ p q : ℕ, q ≠ 0 → p * p = 2 * q * q → False := by
  intro p q hq heq
  -- 關鍵引理：p*p = 2*q*q 且互素 → 矛盾
  have hcopr : Nat.Coprime p q :=
    (Nat.coprime_of_mul_eq_two heq hq)  -- 需引入互素關係
  have hp2 : 2 ∣ p := by
    -- 若 2 ∤ p 則 p*p ≡ 1 (mod 2)，與 heq 矛盾
    by_contra h
    have : p * p % 2 = 1 := by
      rcases Nat.Even_or_Even_or_Odd p with h1 | h1
      · simp [Nat.Even, h1]  -- 簡化
      · have : p % 2 = 1 := h1
        omega
    omega
  have hq2 : 2 ∣ q := by
    have : 2 ∣ p * p := ⟨p, heq⟩
    exact (Nat.prime_two).dvd_of_dvd_mul_left this
  -- 2 ∣ p 且 2 ∣ q 與互素矛盾
  exact hcopr.coprime_dvd_left hp2 hq2 |>.elim

-- 錯誤陳述：忘記非空條件，定理變 trivially true
theorem bad (S : Finset ℕ) : ∀ x ∈ S, x > 0 := by
  intro x hx
  exact absurd (Finset.mem_singleton.mp hx) (by norm_num)  -- 編譯錯誤！
-- 編譯器指出：S 可以是空集，無法推出 x > 0

-- 兩者不等價！
example : ∀ n : ℕ, ∃ m : ℕ, m > n := fun n => ⟨n + 1, Nat.lt_succ_self n⟩
-- ∃ m, ∀ n, m > n 無法證明（編譯器會卡住，因為 m 必須先於 n 給定）

-- 若只想證 ←（充分性），卻寫了 Iff 的半邊，編譯器會卡在另一半
example : (1 : ℕ) < 2 ↔ True := by
  constructor
  · intro _; trivial
  · intro _; norm_num  -- 這邊也對，但若方向寫反會立即報錯

def sqrt_two_irrational():  # Python 只能「測試」
    """用連分數逼近檢查，非證明"""
    from mpmath import mp, mpf, sqrt as msqrt
    mp.dps = 50
    x = msqrt(2)
    # 檢查是否落在有理數密度極高的區間內——只能累積證據
    for q in range(2, 10000):
        p = round(x * q)
        if abs(mpf(p) / q - x) < mpf(10) ** -40:
            return False  # 發現良好逼近，仍非無理性證明
    return True  # 未發現 ≠ 證明

-- 定義自訂戰術：自動處理「兩邊平方且皆非負」型目標
macro "sq_nonneg" : tactic =>
  `(tactic| apply le_of_mul_le_mul_left <;> nlinarith)

-- 使用
example (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a ≤ b) :
    a * a ≤ b * b := by
  sq_nonneg  -- 戰術展開成多個基本推理步驟

-- decide 對有限命題自動構造證明
example : ∀ x : Bool, x = true ∨ x = false := by decide

-- 對較大的有限結構也有效（如 4×4 數獨解的存在性）