Lean4における記法の展開だけを行うsimpセットの作り方

これまで m < n の定義を展開するために dsimp [(· < ·), MyNat.lt] を何度も書いてきました。今回はこの手間を減らすためのタクティクを作成します。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。

単純な方法とその問題点

もっとも素朴な方法は、m < n ↔ m + 1 ≤ n という同値変形を simp に登録してしまうことです。

theorem MyNat.lt_def (m n : MyNat) : m < n ↔ m + 1 ≤ n := by
  rfl

section
  attribute [local simp] MyNat.lt_def

  example (m n : MyNat) : m < n := by
    simp_all
    guard_target =ₛ m + 1 ≤ n
    -- 不要な簡略化規則も適用されてしまっています
    sorry
end

この方法では simp を呼び出すと、MyNat.lt_def 以外の一般的なsimp規則も同時に適用されてしまいます。目的の展開だけを行いたい場合には不便です。

notation_simp の定義

register_simp_attr notation_simp によって専用のsimp属性を作成し、登録された定理だけを simp only で適用するマクロを用意します。

macro_rules
| `(tactic| notation_simp $[[$simpArgs,*]]? $[at $location]?) =>
  let args := simpArgs.map (·.getElems) |>.getD #[]
  `(tactic| simp only [notation_simp, $args,*] $[at $location]?)
end

これは「特定の記法（notation）を展開・簡約するためだけの専用のsimp定理セット（notation_simp）」を定義し、それを呼び出すための短いショートカットとしてタクティクを作成しているものです。

以下で notation_simp に MyNat.lt_def を登録します。

attribute [notation_simp] MyNat.lt_def

動作確認

実際に notation_simp では m < n だけが展開されることが確認できます。

example (m n : MyNat) : m < n := by
  notation_simp

  guard_target =ₛ m + 1 ≤ n
  sorry

notation_simp at * のように、通常の simp タクティクと同じ形で使用できます。

example (m n : MyNat) (h : m < n) : m + 1 ≤ n := by
  notation_simp at *
  assumption

また、simp 自体には影響を与えていないこともわかります。

example (m n : MyNat) : m < n := by
  -- `simp` made no progress
  -- simp

notation_simp? の追加

最後に、展開に使用された定理を表示できる notation_simp? を用意します。

section
open Lean Parser Tactic

syntax "notation_simp?" (simpArgs)? (location)? : tactic

macro_rules
| `(tactic| notation_simp? $[[$simpArgs,*]]? $[at $location]?) =>
  let args := simpArgs.map (·.getElems) |>.getD #[]
  `(tactic| simp? only [notation_simp, $args,*] $[at $location]?)

end

example (m n : MyNat) : m < n := by
  notation_simp?
  -- Try this:
  -- [apply] simp only [MyNat.lt_def]

コードは GitHubリポジトリ で公開しています。