はじめに

本書のゴール

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

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

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

本書の構成

本書は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 タクティクを使って最近追加された一番上のゴールを一番下に移動させます。

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

概要

この章では、パース・エラボレーション・評価など、Leanのコンパイルプロセスに関わる主なステップの概要を説明します。導入で言及したように、Leanのメタプログラミングはこのプロセスの核心に踏み込むことになります。まず基本的なオブジェクトである Expr と Syntax を探求し、それらが何を意味するかを学び、片方をもう一方に（そして反対方向に！）どのように変えることができるかを明らかにします。

次の章では、その詳細を学びます。本書を読み進めながら、時々この章に立ち返り、すべてがどのように組み合わさっているかを思い出すとよいでしょう。

コンパイラにアクセスする

Leanでのメタプログラミングは、パース、構文解析、変換、コード生成といったコンパイルのステップと深く関連しています。

Lean4はLeanの定理証明器をLean自体で再実装したものです。新しいコンパイラはCコードを生成し、ユーザはLeanで効率的な証明自動化を実装し、それを効率的なCコードにコンパイルしてプラグインとしてロードすることができます。Lean4では、Leanパッケージをインポートするだけで、Leanの実装に使用されるすべての内部データ構造にアクセスできます。

Leonardo de Moura, Sebastian Ullrich (The Lean 4 Theorem Prover and Programming Language)

Leanのコンパイルプロセスは以下の図にまとめることができます：

まず、Leanのコード自体である文字列から始まります。それから Syntax オブジェクトになり、次に Expr オブジェクトになります。最終的にそれを実行します。

そのため、コンパイラはLeanのコード文字列、例えば "let a := 2" を見て次のような処理を展開します：

関連する構文ルールの適用 ("let a := 2" ➤ Syntax)

構文解析のステップにおいて、Leanはコードの文字列を宣言された 構文ルール （syntax rules）のどれかにマッチさせ、その文字列を Syntax オブジェクトにしようとします。構文ルール と聞くと仰々しいですが基本的には正規表現です。ある 構文ルール の正規表現にマッチするLean文字列を書くと、そのルールは後続のステップの処理に使用されます。
すべてのマクロの繰り返し適用 (Syntax ➤ Syntax)

エラボレーションのステップでは、各 マクロ （macro）は既存の Syntax オブジェクトを新しい Syntax オブジェクトに単純に変換します。そして新しい Syntax は適用する マクロ が無くなるまで同じように処理が行われます（ステップ1と2を繰り返します）。
elabの単発適用 (Syntax ➤ Expr)

いよいよ構文に意味を吹き込む時です。Leanは name 引数によって適切な 構文ルール にマッチする elab を見つけます（構文ルール と マクロ、elabs はすべてこの引数を持っており、必ずマッチしなければなりません）。新しく見つかった elab は特定の Expr オブジェクトを返します。これでエラボレーションのステップは完了です。

この式（Expr）は評価ステップにおいて実行可能なコードに変換されます。このステップはLeanのコンパイラがよしなに処理してくれるため、指定をする必要はありません。

エラボレーションとデラボレーション

エラボレーション（elaboration）はLeanにおいて多重な意味を持つ用語です。例えば、「エラボレーション」という言葉について、「部分的に指定された式を受け取り、暗黙にされたものを推測する」 を意図した次のような用法に出会うことでしょう：

Leanが処理するために λ x y z, f (x + y) z のような式を入力する場合、あなたは情報を暗黙的なものとしています。例えば、x・y・z の型は文脈から推測しなければならず、+ という表記はオーバーロードされたものかもしれず、そして f に対して暗黙的に埋めなければならない引数があるかもしれません。

この 「部分的に指定された式を受け取り、暗黙にされたものを推測する」 プロセスは エラボレーション （elaboration）として知られています。Leanの エラボレーション アルゴリズムは強力ですが、同時に捉えがたく複雑です。依存型理論のシステムで作業するには、エラボレータ （elaborator）がどのような種類の情報を確実に推論できるかということを知っておくことに加え、エラボレータが失敗した時に出力されるエラーメッセージへの対応方法を知っておくことが必要です。そのためには、Leanの エラボレータ がどのように動作するかということへの一般的な考え方を知っておくと便利です。

Leanが式をパースするとき、まず前処理フェーズに入ります。最初に、Leanは暗黙の引数のための「穴」（hole）を挿入します。項tが Π {x : A}, P x という方を持つ場合、tは利用箇所すべてで @t _ に置き換えられます。次に穴（前のステップで挿入されたもの、またはユーザが明示的に記述したもの）はメタ変数 ?M1・?M2・?M3・... によってインスタンス化されます。オーバーロードされた各記法は選択肢のリスト、つまり取りうる解釈に関連付けられています。同様に、Leanは適用 s t に対して、推論されるtの型を s の引数の型と一致させるために型の強制を挿入する必要がある箇所を検出しようとします。これらも選択するポイントになります。あるエラボレーションの結果、型の強制が不要になる可能性がある場合、リスト上の選択肢の1つが恒等になります。

(Theorem Proving in Lean 2)

一方で、本書では Syntax オブジェクトを Expr オブジェクトに変換するプロセスとしてエラボレーションを定義しました。

これらの定義は相互に排他的なものではありません。エラボレーションとは、確かに Syntax から Expr への変換のことですが、ただこの変換を行うためには、暗黙の引数を推論したり、メタ変数をインスタンス化したり、ユニフィケーションを行ったり、識別子を解決したりなどなど、多くの技法が必要になります。そしてこれらのアクション自体もエラボレーションそのものとして言及されます；これは「部屋の電気を消したかどうかをチェックする」（メタ変数のインスタンス化）を「学校に行く」（エラボレーション）と呼ぶことができるのと同じです。

Leanにはエラボレーションと反対のプロセスも存在し、これは名実ともにデラボレーション（delaboration）と呼ばれます。デラボレーションにおいては、Expr が Syntax オブジェクトに変換されます；そしてフォーマッタがそれを Format オブジェクトに変換し、これがLeanのinfoviewに表示されます。画面に何かログが表示されたり、#check にカーソルを合わせて出力が表示されたりするのはすべてデラボレータ（delaborator）の仕事です。

本書全体を通して、エラボレータについての言及を目にすることでしょう；そして「付録：整形した出力」章では、デラボレータについて読むことができます。

3つの必須コマンドとその糖衣構文

さて、Leanのソースコードを呼んでいると、 パース/エラボレーション/評価のプロセスを指定するための11(+?)種のコマンドを見るでしょう：

上記の画像では notation・prefix・infix・postfix がありますが、これらはすべて macro と同じように syntax と @[macro xxx] def ourMacro を組み合わせたものです。これらのコマンドは macro と異なり、特定の形式の構文のみを定義することができます。

これらのコマンドはすべてLean自体やMathlibのソースコードで多用されるため覚えておく価値は十分にあります。しかし、これらのほとんどは糖衣構文であり、以下の3つの低レベルコマンドの動作を学んでおくことでその動作を理解することができます：syntax （構文ルール）・@[macro xxx] def ourMacro （マクロ）・@[command_elab xxx] def ourElab （elab）。

より具体的な例として、#help コマンドを実装しようとしているとします。そうすると、構文ルール・マクロ・elab を次のように書くことができます：

この図は一行ずつ読むことを想定していません。macro_rules と elab を併用しても何ら問題ありません。しかし、3つの低レベルコマンドを使って #help コマンド（最初の行）を指定したとしましょう。これによって、#help "#explode" もしくは #h "#explode" と書くことができます。どちらのコマンドも #explode コマンドのかなり簡素なドキュメントとして "Displays proof in a Fitch table" を出力します。

もし #h "#explode" と書くと、Leanは syntax (name := shortcut_h) ➤ @[macro shortcut_h] def helpMacro ➤ syntax (name := default_h) ➤ @[command_elab default_h] def helpElab というルートをたどります。もし #help "#explode" と書くと、Leanは syntax (name := default_h) ➤ @[command_elab default_h] def helpElab というルートをたどります。

構文ルール・マクロ・elab のマッチングは name 引数を介して行われることに注意してください。もし macro_rules や他の糖衣構文を使った場合、Leanは自力で適切な name 引数を見つけるでしょう。

コマンド以外のものを定義する場合、: command の代わりに : term や : tactic などの構文カテゴリを書くことができます。elab関数は #help の実装に使用した CommandElab だけでなく TermElab と Tactic など、さまざまな型を使用することができます：

TermElab は Syntax → Option Expr → TermElabM Expr の省略形で、elab関数は Expr オブジェクトを返すことが期待されます。
CommandElab は Syntax → CommandElabM Unit の省略形で、何も返さないべきです。
Tactic は Syntax → TacticM Unit の省略形で、何も返さないべきです。

これはLeanの項・コマンド・タクティクに対する直観的な理解に対応しています。項は実行時に特定の値を返し、コマンドは環境を変更したり何かを出力したりし、タクティクは証明の状態を変更します。

実行順序：構文ルール・マクロ・elab

これら3つの重要なコマンドの実行の流れについては、これまであちこちで匂わせてきましたが、ここで明確にしましょう。実行順序は次のような疑似的なテンプレートに従います：syntax (macro; syntax)* elab 。

以下の例を考えてみましょう。

import Lean
open Lean Elab Command

syntax (name := xxx) "red" : command
syntax (name := yyy) "green" : command
syntax (name := zzz) "blue" : command

@[macro xxx] def redMacro : Macro := λ stx =>
  match stx with
  | _ => `(green)

@[macro yyy] def greenMacro : Macro := λ stx =>
  match stx with
  | _ => `(blue)

@[command_elab zzz] def blueElab : CommandElab := λ stx =>
  Lean.logInfo "finally, blue!"

red -- finally, blue!

この処理は以下のように動きます：

適切な syntax ルールにマッチ（ここでは name := xxx）➤ @[macro xxx] を適用 ➤
適切な syntax ルールにマッチ（ここでは name := yyy）➤ @[macro yyy] を適用 ➤
適切な syntax ルールにマッチ（ここでは name := zzz）➤ zzz に適用されるマクロが見つからず、したがって @[command_elab zzz] を適用します。🎉。

糖衣構文（elab や macro 等）の挙動はこれらの第一原理から理解することができます。

`Syntax`/`Expr`/実行コード間の手動変換

Leanでは syntax・macro・elab を使うことで前述の パース/エラボレーション/評価のステップを自動的に実行してくれますが、しかしタクティクを書く際にはこれらの変換を頻繁に手動で行う必要が出るでしょう。この場合、以下の関数を使うことができます：

Syntax を Expr に変換する関数はすべて「elaboration」の略である「elab」で始まることに注意してください；また、Expr （もしくは Syntax）を実際のコードに変換する関数はすべて「evaluation」の略である「eval」から始まります。

代入の意味：マクロ vs エラボレーション？

原則として、elab 関数でできることは（ほとんど？）すべて macro でできます。ただ単に elab の本体にあるものを macro の中に構文として書くだけで良いです。ただし、この経験則を使うのは macro 使う方が変換が単純でエイリアスの設定が本当に初歩的であるときだけにすべきです。Henrik Böving に曰く：「型や制御フローが絡んでしまうとマクロはもはや妥当ではないでしょう」 (Zulip thread)。

従って、糖衣構文・記法・ショートカットを作るには macro を使い、プログラミングのロジックを含むコードを書き出す場合には、たとえ macro で実装できうるものだとしても elab を使いましょう。

追加のコメント

最後に、これからの章を読むにあたって、いくつかの事柄を明らかにしておきましょう。

メッセージの表示

#assertType の例ではコマンドに何かしら表示させるために logInfo を使いました。これの代わりにデバッグを素早く行いたい場合は dbg_trace を使うことができます。

しかし、以下に見るように両者の振る舞いは少し異なります：

elab "traces" : tactic => do
  let array := List.replicate 2 (List.range 3)
  Lean.logInfo m!"logInfo: {array}"
  dbg_trace f!"dbg_trace: {array}"

example : True := by -- `example` is underlined in blue, outputting:
                     -- dbg_trace: [[0, 1, 2], [0, 1, 2]]
  traces -- now `traces` is underlined in blue, outputting
         -- logInfo: [[0, 1, 2], [0, 1, 2]]
  trivial

型の正しさ

メタレベルで定義されるオブジェクトは定理証明において最も興味があるものではないため、型が正しいことを証明するのは時として退屈になりすぎることがあります。例えば、ある式をたどる再帰関数がwell-foundedであることの証明に関心はありません。そのため、関数が終了すると確信が持てるのなら partial キーワードを使うことができます。最悪のケースでは関数がループにはまり、Leanサーバがvscodeでクラッシュしてしまいますが、カーネルに実装されている基本的な型理論の健全性は影響を受けません。

式

