7.2 決策程序：ring、omega、simp#

本章導讀#

本節介紹三位自動化好幫手： \(ring\) 、 \(omega\) 、 \(simp\) 。它們都是決策程序，也就是針對某一類問題保證能自動判定的小專家。學會何時派誰上場，你的證明會短一半，頭髮也會多留一半。

淺顯說明#

手算 \((a+b)^2\) 展開很煩，對吧？ \(ring\) 就是幫你做這種煩人展開的工人。你只要喊一聲 \(ring\) ，它就把等式兩邊都化成標準加總形式再比對。

\(omega\) 則是整數線性算術的會計師，專管加減法與大小比較。像是 \(x + 2 * y < 10\) 這類條件，它最拿手，但看到乘法 \(x * y\) 就會搖頭。

\(simp\) 像是大掃除隊長，手上有一大本化簡手冊。看到 \(x + 0\) 就擦成 \(x\) ，看到 \(if \; True\) 就擦成第一分支。你可以用 \(simp \; only\) 限制它只能用指定的幾條，也可以用 \(simp \; [h]\) 臨時多給它幾條。

簡單記憶法：等式含乘方找 \(ring\) ，線性不等式找 \(omega\) ，雜項化簡找 \(simp\) 。

正規理論#

決策程序的核心概念是正規形，也就是每個等價類選一個代表元。以交換環上的 \(ring\) 為例，它把多項式化為單項和：

\[ norm(\sum c_i \cdot m_i) = sorted([c_i, m_i]) \]

其中 \(c_i\) 是係數， \(m_i\) 是單項式，化簡後按字典序排序再合併同類項。判定等式 \(e_1 = e_2\) 時，只需檢查：

\[ norm(e_1) = norm(e_2) \]

這就是 \(ring\) 完備的原因：交換環公理下的等式恆真，當且僅當正規形一致。

\(omega\) 處理的是 Presburger 算術，即只含加法與序的整數片段。它的理論基礎是 Cooper 消元與 Omega 測試，把存在量詞逐一消去：

\[ \exists x, L(x) \iff DisjNorm(L) \]

其中 \(L(x)\) 是線性約束的合取， \(DisjNorm\) 是消元後的無量詞析取式。實務上你只需記得：線性加減加 \(omega\) 必勝，非線性乘法則無效。

\(simp\) 的理論是條件重寫系統 closure ，它不斷用等式由左向右改寫目標：

\[ Goal \xrightarrow{l = r} Goal[r/l] \xrightarrow{*} NormalForm \]

\(simp\) 集管理有三種模式，下表為選型指南：

工具	管轄範圍	典型輸入	範例呼叫
\(ring\)	交換環等式	\((x+y)^2\) 展開	\(ring\) 一鍵解決
\(omega\)	線性整數算術	\(x + 2 \le y\) 推論	\(omega\) 自動判定
\(simp\)	通用化簡	\(x + 0\) ， \(List.length\)	\(simp\) 或 \(simp \; only\)
\(simp \; only\)	精準化簡	只用指定引理	\(simp \; only \; [add_zero]\)
\(simp \; [h]\)	追加引理	在預設集上加 \(h\)	\(simp \; [h, add_comm]\)

三工具選型表如下，遇到新目標時照表發包：

目標形狀	首選	備註
環等式，無序無量詞	\(ring\)	含 \(+\) 、 \(*\) 、 \(pow\) 、 \(-\) 皆可
整數線性不等式	\(omega\)	含 \(<=\) 、 \(<\) 、 \(+\) 、常數乘法
含定義展開的雜項目標	\(simp\)	先 \(simp\) 再看殘留目標
怕 \(simp\) 亂改寫	\(simp \; only\)	白名單，最可預測
需搭配自家引理	\(simp \; [h]\)	黑名單加白名單混合

簡易範例#

以下三段各示範一種工具，建議在 VS Code 中逐行執行觀察目標變化。

-- ring：交換環正規形
example (a b : Int) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  ring

-- omega：線性算術
example (x y : Nat) (h1 : x + 2 * y ≤ 10) (h2 : 3 ≤ x) : y ≤ 3 := by
  omega

-- simp：化簡集管理
example (xs : List Nat) : xs ++ [] = xs := by
  simp

-- simp only：只用指定的引理，最安全
example (a : Nat) : a + 0 = a := by
  simp only [Nat.add_zero]

-- simp 加料：臨時加入自己的引理
example (a b : Nat) (h : b = 0) : a + b = a := by
  simp [h]

一個常見組合技是先 \(simp\) 清理，再 \(ring\) 或 \(omega\) 收尾：

example (a b : Nat) (h : b = 0) : (a + b) ^ 2 = a ^ 2 := by
  simp [h]
  ring

若 \(ring\) 卡住，先檢查是否有除法或非交換乘法；若 \(omega\) 失敗，多半是出現了 \(x * y\) 這類非線性項。

歷史典故#

自動化判定的野心由來已久，先看驗證編譯器。 CompCert 大量使用決策程序來消化瑣碎的算術 side condition ，沒有它們，編譯器正確性證明會膨脹數倍。

另一條線是現代 SMT 求解器，見 Z3 與 SMT 革命。 \(omega\) 背後的線性算術判定，正是 SMT 求解器最成熟的理論之一，Lean 把它內建成 tactic 。

最後別忘了奇階定理與 MathComp 。 MathComp 的 \(by \; rewrite\) 風格啟發了 \(simp\) 集的紀律：化簡必須可管理、可重演，而 \(simp \; only\) 正是這種紀律的體現。

習題#

用 \(ring\) 證明 \((a - b) * (a + b) = a^2 - b^2\) ，其中 \(a\) 與 \(b\) 為整數，並說明 \(ring\) 在背後做了哪兩步正規化。
構造一個 \(omega\) 會成功但 \(ring\) 會失敗的目標，再構造一個相反的例子，並用上表解釋原因。
比較 \(simp\) 、 \(simp \; only \; [Nat.add_zero]\) 、 \(simp \; [h]\) 三者的差別，並舉例說明何時該用最嚴格的 \(simp \; only\) 。