はじめに

本書のゴール

本書はLean4におけるメタプログラミングについて十分な知識を得ることを目的にしています：

  • 読者独自によるメタヘルパーを作るところから始めます（∑ のような新しいLeanの記法の定義や、#check のような新しいLeanコマンドの作成、use のようなタクティクの記述など）。
  • Lean4のコアやMathlib4にあるようなメタプログラミングAPIを読み、議論します。

決してLean4のメタプログラミングAPI全体を網羅的に説明するつもりはありません。また、Lean4のモナドによるプログラミングについての話題も扱いません。しかし、本書で提供する例が十分にシンプルであり、モナドプログラミングについての超深い理解がなくとも読者がフォローして理解できることを望みます。このテーマについては Functional Programming in Lean という本がお勧めです。 1

本書の構成

本書はDSLとタクティクを扱う章に十分な文脈を構築できるように構成されています。各章の前提条件を遡ると、依存関係は以下のような構造になっています：

  • 「タクティク」は「マクロ」と「エラボレーション」上に構築されます。
  • 「DSL」は「エラボレーション」上に構築されます。
  • 「マクロ」は「Syntax」上に構築されます。
  • 「エラボレーション」は「Syntax」と「MetaM」上に構築されます。
  • 「MetaM」は「式」上に構築されます。

タクティクの章の後には、重要な概念と帰納の総括を含むチートシートがありまず。そしてその後には付録としてLean4のメタプログラミングの応用例の章を用意しています。ほとのどの章の章末に演習問題があり、本の最後にはそれらの解答が載っています。

本章の残りはメタプログラミングとは何かについてやさしく紹介し、本書で扱う内容の前菜となるような小さな例をいくつか提供します。

注意：それぞれのコード片は自己完結していません。各章の初めから少しずつ実行/読むことを想定しています。

メタとはどういう意味か？

Python・C・Java・Scalaなどほとんどのプログラミング言語でコードを書くとき、通常はあらかじめ定義された構文に従わなければなりません。そうしなければコンパイラやインタプリタは我々の言わんとしていることを理解できないでしょう。Leanにおいては帰納型の定義、関数の実装、定理の証明などがこれにあたります。これを受けてコンパイラはコードをパースし、AST（抽象構文木）を構築し、その構文ノードを言語カーネルが処理できる項に精緻化しなければなりません。このようなコンパイラが行う活動は メタレベル で行われると表現され、これが本書を通じて学んでいくものです。また、言語構文の一般的な使用は オブジェクトレベル で行われると言います。

ほとんどのシステムでは、メタレベルの活動はコードの記述で使う言語とは別の言語で行われます。Isabelleでは、メタレベル言語はMLとScalaです。CoqではOcamlです。AgdaではHaskellです。Lean4では、C++で書かれたいくつかのコンポーネント以外、メタコードのほとんどはLean自身で記述されます。

しかし、Leanのステキな点は、オブジェクトレベルで活動するのとまったく同じ開発環境でカスタム構文ノードを定義し、それを精緻化するメタレベルのルーチンを実装できることです。例えば、ある型の項をインスタンス化し、同じファイル内ですぐに使用するための記法を書くことができます！この概念は一般的に リフレクション と呼ばれています。それゆえLeanでは、メタレベルはオブジェクトレベルに リフレクション されると言うことができます。

RubyやPython、Javascriptなどの言語でメタプログラミングをしたことがある人は、おそらく定義済みのメタプログラミング用のメソッドを利用してその場で何かを定義するという形をとったことがあるでしょう。例えば、Rubyでは Class.new と define_method を使ってプログラムの実行中に新しいクラスと新しいメソッドを定義することができます。

Leanでは通常、新しいコマンドやタクティクを「その場で」定義する必要はありませんが、Leanのメタプログラミングでも理屈上似たようなことが可能であり、同様に簡単に利用できます。例えば、シンプルなワンライナー elab "#help" : command => do ...normal Lean code... を使って新しいLeanのコマンドを定義できます。