式（Expr 型の項）はLeanプログラムの抽象構文木です。つまり、Leanで記述される各項には対応する Expr があります。例えば、関数適用 f e は式 Expr.app ⟦f⟧ ⟦e⟧ で表現されます。ここで ⟦f⟧ は f の表現であり、⟦e⟧ は e の表現です。同様に、Nat という項は Expr.const `Nat [] という式で表されます。（バッククォートと空リストについては後述します。）

Leanのタクティクブロックの最終的な目的は証明したい定理の証明となる項を生成することです。つまり、タクティクの目的は正しい型（の一部）の Expr を生成することです。したがって、メタプログラミングの多くは式を操作することに帰着します：新しい項を構成したり、既存の項を分解したりします。

タクティクブロックが終了すると、Expr はカーネルに送られます。カーネルはこの項がきちんと型付けされているか、定理が主張する型を本当に持っているかをチェックします。結果として、タクティクのバグは致命的なものにはなりません：もしミスがあっても、最終的にはカーネルがそれをキャッチしてくれます。しかし、多くのLeanの内部関数も式がきちんと型付けされていることを仮定しているため、式がカーネルに到達する前にLeanがクラッシュする可能性があります。これを避けるためにLeanは式の操作を支援する多くの関数を提供しています。この章と次の章では最も重要なものを調査します。

Expr の型について実際のものを見てみましょう：

import Lean

namespace Playground

inductive Expr where
  | bvar    : Nat → Expr                              -- bound variables
  | fvar    : FVarId → Expr                           -- free variables
  | mvar    : MVarId → Expr                           -- meta variables
  | sort    : Level → Expr                            -- Sort
  | const   : Name → List Level → Expr                -- constants
  | app     : Expr → Expr → Expr                      -- application
  | lam     : Name → Expr → Expr → BinderInfo → Expr  -- lambda abstraction
  | forallE : Name → Expr → Expr → BinderInfo → Expr  -- (dependent) arrow
  | letE    : Name → Expr → Expr → Expr → Bool → Expr -- let expressions
  -- less essential constructors:
  | lit     : Literal → Expr                          -- literals
  | mdata   : MData → Expr → Expr                     -- metadata
  | proj    : Name → Nat → Expr → Expr                -- projection

end Playground

それぞれのコンストラクタは何をするのでしょうか？

bvar は 束縛変数 （bound variable）です。例えば、fun x => x + 2 や ∑ x, x² などにおいての x です。これはある変数について、それの上に束縛子（binder）がいる場合のその式中での変数の出現を表します。なぜ引数は Nat なのでしょうか？これはde Bruijnインデックスと呼ばれるもので、後で説明します。束縛変数の型はその束縛子を見ればわかります。というのも束縛子は常にその変数の型の情報を持っているからです。
fvar は 自由変数 （free variable）です。これは束縛子で束縛されていない変数のことです。自由変数 x について、それを見ても型が何であるか知ることができないことに注意してください。型を知るには x とその型の宣言を含むコンテキストが必要です。自由変数にはIDがあり、これはその変数を LocalContext のどこを探せばよいかを教えてくれます。Lean 3では、自由変数は「ローカル変数」または「ローカル」と呼ばれていました。
mvar は メタ変数 （metavariable）です。これについては後ほど詳しく説明しますが、プレースホルダや、後で埋める必要のある表現のための「穴」と考えてもらえれば良いです。
sort は Type u や Prop などで使われます。
const はLeanの記述中でそこまでに定義済みの定数です。
app は関数適用です。複数の引数の場合は 部分適用 （partial application）を用います：f x y ↝ app (app f x) y。
lam n t b はラムダ式（fun ($n : $t) => $b）です。引数 b は本体（body）と呼ばれます。束縛する変数の型を指定する必要がある点に注意してください。
forallE n t b は依存矢印式（($n : $t) → $b）です。これはΠ型、もしくはΠ式とも呼ばれ、しばしば ∀ $n : $t, $b と書かれます。依存しない矢印 α → β は β が a に依存しない (a : α) → β の特殊な場合であることに注意してください。forallE の末尾の E は forall キーワードと区別するためのものです。
letE n t v b は let束縛子 （let binder）です（let ($n : $t) := $v in $b）。
lit は リテラル （literal）で、これは 4 や "hello world" などの数値や文字列のリテラルです。リテラルはパフォーマンスを向上させることに役立ちます：式 (10000 : Nat) を Nat.succ $ ... $ Nat.succ Nat.zero のように表現したくはありません。
mdata は式の性質を変えることなく、式に役立つかもしれない追加の情報を保存するためだけのものです。
proj は射影を表します。p : α × β のような構造体があるとすると、射影 π₁ p を app π₁ p として格納するのではなく、proj Prod 0 p と表現します。これは効率化のためです。

おそらく読者は明らかに対応する Expr を持たない多くのLeanプログラムを書くことができることに気付いているでしょう。例えば、match 文や do ブロック、by ブロックはどうすればいいのでしょうか？これらの構文やその他多くの構文はまず式に変換する必要があります。Leanにおいてこの（実質的な）タスクを実行する部分はエラボレータと呼ばれ、それ用の章で説明します。この構成の利点は、いったん Expr への変換が終われば、比較的単純な構造で作業ができることです。（欠点は Expr から高レベルのLeanプログラムに戻るのが難しいことです。）

エラボレータはまた、読者がLeanのプログラムで省略した暗黙の引数や型クラスのインスタンス引数も埋めます。このように Expr レベルでは暗黙的であろうとなかろうと、定数は常にすべての引数に適用されます。これは祝福（というのもソースコードでは明確でなかった多くの情報を得ることができるからです）であり、また呪い（Expr を組み立てる時に暗黙の引数やインスタンス引数を自分で指定しなければならないからです）でもあります。

De Bruijn インデックス

次のラムダ式 (λ f x => f x x) (λ x y => x + y) 5 を考えてみると、変数 x が衝突しているため、これを簡約する際には細心の注意を払う必要があります。

変数名の衝突を避けるために、Expr では de Bruijnインデックス と呼ばれる巧妙な技法を使用します。de Bruijnインデックスにおいて、lam や forallE で束縛された各変数は #n という数値に変換されます。この数字は、この変数を束縛している束縛子を見つけるために Expr ツリーの何番目の束縛子を探せばよいかを示しています。そのため、上記の例は次のようになります（簡潔にするために型引数にはワイルドカード _ を入れています）：app (app (lam `f _ (lam `x _ (app (app #1 #0) #0))) (lam `x _ (lam `y _ (app (app plus #1) #0)))) five。これでβ簡約を実行する際に変数名を変更する必要がなくなります。また、束縛された式を含む2つの Expr が等しいかどうかも簡単にチェックできます。これが bvar のシグネチャが Name → Expr ではなく Nat → Expr である理由です。

もしde Bruijnインデックスがそこまでに定義された束縛子の数よりも大きすぎる場合、loose bvar と言います；そうでない場合は 束縛されている と言います。例えば、式 lam `x _ (app #0 #1) では、bvar #0 は先行する束縛子によって束縛され、#1 はlooseです。Leanがすべてのde Bruijnインデックスを bvar （「束縛変数」）と呼んでいる事実は重要な不変性を示しています：いくつかの低レベルな関数以外では、Leanはすべての式がlooseな bvar を含まないことを期待しています。一方でlooseな bvar を導入したい場合は、直ちに fvar （「自由変数」）に変換します。この具体的な方法については次の章で説明します。

式の中にlooseな bvar が無い場合、その式は 閉じている （closed）と言います。looseな bvar のインスタンスをすべて Expr に置き換えるプロセスは インスタンス化 （instantiation）と呼びます。その逆は 抽象化 （abstraction）と呼ばれます。

もし読者が変数にまつわる標準的な用語に慣れているならLeanの用語は混乱するかもしれないので、ここで対応を挙げます：Leanでの「bvar」は通常単に「変数」と呼ばれます；「loose」は通常「自由」と呼ばれます；「fvar」は「ローカルな仮定」と呼ばれることがあります。

宇宙レベル

いくつかの式は Lean.Level 型で表される宇宙レベルを含みます。宇宙レベルは自然数であり、宇宙パラメータ（universe 宣言で導入されます）、宇宙メタ変数、または2つの宇宙の最大値となります。これらは2種類の式の表現に関連します。

まず、ソートは Expr.sort u で表現されます。ここで u は Level です。Prop は sort Level.zero です；Type は sort (Level.succ Level.zero) です。

次に、宇宙多相な定数は宇宙引数を持ちます。宇宙多相な定数とは宇宙パラメータを持つ型のことです。例えば、pp.universe オプションによる整形表示が示すように、List.map 関数は宇宙多相です：

set_option pp.universes true in
#check @List.map

List.map の接尾辞 .{u_1,u_2} は List.map が2つの宇宙引数 u_1 と u_2 を持つことを意味します。List の後の接尾辞 .{u_1} （これ自体が宇宙多相な定数）は List が宇宙引数 u_1 に適用されることを意味し、.{u_2} についても同様です。

実は、宇宙多相な定数を使うときは必ず正しい宇宙引数に適用しなければなりません。この適用は Expr.const の List Level 引数で表現されます。通常のLeanコードを書くとき、Leanは自動的に宇宙を推論するため、あまり考える必要はありません。しかし、自力で Expr を構築する際には、それぞれの宇宙多相な定数を正しい宇宙引数に適用するように注意しなければなりません。

式の構築

定数

もっとも単純な式は定数です。これにあたってはコンストラクタ const を使い、名前と宇宙レベルのリストを与えます。ここでのほとんどの例では宇宙多相ではない定数のみを使用しており、この場合リストは空になります。

また2つのバッククォートで名前を記述する第二の形式も示します。これは名前が実際に定義された定数を指しているかどうかをチェックするもので、タイプミスを避けるにあたって便利です。

open Lean

def z' := Expr.const `Nat.zero []
#eval z' -- Lean.Expr.const `Nat.zero []

def z := Expr.const ``Nat.zero []
#eval z -- Lean.Expr.const `Nat.zero []

また、バッククォート2つバージョンは与えられた名前を解決し、完全に修飾します。このメカニズムを説明するために、さらに2つの例を挙げましょう。1つ目の式 z₁ は安全ではありません：もし Nat 名前空間が開かれていないコンテキストで使用すると Leanは環境に zero という定数が無いと文句を言います。対照的に、2番目の式 z₂ は完全修飾名 Nat.zero を含んでおり、この問題はありません。

open Nat

def z₁ := Expr.const `zero []
#eval z₁ -- Lean.Expr.const `zero []

def z₂ := Expr.const ``zero []
#eval z₂ -- Lean.Expr.const `Nat.zero []

関数適用

次に考える式の話題は関数適用です。これらは app コンストラクタを使って構築することができ、第1引数には関数の式を、第2引数には引数の式を指定します。

ここでは2つの例を挙げます。ひとつは単純に定数を別の定数に適用したものです。もう一つは式を自然数の関数として与える再帰的定義です。

def one := Expr.app (.const ``Nat.succ []) z
#eval one
-- Lean.Expr.app (Lean.Expr.const `Nat.succ []) (Lean.Expr.const `Nat.zero [])

def natExpr: Nat → Expr
| 0     => z
| n + 1 => .app (.const ``Nat.succ []) (natExpr n)

次では、複数の引数を持つ適用を可能にする mkAppN を用いています。

def sumExpr : Nat → Nat → Expr
| n, m => mkAppN (.const ``Nat.add []) #[natExpr n, natExpr m]

お気づきかもしれませんが、最後の2つの関数については #eval の出力を示しませんでした。これは結果の式が大きくなりすぎて意味を理解するのが難しいからです。

ラムダ抽象

次にコンストラクタ lam を使って、任意の自然数を受け取って Nat.zero を返す単純な関数を作成します。引数の BinderInfo.default は x が（暗黙の引数や型クラスの引数ではなく）明示的な引数であることを表しています。

def constZero : Expr :=
  .lam `x (.const ``Nat []) (.const ``Nat.zero []) BinderInfo.default

#eval constZero
-- Lean.Expr.lam `x (Lean.Expr.const `Nat []) (Lean.Expr.const `Nat.zero [])
--   (Lean.BinderInfo.default)

宇宙レベルに絡んだより込み入った例として、以下の Expr は　List.map (λ x => Nat.add x 1) [] を表します（多少読みやすくするためにいくつかの定義に分割しています）：

def nat : Expr := .const ``Nat []

def addOne : Expr :=
  .lam `x nat
    (mkAppN (.const ``Nat.add []) #[.bvar 0, mkNatLit 1])
    BinderInfo.default

def mapAddOneNil : Expr :=
  mkAppN (.const ``List.map [levelZero, levelZero])
    #[nat, nat, addOne, .app (.const ``List.nil [levelZero]) nat]

ちょっとした技法を使えば（詳しくはエラボレーションの章で）、この Expr をLeanの項にして、より簡単に検査できるようにすることができます。

elab "mapAddOneNil" : term => return mapAddOneNil

#check mapAddOneNil
-- List.map (fun x => Nat.add x 1) [] : List Nat

set_option pp.universes true in
set_option pp.explicit true in
#check mapAddOneNil
-- @List.map.{0, 0} Nat Nat (fun x => x.add 1) (@List.nil.{0} Nat) : List.{0} Nat

#reduce mapAddOneNil
-- []

次の章では、MetaM モナドを探求します。このモナドは多くのほかのモナドの中において、より大きな式をより便利に構築・分解できるようにします。

演習問題

式 1 + 2 を Expr.app で作ってください。
式 1 + 2 を Lean.mkAppN で作ってください。
式 fun x => 1 + x を作ってください
[de Bruijn インデックス] 式 fun a, fun b, fun c, (b * a) + c を作ってください。
式 fun x y => x + y を作ってください。
式 fun x, String.append "hello, " x を作ってください。
式 ∀ x : Prop, x ∧ x を作ってください。
式 Nat → String を作ってください。
式 fun (p : Prop) => (λ hP : p => hP) を作ってください。
[宇宙レベル] 式 Type 6 を作ってください。

`MetaM`

Lean4のメタプログラミングAPIはモナドの小さな動物園を中心に構成されています。主なものは4つあります：

CoreM は環境（environment）へのアクセスを提供します。環境とは、そのプログラムでその時点までに宣言やインポートされたもののあつまりです。
MetaM は メタ変数コンテキスト へのアクセスを提供します。これはその時点までに宣言されているメタ変数と（もしあれば）それらに割り当てられている値のあつまりです。
TermElabM はエラボレーションの際に使用される様々な情報へのアクセスを提供します。
TacticM は現在のゴールのリストにアクセスできます。

これらのモナドはお互いに拡張されているため、MetaM の操作は環境へのアクセスも持ち、TermElabM の計算ではメタ変数を使うことができます。また、この階層にうまく当てはまらないモナドもあります。例えば CommandMonadM は MetaM を拡張していますが、TermElabM を拡張することも、されることもありません。

この章では MetaM モナドの便利な操作をいくつか紹介します。MetaM はすべての式の意味を利用者に与えてくれる点において特に重要です：（CoreM からの）環境は Nat.zero や List.map のような定数に意味を与え、メタ変数コンテキストはメタ変数とローカルの仮定の両方に意味を与えます。

import Lean

open Lean Lean.Expr Lean.Meta

メタ変数

概要

MetaM の「Meta」はメタ変数のことであるため、まずはメタ変数について話しましょう。Leanのユーザは通常メタ変数とあまり関わりません（少なくとも意識的には）が、これはメタプログラミングではあちこちで使われています。メタ変数には2つの見方があります：式の穴として見るか、ゴールとして見るかです。

まずはゴールとしての観点について取り上げましょう。Leanで物事を証明するとき、常に次のようなゴールに基づいて操作を行います：

n m : Nat
⊢ n + m = m + n

これらのゴールは内部的にはメタ変数で表現されます。したがって、各メタ変数は仮定を含む ローカルコンテキスト （ここでは [n : Nat, m : Nat]）と ターゲットの型 （ここでは n + m = m + n）を持ちます。また、メタ変数は一意な名前、例えば m を持ち、通常は ?m と表記します。

ゴールを閉じるには、ターゲットの型の式 e を与えなければなりません。この式にはメタ変数のローカルコンテキストの fvar を含めることができますが、それ以外を含めることはできません。内部的にはこの方法でゴールを閉じることは、メタ変数を 割り当てる （assign）ことに相当します；この割当は ?m := e と書かれます。

メタ変数の2つ目の補助的な見方は、メタ変数が式の穴を表すというものでした。例えば、Eq.trans を適用すると、次のようなゴールが生成されます：

n m : Nat
⊢ n = ?x

n m : Nat
⊢ ?x = m

ここで ?x は別のメタ変数で、両方のゴールのターゲットの型の穴であり、この証明でこの後埋める必要があります。?x の型は Nat であり、そのローカルコンテキストは [n : Nat, m : Nat] です。ここで、最初のゴールを反射律によって解く場合、?x は n でなければならないため、?x := n を割り当てます。きわめて重要なことですが、これは2番目のゴールにも影響します：2番目のゴールはターゲット n = m を持つように「更新」されます（後述しますが、実際には更新はされません）。メタ変数 ?x は出現するすべての個所で同じ式を表しているのです。

メタ変数を通じたタクティクとの会話

タクティクはメタ変数を使って現在のゴールを伝えます。その方法を知るために、次の簡単な（そして少々人為的な）証明を考えてみましょう：

example {α} (a : α) (f : α → α) (h : ∀ a, f a = a) : f (f a) = a := by
  apply Eq.trans
  apply h
  apply h

タクティクモードに入ると、最終的なゴールは仮定 α・a・f・h を含む f (f a) = a 型の式を生成することとなります。そこでLeanはターゲット f (f a) = a とこれらの仮定を含むローカルコンテキストを持つメタ変数 ?m1 を生成します。このメタ変数は現在のゴールとして最初の apply タクティクに渡されます。

次に apply タクティクで Ex.trans を適用を試し成功すると、3つの新しいメタ変数が生成されます：

...
⊢ f (f a) = ?b

...
⊢ ?b = a

...
⊢ α

これらのメタ変数は ?m2・?m3・?b と呼びます。最後の ?b は推移律の証明における中間要素を表し、?m2 と ?m3 に現れます。この証明におけるすべてのメタ変数のローカルコンテキストは同じであるため証明しています。

これらのメタ変数を作成した後、apply は以下を割り当て、

?m1 := @Eq.trans α (f (f a)) ?b a ?m2 ?m3

?m2・?m3・?b が現在のゴールとなったことを報告します。

この時点で2番目の apply タクティクが処理を引き継ぎます。これは ?m2 を現在のゴールとして受け取り、それを h に適用します。これは成功し、タクティクは ?m2 := h (f a) を割り当てます。この割当は ?b が f a でなければならないことを意味するため、タクティクは ?b := f a も割り当てます。割り当てられたメタ変数はオープンなゴールとはみなされないため、残るゴールは ?m3 だけとなります。

ここで3つ目の apply がやってきます。?b が割り当てられたため、?m3 のターゲットは f a = a となります。ここでも h の適用が成功し、タクティクは ?m3 := h a を割り当てます。

この時点で、すべてのメタ変数が次のように割り当てられました：

?m1 := @Eq.trans α (f (f a)) ?b a ?m2 ?m3
?m2 := h (f a)
?m3 := h a
?b  := f a

by ブロックを抜けると、Leanは ?m1 の割当を取り、各メタ変数でその割当を置き換えることで最終的な証明項を構築します。これにより以下を得ます。

@Eq.trans α (f (f a)) (f a) a (h (f a)) (h a)

この例ではメタ変数の2つの見方（式の穴として、あるいはゴールとして）がどのように関連しているかも示しています：最終的に得られたゴールは、最終的な証明項の穴です。

基本操作

これらの概念を具体的にしましょう。MetaM モナドで操作を行うとき、現在宣言されているメタ変数に関する情報を含む MetavarContext 構造体への読み書きアクセスを持ちます。各メタ変数は MVarId （これは一意な Name です）で識別されます。新しいメタ変数を作成するには、以下の型の Lean.Meta.mkFreshExprMVar を使用します。

mkFreshExprMVar (type? : Option Expr) (kind := MetavarKind.natural)
    (userName := Name.anonymous) : MetaM Expr

この引数はそれぞれ以下です：

type?：新しいメタ変数のターゲットの型。none の場合、ターゲットの型は Sort ?u となります。ここで ?u は宇宙レベルのメタ変数です。（これは宇宙レベルのメタ変数の特別なクラスであり、これまで単に「メタ変数」と呼んできた式についてのメタ変数とは区別されます。）
kind：メタ変数の種（kind）。詳しくはメタ変数の種 ¹ を参照してください（通常はデフォルト値が正しいです）。¹
userName：新しいメタ変数のユーザが目にする名前。これはメタ変数がゴールに現れる際に表示されるものになります。MVarId と異なり、この名前は一意である必要はありません。

返却される Expr は必ずメタ変数です。一意であることが保証されている MVarId を取り出すには Lean.Expr.mvarId! を使用します。（ただ、おそらく mkFreshExprMVar は MVarId を返すはずです）

新しいメタ変数のローカルコンテキストは現在のローカルコンテキストを継承します。異なるローカルコンテキストを与えたい場合は、Lean.Meta.mkFreshExprMVarAt を使用します。

メタ変数は初期化時は何も割り当てられません。割り当てるには以下の型を持つ Lean.MVarId.assign を使用します。

assign (mvarId : MVarId) (val : Expr) : MetaM Unit

この関数は MetavarContext を割当 ?mvarId := val で更新します。ここでこの mvarId が割り当てられていないことを確認しなければなりません（もしくは古い割当と新しい割当が定義上等しいことを確認する必要があります）。また、割り当てられた値 val が正しい型であることも確認しなければいけません。これは、(a) val が mvarId のターゲットの型を持たなければならないこと、(b) val が mvarId のローカルコンテキストの fvar しか含まなければならないことを意味します。

#check Lean.MVarId.assign を実行すると、その実際の型は上で示したものより一般的であることがわかります：これは MetavarContext へアクセスを持つ任意のモナドで機能します。しかし、MetaM はその中でも圧倒的に重要であるため、この章では assign や類似の関数の型を MetaM に限定します。

宣言されたメタ変数に関する情報を得るには、Lean.MVarId.getDecl を使用します。この関数は MVarId を渡すと MetavarDecl 構造体を返します。（もし指定された MVarId を持つメタ変数が宣言されていない場合、この関数は例外を投げます。）この MetavarDecl 構造体にはメタ変数についての情報、すなわちメタ変数の型・ローカルコンテキスト・ユーザが目にする名前などが格納されます。この関数には Lean.MVarId.getType などの便利なバージョンがあります。

メタ変数の現在の割り当てを取得するには（もしあれば）、Lean.getExprMVarAssignment? を使用します。メタ変数が割り当てられているかどうかを確認するには Lean.MVarId.isAssigned を使います。しかし、これらの関数がタクティクのコードで使われることは比較的少ないです。というのも大抵は以下の型を持つより強力な操作 Lean.Meta.instantiateMVars が好まれるからです。

instantiateMVars : Expr → MetaM Expr

式 e が与えられている時、instantiateMVars は e 内で割り当てられているメタ変数 ?m をその割当値で置き換えます。割り当てられていないメタ変数はそのままになります。

この操作は自由に使うべきです。メタ変数を割り当てると、そのメタ変数を含む既存の式はすぐには更新されません。これは、例えばある式が等式であるかどうかをチェックするためにマッチを行う際に問題になります。instantiateMVars を使わない場合、式 ?m が、例えばたまたま 0 = n が割り当てられているとした時に、それが等式を表していることを見逃してしまうかもしれません。言い換えると、instantiateMVars は式を現在のメタ変数の状態に合わせてくれるのです。

メタ変数のインスタンス化するには、入力式を完全に走査する必要があるため、実行コストが多少高くつくことがあります。しかし、入力式にメタ変数が含まれていない場合、instantiateMVars は基本的にタダです。これが一般的なケースであるため、ほとんどの状況では instantiateMVars の自由な使用は問題ありません。

先に進む前に、基本的なメタ変数操作がどのように使われるかを示す総合的な例を挙げましょう。より自然な例は以下の節に挙げます。

#eval show MetaM Unit from do
  -- `Nat` 型の新しいメタ変数を2つ作成する。
  let mvar1 ← mkFreshExprMVar (Expr.const ``Nat []) (userName := `mvar1)
  let mvar2 ← mkFreshExprMVar (Expr.const ``Nat []) (userName := `mvar2)
  -- `Nat → Nat` 型の新しいメタ変数を2つ作成する。`mkArrow` 関数は関数型を作ります。
  let mvar3 ← mkFreshExprMVar (← mkArrow (.const ``Nat []) (.const ``Nat []))
    (userName := `mvar3)

  -- 各メタ変数を表示する補助関数を定義。
  let printMVars : MetaM Unit := do
    IO.println s!"  meta1: {← instantiateMVars mvar1}"
    IO.println s!"  meta2: {← instantiateMVars mvar2}"
    IO.println s!"  meta3: {← instantiateMVars mvar3}"

  IO.println "Initially, all metavariables are unassigned:"
  printMVars

  -- `mvar1 : Nat := ?mvar3 ?mvar2` を割当。
  mvar1.mvarId!.assign (.app mvar3 mvar2)
  IO.println "After assigning mvar1:"
  printMVars

  -- `mvar2 : Nat := 0` を割当。
  mvar2.mvarId!.assign (.const ``Nat.zero [])
  IO.println "After assigning mvar2:"
  printMVars

  -- `mvar3 : Nat → Nat := Nat.succ` を割当。
  mvar3.mvarId!.assign (.const ``Nat.succ [])
  IO.println "After assigning mvar3:"
  printMVars
-- Initially, all metavariables are unassigned:
--   meta1: ?_uniq.1
--   meta2: ?_uniq.2
--   meta3: ?_uniq.3
-- After assigning mvar1:
--   meta1: ?_uniq.3 ?_uniq.2
--   meta2: ?_uniq.2
--   meta3: ?_uniq.3
-- After assigning mvar2:
--   meta1: ?_uniq.3 Nat.zero
--   meta2: Nat.zero
--   meta3: ?_uniq.3
-- After assigning mvar3:
--   meta1: Nat.succ Nat.zero
--   meta2: Nat.zero
--   meta3: Nat.succ

ローカルコンテキスト

一意な名前 h を参照している式 e について考えてみます：

e := .fvar (FVarId.mk `h)

この式の型は何でしょうか？この答えは e が解釈されるローカルコンテキストに依存します。あるローカルコンテキストでは h は Nat 型のローカルの仮定かもしれません；また別のローカルコンテキストでは List.map の値を持つローカル定義として宣言されているかもしれません。

したがって、式はそれが意図されたローカルコンテキストで解釈される場合にのみ意味を持ちます。そして先ほど見たように、各メタ変数はそれぞれ独自のローカルコンテキストを持っています。そのため原則的には、式を操作する関数には、その式の解釈を行うゴールを指定する MVarId 引数を追加する必要があります。

これは面倒であるため、Leanでは少し異なる道を選んでいます。MetaM では常にそれを取り囲む LocalContext にアクセスすることができます。これは以下の型を持つ Lean.getLCtx から得られます。

getLCtx : MetaM LocalContext

fvar を含むすべての操作は、この周囲のローカルコンテキストを使用します。

この仕組みの欠点は、周囲のローカルコンテキストを現在取り組んでいるゴールに合わせて常に更新する必要があることです。これを行うには以下の型の Lean.MVarId.withContext を使います。

withContext (mvarId : MVarId) (c : MetaM α) : MetaM α

この関数はメタ変数 mvarId と MetaM の計算 c を取り、周囲のコンテキストを mvarId のローカルコンテキストに設定した上で c を実行します。典型的な使用例は以下のようになります：

def someTactic (mvarId : MVarId) ... : ... :=
  mvarId.withContext do
    ...

このタクティクは現在のゴールをメタ変数 mvarId として受け取ると直ちに現在のローカルコンテキストを設定します。そして do ブロック内のすべての操作は mvarId のローカルコンテキストを使用します。

ローカルコンテキストを適切に設定することで、fvar を操作することができます。メタ変数と同様に fvar は FVarId （一意な Name）で識別されます。基本的な操作は以下の通りです：

Lean.FVarId.getDecl : FVarId → MetaM LocalDecl はローカルの仮定の宣言を取得します。メタ変数と同様に、 LocalDecl はローカルの仮定に関連するすべての情報、例えば型やユーザ向けの名前を含みます。
Lean.Meta.getLocalDeclFromUserName : Name → MetaM LocalDecl は与えられたユーザ向けの名前を持つローカルの仮定の宣言を取得します。もし該当する仮定が複数ある場合は、一番下のものが返されます。無い場合は例外が投げられます。

また、LocalContext の ForIn インスタンスを使用して、ローカルコンテキスト内のすべての仮定に対して反復処理を行うこともできます。典型的なパターンは以下のようになります：

for ldecl in ← getLCtx do
  if ldecl.isImplementationDetail then
    continue
  -- ldecl について何か行う。

このループはこのコンテキスト内のすべての LocalDecl を繰り返し処理します。isImplementationDetail によるチェックでは「実装の詳細」（これはLeanやタクティクによって記録目的で導入されたものを意味します）であるローカルの仮定はスキップされます。これらはユーザに表示されず、タクティクからは無視されることが期待されています。

この時点で、assumption タクティクの MetaM 部分を構築することができます：

def myAssumption (mvarId : MVarId) : MetaM Bool := do
  -- `mvarId` がすでに割当済みかどうかチェック。
  mvarId.checkNotAssigned `myAssumption
  -- `mvarId` のローカルコンテキストを使用する。
  mvarId.withContext do
    -- このターゲットは `mvarId` 型。
    let target ← mvarId.getType
    -- ローカルコンテキストの各仮定に対して：
    for ldecl in ← getLCtx do
      -- もしこの仮定が実装の詳細であればスキップ。
      if ldecl.isImplementationDetail then
        continue
      -- もしこの仮定の型がターゲットの型と定義上等しい場合：
      if ← isDefEq ldecl.type target then
        -- このローカルの仮定をゴールの証明に使用する。
        mvarId.assign ldecl.toExpr
        -- 処理を終了し、true を返す。
        return true
    -- もし適したローカルの仮定が見つからなければ、false を返す。
    return false

myAssumption タクティクにはこれまでに見たことのない3つの関数が含まれています：

Lean.MVarId.checkNotAssigned はメタ変数がすでに割当済みかどうかチェックします。上記で渡している「myAssumption」引数は現在のタクティクの名前です。これはより良いエラーメッセージを生成するために使用されます。
Lean.Meta.isDefEq は2つの定義が定義上等しいかどうかをチェックします。詳細は定義上の等しさの節を参照してください。
Lean.LocalDecl.toExpr はローカルの仮定に対応する fvar 式を構築する補助関数です。

遅延割当

上記のメタ変数の割当についての議論には意図的な嘘が含まれていました：メタ変数の割当には本当は2つの方法があります。ここまででは正規の方法を見てきました；もう一つの方法は 遅延割当 （delayed assignment）と呼ばれます。

遅延割当はタクティクの記述にはほとんど役に立たないので、ここでは詳しく説明しません。遅延割当について詳しく知りたいのであれば、Lean標準ライブラリの MetavarContext.lean のコメントを参照してください。しかし、遅延割当は2つの複雑な問題を引き起こすことを認識すべきです。

まず遅延割当によって、Lean.MVarId.isAssigned と getExprMVarAssignment? は自分の足を打ち抜く中口径の銃へと化します。これらの関数は通常の割当をチェックするだけであるため、Lean.MVarId.isDelayedAssigned と Lean.Meta.getDelayedMVarAssignment? を使う必要があるでしょう。

第二に、遅延割当は直観的な不変条件を破壊します。instantiateMVars の出力に残っているメタ変数は割り当てられていないと思われるかもしれません。というのも割り当てられたメタ変数は代入されるからです。しかし、遅延したメタ変数が代入されるのは、割り当てられた値に未割当のメタ変数が含まれていない場合のみです。そのため、instantiateMVars の後でも遅延割り当てられたメタ変数が式に現れることがあります。

メタ変数の深さ

メタ変数の深さもニッチな機能ですが、時折役に立ちます。どのメタ変数も（自然数の）深さ（depth）を持ち、MetavarContext にも対応する深さがあります。Leanはメタ変数の深さが現在の MetavarContext の深さと等しい場合にのみメタ変数を割り当てます。新しく作成されたメタ変数は MetavarContext の深さを継承するため、デフォルトではすべてのメタ変数が割り当て可能です。

この仕組みはタクティクが一時的なメタ変数を必要とし、かつ一時的でない他のメタ変数が割り当てられないようにする必要がある場合に使用できます。これを保証するために、タクティクは以下の順で処理します：

現在の MetavarContext を保存する。
MetavarContext の深さを加算する。
必要な計算を行い、場合によってはメタ変数を作成したり割り当てたりする。新しく作成されたメタ変数は MetavarContext の現在の深さにあるため割当を行うことができます。古いメタ変数の深さは浅いため、割り当てることができません。
保存された MetavarContext を復元する。これにより、一時的なメタ変数がすべて消去され、MetavarContext の深さがリセットされます。

このパターンは Lean.Meta.withNewMCtxDepth でカプセル化されています。

計算

計算は依存型理論の核となる概念です。項 2・Nat.succ 1・1 + 1 はすべて同じ値を計算するという意味で「同じ」です。これは 定義上等しい （definitionally equal）と呼ばれます。メタプログラミングの観点からすると、これには定義上等しい項が全く異なる式で表現される可能性があるという問題が付随します。しかし、ユーザは通常、2 に対して機能するタクティクは 1 + 1 に対しても機能することを期待するでしょう。そのため、タクティクを書くときには、定義上等しい項が同様に扱われるようにするための追加作業をしなければなりません。

完全正規化

計算でできることの中で最も単純なものは項を正規形にすることです。数値型のいくつかの例外を除いて、T 型の項 t の正規形は T のコンストラクタの適用の列です。例えば、リストの正規形は List.cons と List.nil の適用の列です。

項を正規化する（すなわち正規形にする）関数は Lean.Meta.reduce で、型シグネチャは以下の通りです。

reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : MetaM Expr

これは次のように使うことができます：

def someNumber : Nat := (· + 2) $ 3

#eval Expr.const ``someNumber []
-- Lean.Expr.const `someNumber []

#eval reduce (Expr.const ``someNumber [])
-- Lean.Expr.lit (Lean.Literal.natVal 5)

ちなみに、これは Nat 型の項の正規形が常に Nat のコンストラクタの適用であるとは限らないことを示しています；すなわち Nat はリテラルであることもあります。また、#eval は項を評価するだけでなく、MetaM プログラムを実行するためにも使用できます。

reduce のオプション引数を使うことで、式の特定の部分をスキップすることができます。例えば、reduce e (explicitOnly := true) は式 e の暗黙の引数を正規化しません。これはパフォーマンスを改善します：正規形は非常に大きくなる可能性があるため、ユーザが見ることのない部分をスキップすることは良いアイデアになり得ます。

#reduce コマンドは本質的には reduce の適用です：

#reduce someNumber
-- 5

透過度

Lean4のメタプログラミングの醜いが重要な点は、任意の式がただ1つの正規形を持たないことです。その代わりに、所与の 透過度 （transparency）までの正規形を持ちます。

透過度は Lean.Meta.TransparencyMode の値でこれは4つの値を持つ列挙型です：reducible・instances・default・all。どの MetaM の計算でも、周囲の TransparencyMode にアクセスすることができ、Lean.Meta.getTransparency で取得することができます。

現在の透過度は reduce などの正規化時にどの定数を展開するかを決定します。（定数の展開とは定数をその定義に置き換えるということを意味します。）4つの設定は段階的に多くの定数を展開します：

reducible：@[reducible] 属性でタグ付けされた定数のみを展開します。abbrev は @[reducible] def の省略形であることに注意してください。
instances：@[instance] 属性でタグ付けされた定数や簡約可能な定数を展開します。ここでもまた、instance は @[instance] def の省略形です。
default：@[irreducible] とタグ付けされた定数以外のすべての定数を展開します。
all：@[irreducible] とタグ付けされたものも含めてすべての定数を展開します。

環境の透過度は通常 default です。特定の透過度で操作を実行するには Lean.Meta.withTransparency を使用します。また例えば Lean.Meta.withReducible などの特定の透過度に対する省略形もあります。

これらすべてを例にまとめます（ここでは式を綺麗に表示するために Lean.Meta.ppExpr を使用しています）：

def traceConstWithTransparency (md : TransparencyMode) (c : Name) :
    MetaM Format := do
  ppExpr (← withTransparency md $ reduce (.const c []))

@[irreducible] def irreducibleDef : Nat      := 1
def                defaultDef     : Nat      := irreducibleDef + 1
abbrev             reducibleDef   : Nat      := defaultDef + 1

まず reducibleDef だけを展開する reducible から始めます：

#eval traceConstWithTransparency .reducible ``reducibleDef
-- defaultDef + 1

上記のコマンドを繰り返すだけでなく、Leanに暗黙の引数も表示させてみると、+ の表記が HAdd 型クラスのメンバーである hAdd 関数の適用に相当することがわかります：

set_option pp.explicit true
#eval traceConstWithTransparency .reducible ``reducibleDef
-- @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) defaultDef 1

instances の透過度で簡約する場合、この適用は展開され、Nat.add に置き換えられます：

#eval traceConstWithTransparency .instances ``reducibleDef
-- Nat.add defaultDef 1

default 透過度では、Nat.add が以下のように展開されます：

#eval traceConstWithTransparency .default ``reducibleDef
-- Nat.succ (Nat.succ irreducibleDef)

そして TransparencyMode.all で、ようやく irreducibleDef を展開できるようになります：

#eval traceConstWithTransparency .all ``reducibleDef
-- 3

この #eval コマンドは同じ項である reducibleDef がそれぞれの透過度に対して異なる正規形を持ちうることを表しています。

なぜこのような仰々しい儀式が必要なのでしょうか？基本的にはパフォーマンスのためです：もし正規化が常にすべての定数を展開されるようになると、型クラス探索のような操作は法外に高価になります。このトレードオフは、正規化を含む各操作に対して適切な透過度を選択しなければならないということです。

弱頭正規化

透過度を確保することで、いくつかの正規化のパフォーマンス上の問題に対処できます。しかし、それ以上に重要なことは、多くの目的においては項を完全に正規化する必要は全くないことを認識することです。P ∧ Q 型の仮定を自動的に分割するタクティクを構築しようとしていると仮定しましょう。もし X が P ∧ Q に簡約されるなら、このタクティクは仮定 h : X を認識させたいと思うかもしれません。しかし、もし P がさらに Y ∨ Z に簡約されるとしても、この特定の Y と Z はこのタクティクには無関係です。P を簡約することは不必要な作業です。

このような状況は非常に一般的であるため、完全に正規化する reduce は実際にはほとんど使われません。その代わり、Leanの正規化の主力は whnf で、これは式を 弱頭正規形 （weak head normal form, WHNF）に簡約します。

大雑把に言えば、式 e が弱頭正規形であるのは、それが次のような形を取り、

e = f x₁ ... xₙ   (n ≥ 0)

そして f が（現在の透過度では）簡約できない時です。式の WHNF を簡便にチェックするために、エラボレーションの章で説明するいくつかの関数を使って関数 whnf' を定義します。

open Lean.Elab.Term in
def whnf' (e : TermElabM Syntax) : TermElabM Format := do
  let e ← elabTermAndSynthesize (← e) none
  ppExpr (← whnf e)

さて、ここから WHNF の式の例をいくつか挙げます。

（数値型においてはいくつかの例外がありますが）コンストラクタの適用は WHNF です：

#eval whnf' `(List.cons 1 [])
-- [1]

WHNF の適用の引数は WHNF そのものである場合とそうでない場合があります：

#eval whnf' `(List.cons (1 + 1) [])
-- [1 + 1]

定数の適用は、現在の透過度が定数を展開することを許可しない場合、WHNF になります：

#eval withTransparency .reducible $ whnf' `(List.append [1] [2])
-- List.append [1] [2]

ラムダ式は WHNF です：

#eval whnf' `(λ x : Nat => x)
-- fun x => x

forall は WHNF です：

#eval whnf' `(∀ x, x > 0)
-- ∀ (x : Nat), x > 0

ソートは WHNF です：

#eval whnf' `(Type 3)
-- Type 3

リテラルは WHNF です：

#eval whnf' `((15 : Nat))
-- 15

WHNF である式の中でも、確認がちょっと厄介なものをいくつか紹介しましょう：

?x 0 1  -- Assuming the metavariable `?x` is unassigned, it is in WHNF.
h 0 1   -- Assuming `h` is a local hypothesis, it is in WHNF.

逆に、WHNF ではない式をいくつか挙げましょう。

定数の適用は、もし現在の透過度によって定数を展開できるのであれば WHNF ではありません：

#eval whnf' `(List.append [1])
-- fun x => 1 :: List.append [] x

ラムダ式の適用は WHNF ではありません：

#eval whnf' `((λ x y : Nat => x + y) 1)
-- `fun y => 1 + y`

let 束縛は WHNF ではありません：

#eval whnf' `(let x : Nat := 1; x)
-- 1

ここでまたいくつか厄介な例を挙げます：

?x 0 1 -- Assuming `?x` is assigned (e.g. to `Nat.add`), its application is not
          in WHNF.
h 0 1  -- Assuming `h` is a local definition (e.g. with value `Nat.add`), its
          application is not in WHNF.

本節の動機となったタクティクに戻り、余分な計算を割けて P ∧ Q という形の型にマッチする関数を書いてみましょう。WHNF であれば簡単です：

def matchAndReducing (e : Expr) : MetaM (Option (Expr × Expr)) := do
  match ← whnf e with
  | (.app (.app (.const ``And _) P) Q) => return some (P, Q)
  | _ => return none

whnf を使うことで、もし e が P ∧ Q のような形で評価されれば、それに気づくことができます。しかし、同時に P や Q で不必要な計算を行わないようにできます。

しかし、「無駄な計算をしない」というお題目は、式に対してより深いマッチングを行いたい場合には whnf を複数回使う必要があることも意味しています。例えば、P ∧ Q ∧ R という型のマッチを行いたいとしましょう。これを行う正しい方法は whnf を使うことです：

def matchAndReducing₂ (e : Expr) : MetaM (Option (Expr × Expr × Expr)) := do
  match ← whnf e with
  | (.app (.app (.const ``And _) P) e') =>
    match ← whnf e' with
    | (.app (.app (.const ``And _) Q) R) => return some (P, Q, R)
    | _ => return none
  | _ => return none

このくらいの計算までの深さのマッチであれば自動化できるかもしれません。しかし、誰かがこの自動化を構築するまでは、必要な whnf を自分で見つけ出さなければなりません。

定義上の等しさ

前述したように、定義上の等しさは計算においての同値です。2つの式 t と s は（現在の透過度において）正規形が等しい場合、定義上等しい、もしくは defeq となります。

2つの式が defeq であるかどうかをチェックするには、以下の型シグネチャを持つ Lean.Meta.isDefEq を使用します。

isDefEq : Expr → Expr → MetaM Bool

定義上の等しさは正規形で定義されていますが、実際には isDefEq は非常に高価になりうる引数の正規形の計算をすることはありません。その代わりに、t と s をできるだけ少ない簡約で「一致」させようとします。これは必然的に発見的な試みであり、この発見的な試みが失敗すると isDefEq は非常に高価になる可能性があります。最悪の場合、s と t を頻繁に簡約しなければならず、結局正規形になってしまうこともあります。しかし、通常はこの発見的な手法はうまく働き、isDefEq はそれなりに高速です。

式 t と u に割当可能なメタ変数が含まれている場合、isDefEq はこれらのメタ変数を代入して t と u に defeq となるようにすることができます。これは、isDefEq は t と u を 単一化 （unify）するとも言います；このようなユニフィケーションのクエリは t =?= u と書かれることもあります。例えば、ユニフィケーション List ?m =?= List Nat は成功し、?m := Nat を割り当てます。ユニフィケーション Nat.succ ?m =?= n + 1 は成功し、?m := n を割り当てます。ユニフィケーション ?m₁ + ?m₂ + ?m₃ =?= m + n - k は失敗し、メタ変数は（たとえ式の間に「部分一致」があっても）割り当てられません。

isDefEq がメタ変数を割り当て可能と見なすかどうかは、2つの要素によって決まります：

そのメタ変数の深さが現在の MetavarContext の深さと同じでなければならない。詳しくはメタ変数の深さについての節を参照してください。
それぞれのメタ変数が isDefEq の動作を変更することだけが目的の種（kind、MetavarKind 型の値）を持つこと。可能な種は以下の通りです：
- Natural：isDefEq はメタ変数を自由に割り当てます。これがデフォルトです。
- Synthetic：isDefEq はメタ変数を割り当てることができますが、可能であれば割当を避けます。例えば、?n がnaturalなメタ変数で、?s がsyntheticなメタ変数であるとします。ユニフィケーションの問題 ?s =?= ?n に直面したとき、isDefEq は ?s ではなく ?n に割当を行います。
- Synthetic opaque：isDefeq はメタ変数に割当を決して行いません。

式の構築

前の章では、式を構築するためにいくつかのプリミティブな関数を見ました：Expr.app・Expr.const・mkAppN などです。これらの関数に問題はありませんが、MetaM の追加機能によってより便利な方法が提供されます。

適用

普通のLeanのコードを書くとき、Leanは多くの暗黙の引数や宇宙レベルを推論してくれます。もしそうしてくれなければ、我々のコードはかなり醜くなってしまうでしょう：

def appendAppend (xs ys : List α) := (xs.append ys).append xs

set_option pp.all true in
set_option pp.explicit true in
#print appendAppend
-- def appendAppend.{u_1} : {α : Type u_1} → List.{u_1} α → List.{u_1} α → List.{u_1} α :=
-- fun {α : Type u_1} (xs ys : List.{u_1} α) => @List.append.{u_1} α (@List.append.{u_1} α xs ys) xs

接尾辞 .{u_1} は宇宙レベルであり、すべての多相な定数に与えなければなりません。そしてもちろん、この型 α はこの定義中のいたるところで渡されています。

メタプログラミングで式を組み立てる際にも、全く同じ問題が発生します。上記の定義の右辺の式を手作りすると次のようになります：

def appendAppendRHSExpr₁ (u : Level) (α xs ys : Expr) : Expr :=
  mkAppN (.const ``List.append [u])
    #[α, mkAppN (.const ``List.append [u]) #[α, xs, ys], xs]

暗黙の引数や宇宙レベルを指定しなければならないのは煩わしく、エラーになりやすいです。そこで MetaM は暗黙的な情報を省略するための補助関数を提供しています：以下の型の Lean.Meta.mkAppM です。

mkAppM : Name → Array Expr → MetaM Expr

mkAppN と同様に、mkAppM は適用を構築します。しかし、mkAppN はすべての宇宙レベルと暗黙の引数を渡す必要があるのに対し、mkAppM はそれらを推測してくれます。つまり、明示的な引数を与えるだけでよいため、より短い例を作ってくれます：

def appendAppendRHSExpr₂ (xs ys : Expr) : MetaM Expr := do
  mkAppM ``List.append #[← mkAppM ``List.append #[xs, ys], xs]

この例では α と u が一切ないことに注目してください。また mkAppM の変種として、第一引数に Name の代わりに Expr を取る mkAppM' があります。これによって定数ではない式の適用が可能になります。

しかし、mkAppM は魔法ではありません：例えば mkAppM ``List.append #[] と書くと実行時エラーとなります。これは mkAppM が α 型が何であるか判断しようとしても、append に引数が与えられていないため α は何でも良いこととなり、mkAppM が失敗するからです。

他の mkAppM の変種の中でしばしば便利であるのが、以下の型の Lean.Meta.mkAppOptM です。

mkAppOptM : Name → Array (Option Expr) → MetaM Expr

mkAppM が常に暗黙の引数とインスタンス引数を推論し、常に明示的な引数の提示を要求するのに対して、mkAppOptM ではどの引数を与え、どの引数を推論するのかを自由に選択することができます。これによって、例えばインスタンスを明示的に当てることができるようになり、以下の例のように標準ではない Ord インスタンスを渡すことが可能です。

def revOrd : Ord Nat where
  compare x y := compare y x

def ordExpr : MetaM Expr := do
  mkAppOptM ``compare #[none, Expr.const ``revOrd [], mkNatLit 0, mkNatLit 1]

#eval format <$> ordExpr
-- Ord.compare.{0} Nat revOrd
--   (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))
--   (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))

mkAppM と同様に、mkAppOptM はプライムがついた版の Lean.Meta.mkAppOptM' があり、最初の引数として Name の代わりに Expr を取ります。mkAppM を定義しているファイルには、リストのリテラルや sorry を作成するための様々な補助関数も含まれています。

ラムダ式と forall

他の一般的なタスクとして、λ または ∀ 束縛子を含む式を作成することです。例えば、λ (x : Nat), Nat.add x x という式を作りたいとします。1つの方法はラムダ式を直接書き出すことです：

def doubleExpr₁ : Expr :=
  .lam `x (.const ``Nat []) (mkAppN (.const ``Nat.add []) #[.bvar 0, .bvar 0])
    BinderInfo.default

#eval ppExpr doubleExpr₁
-- fun x => Nat.add x x

これは機能しますが、この bvar の使い方は非常に単調です。Leanではいわゆる locally closed な変数表現を用います。つまり、Lean APIの最低レベルの関数を除いて、すべての関数で式が「loose な bvar」を含まないことを想定しています。ここで bvar が loose であるとは同じ式中で束縛子に束縛されないものを指すのでした。（Lean 以外では、このような変数は通常「自由（free）」と呼ばれます。bvar、すなわち「束縛変数」は bvar が決して自由でないことをその名前で示しています。）

その結果、上記の例で mkAppN を少しレベルの高い mkAppM に置き換えると、実行時エラーが発生します。locally closed の規約に従い、mkAppM は与えられた式に loose な束縛変数が無いことを期待しており、.bvar 0 はまさにこれを満たします。

そこで、bvar を直接使う代わりに、Leanでは2つのステップで束縛変数を持つ式を構築する方針をとります：

一時的なローカルの仮定（fvar）を束縛変数の代わりに使い、式の本体（この例ではラムダ式の本体）を構築します。
これらの fvar を bvar に置き換え、同時に、これに対応するラムダ式の束縛子を追加します。

この処理によって、loose な bvar を持つ式をどのタイミングにおいても扱う必要がなくなります（例外的にステップ2の間は特注の関数によって「アトミックに」実行されます）。このプロセスを例に当てはめると：

def doubleExpr₂ : MetaM Expr :=
  withLocalDecl `x BinderInfo.default (.const ``Nat []) λ x => do
    let body ← mkAppM ``Nat.add #[x, x]
    mkLambdaFVars #[x] body

#eval show MetaM _ from do
  ppExpr (← doubleExpr₂)
-- fun x => Nat.add x x

ここでは新しい関数が2つあります。まず、Lean.Meta.withLocalDecl は以下の型を持ちます。

withLocalDecl (name : Name) (bi : BinderInfo) (type : Expr) (k : Expr → MetaM α) : MetaM α

変数名と束縛子の情報、型が与えられると、withLocalDecl は新しい fvar を作成して k の計算に渡します。fvar は k の実行中はローカルコンテキストで利用可能ですが、実行後に削除されます。

2つ目の新しい関数は Lean.Meta.mkLambdaFVars で、以下の型を持ちます（ここではいくつかのオプション引数を無視しています）。

mkLambdaFVars : Array Expr → Expr → MetaM Expr

この関数は fvar の配列と式 e を取ります。そして各 fvar x に対してラムダの束縛子を1つずつ追加し、e 内で出現する x をすべて新しいラムダの束縛子に対応する束縛変数に置き換えます。こうして返される式は一切 fvar を含みません。withLocalDecl コンテキストを抜けると fvar は消えてしまうためこれは良いことです。（fvar の代わりに mkLambdaFVars に mvar を与えることもできます。）

上記の関数のいくつかの変種が役に立つでしょう：

withLocalDecls は複数の一時的な fvar を宣言します。
mkForallFVars は λ の束縛子の代わりに ∀ の束縛子を作成します。mkLetFVars は let の束縛子を作成します。
mkArrow は mkForallFVars の非依存版で、関数型 X → Y を構築します。この型は非依存であるため、一時的な fvar は不要です。

これらの関数をすべて使えば、次のような大きな式を作ることができます：

λ (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1)

def somePropExpr : MetaM Expr := do
  let funcType ← mkArrow (.const ``Nat []) (.const ``Nat [])
  withLocalDecl `f BinderInfo.default funcType fun f => do
    let feqn ← withLocalDecl `n BinderInfo.default (.const ``Nat []) fun n => do
      let lhs := .app f n
      let rhs := .app f (← mkAppM ``Nat.succ #[n])
      let eqn ← mkEq lhs rhs
      mkForallFVars #[n] eqn
    mkLambdaFVars #[f] feqn

次の例では、今作った式の名前として someProp を登録しており、より扱いやすくしています。このメカニズムについてはエラボレーションの章で説明します。

elab "someProp" : term => somePropExpr

#check someProp
-- fun f => ∀ (n : Nat), f n = f (Nat.succ n) : (Nat → Nat) → Prop
#reduce someProp Nat.succ
-- ∀ (n : Nat), Nat.succ n = Nat.succ (Nat.succ n)

式の分解

MetaM で式をより簡単に構築できるように、式をより簡単に分解することもできます。特に便利なのは、λ と ∀ の束縛子で始まる式を分解する関数群です。

∀ (x₁ : T₁) ... (xₙ : Tₙ), U という形式の型が与えられた時、たいていの場合は結論 U で何をするかということに興味があります。例えば、apply タクティクは e : ∀ ..., U という式が与えられた時、U と現在のターゲットを比較し、e が適用できるかどうかを判断します。

これを行うには、U にたどり着くまで ∀ の束縛子を取り除きながら型の式のマッチを繰り返せば良いです。しかし、これでは束縛されてない bvar を含んだ U が残ってしまい、これは見てきたようにまずいです。その代わりに、以下の型の Lean.Meta.forallTelescope を使用します。

forallTelescope (type : Expr) (k : Array Expr → Expr → MetaM α) : MetaM α

type = ∀ (x₁ : T₁) ... (xₙ : Tₙ), U x₁ ... xₙ が与えられると、この関数は各 ∀ の束縛変数 xᵢ に対して fvar fᵢ を1つずつ作成し、結論 U の各 xᵢ を fᵢ で置換します。次に、fᵢ と結論 U f₁ ... fₙ を渡して計算 k を呼び出します。この計算の中で、fᵢ はローカルコンテキストに登録されます；最終的に、これらは削除されます（withLocalDecl と同様です）。

forallTelescope には便利なバリエーションがたくさんあります：

forallTelescopeReducing：これは forallTelescope と似ていますが、マッチが計算にまで実行されます。つまり、∀ x, P x と異なるが defeq である式 X がある時、forallTelescopeReducing X は X を x と P x に分解します。これに対し非簡約的な forallTelescope は X を量化された式とは認識しません。このマッチは基本的に周囲の透過度を使用して whnf を繰り返し呼び出すことで行われます。
forallBoundedTelescope：これは forallTelescopeReducing と（名前に「reducing」が入っていませんが）似ていますが、これはマッチを指定した数分の ∀ 束縛子の後に停止します。
forallMetaTelescope・forallMetaTelescopeReducing・forallMetaBoundedTelescope：これらはそれぞれ対応する非 meta 版の関数と似ていますが、ここでの束縛変数は fvar の代わりに新しい mvar に置換されます。非 meta 版の関数とは異なり、この meta 版の関数は計算を行った後に新しいメタ変数を削除しないため、メタ変数は無期限に環境に残り続けます。
lambdaTelescope・lambdaTelescopeReducing・lambdaBoundedTelescope・lambdaMetaTelescope：これらは対応する forall 関数と似ていますが、∀ の代わりに λ の束縛子を対象にしています。

テレスコープ関数の1つを使って、独自の apply タクティクを実装することができます：

def myApply (goal : MVarId) (e : Expr) : MetaM (List MVarId) := do
  -- ゴールが未割当かどうかチェックする。
  goal.checkNotAssigned `myApply
  -- このゴールのローカルコンテキストで操作を行う。
  goal.withContext do
    -- ゴールのターゲットの型を取得。
    let target ← goal.getType
    -- 与えられた式の型を取得。
    let type ← inferType e
    -- `type` が `∀ (x₁ : T₁) ... (xₙ : Tₙ), U` の形式を持つ場合、
    -- `xᵢ` に対応する新しいメタ変数を導入し、この結論 `U` を取得する。
    -- （もし `type` がこの形式でない場合、`args` は空で `conclusion = type`　となる。）
    let (args, _, conclusion) ← forallMetaTelescopeReducing type
    -- この結論がこのターゲットを単一化する場合：
    if ← isDefEq target conclusion then
      -- ゴールに `e x₁ ... xₙ` を割り当てる。ここで `xᵢ` は `args` の中の新鮮なメタ変数。
      goal.assign (mkAppN e args)
      -- `isDefEq` は `args` の中のいくつかのメタ変数を割り当てるかもしれないため、
      -- その結果残った新しいゴールを報告する。
      let newGoals ← args.filterMapM λ mvar => do
        let mvarId := mvar.mvarId!
        if ! (← mvarId.isAssigned) && ! (← mvarId.isDelayedAssigned) then
          return some mvarId
        else
          return none
      return newGoals.toList
    -- この結論がターゲットを単一化しない場合、例外を投げる。
    else
      throwTacticEx `myApply goal m!"{e} is not applicable to goal with target {target}"

実際の apply はいくつかの追加の前処理と後処理を行いますが、核となるロジックはここで紹介したものです。このタクティクをテストするには、エラボレーションの呪文が必要です。詳しくはエラボレーションの章で説明します。

elab "myApply" e:term : tactic => do
  let e ← Elab.Term.elabTerm e none
  Elab.Tactic.liftMetaTactic (myApply · e)

example (h : α → β) (a : α) : β := by
  myApply h
  myApply a

バックトラッキング

多くのタクティクはバックトラッキングを当然のものとして必要とします：これは以前の状態へ戻る能力で、あたかもそのタクティクが実行されていなかったかのようになります。いくつか例を挙げましょう：

first | t | u はまず t を実行します。もし t が失敗したら、バックトラックして u を実行します。
try t は t を実行します。もし t が失敗したら、初期状態へとバックトラックし、 t による変更を消去します。
trivial はいくつかのシンプルなタクティク（例えば rfl や contradiction）を使用してゴールを解こうとします。これらのタクティクの適用が成功しなかった場合、trivial はバックトラックします。

良いことに、Leanのコアデータ構造は簡単かつ効率的なバックトラックができるように設計されています。対応する API は Lean.MonadBacktrack クラスで提供されます。MetaM・TermElabM・TacticM はすべてこのクラスのインスタンスです。（CoreM はそうではありませんが、そうなる可能性があります。）

MonadBacktrack は2つの基礎的な操作を提供しています：

Lean.saveState : m s は現在の状態の表現を返します。ここで m は利用しているモナドで、s は状態の型です。例えば MetaM の場合、saveState は現在の環境、現在の MetavarContext とその他様々な情報を含む Lean.Meta.SavedState を返します。
Lean.restoreState : s → m Unit は以前に保存された状態を取り出し、復元します。これは効率的にコンパイラの状態を前の時点のものにリセットします。

これによって、try タクティクの MetaM バージョンを独自に開発することができます：

def tryM (x : MetaM Unit) : MetaM Unit := do
  let s ← saveState
  try
    x
  catch _ =>
    restoreState s

まず状態を保存し、次に x を実行します。もし x が失敗したら状態をバックトラックします。

標準ライブラリには tryM のようなコンビネータがたくさん定義されています。ここでは最も便利なものを紹介します：

Lean.withoutModifyingState (x : m α) : m α はアクション x を実行し、状態をリセットして x の結果を返します。これは例えばメタ変数を代入せずに定義が等しいかどうかをチェックするために使うことができます：
```
withoutModifyingState $ isDefEq x y
```
もし isDefEq が成功すると、x と y にメタ変数が割り当てられる可能性があります。withoutModifyingState を使えば、このようなことが起こらないようにすることができます。
Lean.observing? (x : m α) : m (Option α) はアクション x を実行します。x が成功すると、observing? はその結果を返します。x が失敗した場合（例外を投げた場合）、observing? は状態をバックトラックして none を返します。これは tryM コンビネータのより情報量に富んだバージョンです。
Lean.commitIfNoEx (x : α) : m α は x を実行します。x が成功すると、commitIfNoEx はその結果を返します。x が例外を投げた場合、commitIfNoEx は状態をバックトラックして例外を投げ直します。

ここで組み込みの try ... catch ... finally はバックトラックを行わないことに注意してください。したがって、次のようなコードはおそらく間違っています：

try
  doSomething
catch e =>
  doSomethingElse

catch の枝の doSomethingElse は、doSomething が失敗する前に行った変更を含む状態で実行されます。これらの変更を消去したいはずであるので、代わりにこのように書くべきです：

try
  commitIfNoEx doSomething
catch e =>
  doSomethingElse

もう一つの MonadBacktrack の欠点は、restoreState は状態全体をバックトラックしないことです。キャッシュ・トレースメッセージ・グローバル名のジェネレータなどはバックトラックされないため、これらの部分に加えられた変更は restoreState でリセットされません。これは通常望ましいことです：observing? によって実行されたタクティクがトレースメッセージを生成した場合、そのタクティクが失敗してもトレースメッセージを見ることができます。バックトラックされるものと、されないものの詳細については、Lean.Meta.SavedState.restore と Lean.Core.restore を参照してください。

次の章では、この章ですでに何度か垣間見たエラボレーションの話題に移ります。まずLeanの構文システムについて説明します。このシステムではLeanのパーサにカスタムの構文を追加することができます。

演習問題

[メタ変数] Nat 型のメタ変数を作成し、値 3 を割り当ててください。ここでメタ変数の型を Nat から例えば String に変更してもエラーにならないことに注してください。そのため前述の通り、「(a) その val が mvarId のターゲットの型を持ち、(b) val が mvarId のローカルコンテキストにある fvarId しか含まないこと」を確認する必要があります。
[メタ変数] instantiateMVars (Lean.mkAppN (Expr.const 'Nat.add []) #[mkNatLit 1, mkNatLit 2]) は何を出力するでしょうか？

[メタ変数] 以下のコードの欠けている行を埋めてください。

#eval show MetaM Unit from do
  let oneExpr := Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero [])
  let twoExpr := Expr.app (Expr.const `Nat.succ []) oneExpr

  -- Create `mvar1` with type `Nat`
  -- let mvar1 ← ...
  -- Create `mvar2` with type `Nat`
  -- let mvar2 ← ...
  -- Create `mvar3` with type `Nat`
  -- let mvar3 ← ...

  -- Assign `mvar1` to `2 + ?mvar2 + ?mvar3`
  -- ...

  -- Assign `mvar3` to `1`
  -- ...

  -- Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1`
  ...

[メタ変数] 下記の定理 red とタクティク explore について考えてみましょう。 a) メタ変数 mvarId の type と userName は何になるでしょうか？ b) このメタ変数のローカルコンテキストにあるすべてのローカル宣言の type と userName は何になるでしょうか？それらをすべて表示させてください。
```
elab "explore" : tactic => do
  let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
  let metavarDecl : MetavarDecl ← mvarId.getDecl

  IO.println "Our metavariable"
  -- ...

  IO.println "All of its local declarations"
  -- ...

theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
  explore
  sorry
```
[メタ変数] 上記の定理 red を証明するタクティク solve を書いてください。
[計算] 以下の式の正規形は何になるでしょうか？ a) Bool → Bool 型の fun x => x b) Bool 型の (fun x => x) ((true && false) || true) c) Nat 型の 800 + 2
[計算] Expr.lit (Lean.Literal.natVal 1) で作られた 1 と Expr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero []) で作られた式が定義上等しいことを示してください。
[計算] 以下の式が定義上等しいかどうか判定してください。もし Lean.Meta.isDefEq が成功し、メタ変数の割り当てを導くなら、その割当も書き下してください。 a) 5 =?= (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z)) b) 2 + 1 =?= 1 + 2 c) ?a =?= 2、ここで ?a は String 型 d) ?a + Int =?= "hi" + ?b、ここで ?a と ?b は型を持ちません e) 2 + ?a =?= 3 f) 2 + ?a =?= 2 + 1

