8.1 自寫 tactic 與元程式#

本章導讀#

本節教你從使用者變成工具作者，自己動手寫 tactic 。你會學到三層架構： \(syntax\) 定義語法， \(macro\) 做語法展開， \(elab\) 做完整元程式。外加一個關鍵觀念：衛生性，以及一個小實戰 \(my_have\) 。

淺顯說明#

tactic 本來就是小程式，只是平常你負責呼叫，現在換你來撰寫。想像你在廚房備料， \(syntax\) 是發明一道新菜名， \(macro\) 是把新菜名翻譯成舊食譜，而 \(elab\) 是直接走進廚房，想怎麼炒就怎麼炒，連鍋具都能換。

舉個例子，你每天都要寫 \(have \; h : P := by \; ...\) ，覺得很煩。於是你發明 \(my_have \; P\) ，讓它自動展開成標準寫法，這就是 \(macro\) 。若你想要讀取當前目標、動態產生證明項，那就需要 \(elab\) 出馬。

衛生性是這裡的靈魂，它保證你引入的新名字不會意外抓走使用者原本的名字。就像做菜時你的調味料不會自動跑進別人的湯裡，每個名字都有隱形的身份證。

正規理論#

Lean 4 的元程式有三層，由淺入深排列：

\[ syntax \subset macro \subset elab \]

三層的對照表如下：

層級	關鍵字	輸入輸出	能力與限制
語法層	\(syntax\)	字串轉語法樹	只定義外觀，不定義行為
展開層	\(macro\)	語法樹轉語法樹	可組合現有 tactic ，自動保持衛生性
精英層	\(elab\)	語法樹轉證明項	可存取 \(TacticM\) 、 \(TermElabM\) ，無所不能但要自保衛生性

衛生性的形式定義是：每個識別符都攜帶巨集作用域 \(msc\) 與頂層作用域 \(top\) 。

\[ ident = (name, msc, top) \]

展開時系統自動為新引入的名字加上新鮮的 \(msc\) ，因此：

\[ expand(my_have \; P) \cap FreeVars(ctx) = \emptyset \]

這保證了巨集引入的輔助假設不會捕捉使用者上下文中的同名變數。用一句話記住 \(simp\) 擴充：為引理標上 \(@[simp]\) 屬性就是向 \(simp\) 集註冊新規則，下次 \(simp\) 會自動用它重寫。

元程式的執行模型仍是目標轉換：

\[ Goals \xrightarrow{my\_tactic} Goals' \]

差別只在這次轉換函數是你寫的 Lean 程式，而 Lean 的 \(Quote\) 與 \(Splice\) 記號讓你能優雅地組裝語法樹。

簡易範例#

先看最簡單的 \(macro\) 實戰：把 \(my_have\) 展開成標準的 \(have\) 加 \(ring\) 收尾。

import Lean

-- 定義新語法：my_have 加一個項
syntax "my_have " term : tactic

-- 用 macro 展開：自動取名 h，後面接 ring
macro_rules
  | `(tactic| my_have $p) => `(tactic| (have h : $p := by ring; trace_state))

-- 使用範例
example (a b : Nat) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  my_have (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
  exact h

若需要讀取目標，就升級到 \(elab\) ，下面示範如何寫一個永遠先嘗試 \(rfl\) 的小 tactic 。

import Lean.Elab.Tactic.Basic

-- elab 版：取得主目標，嘗試 rfl，失敗就報錯
elab "my_rfl" : tactic => do
  let goal ← Lean.Elab.Tactic.getMainGoal
  Lean.Elab.Tactic.withMainContext do
    evalTactic (← `(tactic| rfl))
    pure ()

example : 1 + 1 = 2 := by
  my_rfl

最後示範 \(simp\) 擴充的一句話實踐：掛上屬性即註冊。

-- 掛上 simp 屬性，simp 會自動使用它
@[simp]
theorem my_add_zero (a : Nat) : a + 0 = a := Nat.add_zero a

example (x : Nat) : x + 0 + 0 = x := by
  simp

記住分工：能用 \(macro\) 就不要用 \(elab\) ，前者短小衛生，後者強大但要自己小心名字捕捉。

歷史典故#

元程式的祖師爺是 LCF 傳統，可惜不在本次配額內，就直接跳到 Lean 本家。先讀 Lean 誕生，體會 Leonardo de Moura 為何堅持證明器本身要用可程式化的框架打造。

接著看 Lean2 正式發布。 Lean2 首次把 Lua 腳本換成 Lean 自身的元語言，寫 tactic 不必再跳去別的語言。

最後是關鍵的飛躍，見 Lean4 自舉。 Lean4 用自己實現自己， \(syntax\) 、 \(macro\) 、 \(elab\) 三層正是這次重寫的結晶，也讓本節的 \(my_have\) 範例成為可能。

習題#

解釋 \(syntax\) 、 \(macro\) 、 \(elab\) 三層的差別，並說明為何 \(macro\) 自動保持衛生性而 \(elab\) 需要手動小心。
動手改寫 \(my_have\) ，讓它接受兩個參數並自動用 \(omega\) 收尾，測試它在線性算術目標上的行為。
寫一個標有 \(@[simp]\) 的小引理，並用 \(simp \; only\) 驗證它確實被註冊進 \(simp\) 集，再說明何時該用 \(simp\) 擴充而非自寫 \(elab\) 。