しかし、Leanでは特にタクティクを書く場合などでは、「通常のLeanコード」を使うのではなく、LeanのCST（解析木、Leanでは Syntax 型）やAST（抽象構文木、Leanでは Expr 型）を直接操作したいと思うことがよくあります。したがって、Leanのメタプログラミングをマスターすることはより難しいものになります。本書の大部分はこれらの型とその操作方法を学ぶことに費やされます。

メタプログラミングの例

ここで、Leanのメタプログラミングの例をいくつか紹介し、Leanにおけるメタプログラミングがどのようなものであり、それによって何が達成できるかを味わってもらいます。これらの例は単なる説明のためのものであり、今のところは詳細が理解できなくても心配しないでください。

記法の導入（新しい構文の定義）

例えば数学（の一分野）に適した新しい記法を導入したい場合がよくあります。例えば、数学では自然数に 2 を加える関数を x : Nat ↦ x + 2 と書いたり、定義域が自然数であると推測できる場合は単に x ↦ x + 2 と書いたりします。これに対応するLeanの定義 fun x : Nat => x + 2 と fun x => x + 2 は => を使っていますが、これは数学では 含意 を意味するので、混乱する人もいるかもしれません。

macro を使って記法を導入し、Leanの構文（またはそれ以前に定義した構文）に変換することができます。ここでは、関数の ↦ 記法を導入します。

import Lean

macro x:ident ":" t:term " ↦ " y:term : term => do
  `(fun $x : $t => $y)

#eval (x : Nat ↦ x + 2) 2 -- 4

macro x:ident " ↦ " y:term : term => do
  `(fun $x  => $y)

#eval (x ↦  x + 2) 2 -- 4

コマンドの構築

与えられた項が特定の型であるかどうかを示すヘルパーコマンド #assertType を作りたいとします。これの使い方は次のようになります：

#assertType <term> : <type>

このコードを見てみましょう：

elab "#assertType " termStx:term " : " typeStx:term : command =>
  open Lean Lean.Elab Command Term in
  liftTermElabM
    try
      let tp ← elabType typeStx
      discard $ elabTermEnsuringType termStx tp
      synthesizeSyntheticMVarsNoPostponing
      logInfo "success"
    catch | _ => throwError "failure"

/-- info: success -/
#assertType 5  : Nat

/-- error: failure -/
#assertType [] : Nat

まず elab を使って command 構文を定義しました。コンパイラによってパースされると、計算が開始します。

この時点で、コードは CommandElabM モナド中で実行されるはずです。ここで TermElabM モナドにアクセスするために liftTermElabM を使用します。TermElabM モナドでは、elabType と elabTermEnsuringType を使って構文ノード typeStx と termStx から式を組み立てることができます。

まず、期待される型 tp : Expr を精緻化し、次にそれを使って項の式を作成します。この項は tp 型でなければならず、それ以外では例外が投げられます。次に、ここでは問題にならないため結果の項の式を捨てています。なぜなら elabTermEnsuringType はサニティチェックとして呼ばれているからです。

ここでLeanにメタ変数を精緻化するよう強制する synthesizeSyntheticMVarsNoPostponing も追加しています。この行がなければ、#assertType [] : ?_ は succsess となってしまいます。

例外が投げられなければ、精緻化は成功したことになり、logInfo を使って「success」と出力することができます。もしその代わりに何らかのエラーが発生した場合、適切なメッセージを添えて throwError を使用します。

DSLとそのための構文の構築

古典的な文法、つまり加算、乗算、自然数、変数を含む算術式の文法をパースしてみましょう。式のデータをエンコードするためにAST（抽象構文木）を定義し、演算子 + と * を使って算術ASTを構築します。これがこれから解析するASTです：

inductive Arith : Type where
  | add : Arith → Arith → Arith -- e + f
  | mul : Arith → Arith → Arith -- e * f
  | nat : Nat → Arith           -- constant
  | var : String → Arith        -- variable

ここで、構文解析を行う文法を記述するために構文カテゴリを宣言します。ここで + と * の優先順位をコントロールするために、* 構文よりも + 構文に低い優先順位の重みを与えることで、乗算は加算よりも強く束縛する（数字が大きいほど束縛が強くなる）ことを示していることに注意してください。これにより、新しい構文を定義する際に 優先順位 を宣言することができます。