[計算] 次のコードが何を出力することを期待するか書き下してください。

@[reducible] def reducibleDef     : Nat := 1 -- same as `abbrev`
@[instance] def instanceDef       : Nat := 2 -- same as `instance`
def defaultDef                    : Nat := 3
@[irreducible] def irreducibleDef : Nat := 4

@[reducible] def sum := [reducibleDef, instanceDef, defaultDef, irreducibleDef]

#eval show MetaM Unit from do
  let constantExpr := Expr.const `sum []

  Meta.withTransparency Meta.TransparencyMode.reducible do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- ...

  Meta.withTransparency Meta.TransparencyMode.instances do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- ...

  Meta.withTransparency Meta.TransparencyMode.default do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- ...

  Meta.withTransparency Meta.TransparencyMode.all do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- ...

  let reducedExpr ← Meta.reduce constantExpr
  dbg_trace (← ppExpr reducedExpr) -- ...

[式の構築] 式 fun x, 1 + x を2通りで構築してください： a) loose な束縛変数を含んだ単調な方法 b) 便利な関数を用いる方法 Lean.mkAppN はどちらのバージョンで使用できるでしょうか？また、Lean.Meta.mkAppM はどちらのバージョンで使用できるでしょうか？
[式の構築] 式 ∀ (yellow: Nat), yellow を構築してください。
[式の構築] 式 ∀ (n : Nat), n = n + 1 を2通りで構築してください： a) loose な束縛変数を含んだ単調な方法 b) 便利な関数を用いる方法 Lean.mkApp3 はどちらのバージョンで使用できるでしょうか？また、Lean.Meta.mkEq はどちらのバージョンで使用できるでしょうか？
[式の構築] 式 fun (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1) を便利な関数を用いる方法で構築してください。

[式の構築] 次のコードの出力はどうなるでしょうか？

#eval show Lean.Elab.Term.TermElabM _ from do
  let stx : Syntax ← `(∀ (a : Prop) (b : Prop), a ∨ b → b → a ∧ a)
  let expr ← Elab.Term.elabTermAndSynthesize stx none

  let (_, _, conclusion) ← forallMetaTelescope expr
  dbg_trace conclusion -- ...

  let (_, _, conclusion) ← forallMetaBoundedTelescope expr 2
  dbg_trace conclusion -- ...

  let (_, _, conclusion) ← lambdaMetaTelescope expr
  dbg_trace conclusion -- ...

[バックトラッキング] isDefEq を使用して ?a + Int と "hi" + ?b が定義上等しいことをチェックしてください（メタ変数の型には適切な型、または Option.none を使用してください！）。メタ変数の割り当てを戻すには、saveState と restoreState を使用してください。

原文のリンクは「メタ変数の種（#metavariable-kinds）」の節へのリンクでしたが、該当する節が無くリンクが切れていたため、種について取り上げていた節にリンクを張るようにしています。

構文

この章では、Leanにおける構文の宣言とその操作方法について説明します。構文を操作する方法はたくさんあるため、この章ではまだ詳細にあまり深入りせず、ほとんどを後の章に先送りします。

構文の宣言

宣言のためのヘルパー

読者の中には infix や notation コマンドまでもご存じの方もいるかもしれませんが、そうでない方のために簡単におさらいしておきましょう：

import Lean

-- XOR, denoted \oplus
infixl:60 " ⊕ " => fun l r => (!l && r) || (l && !r)

#eval true ⊕ true -- false
#eval true ⊕ false -- true
#eval false ⊕ true -- true
#eval false ⊕ false -- false

-- with `notation`, "left XOR"
notation:10 l:10 " LXOR " r:11 => (!l && r)

#eval true LXOR true -- false
#eval true LXOR false -- false
#eval false LXOR true -- true
#eval false LXOR false -- false

見てわかるように、infixl コマンドによって二項演算の記法を宣言することができます。この二項演算は中置（infix）、つまり演算子がオペランドの間にあることを意味します（これに対して例えば prefix コマンドでは意味が異なります）。infxl の末尾の l は、この記法が左結合であることを意味しており、つまり a ⊕ b ⊕ c は a ⊕ (b ⊕ c) ではなく（これは infixr で実現されます）、(a ⊕ b) ⊕ c とパースされます。このコマンドの右側では、これら2つのパラメータを操作して何らかの値を返す関数を期待しています。一方で、notation コマンドではより自由度が増します：構文定義の中でパラメータをただ「言及」するだけで、右側でそれを操作することができます。これにとどまらず、notation コマンドを使えば、理論的には0から任意の数のパラメータを指定した構文を作ることができます。このためこのコマンドはしばしば「mixfix」記法と呼ばれます。

この2つについて直観的でない部分が2つあります：

演算子の周りに空白を空けていること：「 ⊕ 」、「 LXOR 」。こうすることで、Lean がこれらの構文を後から整形表示する際に、演算子の周りにもスペースを使うようになります。そうしないと構文は l ⊕ r ではなく l⊕r と表示されてしまいます。
60 や 10 などのそれぞれのコマンドの直後にある値は、演算子の優先順位、つまり引数との結合の強さを示しています。このことについて実際の挙動を見てみましょう：

#eval true ⊕ false LXOR false -- false
#eval (true ⊕ false) LXOR false -- false
#eval true ⊕ (false LXOR false) -- true

見てわかるように、Lean のインタプリタは括弧のない最初の項を3つ目の項ではなく2つ目の項と同じようにパースしています。これは ⊕ 記法が LXOR より優先順位が高いため（つまるところ 60 > 10 であるため）、LXOR より先に評価されます。これは * が + の前に評価されるようなルールを実装する方法でもあります。

最後に、この notation の例では、引数に :precedence バインディングがあります：すなわち l:10 と r:11 です。これは左の引数の優先順位が少なくとも 10 以上、右の引数の優先順位が少なくとも 11 以上でなければならないことを意味しています。引数にそれぞれの優先順位を割り当てるには、その引数自体をパースするために使われたルールの優先順位を見ることで行われます。例えば a LXOR b LXOR c を考えてみましょう。理論的にはこれは2つのパースの仕方があります：

(a LXOR b) LXOR c
a LXOR (b LXOR c)

括弧内の引数は優先順位 10 の LXOR ルールによってパースされるため、これらはその外側の LXOR ルールにとっては優先順位 10 の引数として表示されます：

(a LXOR b):10 LXOR c
a LXOR (b LXOR c):10

しかし、LXOR：notation:10 l:10 " LXOR " r:11 の定義をチェックしてみると、右側の引数には少なくとも 11 以上の優先順位が必要であるため、2つ目のパースは不正であり、パース結果は (a LXOR b) LXOR c となり以下が仮定されます：

a は 10 以上の優先順位を持つ
b は 11 以上の優先順位を持つ
c は 11 以上の優先順位を持つ

従って、LXOR は左結合な記法です。読者はこれを右結合にできますか？

注意：ある記法のパラメータに明示的な優先順位が与えられていない場合、それらは暗黙的に優先順位 0 とタグ付けされます。

この節の最後のコメント：Lean は常に可能な限り広いマッチを行おうと試行します。これは3つの重要な意味を持ちます。まず非常に直観的なことですが、ある右結合演算子 ^ があり、Lean が a ^ b ^ c のような式を見た場合、まず a ^ b をパースし、（優先順位が許す限り）これ以上続けられなくなるまでパースを続けようとします。この結果 Lean はこの式を（読者が期待するように）a ^ (b ^ c) とパースします。

第二に、例えば優先順位によって式のどこに括弧が入るかわからないような記法がある場合、例えば以下のような場合を考えます：

notation:65 lhs:65 " ~ " rhs:65 => (lhs - rhs)

a ~ b ~ c のような式は a ~ (b ~ c) としてパースされます。これは Lean が可能な限り広い範囲のパースを見つけようとするからです。一般的な経験則として：優先順位が曖昧な場合、Lean はデフォルトで右結合を使用します。

#eval 5 ~ 3 ~ 3 -- 5 because this is parsed as 5 - (3 - 3)

最後に、下記のような既存のものに被る記法を定義しようとした場合：

-- `a ~ b mod rel` を、ある同値関係 rel に関して a と b が同値であることとして定義
notation:65 a:65 " ~ " b:65 " mod " rel:65 => rel a b

ここで Lean は a ~ b について、先ほどの定義でパースしてしまって mod と関係についての引数をどうしたらよいかわからずにエラーにしてしまうよりも、この記法を利用したいでしょう：

#check 0 ~ 0 mod Eq -- 0 = 0 : Prop

ここでも可能な限り最長のパーサを探すため、mod とその関係についての引数を消費します。

自由形式の構文宣言

上記の infix と notation コマンドを使えば、普通の数学構文を宣言するだけで、すでにかなり遠くまで行けるようになります。しかし、Lean では任意で複雑な構文を導入することもできます。これには syntax と declare_syntax_cat コマンドを使います。syntax コマンドを使うと、既存のいわゆる「構文カテゴリ」に新しい構文ルールを追加することができます。最も一般的な構文カテゴリは以下の通りです：

term、このカテゴリについてはエラボレーションの章で詳しく説明しますが、今のところは「値を持つすべてのもののための構文」と考えておけば良いです。
command、これは #check や def などのトップレベルコマンドのカテゴリです。
TODO: ...

これらを実際に見てみましょう：

syntax "MyTerm" : term

これで 1 + 1 などの代わりに MyTerm と書くことができ、構文的に （syntactically）有効になります。これはコードがコンパイルできる状態であるという意味ではなく、Lean のパーサがそれを理解できるという意味です：

#check_failure MyTerm
-- elaboration function for 'termMyTerm' has not been implemented
--   MyTerm

注意：#check_failure コマンドを使用すると、型付けが正しくない項をエラー無く表示できます。

このいわゆる「エラボレーション関数」の実装は、Lean の基本的な型 Expr の観点からこの構文に実際の意味を与えるものであり、エラボレーションの章で扱う話題です。

notation と infix コマンドは構文宣言とマクロ宣言（マクロについてはマクロの章を参照）を便利にまとめたユーティリティであり、=> の左側の内容で構文を宣言します。前に述べた notation と infix の優先順位に関する原則はすべて syntax にも適用されます。

もちろん、構文木を構築するために、他の構文を独自の宣言に含めることも可能です。例えば、小さな真偽値の表現言語を作ってみることもできます：

namespace Playground2

-- このスコープ修飾子によって、これらの構文宣言がこの `namespace` の中のみに閉じられるようになります。
-- というのもこれらの構文はこの章でこの後も変更するからです。
scoped syntax "⊥" : term -- ⊥ for false
scoped syntax "⊤" : term -- ⊤ for true
scoped syntax:40 term " OR " term : term
scoped syntax:50 term " AND " term : term
#check_failure ⊥ OR (⊤ AND ⊥) -- elaboration function hasn't been implemented but parsing passes

end Playground2

これは機能しますが、AND と OR 演算の左右に任意の項が置けてしまいます。もし構文レベルで真偽値言語だけを受け付けるミニ言語を書きたい場合は、独自の構文カテゴリを宣言する必要があります。これは declare_syntax_cat コマンドを使って行います：

declare_syntax_cat boolean_expr
syntax "⊥" : boolean_expr -- ⊥ for false
syntax "⊤" : boolean_expr -- ⊤ for true
syntax:40 boolean_expr " OR " boolean_expr : boolean_expr
syntax:50 boolean_expr " AND " boolean_expr : boolean_expr

これで独自の構文カテゴリにて作業するようになったため、システムの他の部分とは完全に切り離されました。そして、これらの構文はもはや任意の項で使うことができません：

#check ⊥ AND ⊤ -- expected term

この構文カテゴリをシステムの他の部分に統合するためには、既存の構文を新しい構文で拡張する必要があります。今回の場合は、term のカテゴリに再埋め込みします：

syntax "[Bool|" boolean_expr "]" : term
#check_failure [Bool| ⊥ AND ⊤] -- elaboration function hasn't been implemented but parsing passes

構文コンビネータ

より複雑な構文を宣言するためには、構文に対する基本的な操作がすでに組み込まれていることが望ましいことが多いです。これには以下が含まれます：

構文カテゴリを持たない（つまり拡張できない）補助パーサ
選択肢
繰り返されるパーツ
オプショナルなパーツ

これらはすべて構文カテゴリに基づいたエンコーディングを持っていますが、場合によっては非常に不格好になることがあるため、Lean はこれらすべてを簡単に行う方法を提供しています。

これらすべての動作を確認するために、簡単なバイナリ式の構文を定義します。まず初めに、構文カテゴリに属さない名前付きパーサを宣言します。これは普通の def とよく似ています：

syntax binOne := "O"
syntax binZero := "Z"

これらの名前付き構文パーサは上記の構文カテゴリと同じ位置で使用することができますが、構文カテゴリとの唯一の違いは拡張性がないことです。つまり、構文宣言の中で直接展開されるため、適切な構文カテゴリのように新しいパターンを定義することができません。名前付きのパーサには一般的に便利な組み込みがいくつか存在しており、以下は特記に値するものです：

文字列リテラル用の str
数値リテラル用の num
識別子用の ident
... TODO: better list or link to compiler docs

次に数字を理解するパーサを宣言したいです。 2 進数の数字は 0 か 1 であるため、次のように書くことができます：

syntax binDigit := binZero <|> binOne

ここで <|> 演算子は「左右どちらかを受け入れる」動作を実装しています。また、これらを連鎖させて、任意の数・任意の複雑な他の構文を受け入れるパーサを実現することもできます。ここで 2 進数の概念を定義します。通常、 2 進数は数字を直接並べて書きますが、ここでは繰り返しを表現するためにカンマ区切りの表現を使います：

-- 「+」は「1以上」を示す。「0以上」を実現するには代わりに「*」を使う
-- 「,」は `binDigit` の間の区切り文字を示す。もし省略された場合、デフォルトの区切り文字はスペースになる
syntax binNumber := binDigit,+

構文カテゴリの代わりに名前付きパーサを使えばよいため、これを term カテゴリに簡単に追加することができます：

syntax "bin(" binNumber ")" : term
#check bin(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
#check bin() -- fails to parse because `binNumber` is "one or many": expected 'O' or 'Z'

syntax binNumber' := binDigit,* -- note the *
syntax "emptyBin(" binNumber' ")" : term
#check_failure emptyBin() -- elaboration function hasn't been implemented but parsing passes

パーサごとに 1 つの構文コンビネータしか使えないという制限は一切ないことに注意してください。これらをすべてインラインに記述することも可能です：

syntax "binCompact(" ("Z" <|> "O"),+ ")" : term
#check_failure binCompact(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes

最後の機能として、宣言されている 2 進数リテラルを説明するオプションの文字列コメントを追加しましょう：

-- (...)? 構文は括弧内がオプショナルであることを意味します
syntax "binDoc(" (str ";")? binNumber ")" : term
#check_failure binDoc(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
#check_failure binDoc("mycomment"; Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes

構文に対する操作

上記で説明したように、この章では構文に与えたい意味を Lean に伝える方法については詳しく触れません。しかし、構文を操作する関数の書き方については見ていきます。Lean での他のものと同様に、構文は Lean.Syntax という帰納型によって表現されています。これによって構文を操作することが可能です。この型にはかなり多くの情報が含まれていますが、興味があることのほとんどは次のように単純化できます：

namespace Playground2

inductive Syntax where
  | missing : Syntax
  | node (kind : Lean.SyntaxNodeKind) (args : Array Syntax) : Syntax
  | atom : String -> Syntax
  | ident : Lean.Name -> Syntax

end Playground2

コンストラクタの定義を1つずつ見ていきましょう：

missing は Lean のコンパイラによってパースできないようなものがある際に使われます。このおかげで Lean はファイルの一部で構文エラーがあっても、そこから回復してファイルの残りの部分を理解しようとします。これはまた、このコンストラクタはあまり気にされないものであるということでもあります。
node は名前の通り、構文木のノードです。ノードは kind : SyntaxNodeKind と呼ばれるものを持っています。この SyntaxNodeKind はただの Lean.Name です。基本的に、各 syntax 宣言は自動的に生成された SyntaxNodeKind を受け取り（この名前は syntax (name := foo) ... : cat で明示的に指定することもできます）、これによって Lean に「この関数は特定の構文構築を行う責任がある」ということを伝えます。さらに、木の中の全てのノードと同様に、この関数にも子があり、この場合は Array Syntax をいう形式をとっています。
atom は（1つを除いて）階層の一番下にあるすべての構文オブジェクトを表します。例えば、上の演算子 ⊕ と LXOR は atom として表現されます。
ident は atom で前述したこのルールの例外です。ident と atom の違いは実に明白です：識別子はそれを表すにあたって String の代わりに Lean.Name を持ちます。なぜ Lean.Name が単なる String ではないのかはマクロの章で詳しく説明するマクロの健全性（macro hygiene）と呼ばれる概念に関連しています。今のところ、これらは基本的に等価であると考えることができます。

新しい `Syntax` の構築

Lean で構文がどのように表現されるか学んだので、もちろんのことながらこれらの帰納的な木をすべて手作業で生成するプログラムを書くことができますが、これは恐ろしく退屈であり間違いなく最高に避けたい作業です。幸運なことに、Lean.Syntax 名前空間には非常に広範囲な API が秘められています：

open Lean
#check Syntax -- Syntax. autocomplete

Syntax を作るための興味深い関数は Syntax.mk* で、identのような基本的な Syntax オブジェクトの作成だけでなく、 Syntax.mkApp による複雑なオブジェクトも作成することができます。Syntax.mkApp によって、第1引数の関数を第2引数の引数リスト（すべて Syntax として与えられます）に適用することに相当する Syntax オブジェクトを作成することができます。いくつか例を見てみましょう：

-- 名前のリテラルは名前の前にちょっと ` を付けて書きます
#eval Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"] -- is the syntax of `Nat.add 1 1`
#eval mkNode `«term_+_» #[Syntax.mkNumLit "1", mkAtom "+", Syntax.mkNumLit "1"] -- is the syntax for `1 + 1`

-- `«term_+_» は + の構文用に自動生成された SyntaxNodeKind であることに注意

もし読者が Syntax を作成するこの方法を全く好まないのあれば、著者も全く同感です。しかし、これを綺麗で正しい方法で行うための機構（上記の機構はだいたい正しい部分を担います）は、マクロの章でもいくつか説明します。

`Syntax` に対するマッチ

Syntax の構築が重要なトピックであるように、特にマクロでは構文のマッチも同様に（あるいは実はそれ以上に）興味深いものです。幸運なことに、帰納型自体でマッチする必要はありません：その代わりにいわゆる「構文パターン」を使います。これらは非常にシンプルで、その構文はただ `(the syntax I want to match on) とするだけです。実際に使ってみましょう：

def isAdd11 : Syntax → Bool
  | `(Nat.add 1 1) => true
  | _ => false

#eval isAdd11 (Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"]) -- true
#eval isAdd11 (Syntax.mkApp (mkIdent `Nat.add) #[mkIdent `foo, Syntax.mkNumLit "1"]) -- false

マッチの次のレベルはリテラルにマッチするだけでなく、入力から変数をキャプチャすることです。これは少しファンシーな見た目の構文で行われます：

def isAdd : Syntax → Option (Syntax × Syntax)
  | `(Nat.add $x $y) => some (x, y)
  | _ => none

#eval isAdd (Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"]) -- some ...
#eval isAdd (Syntax.mkApp (mkIdent `Nat.add) #[mkIdent `foo, Syntax.mkNumLit "1"]) -- some ...
#eval isAdd (Syntax.mkApp (mkIdent `Nat.add) #[mkIdent `foo]) -- none

型付けされた構文

この例の x と y は Syntax ではなく TSyntax `term 型であることに注意してください。コンストラクタを見ればわかるように、完璧に TSyntax ではない型だけで構成されている Syntax に対してパターンマッチしたのにも関わらずにこうなってしまっているのは、いったい何が起こっているのでしょうか？基本的に、`() 構文は賢いため、マッチする構文からくる可能性のあるもの（この場合は term）の中で最も一般的な構文カテゴリを把握することができます。この時に型付けされた構文型 TSyntax が用いられます。これはそれのもとになった構文カテゴリの Name でパラメータ化されています。これはプログラマにとって何が起こっているのかを確認するために便利なだけでなく、他にも利点があります。例えば、次の例で構文カテゴリを num に限定すると、Lean はパターンマッチやパニックのオプション無しで、結果の TSyntax `num に対して直接 getNat を呼び出すことができます：

-- ここで項の構文を操作する関数を明示的にマークしている
def isLitAdd : TSyntax `term → Option Nat
  | `(Nat.add $x:num $y:num) => some (x.getNat + y.getNat)
  | _ => none

#eval isLitAdd (Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"]) -- some 2
#eval isLitAdd (Syntax.mkApp (mkIdent `Nat.add) #[mkIdent `foo, Syntax.mkNumLit "1"]) -- none

TSyntax の裏にある Syntax にアクセスしたい場合は、TSyntax.raw で可能ですが、ほとんどの場合は型強制でうまくいきます。その他の TSyntax システムの恩恵についてはマクロの章で見ていきます。

構文の機構について最後に大事な注意を：この基本的な形式では、term カテゴリからの構文にのみしか機能しません。これを自前の構文カテゴリに使いたい場合は `(category| ...) を使う必要があります。

ミニプロジェクト

本章での最後のミニプロジェクトとして、算術式についての小さな言語の構文とそれを評価する Syntax → Nat 型の関数を定義します。以下のコンセプトについては今後の章でさらに見ていきます。

declare_syntax_cat arith

syntax num : arith
syntax arith "-" arith : arith
syntax arith "+" arith : arith
syntax "(" arith ")" : arith

partial def denoteArith : TSyntax `arith → Nat
  | `(arith| $x:num) => x.getNat
  | `(arith| $x:arith + $y:arith) => denoteArith x + denoteArith y
  | `(arith| $x:arith - $y:arith) => denoteArith x - denoteArith y
  | `(arith| ($x:arith)) => denoteArith x
  | _ => 0

-- Elab.TermElabM は無視することができる。
-- ここで重要なことは、 `Syntax` を構築するにあたって以下のようにマッチすることができるだけでなく
-- ``(arith| (12 + 3) - 4)` という記法を使うことができる。
def test : Elab.TermElabM Nat := do
  let stx ← `(arith| (12 + 3) - 4)
  pure (denoteArith stx)

#eval test -- 11

この例を自由に弄って好きなように拡張してみてください。次の章では、主に Syntax を何らかの方法で操作する関数について説明します。

エラボレートのさらなる例

記法のための型クラスの利用

構文システムの代わりに、型システムを通じた記法を追加するために型クラスを使うことができます。これは例えば、型クラス HAdd と Add を使った + や、など Lean のその他の共通の演算子の一般的な定義方法などです。

例えば、部分集合記法のための一般的な記法が欲しいとしましょう。まず初めにすべきことは、この記法を確立したい関数を備えた型クラスを定義することです。

class Subset (α : Type u) where
  subset : α → α → Prop

次のステップは記法の定義です。ここでできることは、単純にコード中に現れる ⊆ のインスタンスをすべて Subset.subset の呼び出しに置き換えることです。というのも型クラスの解決によってどの Subset インスタンスが参照されているかを把握することができるからです。したがって記法はシンプルになります：

-- この例の優先順位は任意
infix:50 " ⊆ " => Subset.subset

これを検証するために簡単な集合論を定義してみましょう：

-- `Set` はそれを保持する要素によって定義される
-- -> その要素の型に対するシンプルな述語
def Set (α : Type u) := α → Prop

def Set.mem (x : α) (X : Set α) : Prop := X x

-- 既存の要素の所属の記法の型クラスへと統合
instance : Membership α (Set α) where
  mem := Set.mem

def Set.empty : Set α := λ _ => False

instance : Subset (Set α) where
  subset X Y := ∀ (x : α), x ∈ X → x ∈ Y

example : ∀ (X : Set α), Set.empty ⊆ X := by
  intro X x
  -- ⊢ x ∈ Set.empty → x ∈ X
  intro h
  exact False.elim h -- empty set has no members

束縛子

変数の束縛子を使用する構文を宣言することは Lean 3 ではかなり非直観的でしたが、Lean 4 ではどのように自然にできるかを簡単に見てみましょう。

この例では、ある性質が成り立つようなすべての要素 x を含む集合のよく知られた記法を定義します：例えば {x ∈ ℕ | x < 10} です。

まず最初に、上記の集合論を少し拡張する必要があります：

-- 「～であるようなすべての要素」という基本的な関数のための記法
def setOf {α : Type} (p : α → Prop) : Set α := p

この関数を用いて、この記法の基本的なバージョンを直観的に定義することができます：

notation "{ " x " | " p " }" => setOf (fun x => p)

#check { (x : Nat) | x ≤ 1 } -- { x | x ≤ 1 } : Set Nat

example : 1 ∈ { (y : Nat) | y ≤ 1 } := by simp[Membership.mem, Set.mem, setOf]
example : 2 ∈ { (y : Nat) | y ≤ 3 ∧ 1 ≤ y } := by simp[Membership.mem, Set.mem, setOf]

この直観的な記法は期待通りの形で渡されるものに対処することができます。

この記法を拡張して {x ∈ X | p x} のような集合論的な書き方を許可し、束縛変数の周りの括弧を省く方法についてはマクロの章を参照してください。

演習問題

5 * 8 💀 4 が 20 を、8 💀 6 💀 1 が 3 を返すような「緊急マイナス 💀」記法を作ってください。

a) notation コマンドを使う場合。 b) infix コマンドを使う場合。 c) syntax コマンドを使う場合。

ヒント：Lean 4 の乗算は infixl:70 " * " => HMul.hMul で定義されています。
以下の構文カテゴリを考えてみましょう：term・command・tactic；そして以下に示す 3 つの構文ルールについて、これらの新しく定義された構文をそれぞれ使ってみましょう。
```
  syntax "good morning" : term
  syntax "hello" : command
  syntax "yellow" : tactic
```
以下のコマンドを許容する syntax ルールを作ってください：
- red red red 4
- blue 7
- blue blue blue blue blue 18
（つまり、複数の red の後に数字が来るか；あるいは複数の blue の後に数字が来るか；red blue blue 5 は機能しません。）

以下のコードテンプレートを使用してください：
```
syntax (name := colors) ...
-- our "elaboration function" that infuses syntax with semantics
@[command_elab colors] def elabColors : CommandElab := λ stx => Lean.logInfo "success!"
```
Mathlib には #help option コマンドがあり、現在の環境で利用可能なすべてのオプションとその説明を表示します。#help option pp.r は部分文字列「pp.r」で始まるすべてのオプションを表示します。

以下のコマンドを許容する syntax ルールを作ってください：
- #better_help option
- #better_help option pp.r
- #better_help option some.other.name
以下のテンプレートを使用してください：
```
syntax (name := help) ...
-- our "elaboration function" that infuses syntax with semantics
@[command_elab help] def elabHelp : CommandElab := λ stx => Lean.logInfo "success!"
```
Mathlib には ∑ 演算子があります。以下の項を許容する syntax ルールを作ってください：
- ∑ x in { 1, 2, 3 }, x^2
- ∑ x in { "apple", "banana", "cherry" }, x.length
以下のテンプレートを使用してください：
```
import Std.Classes.SetNotation
import Std.Util.ExtendedBinder
syntax (name := bigsumin) ...
-- our "elaboration function" that infuses syntax with semantics
@[term_elab bigsumin] def elabSum : TermElab := λ stx tp => return mkNatLit 666
```
ヒント：Std.ExtendedBinder.extBinder パーサを使ってください。ヒント：これらの import を機能させるには読者の Lean プロジェクトに batteries をインストールする必要があります。

マクロ

マクロとは

Lean においてのマクロとは Syntax → MacroM Syntax である関数のことです。MacroM はマクロのためのモナドで、次節で説明する静的な保証をマクロに持たせることができますが、現時点ではおおむね無視しても構いません。

マクロの登録は macro 属性を使用して、特定の構文宣言のハンドラとすることで行われます。コンパイラはこうして入力されたものに対して実際の解析を行う前に、これらの関数に構文の適用を行ってくれます。したがって利用者がすべきことは構文を特定の名前で宣言し、 Lean.Macro 型の関数をそれにバインドするだけです。Syntax の章の LXOR 記法を再現してみましょう：

import Lean

open Lean

syntax:10 (name := lxor) term:10 " LXOR " term:11 : term

@[macro lxor] def lxorImpl : Macro
  | `($l:term LXOR $r:term) => `(!$l && $r) -- we can use the quotation mechanism to create `Syntax` in macros
  | _ => Macro.throwUnsupported

#eval true LXOR true -- false
#eval true LXOR false -- false
#eval false LXOR true -- true
#eval false LXOR false -- false

とても簡単です！マクロが Macro.throwUnsupported 関数を使用すると、「この構文が管理されていないようである」ことを示すことができます。今回の場合、単に絶対に到達しないワイルドカードのパターンを埋めるために使用されています。

しかし、実はその気になれば同じ構文に対して複数のマクロを登録することも可能であり、その場合は各マクロが次々に試行されます（後に登録されたものほど優先度が高くなります。この「高さ」は正しい？）。この試行は、どれかが Macro.throwError を使用して実際のエラー、つまり Macro.throwUnsupported によるもの以外を投げるか成功するまで続けられます。

@[macro lxor] def lxorImpl2 : Macro
  -- 左右の識別子が特定の場合のケースの挙動を変更するための特殊ケース
  | `(true LXOR true) => `(true)
  | _ => Macro.throwUnsupported

#eval true LXOR true -- true, handled by new macro
#eval true LXOR false -- false, still handled by the old

この機能は明らかに あまりにも 強力です！これは後でコードを追加した際に奇妙な挙動を引き起こす可能性があるため、軽い気持ちで使ってはならず、慎重に考えるべきです。次の例は、この奇妙な挙動を示しています：

#eval true LXOR true -- true, handled by new macro

def foo := true
#eval foo LXOR foo -- false, handled by old macro, after all the identifiers have a different name

このマクロがどのように実装されているかを正確に知らなければ、この動作に基づいて問題をデバッグする人は非常に混乱するでしょう。マクロの使用とエラボレーションのような他のメカニズムの使用の使い分けの経験則として、上記の2番目のマクロのように実際のロジックを構築する場合はマクロではなくエラボレータを使用することをお勧めします（エラボレーションの章で説明します）。つまり理想的にはマクロは、人間が手でも簡単に書き出せるがあまりにもめんどくさいような構文から構文へのシンプルな変換のために用いたいのです。

簡略化されたマクロ宣言

ここまででマクロとは何か、マクロを登録する方法などの基本がわかったところで、もう少し自動化された方法を見てみましょう（実は、これから紹介する方法はすべてマクロとして実装されています）。

まず最初に macro_rules というものがあり、これは基本的に、例えば上記で書いたような関数に脱糖します：

syntax:10 term:10 " RXOR " term:11 : term

macro_rules
  | `($l:term RXOR $r:term) => `($l && !$r)

見てわかる通り、これはさまざまなことをかわりに行ってくれます：

構文宣言の名前
macro 属性の登録
throwUnsupported ワイルドカード

これを除けば、この構文はまさにパターンマッチ構文を使った関数のように動作し、理論的には右手側に任意の複雑なマクロ関数をエンコードすることができます。

これでもまだ十分短くないと感じたのなら、macro を使ったさらなるステップを見てみましょう：

macro l:term:10 " ⊕ " r:term:11 : term => `((!$l && $r) || ($l && !$r))

#eval true ⊕ true -- false
#eval true ⊕ false -- true
#eval false ⊕ true -- true
#eval false ⊕ false -- false

見ての通り、macro は notation にもうかなり近くなっています：

構文宣言を代行してくれます
自動的に macro_rules スタイルの関数を書いてくれます

もちろん違いもあります：

notation は term の構文カテゴリに限定されます
notation は右側に任意のマクロコードを書くことができません

`Syntax` Quotations

基本

今までは `(foo $bar) という構文を使って Syntax オブジェクトの作成とマッチを行ってきました。構文に関わる非自明なことに本質的に必要であるため、今こそ完全な説明を行います。

まず最初に、`() という構文を Syntax quotation と呼びます。syntax quotation の中に変数を入れると `($x) となり、この $x の部分を anti-quotation と呼びます。このように x を挿入する場合、x は TSyntax y 型であることが求められます。ここで y は何かしらの構文カテゴリのとある Name です。Lean コンパイラは賢いため、ここで使用が許可されている構文カテゴリを把握することができます。そのため、以下のようなエラーが発生することがあります：

application type mismatch
  x.raw
argument
  x
has type
  TSyntax `a : Type
but is expected to have type
  TSyntax `b : Type

もし a 構文カテゴリにあるものが b 構文として使えると確認していれば、次のような形で強制を宣言することができます：