declare_syntax_cat arith
syntax num                        : arith -- nat for Arith.nat
syntax str                        : arith -- strings for Arith.var
syntax:50 arith:50 " + " arith:51 : arith -- Arith.add
syntax:60 arith:60 " * " arith:61 : arith -- Arith.mul
syntax " ( " arith " ) "          : arith -- bracketed expressions

--# Auxiliary notation for translating `arith` into `term`
-- `arith` を `term` に変換するための補助記法
syntax " ⟪ " arith " ⟫ " : term

--# Our macro rules perform the "obvious" translation:
-- このマクロルールは「明白な」翻訳を行う
macro_rules
  | `(⟪ $s:str ⟫)              => `(Arith.var $s)
  | `(⟪ $num:num ⟫)            => `(Arith.nat $num)
  | `(⟪ $x:arith + $y:arith ⟫) => `(Arith.add ⟪ $x ⟫ ⟪ $y ⟫)
  | `(⟪ $x:arith * $y:arith ⟫) => `(Arith.mul ⟪ $x ⟫ ⟪ $y ⟫)
  | `(⟪ ( $x ) ⟫)              => `( ⟪ $x ⟫ )

#check ⟪ "x" * "y" ⟫
-- Arith.mul (Arith.var "x") (Arith.var "y") : Arith

#check ⟪ "x" + "y" ⟫
-- Arith.add (Arith.var "x") (Arith.var "y") : Arith

#check ⟪ "x" + 20 ⟫
-- Arith.add (Arith.var "x") (Arith.nat 20) : Arith

#check ⟪ "x" + "y" * "z" ⟫ -- precedence
-- Arith.add (Arith.var "x") (Arith.mul (Arith.var "y") (Arith.var "z")) : Arith

#check ⟪ "x" * "y" + "z" ⟫ -- precedence
-- Arith.add (Arith.mul (Arith.var "x") (Arith.var "y")) (Arith.var "z") : Arith

#check ⟪ ("x" + "y") * "z" ⟫ -- brackets
-- Arith.mul (Arith.add (Arith.var "x") (Arith.var "y")) (Arith.var "z")

自前のタクティクの記述

与えられた名前のコンテキストに新しい仮定を追加し、その証明の必要性を最後まで先送りするタクティクを作ってみましょう。Lean3の suffices タクティクと似ていますが、新しいゴールがゴールリストの一番下に来るようにした点が異なります。

これは suppose と呼ばれ、次のように使われます：

suppose <name> : <type>

それではコードを見てみましょう：

open Lean Meta Elab Tactic Term in
elab "suppose " n:ident " : " t:term : tactic => do
  let n : Name := n.getId
  let mvarId ← getMainGoal
  mvarId.withContext do
    let t ← elabType t
    let p ← mkFreshExprMVar t MetavarKind.syntheticOpaque n
    let (_, mvarIdNew) ← MVarId.intro1P $ ← mvarId.assert n t p
    replaceMainGoal [p.mvarId!, mvarIdNew]
  evalTactic $ ← `(tactic|rotate_left)

example : 0 + a = a := by
  suppose add_comm : 0 + a = a + 0
  rw [add_comm]; rfl     -- closes the initial main goal
  rw [Nat.zero_add]; rfl -- proves `add_comm`

まずメインゴールを mvarId に格納し、それを withMVarContext のパラメータとして使用することで、コンテキスト内の他の変数に依存する型でもエラボレーションが機能するようにしています。

今回は mkFreshExprMVar を使って t の証明のためのメタ変数式を作成し、それを intro1P と assert を使ってコンテキストに導入しています。

新しい仮定の証明をゴールとして要求するために、p.mvarId! を先頭に持つリストを渡して replaceMainGoal を呼び出します。そして rotate_left タクティクを使って最近追加された一番上のゴールを一番下に移動させます。

1

訳注：日本語訳は https://lean-ja.github.io/fp-lean-ja/