instance : Coe (TSyntax `a) (TSyntax `b) where
  coe s := ⟨s.raw⟩

これによって Lean は自動的に型キャストを行うことができます。もし a が b の代わりに使えないことに気づいたなら、おめでとうございます、読者は自身の Syntax 関数のバグを発見しました。Lean コンパイラと同様に、特定の TSyntax 型に特化した関数を宣言することもできます。例えば構文の章で見たように次のような関数があります：

#check TSyntax.getNat -- TSyntax.getNat : TSyntax numLitKind → Nat

この関数が受け取る Syntax は数値リテラルであり、当然 Nat に変換できることがわかっているため、これはパニックしないことが保証されています。

パターンマッチで anti-quotation 構文を使うと、構文の章で説明したように、TSyntax y 型の変数 x が得られます。ここで y はパターンマッチに合致した構文カテゴリの Name です。何らかの理由で $x というリテラルを Syntax に挿入したい場合、例えばマクロを作成する場合、anti-quotation を使ってエスケープすることができます： `($$x)。

もし x が解釈される構文の種類を指定したい場合は、次のようにして明示的に指定することができます：`($x:term)。ここで term は他の有効な構文カテゴリ（例えば command）やパーサ（例えば ident）に置き換えることができます。

ここまではすでに構文の章やこの章までに見てきた直観的な内容をより形式的に説明したにすぎません。次はより高度な anti-quotation について説明しましょう。

より高度な anti-quotation

便宜上、書式文字列と同じような方法で anti-quotations を使うこともできます：`($(mkIdent `c)) は次と同じです：let x := mkIdent `c; `($x)。

さらに、いくつかのシチュエーションでは、基本的な Syntax ではなくより複雑なデータ構造に包まれた Syntax、とりわけ多いのが Array (TSyntax c) や TSepArray c s などを扱います。ここで TSepArray c s は Syntax 固有の型であり、区切り文字 s を使って c というカテゴリを区切る Syntax をパターンマッチした場合に得られるものです。例えば、$xs,* を使ってマッチをした場合、xs は TSepArray c "," という型になります。区切り文字を指定せずに（つまり空白で）マッチする特殊なケース $xs* では Array (TSyntax c) となります。

xs : Array (TSyntax c) を扱い、それを quotation に挿入したい場合、主に2つの方法があります：

区切り文字を使用して挿入する。最も一般的なのは , を使って `($xs,*) とします。これは TSepArray c ","" の挿入の仕方でもあります。
区切り文字無しで空白を挿入する。(TODO): `()

例えば：

-- 可能な場合にタプルの最初の要素を構文的に削除する
syntax "cut_tuple " "(" term ", " term,+ ")" : term

macro_rules
  -- タプルにならないため、ペアの片方の要素を削除することは不可能
  | `(cut_tuple ($x, $y)) => `(($x, $y))
  | `(cut_tuple ($x, $y, $xs,*)) => `(($y, $xs,*))

#check cut_tuple (1, 2) -- (1, 2) : Nat × Nat
#check cut_tuple (1, 2, 3) -- (2, 3) : Nat × Nat

本節の最後として、いわゆる「anti-quotation スプライス」を取り上げます。anti-quotation スプライスには2種類あり、まずオプショナルと呼ばれるものから説明します。例えば、オプショナルな引数を持つ構文、独自の let を宣言する場合を考えます（実際のプロジェクトでは、理論を記述する対象の関数型言語の let である可能性が高いでしょう）：

syntax "mylet " ident (" : " term)? " := " term " in " term : term

オプションの (" : " term)? 引数を指定することで、その左側にある項の型を定義することができます。これまで見てきたメソッドでは、オプションの引数がある場合と無い場合の2つの macro_rules を書かなければなりませんでした。しかし、その後に行う構文変換はオプションの引数があっても無くても全く同じように動作するため、ここでスプライスをつかって出来ることは、本質的には両方のケースを一度に定義することです：

macro_rules
  | `(mylet $x $[: $ty]? := $val in $body) => `(let $x $[: $ty]? := $val; $body)

この $[...]? 部分がここでのスプライスであり、基本的に「もしこの構文のこの部分が無い場合、anti-quotation 変数を含む右側においてこの部分を無視すること」ということを意味します。これで、この構文を型の帰属の有無に関わらず実行できるようになりました：

#eval mylet x := 5 in x - 10 -- 0, due to subtraction behaviour of `Nat`
#eval mylet x : Int := 5 in x - 10 -- -5, after all it is an `Int` now

次と最後のスプライスはPythonなどで見られるリスト内包表記を想起させるかもしれません。ここでは map をマクロとして実装したものを使って説明します：

-- リストの各要素に対して最後に渡された関数を実行する
syntax "foreach " "[" term,* "]" term : term

macro_rules
  | `(foreach [ $[$x:term],* ] $func:term) => `(let f := $func; [ $[f $x],* ])

#eval foreach [1,2,3,4] (Nat.add 2) -- [3, 4, 5, 6]

今回の場合、$[...],* の部分がスプライスです。マッチする側では、その中に定義したパターンに（与えた区切り文字を考慮しながら）繰り返しマッチしようとします。しかし、正規のセパレータによるマッチとは異なり、Array や SepArray を返しません。その代わりに、指定したパターンにマッチされるたびに評価される別のスプライスを右側に書くことができます。この評価は繰り返しのたびにマッチされた特定の値で行われます。

健全性の問題とその解決策

C言語のような他の言語のマクロシステムに慣れている人なら、いわゆるマクロの健全性についてご存じでしょう。健全性の問題とは、マクロが識別子を導入する際に、そのマクロが含む構文の識別子と衝突してしまうことです。例えば：

-- このマクロを適用すると、新しい識別子 `x` を束縛する関数が生成される。
macro "const" e:term : term => `(fun x => $e)

-- しかし `x` はユーザによって別で定義されうる
def x : Nat := 42

-- コンパイラは `$e` においてどちらの `x` を使うべきか？
#eval (const x) 10 -- 42

マクロが構文の変換だけを行うことを考えると、上記の eval は 42 ではなく 10 を返すと期待できるかもしれません：つまるところ、返される構文は (fun x => x) 10 となるはずだからです。もちろんこれは作者の意図したことではありませんが、C言語のような原始的なマクロシステムではこのようなことが起こります。では、Lean はこのような健全性の問題をどのように回避しているのでしょうか？これについては Beyond Notations という優れた論文で詳しく述べられています。この論文では Lean のアイデアと実装について詳しく論じられています。実用上、詳細はそれほど興味深いものではないので、ここではトピックの概要を述べるにとどまります。Beyond Notations で説明されているアイデアは「マクロスコープ」と呼ばれる概念に集約されます。新しいマクロが呼び出されるたびに新しいマクロスコープ（基本的には一意の番号）が現在アクティブなすべてのマクロスコープのリストに追加されます。現在のマクロが新しい識別子を導入するとき、実際に追加されるのは次の形式の識別子です：

<actual name>._@.(<module_name>.<scopes>)*.<module_name>._hyg.<scopes>

例えば、モジュール名が Init.Data.List.Basic、名前が foo.bla、マクロスコープが [2, 5] の場合は以下のようになります：

foo.bla._@.Init.Data.List.Basic._hyg.2.5

マクロスコープは一意な番号であるため、名前の末尾に付加されるマクロスコープのリストはすべてのマクロの呼び出しにおいて常に一意であり、したがって上記のようなマクロの健全性の問題は起こり得ません。

この名前生成になぜマクロスコープ以外のものが含まれているのか不思議に思われるかもしれませんが、これは異なるファイル・モジュールからスコープを組み合わせなければならない場合があるからです。処理されるメインモジュールは常に最も右のものです。このような状況は現在のファイルにインポートされたファイルで生成されたマクロを実行する時に発生する可能性があります。

foo.bla._@.Init.Data.List.Basic.2.1.Init.Lean.Expr_hyg.4

末尾の区切り文字 _hyg は関数 Lean.Name.hasMacroScopes のパフォーマンスを向上させるためだけに使用されています。つまりこのフォーマットではこの区切り文字が無くても動作はします。

これには技術的な詳細が多く含まれていました。マクロを使うにあたってはこれらを理解する必要はありません。もし必要であれば、Lean は const の例のような名前の衝突を許さないということだけを覚えておいてください。

これは syntax quotation で導入される全ての名前に拡張されます。つまり、`(def foo := 1) を生成するマクロを書いた場合、foo は健全性の対象であるためユーザは foo にアクセスすることができません。幸い、これを回避する方法があります。例えば、`(def $(mkIdent `foo) := 1) のように mkIdent を使って生の識別子を生成することができます。この場合、識別子は健全性の管理から外れ、ユーザがアクセスできるようになります。

`MonadQuotation` と `MonadRef`

この健全性のメカニズムの説明に基づくと、1つの興味深い疑問が浮かんできます。現在のマクロスコープがどうなっているかを知る方法はあるでしょうか？結局のところ、上で定義したマクロ関数ではスコープの明示的な受け渡しは一切行われていません。関数型プログラミングではよくあることですが、（マクロスコープなどの）管理する必要のある追加状態を持ち始めると、それらはすぐにモナドで管理されます。このケースでは少々ひねられていますが、同様です。

これを単一のモナド MacroM だけに実装する代わりに、MonadQuotation という型クラスを使って、モナド的な方法でマクロスコープを追跡する一般的な概念を抽象化しています。これにより、他のモナドでもこの型クラスを実装するだけでこの健全な Syntax 作成アルゴリズムを簡単に提供できるようになります。

これが `(syntax) で構文のパターンマッチを使用することができる一方で、純粋関数で同じ構文を持つ Syntax を作成することができない理由でもあります：純粋関数にはマクロスコープを追跡するための MonadQuotation を備えた Monad を持たないためです。

では、MonadQuotation 型クラスを簡単に見てみましょう：

namespace Playground

class MonadRef (m : Type → Type) where
  getRef      : m Syntax
  withRef {α} : Syntax → m α → m α

class MonadQuotation (m : Type → Type) extends MonadRef m where
  getCurrMacroScope : m MacroScope
  getMainModule     : m Name
  withFreshMacroScope {α : Type} : m α → m α

end Playground

MonadQuotation は MonadRef に基づいているため、まずは MonadRef を見てみましょう。これのアイデアは非常にシンプルです：MonadRef は Monad 型クラスを以下の観点で拡張したものです。

getRef で取得される Syntax への参照の利用
あるモナドアクション m α を withRed を使って Syntax への新しい参照で評価できる

MonadRef 単体では対して面白くありませんが、MonadQuotation と組み合わさることで意味が生まれます。

見ての通り、MonadQuotation は MonadRef を拡張し、3つの新しい関数を追加しています：

getCurrMacroScope は作成された中で最新の MacroScope を取得します。
getMainModule では（明らかに）メインモジュールの名前を取得します。これは上記で説明した健全な識別子の作成にも使用されます。
withFreshMacroScope は次のマクロスコープを計算し、名前の衝突を避けるためのこの新しいスコープで syntax quotation を行う計算 m α を実行します。これは新しいマクロの呼び出しが発生するたびに内部的に使用されることを意図していますが、例えば構文ブロックを繰り返し生成していて、名前の衝突を避けたい場合など、独自のマクロでこれを使用する意味がある場合もあります。

ここで MonadRef がどのように関わってくるかというと、Lean は特定の位置でのエラーをユーザに示す方法を必要としています。Syntax の章では紹介しませんでしたが、Syntax 型の値は実際にファイル内の位置も持ち運ぶことができます。エラーが検出されると、これは通常 Syntax 型の値に束縛され、Lean にファイルのどこでエラーが発生したかを伝えます。withFreshMacroScope を使って Lean は getRef の結果の位置を導入された各シンボルに適用し、その結果位置を適用しない場合より良いエラー位置が得られます。

エラー位置の動作を見るために、これを利用する小さなマクロを書いてみましょう：

syntax "error_position" ident : term

macro_rules
  | `(error_position all) => Macro.throwError "Ahhh"
  -- `%$tk` 構文によって % より前の Syntax が得られる
  -- ここでは `error_position` であり、`tk` と名付けられる
  | `(error_position%$tk first) => withRef tk (Macro.throwError "Ahhh")

#check_failure error_position all -- the error is indicated at `error_position all`
#check_failure error_position first -- the error is only indicated at `error_position`

このようにエラーの位置をコントロールすることは、良いユーザエクスペリエンスにとって非常に重要であることは明らかでしょう。

ミニプロジェクト

この節の最後のミニプロジェクトとして、構文の章で出てきた算術 DSL を、今回はマクロを使ってもう少し高度な方法で再構築し、実際に Lean の構文に完全に統合できるようにします。

declare_syntax_cat arith

syntax num : arith
syntax arith "-" arith : arith
syntax arith "+" arith : arith
syntax "(" arith ")" : arith
syntax "[Arith|" arith "]" : term

macro_rules
  | `([Arith| $x:num]) => `($x)
  | `([Arith| $x:arith + $y:arith]) => `([Arith| $x] + [Arith| $y]) -- recursive macros are possible
  | `([Arith| $x:arith - $y:arith]) => `([Arith| $x] - [Arith| $y])
  | `([Arith| ($x:arith)]) => `([Arith| $x])

#eval [Arith| (12 + 3) - 4] -- 11

ここでも自由に遊んでみてください。変数を使った式のようなより複雑なものを作りたい場合は、マクロを使う代わりに帰納型を作ることを検討してみてください。算術式の項を帰納型にした場合、何らかの形で変数に代入し、その式を評価する関数を書くことができます。また、特別な構文や思いついたものを使って、任意の term を算術式に埋め込んでみることもできます。

さらなるエラボレートの例

束縛子 2.0

構文の章で約束したように、パワーアップした束縛子を導入しましょう。まず集合論を再び導入することから始めます：

def Set (α : Type u) := α → Prop
def Set.mem (x : α) (X : Set α) : Prop := X x

-- すでに存在する所属の記法用の型クラスに統合
instance : Membership α (Set α) where
  mem := Set.mem

def Set.empty : Set α := λ _ => False

-- 「～であるようなすべての要素」という基本的な関数のための記法
def setOf {α : Type} (p : α → Prop) : Set α := p

この節の目標は {x : X | p x} と {x ∈ X, p x} の両方の表記を可能にすることです。原理的には2つの方法があります：

対象の変数を束縛する方法についての構文とマクロを定義する
Σ や Π などの他の束縛構文でも再利用できるような束縛の構文カテゴリを定義し、{ | } の場合のマクロを実装する

本節では、再利用が容易なアプローチ 2 を使用します。

declare_syntax_cat binder_construct
syntax "{" binder_construct "|" term "}" : term

さて、本題である2つの束縛子を定義してみましょう：

syntax ident " : " term : binder_construct
syntax ident " ∈ " term : binder_construct

そして最後に構文を拡張するためのマクロです：

macro_rules
  | `({ $var:ident : $ty:term | $body:term }) => `(setOf (fun ($var : $ty) => $body))
  | `({ $var:ident ∈ $s:term | $body:term }) => `(setOf (fun $var => $var ∈ $s ∧ $body))

-- 以前の例は改良した構文では以下のようになる：
#check { x : Nat | x ≤ 1 } -- setOf fun x => x ≤ 1 : Set Nat

example : 1 ∈ { y : Nat | y ≤ 1 } := by simp[Membership.mem, Set.mem, setOf]
example : 2 ∈ { y : Nat | y ≤ 3 ∧ 1 ≤ y } := by simp[Membership.mem, Set.mem, setOf]

-- 新しい例：
def oneSet : Set Nat := λ x => x = 1
#check { x ∈ oneSet | 10 ≤ x } -- setOf fun x => x ∈ oneSet ∧ 10 ≤ x : Set Nat

example : ∀ x, ¬(x ∈ { y ∈ oneSet | y ≠ 1 }) := by
  intro x h
  -- h : x ∈ setOf fun y => y ∈ oneSet ∧ y ≠ 1
  -- ⊢ False
  cases h
  -- : x ∈ oneSet
  -- : x ≠ 1
  contradiction

さらに読む

マクロについてさらに知りたい場合は以下を読むと良いでしょう：

API のドキュメント：TODO link
ソースコード：Init.Prelude の前半部分。Lean において構文を構築するためにこれらは重要であるため、これらの宣言はファイル中のかなり初めのほうにあることがわかるでしょう。
前述した論文 Beyond Notations

エラボレーション

エラボレータは、ユーザが目にする Syntax をコンパイラの他の部分がそれを処理できるようなものに変換するコンポーネントです。ほとんどの場合、これは Syntax を Expr に変換することを意味しますが、#check や #eval のような他の使用例もあります。このためエラボレータは非常に大きなコードとなっており、ここに格納されています。

コマンドのエラボレーション

コマンドは Syntax の最上位レベルであり、Lean ファイルはコマンドのリストで構成されます。最もよく使われるコマンドは宣言であり、例えば以下です：

def
inductive
structure

しかし、これ以外にもコマンドは存在しており、特筆すべきなものとして #check や #eval などのタイプです。すべてのコマンドは command という構文カテゴリに属しているため、カスタムコマンドを宣言するには、その構文をそのカテゴリに登録する必要があります。

コマンドに意味を与える

次のステップは構文にセマンティクスを与えることです。コマンドの場合、これはいわゆるコマンドエラボレータを登録することで行われます。

コマンドエラボレータは CommandElab という型を持っており、これは Syntax → CommandElabM Unit という型のエイリアスです。これがすることは、コマンドが呼ばれた際に期待されるものを表現した Syntax を取り、CommandElabM モナド上の副作用を生み出します。最終的な戻り値は Unit です。CommandElabM モナドには主に4種類の副作用があります：

Monad を拡張した MonadLog と AddMessageContext を使って #check のようにユーザにメッセージをログ出力する。これは Lean.Elab.Log にある関数で行われ、特に有名なものは logInfo・logWarning・logError です。
Monad を拡張した MonadEnv を使って Environment とやり取りする。これはコンパイラに関連するすべての情報が格納される場所であり、すべての既知の宣言・その型・ドキュメント文字列・値などが格納されています。現在の環境は getEnv で取得でき、更新は setEnv で設定できます。ここで Environment に情報を追加するにあたっては setEnv のラッパーである addDecl などを用いることが大体において正しい方法であることに注意してください。
IO の実行。CommandElabM はあらゆる IO 操作を実行することができます。例えば、ファイルを読み込んでその内容に基づいて宣言を行うことができます。
例外の送出。このモナドはどんな IO でも実行できるため、例外を throwError で投げることは自然です。

さらに、CommandElabM がサポートする Monad の拡張はほかにもたくさんあります：

マクロと同じような Syntax quotation 用の MonadRef と MonadQuotation
オプションのフレームワークとのやり取りのための MonadOptions
デバッグトレースの情報のための MonadTrace
TODO: 関連性があるかどうかはわかりませんが、他にもいくつかあります。Lean.Elab.Command のインスタンスを参照してください。

コマンドのエラボレーション

さて、コマンドエラボレータの種類を理解したところで、エラボレーションのプロセスが実際にどのように機能するのかを簡単に見てみましょう。

現在の Syntax に適用できるマクロがあるかどうかをチェックする。適用可能なマクロがあり、例外が投げられなければ、結果の Syntax がコマンドとして再帰的にエラボレートされます。
マクロを適用できない場合は、エラボレートする Syntax の SyntaxKind に対して登録されているすべての CommandElab を検索する。これは command_elab 属性を使用して登録されています。
これらの CommandElab はすべて unsupportedSyntaxException を投げるものが出現するまで順番に試行されます。これは、そのエラボレータがこの特定の Syntax の構築に対して「責任を負っている」ことを示す Lean 流の方法です。これらのエラボレータは何かが間違っていることをユーザに示すために通常の例外を投げうることに注意してください。責任を持つエラボレータが見つからない場合、コマンドのエラボレーションは unexpected syntax エラーメッセージとともに中断されます。

見てわかるように、この手順の背後にある一般的な考え方は通常のマクロ展開とよく似ています。

自分用のものを作る

これで CommandElab とは何か、そしてそれがどのように使われるかわかったので、次は自分用のものを作る方法に着目します。そのための手順は上で学んだとおりです：

構文を定義する
エラボレータを定義する
command_elab 属性を用いて、構文を担当するエラボレータを登録する。

これがどのように実現されるか見てみましょう：

import Lean

open Lean Elab Command Term Meta

syntax (name := mycommand1) "#mycommand1" : command -- declare the syntax

@[command_elab mycommand1]
def mycommand1Impl : CommandElab := fun stx => do -- declare and register the elaborator
  logInfo "Hello World"

#mycommand1 -- Hello World

これは少々ボイラープレート的だと思われるかもしれませんが、Lean の開発者もそう思っていたようです。そこで彼らはこれのためのマクロを追加しました！

elab "#mycommand2" : command =>
  logInfo "Hello World"

#mycommand2 -- Hello World

コマンドのエラボレーションは同じ構文に対して複数のエラボレータの登録をサポートしているため、必要な時には実は構文のオーバーロードが可能である点に注意してください。

@[command_elab mycommand1]
def myNewImpl : CommandElab := fun stx => do
  logInfo "new!"

#mycommand1 -- new!

さらに、unsupportedSyntaxException を投げることで、構文の一部だけをオーバーロードすることも可能で、その場合はデフォルトのハンドラに処理させるか、elab コマンドに処理を処理をまかせます。

以下の例では、元の #check 構文を拡張しているのではなく、この特定の構文のために新しい SyntaxKind を追加しています。しかし利用者からすれば、このコマンドの効果は基本的に同じです。

elab "#check" "mycheck" : command => do
  logInfo "Got ya!"

これは実際にはオリジナルの #check を拡張したものです。

@[command_elab Lean.Parser.Command.check] def mySpecialCheck : CommandElab := fun stx => do
  if let some str := stx[1].isStrLit? then
    logInfo s!"Specially elaborated string literal!: {str} : String"
  else
    throwUnsupportedSyntax

#check mycheck -- Got ya!
#check "Hello" -- Specially elaborated string literal!: Hello : String
#check Nat.add -- Nat.add : Nat → Nat → Nat

ミニプロジェクト

この節の最後のミニプロジェクトとして、実際に役立つコマンドエラボレータを作ってみましょう。これはコマンドを受け取り、elabCommand（コマンドのエラボレーションのエントリポイント）と同じメカニズムを使って、与えたコマンドに関連するマクロやエラボレータを教えてくれます。

しかし、実際に elabCommand を再実装する労力は省きます。

elab "#findCElab " c:command : command => do
  let macroRes ← liftMacroM <| expandMacroImpl? (←getEnv) c
  match macroRes with
  | some (name, _) => logInfo s!"Next step is a macro: {name.toString}"
  | none =>
    let kind := c.raw.getKind
    let elabs := commandElabAttribute.getEntries (←getEnv) kind
    match elabs with
    | [] => logInfo s!"There is no elaborators for your syntax, looks like its bad :("
    | _ => logInfo s!"Your syntax may be elaborated by: {elabs.map (fun el => el.declName.toString)}"

#findCElab def lala := 12 -- Your syntax may be elaborated by: [Lean.Elab.Command.elabDeclaration]
#findCElab abbrev lolo := 12 -- Your syntax may be elaborated by: [Lean.Elab.Command.elabDeclaration]
#findCElab #check foo -- even our own syntax!: Your syntax may be elaborated by: [mySpecialCheck, Lean.Elab.Command.elabCheck]
#findCElab open Hi -- Your syntax may be elaborated by: [Lean.Elab.Command.elabOpen]
#findCElab namespace Foo -- Your syntax may be elaborated by: [Lean.Elab.Command.elabNamespace]
#findCElab #findCElab open Bar -- even itself!: Your syntax may be elaborated by: [«_aux_lean_elaboration___elabRules_command#findCElab__1»]

TODO: 今すぐには何も思い浮かばないが、# スタイルではないコマンド、つまり宣言を示すミニプロジェクトも追加すべきかもしれない。 TODO: lemma/theorem に似ているが、自動的に sorry してくれる conjecture 宣言を定義する。sorry は「推測」が真であると予想されることを反映するために、カスタムのものにすることもできる。

項のエラボレーション

項はある種の Expr を表す Syntax オブジェクトです。項エラボレータは私たちが書くコードのほとんどを処理するものです。特に、定義や型（これらも単なる Expr であるため）など、すべての値をエラボレートします。

すべての項は term 構文カテゴリに属しています（この動作はマクロの章ですでに見ています）。したがって、カスタムの項を宣言するには、その構文をこのカテゴリに登録する必要があります。

項に意味を与える

コマンドのエラボレーションと同様に、次のステップは構文にセマンティクスを与えることです。項の場合、これはいわゆる項エラボレータを登録することで行われます。

項エラボレータは TermElab という型を持っており、これは Syntax → Option Expr → TermElabM Expr という型のエイリアスです。この型の時点ですでにコマンドのエラボレーションとはかなり異なっています：

コマンドのエラボレーションと同様に、この Syntax はユーザがこの項を作成するために使用したものです。
Option Expr は期待される項の型ですが、これは常にわかるとは限らないため、Option 引数となっています。
コマンドのエラボレーションとは異なり、項のエラボレーションはその副作用によって実行されるだけでなく、TermElabM Expr が戻り値には実際の興味の対象、つまりその Syntax オブジェクトを表す Expr を含んでいます。

TermElabM は基本的にすべての点で CommandElabM をアップグレードしたものです：これは上述したものをすべてに加えてさらに2つの機能をサポートしています。一つ目は非常にシンプルです：IO コードを実行することに加えて、MetaM のコードも実行することができるため、Expr をうまく構築することができます。2つ目はエラボレーションのループという項に特化したものです。

項のエラボレーション

項のエラボレーションの基本的なアイデアはコマンドのエラボレーションと同じです：マクロを展開し、term_elab 属性によって Syntax に登録された項エラボレータを全て完了するまで再帰的に実行します（term_elab 属性が項のエラボレーションを実行することもあります）。しかし、項エラボレータが実行中にできる特別なアクションが1つあります。

項エラボレータは Except.postpone を投げることがあります。これは項エラボレータが作業を続けるためにさらなる情報を必要としていることを示します。この不足している情報を表現するために、Lean はいわゆる synthetic metavariable を使用します。以前からご存じのように、メタ変数は埋められることを待っている Expr の穴です。synthetic metavariable はそれを解決するための特別なメソッドを持っている点で異なっており、SyntheticMVarKind に登録されています。現時点では4種類あります：

typeClass、メタ変数は型クラスの統合で解決される
coe、メタ変数は強制によって解決される（型クラスの特殊なケース）
tactic、メタ変数はタクティクの項であり、タクティクを実行することで解決される
postponed、Except.postpone で生成される

このような synthetic metavariable が作成されると、次の上位レベルの項エラボレータが継続されます。ある時点で延期されたメタ変数の実行は、その実行が完了できる望みができた時に項エラボレータによって再開されます。次の例でこれを実際に見てみましょう：

#check set_option trace.Elab.postpone true in List.foldr .add 0 [1,2,3] -- [Elab.postpone] .add : ?m.5695 → ?m.5696 → ?m.5696

ここで起こったことは、関数適用のエラボレータがジェネリックな関数である List.foldr に対して開始し、暗黙の型パラメータのメタ変数を作成したことです。そして最初の引数 .add をエラボレートしようとしました。

.name がどのように機能するかご存じでない方のために説明しておくと、基本的な考え方は大体（今回のケースのように）Lean が関数（今回の場合は Nat.add）の出力型（今回の場合は Nat）を推測できるべきというものです。このような場合、.name 機能は名前空間 Nat で name という名前の関数を単純に検索します。これはある型のコンストラクタをその名前空間を参照したり開いたりすることなく使用したい場合に特に便利ですが、上記のように使用することもできます。

さて、例に戻ると Lean はこの時点で .add が型 ?m1 → ?m2 → ?m2（ここで ?x はメタ変数の記法です）を持つ必要があることを知っています。.add のエラボレータは ?m2 の実際の値を知る必要があるため、項エラボレータは実行を延期します（これは .add の代わりに内部的に synthetic metavariable を作成することで行われます）。他の2つの引数のエラボレーションによって ?m2 が Nat でなければならないという事実が得られるため、.add のエラボレータが続行されると、この情報を使ってエラボレーションを完了することができます。

また、これがうまくいかないケースを引き起こすことも簡単にできます。例えば：

#check_failure set_option trace.Elab.postpone true in List.foldr .add
-- [Elab.postpone] .add : ?m.5808 → ?m.5809 → ?m.5809
-- invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
  -- ?m.5808 → ?m.5809 → ?m.5809

この場合、.add はまず実行を延期し、その後再び呼び出されましたが、エラボレーションを終えるのに十分な情報を持っていなかったことで失敗しました。

自分用のものを作る

新しい項エラボレータの追加は、新しいコマンドエラボレータの追加と基本的に同じように機能するため、ごく簡単に見ておきましょう：

syntax (name := myterm1) "myterm 1" : term

def mytermValues := [1, 2]

@[term_elab myterm1]
def myTerm1Impl : TermElab := fun stx type? =>
  mkAppM ``List.get! #[.const ``mytermValues [], mkNatLit 0] -- `MetaM` code

#eval myterm 1 -- 1

-- `elab` も機能する
elab "myterm 2" : term => do
  mkAppM ``List.get! #[.const ``mytermValues [], mkNatLit 1] -- `MetaM` code

#eval myterm 2 -- 2

小さなプロジェクト

本章の最後のミニプロジェクトとして、最もよく使われる Lean の構文糖衣の1つである ⟨a,b,c⟩ 記法を単一コンストラクタ型のショートハンドとして再現します：

-- オリジナルと紛らわしくならないようにちょっとだけ変えている
syntax (name := myanon) "⟨⟨" term,* "⟩⟩" : term

def getCtors (typ : Name) : MetaM (List Name) := do
  let env ← getEnv
  match env.find? typ with
  | some (ConstantInfo.inductInfo val) =>
    pure val.ctors
  | _ => pure []

@[term_elab myanon]
def myanonImpl : TermElab := fun stx typ? => do
  -- 型がわからないメタ変数である場合、実行を延期しようとする。
  -- メタ変数は関数のエラボレータのように、それらが何であるか解明するための情報が
  -- まだ十分手に入れられない際に暗黙のパラメータの値を埋めるために用いられる。
  -- 項エラボレータが実行を延期できるのは一度だけであるため、エラボレータが無限ループに陥ることはない。
  -- 従って、ここでは実行の延期だけを試みるが、そうしないと例外を引き起こすかもしれない。
  tryPostponeIfNoneOrMVar typ?
  -- もし延期しても型が見つからなかった場合はエラーとなる。
  let some typ := typ? | throwError "expected type must be known"
  if typ.isMVar then
    throwError "expected type must be known"
  let Expr.const base .. := typ.getAppFn | throwError s!"type is not of the expected form: {typ}"
  let [ctor] ← getCtors base | throwError "type doesn't have exactly one constructor"
  let args := TSyntaxArray.mk stx[1].getSepArgs
  let stx ← `($(mkIdent ctor) $args*) -- syntax quotations
  elabTerm stx typ -- call term elaboration recursively

#check (⟨⟨1, sorry⟩⟩ : Fin 12) -- { val := 1, isLt := (_ : 1 < 12) } : Fin 12
#check_failure ⟨⟨1, sorry⟩⟩ -- expected type must be known
#check_failure (⟨⟨0⟩⟩ : Nat) -- type doesn't have exactly one constructor
#check_failure (⟨⟨⟩⟩ : Nat → Nat) -- type is not of the expected form: Nat -> Nat

最後の注釈として、elab 構文の糖衣構文を代わりに使うことで、延期の動作を短くすることができます：

-- この `t` 構文は `myanonImpl` の最初の2行を効果的に実行する。
elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
  sorry

演習問題

以下のコードについて考えてみましょう。syntax + @[term_elab hi]... : TermElab の組み合わせの代わりに elab だけを使って書き換えてください。

syntax (name := hi) term " ♥ " " ♥ "? " ♥ "? : term

@[term_elab hi]
def heartElab : TermElab := fun stx tp =>
  match stx with
    | `($l:term ♥) => do
      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)
    | `($l:term ♥♥) => do
      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
    | `($l:term ♥♥♥) => do
      let nExpr ← elabTermEnsuringType l (mkConst `Nat)
      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
    | _ =>
      throwUnsupportedSyntax

以下は実際の mathlib のコマンド alias から抜粋した構文です。
```
syntax (name := our_alias) (docComment)? "our_alias " ident " ← " ident* : command
```
これについて alias hi ← hello yes で ← の牛との識別子、つまり「hello」と「yes」を出力するようにしたいです。

これらのセマンティクスを追加してください：

a) syntax + @[command_elab alias] def elabOurAlias : CommandElab を使用する b) syntax + elab_rules を使用する c) elab を使用する
以下は実際の mathlib の nth_rewrite から抜粋した構文です。
```
open Parser.Tactic
syntax (name := nthRewriteSeq) "nth_rewrite " (config)? num rwRuleSeq (ppSpace location)? : tactic
```
これについて nth_rewrite 5 [←add_zero a] at h でユーザが場所を指定した場合は "rewrite location!" を、場所を指定しなかった場合は "rewrite target!" を出力するようにしたいです。

これらのセマンティクスを追加してください：

a) syntax + @[command_elab alias] def elabOurAlias : CommandElab を使用する b) syntax + elab_rules を使用する c) elab を使用する

エラボレーションによる DSL の埋め込み

この章では DSL を構築するためにどのようにエラボレーションを使うかについて学びます。ここでは MetaM の全機能を探求することはせずに、単にこの低レベルの機構にアクセスする方法を紹介します。

具体的には、IMP の構文を Lean が理解できるようにします。これは単純な命令型言語で、操作的意味論・表示的意味論の教育によく用いられます。

この本と同じエンコーディングですべてを定義するつもりはありません。例えば、この本では算術式や真偽値の式を定義しています。本章では別の方針を取り、単項演算子や二項演算子を取る一般的な式を定義します。

つまり、1 + true のような奇妙さを許容します！しかし、これはエンコーディングや文法、ひいてはメタプログラミングの教材として単純化することになります。

AST の定義

まず、アトミックなリテラルの値を定義します。

import Lean

open Lean Elab Meta

inductive IMPLit
  | nat  : Nat  → IMPLit
  | bool : Bool → IMPLit

次は唯一の単項演算子です。

inductive IMPUnOp
  | not

これらは二項演算子です。

inductive IMPBinOp
  | and | add | less

ここで、今回扱いたい式を定義します。

inductive IMPExpr
  | lit : IMPLit → IMPExpr
  | var : String → IMPExpr
  | un  : IMPUnOp → IMPExpr → IMPExpr
  | bin : IMPBinOp → IMPExpr → IMPExpr → IMPExpr

そして最後に、言語のコマンドです。この本に従って、「プログラムの各部分もプログラムである」としましょう：

inductive IMPProgram
  | Skip   : IMPProgram
  | Assign : String → IMPExpr → IMPProgram
  | Seq    : IMPProgram → IMPProgram → IMPProgram
  | If     : IMPExpr → IMPProgram → IMPProgram → IMPProgram
  | While  : IMPExpr → IMPProgram → IMPProgram

リテラルのエラボレート

さて、データ型ができたので、Syntax の項を Expr の項にエラボレートしましょう。まずはリテラルの構文とそのエラボレーション関数を定義します。

declare_syntax_cat imp_lit
syntax num       : imp_lit
syntax "true"    : imp_lit
syntax "false"   : imp_lit

def elabIMPLit : Syntax → MetaM Expr
  -- `mkAppM` は対象の関数の `Name` とその引数から `Expr.app` を作成する
  -- `mkNatLit` は `Nat` から `Expr` を作成する
  | `(imp_lit| $n:num) => mkAppM ``IMPLit.nat  #[mkNatLit n.getNat]
  | `(imp_lit| true  ) => mkAppM ``IMPLit.bool #[.const ``Bool.true []]
  | `(imp_lit| false ) => mkAppM ``IMPLit.bool #[.const ``Bool.false []]
  | _ => throwUnsupportedSyntax

elab "test_elabIMPLit " l:imp_lit : term => elabIMPLit l

#reduce test_elabIMPLit 4     -- IMPLit.nat 4
#reduce test_elabIMPLit true  -- IMPLit.bool true
#reduce test_elabIMPLit false -- IMPLit.bool true

式のエラボレート

式をエラボレートするために、単項演算子と二項演算子をエラボレートする方法も必要です。

これらは純粋関数（Syntax → Expr）にすることもできますが、マッチの網羅時に例外を簡単に投げられるように MetaM に留まることとします。

declare_syntax_cat imp_unop
syntax "not"     : imp_unop

def elabIMPUnOp : Syntax → MetaM Expr
  | `(imp_unop| not) => return .const ``IMPUnOp.not []
  | _ => throwUnsupportedSyntax

declare_syntax_cat imp_binop
syntax "+"       : imp_binop
syntax "and"     : imp_binop
syntax "<"       : imp_binop

def elabIMPBinOp : Syntax → MetaM Expr
  | `(imp_binop| +)   => return .const ``IMPBinOp.add []
  | `(imp_binop| and) => return .const ``IMPBinOp.and []
  | `(imp_binop| <)   => return .const ``IMPBinOp.less []
  | _ => throwUnsupportedSyntax

ここで式の構文を定義します：

declare_syntax_cat                   imp_expr
syntax imp_lit                     : imp_expr
syntax ident                       : imp_expr
syntax imp_unop imp_expr           : imp_expr
syntax imp_expr imp_binop imp_expr : imp_expr

IMP プログラマがパースの優先順位を示せるように括弧も許可しましょう。

syntax "(" imp_expr ")" : imp_expr

これで式をエラボレートできます。式は再帰的であることに注意してください。これは elabIMPExpr 関数が再帰的である必要があることを意味します！Lean は Syntax の消費だけでは終了を証明できないため partial を使う必要があります。

partial def elabIMPExpr : Syntax → MetaM Expr
  | `(imp_expr| $l:imp_lit) => do
    let l ← elabIMPLit l
    mkAppM ``IMPExpr.lit #[l]
  -- `mkStrLit` は `String` から `Expr` を作成する
  | `(imp_expr| $i:ident) => mkAppM ``IMPExpr.var #[mkStrLit i.getId.toString]
  | `(imp_expr| $b:imp_unop $e:imp_expr) => do
    let b ← elabIMPUnOp b
    let e ← elabIMPExpr e -- recurse!
    mkAppM ``IMPExpr.un #[b, e]
  | `(imp_expr| $l:imp_expr $b:imp_binop $r:imp_expr) => do
    let l ← elabIMPExpr l -- recurse!
    let r ← elabIMPExpr r -- recurse!
    let b ← elabIMPBinOp b
    mkAppM ``IMPExpr.bin #[b, l, r]
  | `(imp_expr| ($e:imp_expr)) => elabIMPExpr e
  | _ => throwUnsupportedSyntax

elab "test_elabIMPExpr " e:imp_expr : term => elabIMPExpr e

#reduce test_elabIMPExpr a
-- IMPExpr.var "a"

#reduce test_elabIMPExpr a + 5
-- IMPExpr.bin IMPBinOp.add (IMPExpr.var "a") (IMPExpr.lit (IMPLit.nat 5))

#reduce test_elabIMPExpr 1 + true
-- IMPExpr.bin IMPBinOp.add (IMPExpr.lit (IMPLit.nat 1)) (IMPExpr.lit (IMPLit.bool true))

プログラムのエラボレート

そしてこれで IMP プログラムをエラボレートするために必要なものがすべて手に入りました！

declare_syntax_cat           imp_program
syntax "skip"              : imp_program
syntax ident ":=" imp_expr : imp_program

syntax imp_program ";;" imp_program : imp_program

syntax "if" imp_expr "then" imp_program "else" imp_program "fi" : imp_program
syntax "while" imp_expr "do" imp_program "od" : imp_program

partial def elabIMPProgram : Syntax → MetaM Expr
  | `(imp_program| skip) => return .const ``IMPProgram.Skip []
  | `(imp_program| $i:ident := $e:imp_expr) => do
    let i : Expr := mkStrLit i.getId.toString
    let e ← elabIMPExpr e
    mkAppM ``IMPProgram.Assign #[i, e]
  | `(imp_program| $p₁:imp_program ;; $p₂:imp_program) => do
    let p₁ ← elabIMPProgram p₁
    let p₂ ← elabIMPProgram p₂
    mkAppM ``IMPProgram.Seq #[p₁, p₂]
  | `(imp_program| if $e:imp_expr then $pT:imp_program else $pF:imp_program fi) => do
    let e ← elabIMPExpr e
    let pT ← elabIMPProgram pT
    let pF ← elabIMPProgram pF
    mkAppM ``IMPProgram.If #[e, pT, pF]
  | `(imp_program| while $e:imp_expr do $pT:imp_program od) => do
    let e ← elabIMPExpr e
    let pT ← elabIMPProgram pT
    mkAppM ``IMPProgram.While #[e, pT]
  | _ => throwUnsupportedSyntax

そしてついにエラボレーションのパイプラインを完全にテストすることができます。以下の構文を使ってみましょう：

elab ">>" p:imp_program "<<" : term => elabIMPProgram p

#reduce >>
a := 5;;
if not a and 3 < 4 then
  c := 5
else
  a := a + 1
fi;;
b := 10
<<
-- IMPProgram.Seq (IMPProgram.Assign "a" (IMPExpr.lit (IMPLit.nat 5)))
--   (IMPProgram.Seq
--     (IMPProgram.If
--       (IMPExpr.un IMPUnOp.not
--         (IMPExpr.bin IMPBinOp.and (IMPExpr.var "a")
--           (IMPExpr.bin IMPBinOp.less (IMPExpr.lit (IMPLit.nat 3)) (IMPExpr.lit (IMPLit.nat 4)))))
--       (IMPProgram.Assign "c" (IMPExpr.lit (IMPLit.nat 5)))
--       (IMPProgram.Assign "a" (IMPExpr.bin IMPBinOp.add (IMPExpr.var "a") (IMPExpr.lit (IMPLit.nat 1)))))
--     (IMPProgram.Assign "b" (IMPExpr.lit (IMPLit.nat 10))))

タクティク

タクティクはカスタム状態を操作する Lean のプログラムです。すべてのタクティクは最終的に TacticM Unit 型になります。これは以下の型です：

-- from Lean/Elab/Tactic/Basic.lean
TacticM = ReaderT Context $ StateRefT State TermElabM

しかし、TacticM の使い方を説明する前に、マクロベースのタクティクを探求してみましょう。

マクロ展開によるタクティク

Lean 4 のインフラの他の大部分と同様に、タクティクも軽量なマクロ展開によって宣言することができます。

例えば、例としてエラボレートされると sorry になるタクティク custom_sorry_macro を作ってみます。これを構文 custom_sorry_macro のピースを構文 sorry のピースに展開するマクロ展開として書くことができます：

import Lean.Elab.Tactic

macro "custom_sorry_macro" : tactic => `(tactic| sorry)

example : 1 = 42 := by
  custom_sorry_macro

`trivial` の実装：マクロ展開による拡張可能なタクティク

より複雑な例として、初めは全く実装されておらず、後からより機能を拡張できるタクティクを書くことができ、ここでは custom_tactic という名前で作成します。まず、タクティクを実装せずに宣言するところからはじめます：

syntax "custom_tactic" : tactic

/-- error: tactic 'tacticCustom_tactic' has not been implemented -/
example : 42 = 42 := by
  custom_tactic
  sorry

ここで rfl タクティクを custom_tactic に追加することで、先ほどの定理を証明することができます。

macro_rules
| `(tactic| custom_tactic) => `(tactic| rfl)

example : 42 = 42 := by
   custom_tactic
-- ゴールが達成されました 🎉

次に、rfl ですぐに捌けない、より難しい問題に挑戦してみましょう：

#check_failure (by custom_tactic : 43 = 43 ∧ 42 = 42)
-- type mismatch
--   Iff.rfl
-- has type
--   ?m.1437 ↔ ?m.1437 : Prop
-- but is expected to have type
--   43 = 43 ∧ 42 = 42 : Prop

custom_tactic タクティクを拡張して、apply And.intro で And を分解し、custom_tactic を（再帰的に（！））2つのケースに (<;> trivial) で適用し、生成されたサブケース 43 = 43・42 = 42 を解決します。

macro_rules
| `(tactic| custom_tactic) => `(tactic| apply And.intro <;> custom_tactic)

上記の宣言では <;> を使っていますが、これは タクティクコンビネータ です。ここで、a <;> b は「タクティク a を実行し、a が生成した各ゴールに b を適用する」という意味です。したがって、And.intro <;> custom_tactic は「And.intro を実行し、次に各ゴールに custom_tactic を実行する」という意味になります。先ほどの定理でテストしてみると、定理をさばけていることがわかります。

example : 43 = 43 ∧ 42 = 42 := by
  custom_tactic
-- ゴールが達成されました 🎉

本節のまとめとして、ここでは拡張可能なタクティク custom_tactic を宣言しました。初めはこのタクティクは全くエラボレーションを持っていませんでした。そこに rfl を custom_tactic のエラボレーションとして追加し、42 = 42 というゴールを解けるようにしました。次により難しい定理である 43 = 43 ∧ 42 = 42 を試しましたが、custom_tactic では解くことができませんでした。そこで custom_tactic をリッチ化して、And.intro で「and」を分割し、2つのサブケースで custom_tactic を 再帰的に に呼び出すことができました。

`<;>` の実装：マクロ展開によるタクティクコンビネータ

前節で a <;> b は「a を実行し、続いてすべてのゴールに b を実行する」という意味だと言ったことを思い出してください。実は <;> 自体がタクティクマクロです。この節では、a and_then b という構文を定義し、これで「a を実行し、続いてすべてのゴールに b を実行する」を意味するようにします。

-- 1. 構文 `and_then` を定義
syntax tactic " and_then " tactic : tactic

-- 2. `a` を実行し、`a` が生成したすべてのゴールに対して `b` を実行するように戦術を展開するエキスパンダを書く。
macro_rules
| `(tactic| $a:tactic and_then $b:tactic) =>
    `(tactic| $a:tactic; all_goals $b:tactic)

-- 3. このタクティクをテストする。
theorem test_and_then: 1 = 1 ∧ 2 = 2 := by
  apply And.intro and_then rfl

#print test_and_then
-- theorem test_and_then : 1 = 1 ∧ 2 = 2 :=
-- { left := Eq.refl 1, right := Eq.refl 2 }

`TacticM` の探求

最もシンプルなタクティク：`sorry`

本節では、証明を申し訳程度に埋めるタクティクを書きたいと思います：

example : 1 = 2 := by
  custom_sorry

このようなタクティクについてまず宣言するところから始めます：

elab "custom_sorry_0" : tactic => do
  return

example : 1 = 2 := by
  custom_sorry_0
-- unsolved goals: ⊢ 1 = 2
  sorry

これは Lean に構文の拡張を定義しており、この構文のピースを tactic 構文カテゴリに属するものとして custom_sorry_0 と命名しています。これは tactic をエラボレートするコンテキストにおいて、構文のピース custom_sorry_0 を => の右側に書かかれたもの（タクティクの実際の実装）へとエラボレートしなければならないことをエラボレータに知らせています。

次に、α 型の項を機械的に合成できる sorryAx α で埋めるために TacticM Unit で項を書きます。これを行うには、まず Lean.Elab.Tactic.getMainGoal : Tactic MVarId でゴールにアクセスします。これはメインのゴールをメタ変数として表現して返します。命題としての型の考え方の下では、このゴールの型は命題 1 = 2 でなければならないことを思い出してください。これを確認するために goal の型を表示します。

しかし、これにあたって更新されたコンテキストで TacticM を計算する Lean.Elab.Tactic.withMainContext でタクティクを開始する必要があります。

elab "custom_sorry_1" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goal ← Lean.Elab.Tactic.getMainGoal
    let goalDecl ← goal.getDecl
    let goalType := goalDecl.type
    dbg_trace f!"goal type: {goalType}"

example : 1 = 2 := by
  custom_sorry_1
-- goal type: Eq.{1} Nat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))
-- unsolved goals: ⊢ 1 = 2
  sorry

ゴールを sorry するために、ヘルパー Lean.Elab.admitGoal を使用することができます：

elab "custom_sorry_2" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goal ← Lean.Elab.Tactic.getMainGoal
    Lean.Elab.admitGoal goal

theorem test_custom_sorry : 1 = 2 := by
  custom_sorry_2

#print test_custom_sorry
-- theorem test_custom_sorry : 1 = 2 :=
-- sorryAx (1 = 2) true

これで unsolved goals: ⊢ 1 = 2 というエラーが現れなくなります。

`custom_assump` タクティク：仮定へのアクセス

本節では、ゴールを証明するための仮定へのアクセス方法を学びます。特に、仮定の中からゴールと完全一致するものを探し、可能であれば定理を解く custom_assump というタクティクの実装を試みます。

以下の例では、custom_assump が (H2 : 2 = 2) を使って (2 = 2) を解くことを期待しています：

theorem assump_correct (H1 : 1 = 1) (H2 : 2 = 2) : 2 = 2 := by
  custom_assump

#print assump_correct
-- theorem assump_correct : 1 = 1 → 2 = 2 → 2 = 2 :=
-- fun H1 H2 => H2

ゴールに一致する仮定が無い場合、custom_assump タクティクがエラーを投げることを期待します。これによってお望みの型の仮定を見つけられなかったことがわかります：

theorem assump_wrong (H1 : 1 = 1) : 2 = 2 := by
  custom_assump

#print assump_wrong
-- tactic 'custom_assump' failed, unable to find matching hypothesis of type (2 = 2)
-- H1 : 1 = 1
-- ⊢ 2 = 2

まず、ゴールとゴールの型にアクセスし、何を証明しようとしているのかを知ることから始めます。この goal の変数はこの後すぐエラーメッセージを作成するのに役立ちます。

elab "custom_assump_0" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goalType ← Lean.Elab.Tactic.getMainTarget
    dbg_trace f!"goal type: {goalType}"

example (H1 : 1 = 1) (H2 : 2 = 2): 2 = 2 := by
  custom_assump_0
-- goal type: Eq.{1} Nat (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))
-- unsolved goals
-- H1 : 1 = 1
-- H2 : 2 = 2
-- ⊢ 2 = 2
  sorry

example (H1 : 1 = 1): 2 = 2 := by
  custom_assump_0
-- goal type: Eq.{1} Nat (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))
-- unsolved goals
-- H1 : 1 = 1
-- ⊢ 2 = 2
  sorry

次に、LocalContext というデータ構造に格納されている仮定のリストにアクセスします。これは Lean.MonadLCtx.getLCtx でアクセスできます。この LocalContext には LocalDeclaration が含まれており、宣言につけられた名前（.userName）や宣言の式（.toExpr）などの情報を取り出すことができます。ローカル宣言を表示する list_local_decls というタクティクを書いてみましょう：

elab "list_local_decls_1" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let ctx ← Lean.MonadLCtx.getLCtx -- get the local context.
    ctx.forM fun decl: Lean.LocalDecl => do
      let declExpr := decl.toExpr -- Find the expression of the declaration.
      let declName := decl.userName -- Find the name of the declaration.
      dbg_trace f!"+ local decl: name: {declName} | expr: {declExpr}"

example (H1 : 1 = 1) (H2 : 2 = 2): 1 = 1 := by
  list_local_decls_1
-- + local decl: name: test_list_local_decls_1 | expr: _uniq.3339
-- + local decl: name: H1 | expr: _uniq.3340
-- + local decl: name: H2 | expr: _uniq.3341
  rfl

さて、仮定と同じ型を持つローカル宣言を探していたことを思い出してください。ローカル宣言の式に対して Lean.Meta.inferType を呼び出して LocalDecl の型を取得します。

elab "list_local_decls_2" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let ctx ← Lean.MonadLCtx.getLCtx -- get the local context.
    ctx.forM fun decl: Lean.LocalDecl => do
      let declExpr := decl.toExpr -- Find the expression of the declaration.
      let declName := decl.userName -- Find the name of the declaration.
      let declType ← Lean.Meta.inferType declExpr -- **NEW:** Find the type.
      dbg_trace f!"+ local decl: name: {declName} | expr: {declExpr} | type: {declType}"

example (H1 : 1 = 1) (H2 : 2 = 2): 1 = 1 := by
  list_local_decls_2
  -- + local decl: name: test_list_local_decls_2 | expr: _uniq.4263 | type: (Eq.{1} Nat ...)
  -- + local decl: name: H1 | expr: _uniq.4264 | type: Eq.{1} Nat ...)
  -- + local decl: name: H2 | expr: _uniq.4265 | type: Eq.{1} Nat ...)
  rfl

これらの LocalDecl の型がゴールの型と等しいかどうかを Lean.Meta.isExprDefEq でチェックします。以下では eq? で型が等しいかどうかをチェックし、H1 はゴールと同じ型を持ち（local decl[EQUAL? true]: name: H1）、H2 は同じ型を持たない（local decl[EQUAL? false]: name: H2 ）ことを表示しています：

elab "list_local_decls_3" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goalType ← Lean.Elab.Tactic.getMainTarget
    let ctx ← Lean.MonadLCtx.getLCtx -- get the local context.
    ctx.forM fun decl: Lean.LocalDecl => do
      let declExpr := decl.toExpr -- Find the expression of the declaration.
      let declName := decl.userName -- Find the name of the declaration.
      let declType ← Lean.Meta.inferType declExpr -- Find the type.
      let eq? ← Lean.Meta.isExprDefEq declType goalType -- **NEW** Check if type equals goal type.
      dbg_trace f!"+ local decl[EQUAL? {eq?}]: name: {declName}"

example (H1 : 1 = 1) (H2 : 2 = 2): 1 = 1 := by
  list_local_decls_3
-- + local decl[EQUAL? false]: name: test_list_local_decls_3
-- + local decl[EQUAL? true]: name: H1
-- + local decl[EQUAL? false]: name: H2
  rfl

最後に、これらのパーツをまとめて、すべての宣言でループし、正しい型を持つ宣言を見つけるタクティクを書きます。lctx.findDeclM? で宣言のループを行います。この宣言の型は Lean.Meta.inferType で推測します。Lean.Meta.isExprDefEq で宣言がゴールと同じ型であることを確認します：

elab "custom_assump_1" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goalType ← Lean.Elab.Tactic.getMainTarget
    let lctx ← Lean.MonadLCtx.getLCtx
    -- ローカルの宣言に対して繰り返し…
    let option_matching_expr ← lctx.findDeclM? fun ldecl: Lean.LocalDecl => do
      let declExpr := ldecl.toExpr -- Find the expression of the declaration.
      let declType ← Lean.Meta.inferType declExpr -- Find the type.
      if (← Lean.Meta.isExprDefEq declType goalType) -- Check if type equals goal type.
      then return some declExpr -- If equal, success!
      else return none          -- Not found.
    dbg_trace f!"matching_expr: {option_matching_expr}"

example (H1 : 1 = 1) (H2 : 2 = 2) : 2 = 2 := by
  custom_assump_1
-- matching_expr: some _uniq.6241
  rfl

example (H1 : 1 = 1) : 2 = 2 := by
  custom_assump_1
-- matching_expr: none
  rfl

マッチする式を見つけることができたため、このマッチによって定理を閉じる必要があります。これには Lean.Elab.Tactic.closeMainGoal を用います。マッチする式が無い場合、Lean.Meta.throwTacticEx で例外を投げ、これによって与えられたゴールに対応するエラーを報告することができます。この例外を投げるとき、m!"..." を使って例外をフォーマットし、MessageData を構築します。これは f!"..." による Format よりもきれいなエラーメッセージを提供します。これは MessageData が デラボレーション も実行し、(Eq.{1} Nat (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) のような Lean の生の項を (2 = 2) のような読みやすい文字列に変換してくれます。以下に示す一連のコードはこれらを示しています：

elab "custom_assump_2" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goal ← Lean.Elab.Tactic.getMainGoal
    let goalType ← Lean.Elab.Tactic.getMainTarget
    let ctx ← Lean.MonadLCtx.getLCtx
    let option_matching_expr ← ctx.findDeclM? fun decl: Lean.LocalDecl => do
      let declExpr := decl.toExpr
      let declType ← Lean.Meta.inferType declExpr
      if ← Lean.Meta.isExprDefEq declType goalType
        then return Option.some declExpr
        else return Option.none
    match option_matching_expr with
    | some e => Lean.Elab.Tactic.closeMainGoal e
    | none =>
      Lean.Meta.throwTacticEx `custom_assump_2 goal
        (m!"unable to find matching hypothesis of type ({goalType})")

example (H1 : 1 = 1) (H2 : 2 = 2) : 2 = 2 := by
  custom_assump_2

#check_failure (by custom_assump_2 : (H1 : 1 = 1) → 2 = 2)
-- tactic 'custom_assump_2' failed, unable to find matching hypothesis of type (2 = 2)
-- H1 : 1 = 1
-- ⊢ 2 = 2

コンテキストの調整

これまではコンテキストを使って読み込みのような操作のみを行ってきました。しかし、コンテキストを変更したい場合はどうすればいいのでしょうか？本節では、ゴールの順番を変更する方法と、ゴールに内容（新しい仮定）を追加する方法を説明します。

項をエラボレートした後、補助関数 Lean.Elab.Tactic.liftMetaTactic を使う必要があります。これは MetaM で計算を実行することができ、同時にゴールの MVarId を与えてくれます。計算の最後に、liftMetaTactic は結果のゴールのリストとして List MVarId を返すことを期待します。

custom_let と custom_have の唯一の違いは、前者は Lean.MVarId.define を使うのに対して、後者は Lean.MVarId.assert を使うということだけです：

open Lean.Elab.Tactic in
elab "custom_let " n:ident " : " t:term " := " v:term : tactic =>
  withMainContext do
    let t ← elabTerm t none
    let v ← elabTermEnsuringType v t
    liftMetaTactic fun mvarId => do
      let mvarIdNew ← mvarId.define n.getId t v
      let (_, mvarIdNew) ← mvarIdNew.intro1P
      return [mvarIdNew]

open Lean.Elab.Tactic in
elab "custom_have " n:ident " : " t:term " := " v:term : tactic =>
  withMainContext do
    let t ← elabTerm t none
    let v ← elabTermEnsuringType v t
    liftMetaTactic fun mvarId => do
      let mvarIdNew ← mvarId.assert n.getId t v
      let (_, mvarIdNew) ← mvarIdNew.intro1P
      return [mvarIdNew]

theorem test_faq_have : True := by
  custom_let n : Nat := 5
  custom_have h : n = n := rfl
-- n : Nat := 5
-- h : n = n
-- ⊢ True
  trivial

ゴールのリストの「取得」と「設定」

これらを説明するために、ゴールのリストを反転させるタクティクを作ってみましょう。Lean.Elab.Tactic.getGoals と Lean.Elab.Tactic.setGoals を用います：

elab "reverse_goals" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goals : List Lean.MVarId ← Lean.Elab.Tactic.getGoals
    Lean.Elab.Tactic.setGoals goals.reverse

theorem test_reverse_goals : (1 = 2 ∧ 3 = 4) ∧ 5 = 6 := by
  constructor
  constructor
-- case left.left
-- ⊢ 1 = 2
-- case left.right
-- ⊢ 3 = 4
-- case right
-- ⊢ 5 = 6
  reverse_goals
-- case right
-- ⊢ 5 = 6
-- case left.right
-- ⊢ 3 = 4
-- case left.left
-- ⊢ 1 = 2
  all_goals sorry

FAQ

本節では、タクティクを書く際によく使われるパターンを集め、共通のパターンを見つけやすくします。

問：ゴールはどう使えばよいですか？

答：ゴールはメタ変数として表現されます。Lean.Elab.Tactic.Basic モジュールには、新しいゴールを追加したり、ゴールを切り替えたりするための多くの関数があります。

問：メインのゴールはどのようにして取得できますか？

答：Lean.Elab.Tactic.getMainGoal を使います。

elab "faq_main_goal" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goal ← Lean.Elab.Tactic.getMainGoal
    dbg_trace f!"goal: {goal.name}"

example : 1 = 1 := by
  faq_main_goal
-- goal: _uniq.9298
  rfl

問：ゴールのリストはどのようにして取得できますか？

答：getGoals を使います。

elab "faq_get_goals" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goals ← Lean.Elab.Tactic.getGoals
    goals.forM $ fun goal => do
      let goalType ← goal.getType
      dbg_trace f!"goal: {goal.name} | type: {goalType}"

example (b : Bool) : b = true := by
  cases b
  faq_get_goals
-- goal: _uniq.10067 | type: Eq.{1} Bool Bool.false Bool.true
-- goal: _uniq.10078 | type: Eq.{1} Bool Bool.true Bool.true
  sorry
  rfl

問：あるゴールに対して現在の仮定はどのようにして取得できますか？

答：ローカルコンテキストを提供する Lean.MonadLCtx.getLCtx を使い、foldM や forM などのアクセサを使って LocalContext の LocalDeclaration を繰り返し処理します。

elab "faq_get_hypotheses" : tactic =>
  Lean.Elab.Tactic.withMainContext do
  let ctx ← Lean.MonadLCtx.getLCtx -- get the local context.
  ctx.forM (fun (decl : Lean.LocalDecl) => do
    let declExpr := decl.toExpr -- Find the expression of the declaration.
    let declType := decl.type -- Find the type of the declaration.
    let declName := decl.userName -- Find the name of the declaration.
    dbg_trace f!" local decl: name: {declName} | expr: {declExpr} | type: {declType}"
  )

example (H1 : 1 = 1) (H2 : 2 = 2): 3 = 3 := by
  faq_get_hypotheses
  -- local decl: name: _example | expr: _uniq.10814 | type: ...
  -- local decl: name: H1 | expr: _uniq.10815 | type: ...
  -- local decl: name: H2 | expr: _uniq.10816 | type: ...
  rfl

問：タクティクはどのように評価できますか？

答：与えられたタクティクの構文を評価する Lean.Elab.Tactic.evalTactic: Syntax → TacticM Unit を使います。マクロ `(tactic| ⋯) を使ってタクティク構文を作ることができます。

例えば、次のコード片で try rfl を呼び出すことができます：

Lean.Elab.Tactic.evalTactic (← `(tactic| try rfl))

問：2つの式が等しいかどうかはどのようにしてチェックできますか？

答：Lean.Meta.isExprDefEq <expr-1> <expr-2> を使います。

#check Lean.Meta.isExprDefEq
-- Lean.Meta.isExprDefEq : Lean.Expr → Lean.Expr → Lean.MetaM Bool

問：タクティクから例外を投げるにはどうしたらよいですか？

答：throwTacticEx <tactic-name> <goal-mvar> <error> を使います。

elab "faq_throw_error" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goal ← Lean.Elab.Tactic.getMainGoal
    Lean.Meta.throwTacticEx `faq_throw_error goal "throwing an error at the current goal"

#check_failure (by faq_throw_error : (b : Bool) → b = true)
-- tactic 'faq_throw_error' failed, throwing an error at the current goal
-- ⊢ ∀ (b : Bool), b = true

問：Lean.Elab.Tactic.* と Lean.Meta.Tactic.* の違いはなんですか？

答：Lean.Meta.Tactic.* には Meta モナドを使って書き換えのような基本的な機能を実装する低レベルのコードが含まれています。Lean.Elab.Tactic.* は Lean.Meta での低レベルの開発をタクティク的なインフラストラクチャと構文解析のフロントエンドに接続する高レベルのコードを含みます。

演習問題

p ∧ q ↔ q ∧ p という定理を考えてみましょう。これの証明は証明項として書くこともタクティクを使って構成することもできます。この定理を 証明項として と書くとき、_ を特定の式として埋めて徐々に証明を進めます。このような各ステップがタクティクに対応します。

この証明項を書くためのステップの組み合わせはたくさんありますが、以下に書く一連のステップを考えてみましょう。各ステップをタクティクとして書いてください。タクティク step_1 は埋めてあるため残りのタクティクも同じように書いてください。（練習のために、mkFreshExprMVar・mvarId.assign・modify fun _ => { goals := ~) などの低レベルの API を使うようにしてください。）

-- [this is the initial goal]
example : p ∧ q ↔ q ∧ p :=
  _

-- step_1
example : p ∧ q ↔ q ∧ p :=
  Iff.intro _ _

-- step_2
example : p ∧ q ↔ q ∧ p :=
  Iff.intro
    (
      fun hA =>
      _
    )
    (
      fun hB =>
      (And.intro hB.right hB.left)
    )

-- step_3
example : p ∧ q ↔ q ∧ p :=
  Iff.intro
    (
      fun hA =>
      (And.intro _ _)
    )
    (
      fun hB =>
      (And.intro hB.right hB.left)
    )

-- step_4
example : p ∧ q ↔ q ∧ p :=
  Iff.intro
    (
      fun hA =>
      (And.intro hA.right hA.left)
    )
    (
      fun hB =>
      (And.intro hB.right hB.left)
    )

elab "step_1" : tactic => do
  let mvarId ← getMainGoal
  let goalType ← getMainTarget

  let Expr.app (Expr.app (Expr.const `Iff _) a) b := goalType | throwError "Goal type is not of the form `a ↔ b`"

  -- 1. Create new `_`s with appropriate types.
  let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red")
  let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue")

  -- 2. Assign the main goal to the expression `Iff.intro _ _`.
  mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2])

  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }

theorem gradual (p q : Prop) : p ∧ q ↔ q ∧ p := by
  step_1
  step_2
  step_3
  step_4

1つ目の演習問題では、ゴールの更新に低レベル API modify を持ちいました。liftMetaTactic・setGoals・appendGoals・replaceMainGoal・closeMainGoal など、これらはすべて modify fun s : State => { s with goals := myMvarIds } の上に構築された構文糖衣です。以下の forker タクティクを次の内容で書き換えてください：

a) liftMetaTactic b) setGoals c) replaceMainGoal

elab "forker" : tactic => do
  let mvarId ← getMainGoal
  let goalType ← getMainTarget

  let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId (m!"Goal is not of the form P ∧ Q")

  mvarId.withContext do
    let mvarIdP ← mkFreshExprMVar p (userName := "red")
    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")

    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
    mvarId.assign proofTerm

    modify fun state => { goals := [mvarIdP.mvarId!, mvarIdQ.mvarId!] ++ state.goals.drop 1 }

example (A B C : Prop) : A → B → C → (A ∧ B) ∧ C := by
  intro hA hB hC
  forker
  forker
  assumption
  assumption
  assumption

1つ目の演習問題では、step_2 を使って独自の intro を作成しました（仮定名はハードコードされていますが、基本的には同じものです）。タクティクを書く際は通常、intro・intro1・intro1P・introN・introNP などの関数を利用したくなります。

以下の各ポイントについて、introducer タクティクを作ってください（各ポイントにつき1つずつ）。これらはゴール (ab: a = b) → (bc: b = c) → (a = c) を以下のゴールに変換します：

a) 仮定 (ab✝: a = b) と (bc✝: b = c) をもとに (a = c) というゴールへ変換する。 b) 仮定 (ab: a = b) をもとに (bc: b = c) → (a = c) というゴールへ変換する。 c) 仮定 (hello: a = b) をもとに (bc: b = c) → (a = c) というゴールへ変換する。
```
example (a b c : Nat) : (ab: a = b) → (bc: b = c) → (a = c) := by
  introductor
  sorry
```
ヒント：intro1P と introNP の "P" は "Preserve" を意味します。

Lean4 チートシート

情報の抽出

ゴールの抽出：Lean.Elab.Tactic.getMainGoal

これは let goal ← Lean.Elab.Tactic.getMainGoal のように使います。
メタ変数からの宣言の抽出：mvarId.getDecl、ここで mvarId : Lean.MVarId がコンテキストにあるとします。例えば、ゴールの mvarId は getMainGoal を使用して抽出することができます。
メタ変数の型の抽出：mvarId.getType、ここで mvarId : Lean.MVarId がコンテキストにあるとします。
メインのゴールの型の抽出：Lean.Elab.Tactic.getMainTarget

これは let goal_type ← Lean.Elab.Tactic.getMainTarget のように使います。

これは下記と同じ結果になります。

let goal ← Lean.Elab.Tactic.getMainGoal
let goal_type ← goal.getType

ローカルコンテキストの抽出：Lean.MonadLCtx.getLCtx

これは let lctx ← Lean.MonadLCtx.getLCtx のように使います。
宣言の名前の抽出：Lean.LocalDecl.userName ldecl、ここで ldecl : Lean.LocalDecl がコンテキストにあるとします。
式の型の抽出：Lean.Meta.inferType expr、ここで expr : Lean.Expr がコンテキストにあるとします。

これは let expr_type ← Lean.Meta.inferType expr のように使います。

式で遊ぶ

宣言を式に変換する：Lean.LocalDecl.toExpr

これは ldecl : Lean.LocalDecl がコンテキストにある場合に ldecl.toExpr のように使います。

この ldecl は例えば、let ldecl ← Lean.MonadLCtx.getLCtx などで取得されます。
2つの式が定義上等しいかどうかのチェック：Lean.Meta.isDefEq ex1 ex2、ここで ex1 ex2 : Lean.Expr がコンテキストにあるとします。これは Lean.MetaM Bool を返します。
ゴールを閉じる：Lean.Elab.Tactic.closeMainGoal expr、ここで expr : Lean.Expr がコンテキストにあるとします。

さらなるコマンド

メタ-sorry：Lean.Elab.admitGoal goal、ここで goal : Lean.MVarId がコンテキストにあるとします。

表示とエラー

通常の用途での「永久な」メッセージの表示：

Lean.logInfo f!"Hi, I will print\n{Syntax}"
デバッグ中のメッセージの表示：

dbg_trace f!"1) goal: {Syntax_that_will_be_interpreted}".
例外を投げる：Lean.Meta.throwTacticEx name mvar message_data、ここで name : Lean.Name はタクティクの名前で mvar はエラーのデータを保持しているとします。

これは Lean.Meta.throwTacticEx `tac goal (m!"unable to find matching hypothesis of type ({goal_type})") のように用い、ここでフォーマッタ m! は項をより見やすく表示する MessageData を構築します。

TODO: Add?

Lean.LocalContext.forM
Lean.LocalContext.findDeclM?

付録：オプション

オプションはメタプログラムと Lean のコンパイラの両方に特別な設定を伝える機能です。基本的にこれは KVMap であり、Name から Lean.DataValue への単純なマップです。現在、6種類のデータ値を有します：

String
Bool
Name
Nat
Int
Syntax

set_option コマンドを使うことで、とても簡単に Lean コンパイラにプログラムに対して何か違うことを行うように指示するオプションを設定することができます：

import Lean
open Lean

#check 1 + 1 -- 1 + 1 : Nat

set_option pp.explicit true -- No custom syntax in pretty printing

#check 1 + 1 -- @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) 1 1 : Nat

set_option pp.explicit false

さらに、オプションの値をすぐ次のコマンドや項だけに限定することもできます：

set_option pp.explicit true in
#check 1 + 1 -- @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) 1 1 : Nat

#check 1 + 1 -- 1 + 1 : Nat

#check set_option trace.Meta.synthInstance true in 1 + 1 -- the trace of the type class synthesis for `OfNat` and `HAdd`

もし今すぐ利用可能なオプションを取り出したい場合は、set_option コマンドを実行し、カーソルをその名前が書かれている場所に移動するだけで、自動補完の候補としてそれらのオプションのリストが表示されるでしょう。メタ関連でデバッグをしているときに最も役に立つオプションは trace. から始まるものです。

メタプログラミングにおけるオプション

これでオプションを設定する方法がわかったので、メタプログラムがオプションにアクセスする方法を見てみましょう。最も一般的な方法は MonadOptions 型クラスを通じたもので、これは Monad に関数 getOptions : m Options を拡張したものです。現時点でこれは以下に対して実装されています：

CoreM
CommandElabM
LevelElabM
上記のいずれかの操作を持ち上げることができるすべてのモナド（例えば、CoreM から MetaM）

一度 Options オブジェクトを取得すれば、Options.get を使って情報を照会することができます。これを示すために、pp.explicit の値を表示するコマンドを書いてみましょう。

elab "#getPPExplicit" : command => do
  let opts ← getOptions
  -- defValue = default value
  logInfo s!"pp.explicit : {opts.get pp.explicit.name pp.explicit.defValue}"

#getPPExplicit -- pp.explicit : false

set_option pp.explicit true in
#getPPExplicit -- pp.explicit : true

pp.explicit を取得するた実際の実装である Lean.getPPExplicit は代わりに pp.all がデフォルト値として設定されているかどうかを使用することに注意してください。

独自のオプションを作る

独自のオプションを宣言するのも非常に簡単です。Lean コンパイラはこのために register_option というマクロを用意しています。実際に使ってみましょう：

register_option book.myGreeting : String := {
  defValue := "Hello World"
  group := "pp"
  descr := "just a friendly greeting"
}

しかし、初期化の制約があるため、宣言したオプションをそのまま同じファイルで使うことはできません。

付録：プリティプリント

プリティプリンタとは、Lean がエラボレートした項をユーザに提示するために使用されるものです。これは Expr を Syntax に変換し、さらに高レベルのプリティプリント用データ構造に戻すことで行われます。これは Lean が Expr を作成する際に使用した実際の Syntax を思い出すわけではないことを意味します：もしそうであればその方法を指示するコードがあるはずですから。全体像として、プリティプリンタは3つの部分から構成されています：

デラボレータ、この部分は簡単に独自のコードで拡張ができることもあり最も興味深い部分です。このパートの仕事は Expr を Syntax に戻すことです。
parenthesizer は Syntax 木に便利だと思われる位置に括弧を追加する役割を持ちます。
フォーマッタ は括弧が付けられた Syntax 木に明示的なスペースを入れるなどのよりプリティプリントな情報を含む Format オブジェクトに変換する役割を持ちます。

デラボレーション

その名前が示すように、デラボレータはある意味においてエラボレータの反対です。デラボレータの仕事は、エラボレータが生成した Expr を受け取り、Syntax に戻すことです。ここで生成される Syntax はエラボレートされると、デラボレータに入力された Expr と同じものを出力しなければなりません。

デラボレータは Lean.PrettyPrinter.Delaborator.Delab という型を持ちます。これは DelabM Syntax のエイリアスで、DelabM はデラボレーションのためのモナドです。この機構についてはすべてここにて定義されています。DelabM は非常に多くのオプションを提供しており、これはドキュメントから探すことができます（TODO: Docs link）。ここでは単に最も関連性のある部分を強調します。

MonadQuotation インスタンスを持っており、おなじみのquotation構文を使って Syntax オブジェクトを宣言することができます。
MetaM のコードを実行することができます。
例外を投げるための MonadExcept インスタンスを持ちます。
whenPPOption のような関数を使うことで pp オプションを操作することができます。
現在の部分式を取得するには SubExpr.getExpr を使用します。また、SubExpr モジュールには、この概念を扱う API 全体が定義されています。

独自のデラボレータを作る

メタプログラミングの多くのものと同様に、エラボレータは属性に基づいており、今回の場合では delab です。delab は引数として Name を受け取り、この名前は Expr コンストラクタの名前で始まる必要があり、最も一般的あなのは const か app です。このコンストラクタ名の後にデラボレートしたい定数の名前が続きます。例えば、関数 foo を特別な方法でデラボレートしたい場合は app.foo を使います。これを実際にやってみましょう：

import Lean

open Lean PrettyPrinter Delaborator SubExpr

def foo : Nat → Nat := fun x => 42

@[delab app.foo]
def delabFoo : Delab := do
  `(1)

#check foo -- 1 : Nat → Nat
#check foo 13 -- 1 : Nat, full applications are also pretty printed this way

この Syntax を再度エラボレートしても同じ Expr は得られないため、明らかに良いデラボレータではありません。他の多くのメタプログラミングの属性と同様に、デラボレータをオーバーロードすることもできます：

@[delab app.foo]
def delabfoo2 : Delab := do
  `(2)

#check foo -- 2 : Nat → Nat

それを使うかを判断するメカニズムも同じです。デラボレータは登録された順番の逆順に、「Expr に対して責任が無いと感じる」ことを示すエラーを投げないものまで試行されます。デラボレータの場合、これは failure を使って行われます：

@[delab app.foo]
def delabfoo3 : Delab := do
  failure
  `(3)

#check foo -- 2 : Nat → Nat, still 2 since 3 failed

foo のための適切なデラボレータを書くためにはもう少し高度な機構を使う必要があります：

@[delab app.foo]
def delabfooFinal : Delab := do
  let e ← getExpr
  guard $ e.isAppOfArity' `foo 1 -- only delab full applications this way
  let fn := mkIdent `fooSpecial
  let arg ← withAppArg delab
  `($fn $arg)

#check foo 42 -- fooSpecial 42 : Nat
#check foo -- 2 : Nat → Nat, still 2 since 3 failed

読者は delabFooFinal を拡張して、完全でない適用も考慮することができるでしょうか？

Unexpanders

デラボレータは明らかに強力ですが、使う必要がないことも良くあります。Lean コンパイラにて @[delab か @[builtin_delab（コンパイラ用の特別バージョンの delab 属性）を探してみるとほとんど出てこないことがわかるでしょう。というのも、プリティプリントの大部分はいわゆる unexpander によって行われるからです。デラボレータとは異なり、これらは Lean.PrettyPrinter.Unexpander 型で、これは Syntax → Lean.PrettyPrinter.UnexpandM Syntax のエイリアスです。見ての通り、これらは Syntax から Syntax への変換で、マクロの逆であることを除けばマクロによく似ています。UnexpandM モナドは DelabM よりもかなり弱いですが、それでも下記の機能を持ちます：

syntax quotation のための MonadQuotation
例外の送出機能、ただこれはあまり有益なものではありません：唯一有効なのは throw () だけです。

unexpander は常にある1つの定数の適用に対して固有です。これらは app_unexpander 属性と、それに続く対象の定数名を使って登録されます。unexpander には暗黙の引数無しで Expr がデラボレートされた後に、定数の適用全体が渡されます。これを実際に見てみましょう：

def myid {α : Type} (x : α) := x

@[app_unexpander myid]
def unexpMyId : Unexpander
  -- 健全性を無効にすることで、マクロスコープなどを使わずに `id` を実際に返すことができる。
  | `(myid $arg) => set_option hygiene false in `(id $arg)
  | `(myid) => pure $ mkIdent `id
  | _ => throw ()

#check myid 12 -- id 12 : Nat
#check myid -- id : ?m.3870 → ?m.3870

unexpander についていくつかの良例は NotationExtra を参照してください。

ミニプロジェクト

いつものように、章の最後にてちょっとしたミニプロジェクトに取り組んでみます。今回はミニプログラミング言語のための独自の unexpander を作ります。infix や notation のような構文を定義するための多くの方法には必要なプリティプリンタコードを生成する機能がすでに組み込まれていることに注意してください（ただし、macro_rules には含まれていません）。そのため、簡単な構文であれば、自分でこれを行う必要はないでしょう。

declare_syntax_cat lang
syntax num   : lang
syntax ident : lang
syntax "let " ident " := " lang " in " lang: lang
syntax "[Lang| " lang "]" : term

inductive LangExpr
  | numConst : Nat → LangExpr
  | ident    : String → LangExpr
  | letE     : String → LangExpr → LangExpr → LangExpr

macro_rules
  | `([Lang| $x:num ]) => `(LangExpr.numConst $x)
  | `([Lang| $x:ident]) => `(LangExpr.ident $(Lean.quote (toString x.getId)))
  | `([Lang| let $x:ident := $v:lang in $b:lang]) => `(LangExpr.letE $(Lean.quote (toString x.getId)) [Lang| $v] [Lang| $b])

instance : Coe NumLit (TSyntax `lang) where
  coe s := ⟨s.raw⟩

instance : Coe Ident (TSyntax `lang) where
  coe s := ⟨s.raw⟩

-- LangExpr.letE "foo" (LangExpr.numConst 12)
--   (LangExpr.letE "bar" (LangExpr.ident "foo") (LangExpr.ident "foo")) : LangExpr
#check [Lang|
  let foo := 12 in
  let bar := foo in
  foo
]

見ての通り、現時点の表示される出力はかなり醜いものになっています。unexpander を使えばもっとよくなります：

@[app_unexpander LangExpr.numConst]
def unexpandNumConst : Unexpander
  | `(LangExpr.numConst $x:num) => `([Lang| $x])
  | _ => throw ()

@[app_unexpander LangExpr.ident]
def unexpandIdent : Unexpander
  | `(LangExpr.ident $x:str) =>
    let str := x.getString
    let name := mkIdent $ Name.mkSimple str
    `([Lang| $name])
  | _ => throw ()

@[app_unexpander LangExpr.letE]
def unexpandLet : Unexpander
  | `(LangExpr.letE $x:str [Lang| $v:lang] [Lang| $b:lang]) =>
    let str := x.getString
    let name := mkIdent $ Name.mkSimple str
    `([Lang| let $name := $v in $b])
  | _ => throw ()

-- [Lang| let foo := 12 in foo] : LangExpr
#check [Lang|
  let foo := 12 in foo
]

-- [Lang| let foo := 12 in let bar := foo in foo] : LangExpr
#check [Lang|
  let foo := 12 in
  let bar := foo in
  foo
]

この方がずっと良いです！いつものように読者は、括弧でくくられた式や、より多くのデータ値、term の引用など思いついたものを使って自分で言語を拡張することをお勧めします。

import Lean
open Lean Meta

Solutions

Expressions: Solutions

1.

def one : Expr :=
  Expr.app (Expr.app (Expr.const `Nat.add []) (mkNatLit 1)) (mkNatLit 2)

elab "one" : term => return one
#check one  -- Nat.add 1 2 : Nat
#reduce one -- 3

2.

def two : Expr :=
  Lean.mkAppN (Expr.const `Nat.add []) #[mkNatLit 1, mkNatLit 2]

elab "two" : term => return two
#check two  -- Nat.add 1 2 : Nat
#reduce two -- 3

3.

def three : Expr :=
  Expr.lam `x (Expr.const `Nat [])
  (Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 1, Expr.bvar 0])
  BinderInfo.default

elab "three" : term => return three
#check three    -- fun x => Nat.add 1 x : Nat → Nat
#reduce three 6 -- 7

4.

def four : Expr :=
  Expr.lam `a (Expr.const `Nat [])
  (
    Expr.lam `b (Expr.const `Nat [])
    (
      Expr.lam `c (Expr.const `Nat [])
      (
        Lean.mkAppN
        (Expr.const `Nat.add [])
        #[
          (Lean.mkAppN (Expr.const `Nat.mul []) #[Expr.bvar 1, Expr.bvar 2]),
          (Expr.bvar 0)
        ]
      )
      BinderInfo.default
    )
    BinderInfo.default
  )
  BinderInfo.default

elab "four" : term => return four
#check four -- fun a b c => Nat.add (Nat.mul b a) c : Nat → Nat → Nat → Nat
#reduce four 666 1 2 -- 668

5.

def five :=
  Expr.lam `x (Expr.const `Nat [])
  (
    Expr.lam `y (Expr.const `Nat [])
    (Lean.mkAppN (Expr.const `Nat.add []) #[Expr.bvar 1, Expr.bvar 0])
    BinderInfo.default
  )
  BinderInfo.default

elab "five" : term => return five
#check five      -- fun x y => Nat.add x y : Nat → Nat → Nat
#reduce five 4 5 -- 9

6.

def six :=
  Expr.lam `x (Expr.const `String [])
  (Lean.mkAppN (Expr.const `String.append []) #[Lean.mkStrLit "Hello, ", Expr.bvar 0])
  BinderInfo.default

elab "six" : term => return six
#check six        -- fun x => String.append "Hello, " x : String → String
#eval six "world" -- "Hello, world"

7.

def seven : Expr :=
  Expr.forallE `x (Expr.sort Lean.Level.zero)
  (Expr.app (Expr.app (Expr.const `And []) (Expr.bvar 0)) (Expr.bvar 0))
  BinderInfo.default

elab "seven" : term => return seven
#check seven  -- ∀ (x : Prop), x ∧ x : Prop
#reduce seven -- ∀ (x : Prop), x ∧ x

8.

def eight : Expr :=
  Expr.forallE `notUsed
  (Expr.const `Nat []) (Expr.const `String [])
  BinderInfo.default

elab "eight" : term => return eight
#check eight  -- Nat → String : Type
#reduce eight -- Nat → String

9.

def nine : Expr :=
  Expr.lam `p (Expr.sort Lean.Level.zero)
  (
    Expr.lam `hP (Expr.bvar 0)
    (Expr.bvar 0)
    BinderInfo.default
  )
  BinderInfo.default

elab "nine" : term => return nine
#check nine  -- fun p hP => hP : ∀ (p : Prop), p → p
#reduce nine -- fun p hP => hP

10.

def ten : Expr :=
  Expr.sort (Nat.toLevel 7)

elab "ten" : term => return ten
#check ten  -- Type 6 : Type 7
#reduce ten -- Type 6

import Lean
open Lean Meta

`MetaM`: Solutions

1.

#eval show MetaM Unit from do
  let hi ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `hi)
  IO.println s!"value in hi: {← instantiateMVars hi}" -- ?_uniq.1

  hi.mvarId!.assign (Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero []))
  IO.println s!"value in hi: {← instantiateMVars hi}" -- Nat.succ Nat.zero

2.

-- It would output the same expression we gave it - there were no metavariables to instantiate.
#eval show MetaM Unit from do
  let instantiatedExpr ← instantiateMVars (Expr.lam `x (Expr.const `Nat []) (Expr.bvar 0) BinderInfo.default)
  IO.println instantiatedExpr -- fun (x : Nat) => x

3.

#eval show MetaM Unit from do
  let oneExpr := Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero [])
  let twoExpr := Expr.app (Expr.const `Nat.succ []) oneExpr

  -- Create `mvar1` with type `Nat`
  let mvar1 ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `mvar1)
  -- Create `mvar2` with type `Nat`
  let mvar2 ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `mvar2)
  -- Create `mvar3` with type `Nat`
  let mvar3 ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `mvar3)

  -- Assign `mvar1` to `2 + ?mvar2 + ?mvar3`
  mvar1.mvarId!.assign (Lean.mkAppN (Expr.const `Nat.add []) #[(Lean.mkAppN (Expr.const `Nat.add []) #[twoExpr, mvar2]), mvar3])

  -- Assign `mvar3` to `1`
  mvar3.mvarId!.assign oneExpr

  -- Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1`
  let instantiatedMvar1 ← instantiateMVars mvar1
  IO.println instantiatedMvar1 -- Nat.add (Nat.add 2 ?_uniq.2) 1

4.

elab "explore" : tactic => do
  let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
  let metavarDecl : MetavarDecl ← mvarId.getDecl

  IO.println "Our metavariable"
  -- [anonymous] : 2 = 2
  IO.println s!"\n{metavarDecl.userName} : {metavarDecl.type}"

  IO.println "\nAll of its local declarations"
  let localContext : LocalContext := metavarDecl.lctx
  for (localDecl : LocalDecl) in localContext do
    if localDecl.isImplementationDetail then
      -- (implementation detail) red : 1 = 1 → 2 = 2 → 2 = 2
      IO.println s!"\n(implementation detail) {localDecl.userName} : {localDecl.type}"
    else
      -- hA : 1 = 1
      -- hB : 2 = 2
      IO.println s!"\n{localDecl.userName} : {localDecl.type}"

theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
  explore
  sorry

5.

-- The type of our metavariable `2 + 2`. We want to find a `localDecl` that has the same type, and `assign` our metavariable to that `localDecl`.
elab "solve" : tactic => do
  let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
  let metavarDecl : MetavarDecl ← mvarId.getDecl

  let localContext : LocalContext := metavarDecl.lctx
  for (localDecl : LocalDecl) in localContext do
    if ← Lean.Meta.isDefEq localDecl.type metavarDecl.type then
      mvarId.assign localDecl.toExpr

theorem redSolved (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
  solve

6.

def sixA : Bool → Bool := fun x => x
-- .lam `x (.const `Bool []) (.bvar 0) (Lean.BinderInfo.default)
#eval Lean.Meta.reduce (Expr.const `sixA [])

def sixB : Bool := (fun x => x) ((true && false) || true)
-- .const `Bool.true []
#eval Lean.Meta.reduce (Expr.const `sixB [])

def sixC : Nat := 800 + 2
-- .lit (Lean.Literal.natVal 802)
#eval Lean.Meta.reduce (Expr.const `sixC [])

7.

#eval show MetaM Unit from do
  let litExpr := Expr.lit (Lean.Literal.natVal 1)
  let standardExpr := Expr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero [])

  let isEqual ← Lean.Meta.isDefEq litExpr standardExpr
  IO.println isEqual -- true

8.

-- a) `5 =?= (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))`
-- Definitionally equal.
def expr2 := (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))
#eval show MetaM Unit from do
  let expr1 := Lean.mkNatLit 5
  let expr2 := Expr.const `expr2 []
  let isEqual ← Lean.Meta.isDefEq expr1 expr2
  IO.println isEqual -- true

-- b) `2 + 1 =?= 1 + 2`
-- Definitionally equal.
#eval show MetaM Unit from do
  let expr1 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 2, Lean.mkNatLit 1]
  let expr2 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 1, Lean.mkNatLit 2]
  let isEqual ← Lean.Meta.isDefEq expr1 expr2
  IO.println isEqual -- true

-- c) `?a =?= 2`, where `?a` has a type `String`
-- Not definitionally equal.
#eval show MetaM Unit from do
  let expr1 ← Lean.Meta.mkFreshExprMVar (Expr.const `String []) (userName := `expr1)
  let expr2 := Lean.mkNatLit 2
  let isEqual ← Lean.Meta.isDefEq expr1 expr2
  IO.println isEqual -- false

-- d) `?a + Int =?= "hi" + ?b`, where `?a` and `?b` don't have a type
-- Definitionally equal.
-- `?a` is assigned to `"hi"`, `?b` is assigned to `Int`.
#eval show MetaM Unit from do
  let a ← Lean.Meta.mkFreshExprMVar Option.none (userName := `a)
  let b ← Lean.Meta.mkFreshExprMVar Option.none (userName := `b)
  let expr1 := Lean.mkAppN (Expr.const `Nat.add []) #[a, Expr.const `Int []]
  let expr2 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkStrLit "hi", b]
  let isEqual ← Lean.Meta.isDefEq expr1 expr2
  IO.println isEqual -- true

  IO.println s!"a: {← instantiateMVars a}"
  IO.println s!"b: {← instantiateMVars b}"

-- e) `2 + ?a =?= 3`
-- Not definitionally equal.
#eval show MetaM Unit from do
  let a ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `a)
  let expr1 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 2, a]
  let expr2 := Lean.mkNatLit 3
  let isEqual ← Lean.Meta.isDefEq expr1 expr2
  IO.println isEqual -- false

-- f) `2 + ?a =?= 2 + 1`
-- Definitionally equal.
-- `?a` is assigned to `1`.
#eval show MetaM Unit from do
  let a ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `a)
  let expr1 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 2, a]
  let expr2 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 2, Lean.mkNatLit 1]
  let isEqual ← Lean.Meta.isDefEq expr1 expr2
  IO.println isEqual -- true

  IO.println s!"a: {← instantiateMVars a}"

9.

@[reducible] def reducibleDef     : Nat := 1 -- same as `abbrev`
@[instance] def instanceDef       : Nat := 2 -- same as `instance`
def defaultDef                    : Nat := 3
@[irreducible] def irreducibleDef : Nat := 4

@[reducible] def sum := [reducibleDef, instanceDef, defaultDef, irreducibleDef]

#eval show MetaM Unit from do
  let constantExpr := Expr.const `sum []

  Meta.withTransparency Meta.TransparencyMode.reducible do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- [1, instanceDef, defaultDef, irreducibleDef]

  Meta.withTransparency Meta.TransparencyMode.instances do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- [1, 2, defaultDef, irreducibleDef]

  Meta.withTransparency Meta.TransparencyMode.default do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- [1, 2, 3, irreducibleDef]

  Meta.withTransparency Meta.TransparencyMode.all do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- [1, 2, 3, 4]

  -- Note: if we don't set the transparency mode, we get a pretty strong `TransparencyMode.default`.
  let reducedExpr ← Meta.reduce constantExpr
  dbg_trace (← ppExpr reducedExpr) -- [1, 2, 3, irreducibleDef]

10.

-- Non-idiomatic: we can only use `Lean.mkAppN`.
def tenA : MetaM Expr := do
  let body := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 1, Expr.bvar 0]
  return Expr.lam `x (Expr.const `Nat []) body BinderInfo.default

-- Idiomatic: we can use both `Lean.mkAppN` and `Lean.Meta.mkAppM`.
def tenB : MetaM Expr := do
  Lean.Meta.withLocalDecl `x .default (Expr.const `Nat []) (fun x => do
    -- let body := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 1, x]
    let body ← Lean.Meta.mkAppM `Nat.add #[Lean.mkNatLit 1, x]
    Lean.Meta.mkLambdaFVars #[x] body
  )

#eval show MetaM _ from do
  ppExpr (← tenA) -- fun x => Nat.add 1 x
#eval show MetaM _ from do
  ppExpr (← tenB) -- fun x => Nat.add 1 x

11.

def eleven : MetaM Expr :=
  return Expr.forallE `yellow (Expr.const `Nat []) (Expr.bvar 0) BinderInfo.default

#eval show MetaM _ from do
  dbg_trace (← eleven) -- forall (yellow : Nat), yellow

12.

-- Non-idiomatic: we can only use `Lean.mkApp3`.
def twelveA : MetaM Expr := do
  let nPlusOne := Expr.app (Expr.app (Expr.const `Nat.add []) (Expr.bvar 0)) (Lean.mkNatLit 1)
  let forAllBody := Lean.mkApp3 (Expr.const ``Eq []) (Expr.const `Nat []) (Expr.bvar 0) nPlusOne
  let forAll := Expr.forallE `n (Expr.const `Nat []) forAllBody BinderInfo.default
  return forAll

-- Idiomatic: we can use both `Lean.mkApp3` and `Lean.Meta.mkEq`.
def twelveB : MetaM Expr := do
  withLocalDecl `n BinderInfo.default (Expr.const `Nat []) (fun x => do
    let nPlusOne := Expr.app (Expr.app (Expr.const `Nat.add []) x) (Lean.mkNatLit 1)
    -- let forAllBody := Lean.mkApp3 (Expr.const ``Eq []) (Expr.const `Nat []) x nPlusOne
    let forAllBody ← Lean.Meta.mkEq x nPlusOne
    let forAll := mkForallFVars #[x] forAllBody
    forAll
  )

#eval show MetaM _ from do
  ppExpr (← twelveA) -- (n : Nat) → Eq Nat n (Nat.add n 1)

#eval show MetaM _ from do
  ppExpr (← twelveB) -- ∀ (n : Nat), n = Nat.add n 1

13.

def thirteen : MetaM Expr := do
  withLocalDecl `f BinderInfo.default (Expr.forallE `a (Expr.const `Nat []) (Expr.const `Nat []) .default) (fun y => do
    let lamBody ← withLocalDecl `n BinderInfo.default (Expr.const `Nat []) (fun x => do
      let fn := Expr.app y x
      let fnPlusOne := Expr.app y (Expr.app (Expr.app (Expr.const `Nat.add []) (x)) (Lean.mkNatLit 1))
      let forAllBody := mkApp3 (mkConst ``Eq []) (Expr.const `Nat []) fn fnPlusOne
      let forAll := mkForallFVars #[x] forAllBody
      forAll
    )
    let lam := mkLambdaFVars #[y] lamBody
    lam
  )

#eval show MetaM _ from do
  ppExpr (← thirteen) -- fun f => (n : Nat) → Eq Nat (f n) (f (Nat.add n 1))

14.

#eval show Lean.Elab.Term.TermElabM _ from do
  let stx : Syntax ← `(∀ (a : Prop) (b : Prop), a ∨ b → b → a ∧ a)
  let expr ← Elab.Term.elabTermAndSynthesize stx none

  let (_, _, conclusion) ← forallMetaTelescope expr
  dbg_trace conclusion -- And ?_uniq.10 ?_uniq.10

  let (_, _, conclusion) ← forallMetaBoundedTelescope expr 2
  dbg_trace conclusion -- (Or ?_uniq.14 ?_uniq.15) -> ?_uniq.15 -> (And ?_uniq.14 ?_uniq.14)

  let (_, _, conclusion) ← lambdaMetaTelescope expr
  dbg_trace conclusion -- forall (a.1 : Prop) (b.1 : Prop), (Or a.1 b.1) -> b.1 -> (And a.1 a.1)

15.

#eval show MetaM Unit from do
  let a ← Lean.Meta.mkFreshExprMVar (Expr.const `String []) (userName := `a)
  let b ← Lean.Meta.mkFreshExprMVar (Expr.sort (Nat.toLevel 1)) (userName := `b)
  -- ?a + Int
  let c := Lean.mkAppN (Expr.const `Nat.add []) #[a, Expr.const `Int []]
  -- "hi" + ?b
  let d := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkStrLit "hi", b]

  IO.println s!"value in c: {← instantiateMVars c}" -- Nat.add ?_uniq.1 Int
  IO.println s!"value in d: {← instantiateMVars d}" -- Nat.add String ?_uniq.2

  let state : SavedState ← saveState
  IO.println "\nSaved state\n"

  if ← Lean.Meta.isDefEq c d then
    IO.println true
    IO.println s!"value in c: {← instantiateMVars c}"
    IO.println s!"value in d: {← instantiateMVars d}"

  restoreState state
  IO.println "\nRestored state\n"

  IO.println s!"value in c: {← instantiateMVars c}"
  IO.println s!"value in d: {← instantiateMVars d}"

import Lean
import Lean.Parser.Syntax
import Std.Util.ExtendedBinder

open Lean Elab Command Term

`Syntax`: Solutions

1.

namespace a
  scoped notation:71 lhs:50 " 💀 " rhs:72 => lhs - rhs
end a

namespace b
  set_option quotPrecheck false
  scoped infixl:71 " 💀 " => fun lhs rhs => lhs - rhs
end b

namespace c
  scoped syntax:71 term:50 " 💀 " term:72 : term
  scoped macro_rules | `($l:term 💀 $r:term) => `($l - $r)
end c

open a
#eval 5 * 8 💀 4 -- 20
#eval 8 💀 6 💀 1 -- 1

2.

syntax "good morning" : term
syntax "hello" : command
syntax "yellow" : tactic

-- Note: the following are highlighted in red, however that's just because we haven't implemented the semantics ("elaboration function") yet - the syntax parsing stage works.

#check_failure good morning -- the syntax parsing stage works

/-- error: elaboration function for 'commandHello' has not been implemented -/
hello -- the syntax parsing stage works

/-- error: tactic 'tacticYellow' has not been implemented -/
example : 2 + 2 = 4 := by
  yellow -- the syntax parsing stage works

#check_failure yellow -- error: `unknown identifier 'yellow'`

3.

syntax (name := colors) (("blue"+) <|> ("red"+)) num : command

@[command_elab colors]
def elabColors : CommandElab := fun stx => Lean.logInfo "success!"

blue blue 443
red red red 4

4.

syntax (name := help) "#better_help" "option" (ident)? : command

@[command_elab help]
def elabHelp : CommandElab := fun stx => Lean.logInfo "success!"

#better_help option
#better_help option pp.r
#better_help option some.other.name

5.

-- Note: std4 has to be in dependencies of your project for this to work.
syntax (name := bigsumin) "∑ " Std.ExtendedBinder.extBinder "in " term "," term : term

@[term_elab bigsumin]
def elabSum : TermElab := fun stx tp =>
  return mkNatLit 666

#eval ∑ x in { 1, 2, 3 }, x^2

def hi := (∑ x in { "apple", "banana", "cherry" }, x.length) + 1
#eval hi

import Lean
open Lean Elab Command Term Meta

Elaboration: Solutions

1.

elab n:term "♥" a:"♥"? b:"♥"? : term => do
  let nExpr : Expr ← elabTermEnsuringType n (mkConst `Nat)
  if let some a := a then
    if let some b := b then
      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
    else
      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
  else
    return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)

#eval 7 ♥ -- 8
#eval 7 ♥♥ -- 9
#eval 7 ♥♥♥ -- 10

2.

-- a) using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`
syntax (name := aliasA) (docComment)? "aliasA " ident " ← " ident* : command

@[command_elab «aliasA»]
def elabOurAlias : CommandElab := λ stx =>
  match stx with
  | `(aliasA $x:ident ← $ys:ident*) =>
    for y in ys do
      Lean.logInfo y
  | _ =>
    throwUnsupportedSyntax

aliasA hi.hello ← d.d w.w nnn

-- b) using `syntax` + `elab_rules`.
syntax (name := aliasB) (docComment)? "aliasB " ident " ← " ident* : command

elab_rules : command
  | `(command | aliasB $m:ident ← $ys:ident*) =>
    for y in ys do
      Lean.logInfo y

aliasB hi.hello ← d.d w.w nnn

-- c) using `elab`
elab "aliasC " x:ident " ← " ys:ident* : command =>
  for y in ys do
    Lean.logInfo y

aliasC hi.hello ← d.d w.w nnn

3.

open Parser.Tactic

-- a) using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.
syntax (name := nthRewriteA) "nth_rewriteA " (config)? num rwRuleSeq (ppSpace location)? : tactic

@[tactic nthRewriteA] def elabNthRewrite : Lean.Elab.Tactic.Tactic := fun stx => do
  match stx with
  | `(tactic| nth_rewriteA $[$cfg]? $n $rules $_loc) =>
    Lean.logInfo "rewrite location!"
  | `(tactic| nth_rewriteA $[$cfg]? $n $rules) =>
    Lean.logInfo "rewrite target!"
  | _ =>
    throwUnsupportedSyntax

-- b) using `syntax` + `elab_rules`.
syntax (name := nthRewriteB) "nth_rewriteB " (config)? num rwRuleSeq (ppSpace location)? : tactic

elab_rules (kind := nthRewriteB) : tactic
  | `(tactic| nth_rewriteB $[$cfg]? $n $rules $_loc) =>
    Lean.logInfo "rewrite location!"
  | `(tactic| nth_rewriteB $[$cfg]? $n $rules) =>
    Lean.logInfo "rewrite target!"

-- c) using `elab`.
elab "nth_rewriteC " (config)? num rwRuleSeq loc:(ppSpace location)? : tactic =>
  if let some loc := loc then
    Lean.logInfo "rewrite location!"
  else
    Lean.logInfo "rewrite target!"

example : 2 + 2 = 4 := by
  nth_rewriteC 2 [← add_zero] at h
  nth_rewriteC 2 [← add_zero]
  sorry

import Lean.Elab.Tactic
open Lean Elab Tactic Meta

1.

elab "step_1" : tactic => do
  let mvarId ← getMainGoal
  let goalType ← getMainTarget

  let Expr.app (Expr.app (Expr.const `Iff _) a) b := goalType | throwError "Goal type is not of the form `a ↔ b`"

  -- 1. Create new `_`s with appropriate types.
  let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red")
  let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue") 

  -- 2. Assign the main goal to the expression `Iff.intro _ _`.
  mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2])

  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }

elab "step_2" : tactic => do
  let some redMvarId ← (← get).goals.findM? (fun mvarId => do
    return (← mvarId.getDecl).userName == `red
  ) | throwError "No mvar with username `red`"
  let some blueMvarId ← (← get).goals.findM? (fun mvarId => do
    return (← mvarId.getDecl).userName == `blue
  ) | throwError "No mvar with username `blue`"

  ---- HANDLE `red` goal
  let Expr.forallE _ redFrom redTo _ := (← redMvarId.getDecl).type | throwError "Goal type is not of the form `a → b`"
  let handyRedMvarId ← withLocalDecl `hA BinderInfo.default redFrom (fun fvar => do
    -- 1. Create new `_`s with appropriate types.
    let mvarId1 ← mkFreshExprMVar redTo MetavarKind.syntheticOpaque `red
    -- 2. Assign the main goal to the expression `fun hA => _`.
    redMvarId.assign (← mkLambdaFVars #[fvar] mvarId1)
    -- just a handy way to return a handyRedMvarId for the next code
    return mvarId1.mvarId!
  )
  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [handyRedMvarId, blueMvarId] }

  ---- HANDLE `blue` goal
  let Expr.forallE _ blueFrom _ _ := (← blueMvarId.getDecl).type | throwError "Goal type is not of the form `a → b`"
  -- 1. Create new `_`s with appropriate types.
  -- None needed!
  -- 2. Assign the main goal to the expression `fun hB : q ∧ p => (And.intro hB.right hB.left)`.
  Lean.Meta.withLocalDecl `hB .default blueFrom (fun hB => do
    let body ← Lean.Meta.mkAppM `And.intro #[← Lean.Meta.mkAppM `And.right #[hB], ← Lean.Meta.mkAppM `And.left #[hB]]
    blueMvarId.assign (← Lean.Meta.mkLambdaFVars #[hB] body)
  )
  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [handyRedMvarId] }

elab "step_3" : tactic => do
  let mvarId ← getMainGoal
  let goalType ← getMainTarget
  let mainDecl ← mvarId.getDecl

  let Expr.app (Expr.app (Expr.const `And _) q) p := goalType | throwError "Goal type is not of the form `And q p`"

  -- 1. Create new `_`s with appropriate types.
  let mvarId1 ← mkFreshExprMVarAt mainDecl.lctx mainDecl.localInstances q (userName := "red1")
  let mvarId2 ← mkFreshExprMVarAt mainDecl.lctx mainDecl.localInstances p (userName := "red2")

  -- 2. Assign the main goal to the expression `And.intro _ _`.
  mvarId.assign (← mkAppM `And.intro #[mvarId1, mvarId2])

  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }

elab "step_4" : tactic => do
  let some red1MvarId ← (← get).goals.findM? (fun mvarId => do
    return (← mvarId.getDecl).userName == `red1
  ) | throwError "No mvar with username `red1`"
  let some red2MvarId ← (← get).goals.findM? (fun mvarId => do
    return (← mvarId.getDecl).userName == `red2
  ) | throwError "No mvar with username `red2`"

  ---- HANDLE `red1` goal
  -- 1. Create new `_`s with appropriate types.
  -- None needed!
  -- 2. Assign the main goal to the expression `hA.right`.
  let some hA := (← red1MvarId.getDecl).lctx.findFromUserName? `hA | throwError "No hypothesis with name `hA` (in goal `red1`)"
  red1MvarId.withContext do
    red1MvarId.assign (← mkAppM `And.right #[hA.toExpr])
  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [red2MvarId] }

  ---- HANDLE `red2` goal
  -- 1. Create new `_`s with appropriate types.
  -- None needed!
  -- 2. Assign the main goal to the expression `hA.left`.
  let some hA := (← red2MvarId.getDecl).lctx.findFromUserName? `hA | throwError "No hypothesis with name `hA` (in goal `red2`)"
  red2MvarId.withContext do
    red2MvarId.assign (← mkAppM `And.left #[hA.toExpr])
  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [] }

theorem gradual (p q : Prop) : p ∧ q ↔ q ∧ p := by
  step_1
  step_2
  step_3
  step_4

2.

elab "forker_a" : tactic => do
  liftMetaTactic fun mvarId => do
    let (Expr.app (Expr.app (Expr.const `And _) p) q) ← mvarId.getType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")

    let mvarIdP ← mkFreshExprMVar p (userName := "red")
    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")

    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
    mvarId.assign proofTerm

    return [mvarIdP.mvarId!, mvarIdQ.mvarId!]

elab "forker_b" : tactic => do
  let mvarId ← getMainGoal
  let goalType ← getMainTarget

  let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")

  mvarId.withContext do
    let mvarIdP ← mkFreshExprMVar p (userName := "red")
    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")

    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
    mvarId.assign proofTerm

    setGoals ([mvarIdP.mvarId!, mvarIdQ.mvarId!] ++ (← getGoals).drop 1)

elab "forker_c" : tactic => do
  let mvarId ← getMainGoal
  let goalType ← getMainTarget

  let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")

  mvarId.withContext do
    let mvarIdP ← mkFreshExprMVar p (userName := "red")
    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")

    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
    mvarId.assign proofTerm

    replaceMainGoal [mvarIdP.mvarId!, mvarIdQ.mvarId!]

example (A B C : Prop) : A → B → C → (A ∧ B) ∧ C := by
  intro hA hB hC
  forker_a
  forker_a
  assumption
  assumption
  assumption

3.

elab "introductor_a" : tactic => do
  withMainContext do
    liftMetaTactic fun mvarId => do
      let (_, mvarIdNew) ← mvarId.introN 2
      return [mvarIdNew]

elab "introductor_b" : tactic => do
  withMainContext do
    liftMetaTactic fun mvarId => do
      let (_, mvarIdNew) ← mvarId.intro1P
      return [mvarIdNew]

elab "introductor_c" : tactic => do
  withMainContext do
    liftMetaTactic fun mvarId => do
      let (_, mvarIdNew) ← mvarId.intro `wow
      return [mvarIdNew]

-- So:
-- `intro`   - **intro**, specify the name manually
-- `intro1`  - **intro**, make the name inacessible
-- `intro1P` - **intro**, preserve the original name
-- `introN`  - **intro many**, specify the names manually
-- `introNP` - **intro many**, preserve the original names

example (a b c : Nat) : (ab: a = b) → (bc: b = c) → (a = c) := by
  introductor_a
  -- introductor_b
  -- introductor_c
  sorry

Metaprogramming in Lean 4 日本語訳