はじめに
本書のゴール
本書はLean4におけるメタプログラミングについて十分な知識を得ることを目的にしています：
- 読者独自によるメタヘルパーを作るところから始めます（
∑のような新しいLeanの記法の定義や、#checkのような新しいLeanコマンドの作成、useのようなタクティクの記述など）。 - Lean4のコアやMathlib4にあるようなメタプログラミングAPIを読み、議論します。
決してLean4のメタプログラミングAPI全体を網羅的に説明するつもりはありません。また、Lean4のモナドによるプログラミングについての話題も扱いません。しかし、本書で提供する例が十分にシンプルであり、モナドプログラミングについての超深い理解がなくとも読者がフォローして理解できることを望みます。このテーマについては Functional Programming in Lean という本がお勧めです。 1
本書の構成
本書はDSLとタクティクを扱う章に十分な文脈を構築できるように構成されています。各章の前提条件を遡ると、依存関係は以下のような構造になっています：
- 「タクティク」は「マクロ」と「エラボレーション」上に構築されます。
- 「DSL」は「エラボレーション」上に構築されます。
- 「マクロ」は「
Syntax」上に構築されます。 - 「エラボレーション」は「
Syntax」と「MetaM」上に構築されます。 - 「
MetaM」は「式」上に構築されます。
タクティクの章の後には、重要な概念と帰納の総括を含むチートシートがありまず。そしてその後には付録としてLean4のメタプログラミングの応用例の章を用意しています。ほとのどの章の章末に演習問題があり、本の最後にはそれらの解答が載っています。
本章の残りはメタプログラミングとは何かについてやさしく紹介し、本書で扱う内容の前菜となるような小さな例をいくつか提供します。
注意：それぞれのコード片は自己完結していません。各章の初めから少しずつ実行/読むことを想定しています。
メタとはどういう意味か？
Python・C・Java・Scalaなどほとんどのプログラミング言語でコードを書くとき、通常はあらかじめ定義された構文に従わなければなりません。そうしなければコンパイラやインタプリタは我々の言わんとしていることを理解できないでしょう。Leanにおいては帰納型の定義、関数の実装、定理の証明などがこれにあたります。これを受けてコンパイラはコードをパースし、AST（抽象構文木）を構築し、その構文ノードを言語カーネルが処理できる項に精緻化しなければなりません。このようなコンパイラが行う活動は メタレベル で行われると表現され、これが本書を通じて学んでいくものです。また、言語構文の一般的な使用は オブジェクトレベル で行われると言います。
ほとんどのシステムでは、メタレベルの活動はコードの記述で使う言語とは別の言語で行われます。Isabelleでは、メタレベル言語はMLとScalaです。CoqではOcamlです。AgdaではHaskellです。Lean4では、C++で書かれたいくつかのコンポーネント以外、メタコードのほとんどはLean自身で記述されます。
しかし、Leanのステキな点は、オブジェクトレベルで活動するのとまったく同じ開発環境でカスタム構文ノードを定義し、それを精緻化するメタレベルのルーチンを実装できることです。例えば、ある型の項をインスタンス化し、同じファイル内ですぐに使用するための記法を書くことができます！この概念は一般的に リフレクション と呼ばれています。それゆえLeanでは、メタレベルはオブジェクトレベルに リフレクション されると言うことができます。
RubyやPython、Javascriptなどの言語でメタプログラミングをしたことがある人は、おそらく定義済みのメタプログラミング用のメソッドを利用してその場で何かを定義するという形をとったことがあるでしょう。例えば、Rubyでは Class.new と define_method を使ってプログラムの実行中に新しいクラスと新しいメソッドを定義することができます。
Leanでは通常、新しいコマンドやタクティクを「その場で」定義する必要はありませんが、Leanのメタプログラミングでも理屈上似たようなことが可能であり、同様に簡単に利用できます。例えば、シンプルなワンライナー elab "#help" : command => do ...normal Lean code... を使って新しいLeanのコマンドを定義できます。
しかし、Leanでは特にタクティクを書く場合などでは、「通常のLeanコード」を使うのではなく、LeanのCST（解析木、Leanでは Syntax 型）やAST（抽象構文木、Leanでは Expr 型）を直接操作したいと思うことがよくあります。したがって、Leanのメタプログラミングをマスターすることはより難しいものになります。本書の大部分はこれらの型とその操作方法を学ぶことに費やされます。
メタプログラミングの例
ここで、Leanのメタプログラミングの例をいくつか紹介し、Leanにおけるメタプログラミングがどのようなものであり、それによって何が達成できるかを味わってもらいます。これらの例は単なる説明のためのものであり、今のところは詳細が理解できなくても心配しないでください。
記法の導入（新しい構文の定義）
例えば数学（の一分野）に適した新しい記法を導入したい場合がよくあります。例えば、数学では自然数に 2 を加える関数を x : Nat ↦ x + 2 と書いたり、定義域が自然数であると推測できる場合は単に x ↦ x + 2 と書いたりします。これに対応するLeanの定義 fun x : Nat => x + 2 と fun x => x + 2 は => を使っていますが、これは数学では 含意 を意味するので、混乱する人もいるかもしれません。
macro を使って記法を導入し、Leanの構文（またはそれ以前に定義した構文）に変換することができます。ここでは、関数の ↦ 記法を導入します。
import Lean
macro x:ident ":" t:term " ↦ " y:term : term => do
`(fun $x : $t => $y)
#eval (x : Nat ↦ x + 2) 2 -- 4
macro x:ident " ↦ " y:term : term => do
`(fun $x => $y)
#eval (x ↦ x + 2) 2 -- 4
コマンドの構築
与えられた項が特定の型であるかどうかを示すヘルパーコマンド #assertType を作りたいとします。これの使い方は次のようになります：
#assertType <term> : <type>
このコードを見てみましょう：
elab "#assertType " termStx:term " : " typeStx:term : command =>
open Lean Lean.Elab Command Term in
liftTermElabM
try
let tp ← elabType typeStx
discard $ elabTermEnsuringType termStx tp
synthesizeSyntheticMVarsNoPostponing
logInfo "success"
catch | _ => throwError "failure"
/-- info: success -/
#assertType 5 : Nat
/-- error: failure -/
#assertType [] : Nat
まず elab を使って command 構文を定義しました。コンパイラによってパースされると、計算が開始します。
この時点で、コードは CommandElabM モナド中で実行されるはずです。ここで TermElabM モナドにアクセスするために liftTermElabM を使用します。TermElabM モナドでは、elabType と elabTermEnsuringType を使って構文ノード typeStx と termStx から式を組み立てることができます。
まず、期待される型 tp : Expr を精緻化し、次にそれを使って項の式を作成します。この項は tp 型でなければならず、それ以外では例外が投げられます。次に、ここでは問題にならないため結果の項の式を捨てています。なぜなら elabTermEnsuringType はサニティチェックとして呼ばれているからです。
ここでLeanにメタ変数を精緻化するよう強制する synthesizeSyntheticMVarsNoPostponing も追加しています。この行がなければ、#assertType [] : ?_ は succsess となってしまいます。
例外が投げられなければ、精緻化は成功したことになり、logInfo を使って「success」と出力することができます。もしその代わりに何らかのエラーが発生した場合、適切なメッセージを添えて throwError を使用します。
DSLとそのための構文の構築
古典的な文法、つまり加算、乗算、自然数、変数を含む算術式の文法をパースしてみましょう。式のデータをエンコードするためにAST（抽象構文木）を定義し、演算子 + と * を使って算術ASTを構築します。これがこれから解析するASTです：
inductive Arith : Type where
| add : Arith → Arith → Arith -- e + f
| mul : Arith → Arith → Arith -- e * f
| nat : Nat → Arith -- constant
| var : String → Arith -- variable
ここで、構文解析を行う文法を記述するために構文カテゴリを宣言します。ここで + と * の優先順位をコントロールするために、* 構文よりも + 構文に低い優先順位の重みを与えることで、乗算は加算よりも強く束縛する（数字が大きいほど束縛が強くなる）ことを示していることに注意してください。これにより、新しい構文を定義する際に 優先順位 を宣言することができます。
declare_syntax_cat arith
syntax num : arith -- nat for Arith.nat
syntax str : arith -- strings for Arith.var
syntax:50 arith:50 " + " arith:51 : arith -- Arith.add
syntax:60 arith:60 " * " arith:61 : arith -- Arith.mul
syntax " ( " arith " ) " : arith -- bracketed expressions
--# Auxiliary notation for translating `arith` into `term`
-- `arith` を `term` に変換するための補助記法
syntax " ⟪ " arith " ⟫ " : term
--# Our macro rules perform the "obvious" translation:
-- このマクロルールは「明白な」翻訳を行う
macro_rules
| `(⟪ $s:str ⟫) => `(Arith.var $s)
| `(⟪ $num:num ⟫) => `(Arith.nat $num)
| `(⟪ $x:arith + $y:arith ⟫) => `(Arith.add ⟪ $x ⟫ ⟪ $y ⟫)
| `(⟪ $x:arith * $y:arith ⟫) => `(Arith.mul ⟪ $x ⟫ ⟪ $y ⟫)
| `(⟪ ( $x ) ⟫) => `( ⟪ $x ⟫ )
#check ⟪ "x" * "y" ⟫
-- Arith.mul (Arith.var "x") (Arith.var "y") : Arith
#check ⟪ "x" + "y" ⟫
-- Arith.add (Arith.var "x") (Arith.var "y") : Arith
#check ⟪ "x" + 20 ⟫
-- Arith.add (Arith.var "x") (Arith.nat 20) : Arith
#check ⟪ "x" + "y" * "z" ⟫ -- precedence
-- Arith.add (Arith.var "x") (Arith.mul (Arith.var "y") (Arith.var "z")) : Arith
#check ⟪ "x" * "y" + "z" ⟫ -- precedence
-- Arith.add (Arith.mul (Arith.var "x") (Arith.var "y")) (Arith.var "z") : Arith
#check ⟪ ("x" + "y") * "z" ⟫ -- brackets
-- Arith.mul (Arith.add (Arith.var "x") (Arith.var "y")) (Arith.var "z")
自前のタクティクの記述
与えられた名前のコンテキストに新しい仮定を追加し、その証明の必要性を最後まで先送りするタクティクを作ってみましょう。Lean3の suffices タクティクと似ていますが、新しいゴールがゴールリストの一番下に来るようにした点が異なります。
これは suppose と呼ばれ、次のように使われます：
suppose <name> : <type>
それではコードを見てみましょう：
open Lean Meta Elab Tactic Term in
elab "suppose " n:ident " : " t:term : tactic => do
let n : Name := n.getId
let mvarId ← getMainGoal
mvarId.withContext do
let t ← elabType t
let p ← mkFreshExprMVar t MetavarKind.syntheticOpaque n
let (_, mvarIdNew) ← MVarId.intro1P $ ← mvarId.assert n t p
replaceMainGoal [p.mvarId!, mvarIdNew]
evalTactic $ ← `(tactic|rotate_left)
example : 0 + a = a := by
suppose add_comm : 0 + a = a + 0
rw [add_comm]; rfl -- closes the initial main goal
rw [Nat.zero_add]; rfl -- proves `add_comm`
まずメインゴールを mvarId に格納し、それを withMVarContext のパラメータとして使用することで、コンテキスト内の他の変数に依存する型でもエラボレーションが機能するようにしています。
今回は mkFreshExprMVar を使って t の証明のためのメタ変数式を作成し、それを intro1P と assert を使ってコンテキストに導入しています。
新しい仮定の証明をゴールとして要求するために、p.mvarId! を先頭に持つリストを渡して replaceMainGoal を呼び出します。そして rotate_left タクティクを使って最近追加された一番上のゴールを一番下に移動させます。
訳注：日本語訳は 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つが恒等になります。
一方で、本書では 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）。詳しくは メタ変数の種 1 を参照してください（通常はデフォルト値が正しいです）。1userName：新しいメタ変数のユーザが目にする名前。これはメタ変数がゴールに現れる際に表示されるものになります。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はメタ変数に割当を決して行いません。
- Natural：
式の構築
前の章では、式を構築するためにいくつかのプリミティブな関数を見ました：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 yisDefEqが成功すると、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 => xb)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 + 2c)?a =?= 2、ここで?aはString型 d)?a + Int =?= "hi" + ?b、ここで?aと?bは型を持ちません e)2 + ?a =?= 3f)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 ca LXOR (b LXOR c)
括弧内の引数は優先順位 10 の LXOR ルールによってパースされるため、これらはその外側の LXOR ルールにとっては優先順位 10 の引数として表示されます：
(a LXOR b):10 LXOR ca 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 4blue 7blue 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 をインストールする必要があります。
Macros
What is a macro
Macros in Lean are Syntax → MacroM Syntax functions. MacroM is the macro
monad which allows macros to have some static guarantees we will discuss in the
next section, you can mostly ignore it for now.
Macros are registered as handlers for a specific syntax declaration using the
macro attribute. The compiler will take care of applying these function
to the syntax for us before performing actual analysis of the input. This
means that the only thing we have to do is declare our syntax with a specific
name and bind a function of type Lean.Macro to it. Let's try to reproduce
the LXOR notation from the Syntax chapter:
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
That was quite easy! The Macro.throwUnsupported function can be used by a macro
to indicate that "it doesn't feel responsible for this syntax". In this case
it's merely used to fill a wildcard pattern that should never be reached anyways.
However we can in fact register multiple macros for the same syntax this way
if we desire, they will be tried one after another (the later registered ones have
higher priority) -- is "higher" correct?
until one throws either a real error using Macro.throwError or succeeds, that
is it does not Macro.throwUnsupported. Let's see this in action:
@[macro lxor] def lxorImpl2 : Macro
-- special case that changes behaviour of the case where the left and
-- right hand side are these specific identifiers
| `(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
This capability is obviously very powerful! It should not be used lightly and without careful thinking since it can introduce weird behaviour while writing code later on. The following example illustrates this weird behaviour:
#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
Without knowing exactly how this macro is implemented this behaviour will be very confusing to whoever might be debugging an issue based on this. The rule of thumb for when to use a macro vs. other mechanisms like elaboration is that as soon as you are building real logic like in the 2nd macro above, it should most likely not be a macro but an elaborator (explained in the elaboration chapter). This means ideally we want to use macros for simple syntax to syntax translations, that a human could easily write out themselves as well but is too lazy to.
Simplifying macro declaration
Now that we know the basics of what a macro is and how to register it we can take a look at slightly more automated ways to do this (in fact all of the ways about to be presented are implemented as macros themselves).
First things first there is macro_rules which basically desugars to
functions like the ones we wrote above, for example:
syntax:10 term:10 " RXOR " term:11 : term
macro_rules
| `($l:term RXOR $r:term) => `($l && !$r)
As you can see, it figures out lot's of things on its own for us:
- the name of the syntax declaration
- the
macroattribute registration - the
throwUnsupportedwildcard
apart from this it just works like a function that is using pattern matching syntax, we can in theory encode arbitrarily complex macro functions on the right hand side.
If this is still not short enough for you, there is a next step using the
macro 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
As you can see, macro is quite close to notation already:
- it performed syntax declaration for us
- it automatically wrote a
macro_rulesstyle function to match on it
The are of course differences as well:
notationis limited to thetermsyntax categorynotationcannot have arbitrary macro code on the right hand side
Syntax Quotations
The basics
So far we've handwaved the `(foo $bar) syntax to both create and
match on Syntax objects but it's time for a full explanation since
it will be essential to all non trivial things that are syntax related.
First things first we call the `() syntax a Syntax quotation.
When we plug variables into a syntax quotation like this: `($x)
we call the $x part an anti-quotation. When we insert x like this
it is required that x is of type TSyntax y where y is some Name
of a syntax category. The Lean compiler is actually smart enough to figure
the syntax categories that are allowed in this place out. Hence you might
sometimes see errors of the form:
application type mismatch
x.raw
argument
x
has type
TSyntax `a : Type
but is expected to have type
TSyntax `b : Type
If you are sure that your thing from the a syntax category can be
used as a b here you can declare a coercion of the form:
instance : Coe (TSyntax `a) (TSyntax `b) where
coe s := ⟨s.raw⟩
Which will allow Lean to perform the type cast automatically. If you
notice that your a can not be used in place of the b here congrats,
you just discovered a bug in your Syntax function. Similar to the Lean
compiler, you could also declare functions that are specific to certain
TSyntax variants. For example as we have seen in the syntax chapter
there exists the function:
#check TSyntax.getNat -- TSyntax.getNat : TSyntax numLitKind → Nat
Which is guaranteed to not panic because we know that the Syntax that
the function is receiving is a numeric literal and can thus naturally
be converted to a Nat.
If we use the antiquotation syntax in pattern matching it will, as discussed
in the syntax chapter, give us a variable x of type TSyntax y where
y is the Name of the syntax category that fits in the spot where we pattern matched.
If we wish to insert a literal $x into the Syntax for some reason,
for example macro creating macros, we can escape the anti quotation using: `($$x).
If we want to specify the syntax kind we wish x to be interpreted as
we can make this explicit using: `($x:term) where term can be
replaced with any other valid syntax category (e.g. command) or parser
(e.g. ident).
So far this is only a more formal explanation of the intuitive things we've already seen in the syntax chapter and up to now in this chapter, next we'll discuss some more advanced anti-quotations.
Advanced anti-quotations
For convenience we can also use anti-quotations in a way similar to
format strings: `($(mkIdent `c)) is the same as: let x := mkIdent `c; `($x).
Furthermore there are sometimes situations in which we are not working
with basic Syntax but Syntax wrapped in more complex datastructures,
most notably Array (TSyntax c) or TSepArray c s. Where TSepArray c s, is a
Syntax specific type, it is what we get if we pattern match on some
Syntax that users a separator s to separate things from the category c.
For example if we match using: $xs,*, xs will have type TSepArray c ",",.
With the special case of matching on no specific separator (i.e. whitespace):
$xs* in which we will receive an Array (TSyntax c).
If we are dealing with xs : Array (TSyntax c) and want to insert it into
a quotation we have two main ways to achieve this:
- Insert it using a separator, most commonly
,:`($xs,*). This is also the way to insert aTSepArray c ","" - Insert it point blank without a separator (TODO):
`()
For example:
-- syntactically cut away the first element of a tuple if possible
syntax "cut_tuple " "(" term ", " term,+ ")" : term
macro_rules
-- cutting away one element of a pair isn't possible, it would not result in a tuple
| `(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
The last thing for this section will be so called "anti-quotation splices".
There are two kinds of anti quotation splices, first the so called optional
ones. For example we might declare a syntax with an optional argument,
say our own let (in real projects this would most likely be a let
in some functional language we are writing a theory about):
syntax "mylet " ident (" : " term)? " := " term " in " term : term
There is this optional (" : " term)? argument involved which can let
the user define the type of the term to the left of it. With the methods
we know so far we'd have to write two macro_rules now, one for the case
with, one for the case without the optional argument. However the rest
of the syntactic translation works exactly the same with and without
the optional argument so what we can do using a splice here is to essentially
define both cases at once:
macro_rules
| `(mylet $x $[: $ty]? := $val in $body) => `(let $x $[: $ty]? := $val; $body)
The $[...]? part is the splice here, it basically says "if this part of
the syntax isn't there, just ignore the parts on the right hand side that
involve anti quotation variables involved here". So now we can run
this syntax both with and without type ascription:
#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
The second and last splice might remind readers of list comprehension
as seen for example in Python. We will demonstrate it using an implementation
of map as a macro:
-- run the function given at the end for each element of the list
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]
In this case the $[...],* part is the splice. On the match side it tries
to match the pattern we define inside of it repetitively (given the separator
we tell it to). However unlike regular separator matching it does not
give us an Array or SepArray, instead it allows us to write another
splice on the right hand side that gets evaluated for each time the
pattern we specified matched, with the specific values from the match
per iteration.
Hygiene issues and how to solve them
If you are familiar with macro systems in other languages like C you probably know about so called macro hygiene issues already. A hygiene issue is when a macro introduces an identifier that collides with an identifier from some syntax that it is including. For example:
-- Applying this macro produces a function that binds a new identifier `x`.
macro "const" e:term : term => `(fun x => $e)
-- But `x` can also be defined by a user
def x : Nat := 42
-- Which `x` should be used by the compiler in place of `$e`?
#eval (const x) 10 -- 42
Given the fact that macros perform only syntactic translations one might
expect the above eval to return 10 instead of 42: after all, the resulting
syntax should be (fun x => x) 10. While this was of course not the intention
of the author, this is what would happen in more primitive macro systems like
the one of C. So how does Lean avoid these hygiene issues? You can read
about this in detail in the excellent Beyond Notations
paper which discusses the idea and implementation in Lean in detail.
We will merely give an overview of the topic, since the details are not
that interesting for practical uses. The idea described in Beyond Notations
comes down to a concept called "macro scopes". Whenever a new macro
is invoked, a new macro scope (basically a unique number) is added to
a list of all the macro scopes that are active right now. When the current
macro introduces a new identifier what is actually getting added is an
identifier of the form:
<actual name>._@.(<module_name>.<scopes>)*.<module_name>._hyg.<scopes>
For example, if the module name is Init.Data.List.Basic, the name is
foo.bla, and macros scopes are [2, 5] we get:
foo.bla._@.Init.Data.List.Basic._hyg.2.5
Since macro scopes are unique numbers the list of macro scopes appended in the end of the name will always be unique across all macro invocations, hence macro hygiene issues like the ones above are not possible.
If you are wondering why there is more than just the macro scopes to this name generation, that is because we may have to combine scopes from different files/modules. The main module being processed is always the right most one. This situation may happen when we execute a macro generated in a file imported in the current file.
foo.bla._@.Init.Data.List.Basic.2.1.Init.Lean.Expr_hyg.4
The delimiter _hyg at the end is used just to improve performance of
the function Lean.Name.hasMacroScopes -- the format could also work without it.
This was a lot of technical details. You do not have to understand them
in order to use macros, if you want you can just keep in mind that Lean
will not allow name clashes like the one in the const example.
Note that this extends to all names that are introduced using syntax
quotations, that is if you write a macro that produces:
`(def foo := 1), the user will not be able to access foo
because the name will subject to hygiene. Luckily there is a way to
circumvent this. You can use mkIdent to generate a raw identifier,
for example: `(def $(mkIdent `foo) := 1). In this case it won't
be subject to hygiene and accessible to the user.
MonadQuotation and MonadRef
Based on this description of the hygiene mechanism one interesting question pops up, how do we know what the current list of macro scopes actually is? After all in the macro functions that were defined above there is never any explicit passing around of the scopes happening. As is quite common in functional programming, as soon as we start having some additional state that we need to bookkeep (like the macro scopes) this is done with a monad, this is the case here as well with a slight twist.
Instead of implementing this for only a single monad MacroM the general
concept of keeping track of macro scopes in monadic way is abstracted
away using a type class called MonadQuotation. This allows any other
monad to also easily provide this hygienic Syntax creation mechanism
by simply implementing this type class.
This is also the reason that while we are able to use pattern matching on syntax
with `(syntax) we cannot just create Syntax with the same
syntax in pure functions: there is no Monad implementing MonadQuotation
involved in order to keep track of the macro scopes.
Now let's take a brief look at the MonadQuotation type class:
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
Since MonadQuotation is based on MonadRef, let's take a look at MonadRef
first. The idea here is quite simple: MonadRef is meant to be seen as an extension
to the Monad typeclass which
- gives us a reference to a
Syntaxvalue withgetRef - can evaluate a certain monadic action
m αwith a new reference to aSyntaxusingwithRef
On it's own MonadRef isn't exactly interesting, but once it is combined with
MonadQuotation it makes sense.
As you can see MonadQuotation extends MonadRef and adds 3 new functions:
getCurrMacroScopewhich obtains the latestMacroScopethat was createdgetMainModulewhich (obviously) obtains the name of the main module, both of these are used to create these hygienic identifiers explained abovewithFreshMacroScopewhich will compute the next macro scope and run some computationm αthat performs syntax quotation with this new macro scope in order to avoid name clashes. While this is mostly meant to be used internally whenever a new macro invocation happens, it can sometimes make sense to use this in our own macros, for example when we are generating some syntax block repeatedly and want to avoid name clashes.
How MonadRef comes into play here is that Lean requires a way to indicate
errors at certain positions to the user. One thing that wasn't introduced
in the Syntax chapter is that values of type Syntax actually carry their
position in the file around as well. When an error is detected, it is usually
bound to a Syntax value which tells Lean where to indicate the error in the file.
What Lean will do when using withFreshMacroScope is to apply the position of
the result of getRef to each introduced symbol, which then results in better
error positions than not applying any position.
To see error positioning in action, we can write a little macro that makes use of it:
syntax "error_position" ident : term
macro_rules
| `(error_position all) => Macro.throwError "Ahhh"
-- the `%$tk` syntax gives us the Syntax of the thing before the %,
-- in this case `error_position`, giving it the name `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`
Obviously controlling the positions of errors in this way is quite important for a good user experience.
Mini project
As a final mini project for this section we will re-build the arithmetic DSL from the syntax chapter in a slightly more advanced way, using a macro this time so we can actually fully integrate it into the Lean syntax.
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
Again feel free to play around with it. If you want to build more complex
things, like expressions with variables, maybe consider building an inductive type
using macros instead. Once you got your arithmetic expression term
as an inductive, you could then write a function that takes some form of
variable assignment and evaluates the given expression for this
assignment. You could also try to embed arbitrary terms into your
arith language using some special syntax or whatever else comes to your mind.
More elaborate examples
Binders 2.0
As promised in the syntax chapter here is Binders 2.0. We'll start by reintroducing our theory of sets:
def Set (α : Type u) := α → Prop
def Set.mem (x : α) (X : Set α) : Prop := X x
-- Integrate into the already existing typeclass for membership notation
instance : Membership α (Set α) where
mem := Set.mem
def Set.empty : Set α := λ _ => False
-- the basic "all elements such that" function for the notation
def setOf {α : Type} (p : α → Prop) : Set α := p
The goal for this section will be to allow for both {x : X | p x}
and {x ∈ X, p x} notations. In principle there are two ways to do this:
- Define a syntax and macro for each way to bind a variable we might think of
- Define a syntax category of binders that we could reuse across other
binder constructs such as
ΣorΠas well and implement macros for the{ | }case
In this section we will use approach 2 because it is more easily reusable.
declare_syntax_cat binder_construct
syntax "{" binder_construct "|" term "}" : term
Now let's define the two binders constructs we are interested in:
syntax ident " : " term : binder_construct
syntax ident " ∈ " term : binder_construct
And finally the macros to expand our syntax:
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))
-- Old examples with better syntax:
#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]
-- New examples:
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
Reading further
If you want to know more about macros you can read:
- the API docs: TODO link
- the source code: the lower parts of Init.Prelude as you can see they are declared quite early in Lean because of their importance to building up syntax
- the aforementioned Beyond Notations paper
Elaboration
The elaborator is the component in charge of turning the user facing
Syntax into something with which the rest of the compiler can work.
Most of the time, this means translating Syntax into Exprs but
there are also other use cases such as #check or #eval. Hence the
elaborator is quite a large piece of code, it lives
here.
Command elaboration
A command is the highest level of Syntax, a Lean file is made
up of a list of commands. The most commonly used commands are declarations,
for example:
definductivestructure
but there are also other ones, most notably #check, #eval and friends.
All commands live in the command syntax category so in order to declare
custom commands, their syntax has to be registered in that category.
Giving meaning to commands
The next step is giving some semantics to the syntax. With commands, this is done by registering a so called command elaborator.
Command elaborators have type CommandElab which is an alias for:
Syntax → CommandElabM Unit. What they do, is take the Syntax that
represents whatever the user wants to call the command and produce some
sort of side effect on the CommandElabM monad, after all the return
value is always Unit. The CommandElabM monad has 4 main kinds of
side effects:
- Logging messages to the user via the
MonadextensionsMonadLogandAddMessageContext, like#check. This is done via functions that can be found inLean.Elab.Log, the most notable ones being:logInfo,logWarningandlogError. - Interacting with the
Environmentvia theMonadextensionMonadEnv. This is the place where all of the relevant information for the compiler is stored, all known declarations, their types, doc-strings, values etc. The current environment can be obtained viagetEnvand set viasetEnvonce it has been modified. Note that quite often wrappers aroundsetEnvlikeaddDeclare the correct way to add information to theEnvironment. - Performing
IO,CommandElabMis capable of running anyIOoperation. For example reading from files and based on their contents perform declarations. - Throwing errors, since it can run any kind of
IO, it is only natural that it can throw errors viathrowError.
Furthermore there are a bunch of other Monad extensions that are supported
by CommandElabM:
MonadRefandMonadQuotationforSyntaxquotations like in macrosMonadOptionsto interact with the options frameworkMonadTracefor debug trace information- TODO: There are a few others though I'm not sure whether they are relevant,
see the instance in
Lean.Elab.Command
Command elaboration
Now that we understand the type of command elaborators let's take a brief look at how the elaboration process actually works:
- Check whether any macros can be applied to the current
Syntax. If there is a macro that does apply and does not throw an error the resultingSyntaxis recursively elaborated as a command again. - If no macro can be applied, we search for all
CommandElabs that have been registered for theSyntaxKindof theSyntaxwe are elaborating, using thecommand_elabattribute. - All of these
CommandElabare then tried in order until one of them does not throw anunsupportedSyntaxException, Lean's way of indicating that the elaborator "feels responsible" for this specificSyntaxconstruct. Note that it can still throw a regular error to indicate to the user that something is wrong. If no responsible elaborator is found, then the command elaboration is aborted with anunexpected syntaxerror message.
As you can see the general idea behind the procedure is quite similar to ordinary macro expansion.
Making our own
Now that we know both what a CommandElab is and how they are used, we can
start looking into writing our own. The steps for this, as we learned above, are:
- Declaring the syntax
- Declaring the elaborator
- Registering the elaborator as responsible for the syntax via the
command_elabattribute.
Let's see how this is done:
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
You might think that this is a little boiler-platey and it turns out the Lean devs did as well so they added a macro for this!
elab "#mycommand2" : command =>
logInfo "Hello World"
#mycommand2 -- Hello World
Note that, due to the fact that command elaboration supports multiple registered elaborators for the same syntax, we can in fact overload syntax, if we want to.
@[command_elab mycommand1]
def myNewImpl : CommandElab := fun stx => do
logInfo "new!"
#mycommand1 -- new!
Furthermore it is also possible to only overload parts of syntax by
throwing an unsupportedSyntaxException in the cases we want the default
handler to deal with it or just letting the elab command handle it.
In the following example, we are not extending the original #check syntax,
but adding a new SyntaxKind for this specific syntax construct.
However, from the point of view of the user, the effect is basically the same.
elab "#check" "mycheck" : command => do
logInfo "Got ya!"
This is actually extending the original #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
Mini project
As a final mini project for this section let's build a command elaborator
that is actually useful. It will take a command and use the same mechanisms
as elabCommand (the entry point for command elaboration) to tell us
which macros or elaborators are relevant to the command we gave it.
We will not go through the effort of actually reimplementing elabCommand though
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: Maybe we should also add a mini project that demonstrates a
non # style command aka a declaration, although nothing comes to mind right now.
TODO: Define a conjecture declaration, similar to lemma/theorem, except that
it is automatically sorried. The sorry could be a custom one, to reflect that
the "conjecture" might be expected to be true.
Term elaboration
A term is a Syntax object that represents some sort of Expr.
Term elaborators are the ones that do the work for most of the code we write.
Most notably they elaborate all the values of things like definitions,
types (since these are also just Expr) etc.
All terms live in the term syntax category (which we have seen in action
in the macro chapter already). So, in order to declare custom terms, their
syntax needs to be registered in that category.
Giving meaning to terms
As with command elaboration, the next step is giving some semantics to the syntax. With terms, this is done by registering a so called term elaborator.
Term elaborators have type TermElab which is an alias for:
Syntax → Option Expr → TermElabM Expr. This type is already
quite different from command elaboration:
- As with command elaboration the
Syntaxis whatever the user used to create this term - The
Option Expris the expected type of the term, since this cannot always be known it is only anOptionargument - Unlike command elaboration, term elaboration is not only executed
because of its side effects -- the
TermElabM Exprreturn value does actually contain something of interest, namely, theExprthat represents theSyntaxobject.
TermElabM is basically an upgrade of CommandElabM in every regard:
it supports all the capabilities we mentioned above, plus two more.
The first one is quite simple: On top of running IO code it is also
capable of running MetaM code, so Exprs can be constructed nicely.
The second one is very specific to the term elaboration loop.
Term elaboration
The basic idea of term elaboration is the same as command elaboration:
expand macros and recurse or run term elaborators that have been registered
for the Syntax via the term_elab attribute (they might in turn run term elaboration)
until we are done. There is, however, one special action that a term elaborator
can do during its execution.
A term elaborator may throw Except.postpone. This indicates that
the term elaborator requires more
information to continue its work. In order to represent this missing information,
Lean uses so called synthetic metavariables. As you know from before, metavariables
are holes in Exprs that are waiting to be filled in. Synthetic metavariables are
different in that they have special methods that are used to solve them,
registered in SyntheticMVarKind. Right now, there are four of these:
typeClass, the metavariable should be solved with typeclass synthesiscoe, the metavariable should be solved via coercion (a special case of typeclass)tactic, the metavariable is a tactic term that should be solved by running a tacticpostponed, the ones that are created atExcept.postpone
Once such a synthetic metavariable is created, the next higher level term elaborator will continue. At some point, execution of postponed metavariables will be resumed by the term elaborator, in hopes that it can now complete its execution. We can try to see this in action with the following example:
#check set_option trace.Elab.postpone true in List.foldr .add 0 [1,2,3] -- [Elab.postpone] .add : ?m.5695 → ?m.5696 → ?m.5696
What happened here is that the elaborator for function applications started
at List.foldr which is a generic function so it created metavariables
for the implicit type parameters. Then, it attempted to elaborate the first argument .add.
In case you don't know how .name works, the basic idea is that quite
often (like in this case) Lean should be able to infer the output type (in this case Nat)
of a function (in this case Nat.add). In such cases, the .name feature will then simply
search for a function named name in the namespace Nat. This is especially
useful when you want to use constructors of a type without referring to its
namespace or opening it, but can also be used like above.
Now back to our example, while Lean does at this point already know that .add
needs to have type: ?m1 → ?m2 → ?m2 (where ?x is notation for a metavariable)
the elaborator for .add does need to know the actual value of ?m2 so the
term elaborator postpones execution (by internally creating a synthetic metavariable
in place of .add), the elaboration of the other two arguments then yields the fact that
?m2 has to be Nat so once the .add elaborator is continued it can work with
this information to complete elaboration.
We can also easily provoke cases where this does not work out. For example:
#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
In this case .add first postponed its execution, then got called again
but didn't have enough information to finish elaboration and thus failed.
Making our own
Adding new term elaborators works basically the same way as adding new command elaborators so we'll only take a very brief look:
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
-- Also works with `elab`
elab "myterm 2" : term => do
mkAppM ``List.get! #[.const ``mytermValues [], mkNatLit 1] -- `MetaM` code
#eval myterm 2 -- 2
Mini project
As a final mini project for this chapter we will recreate one of the most
commonly used Lean syntax sugars, the ⟨a,b,c⟩ notation as a short hand
for single constructor types:
-- slightly different notation so no ambiguity happens
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
-- Attempt to postpone execution if the type is not known or is a metavariable.
-- Metavariables are used by things like the function elaborator to fill
-- out the values of implicit parameters when they haven't gained enough
-- information to figure them out yet.
-- Term elaborators can only postpone execution once, so the elaborator
-- doesn't end up in an infinite loop. Hence, we only try to postpone it,
-- otherwise we may cause an error.
tryPostponeIfNoneOrMVar typ?
-- If we haven't found the type after postponing just error
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
As a final note, we can shorten the postponing act by using an additional
syntax sugar of the elab syntax instead:
-- This `t` syntax will effectively perform the first two lines of `myanonImpl`
elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
sorry
Exercises
-
Consider the following code. Rewrite
syntax+@[term_elab hi]... : TermElabcombination using justelab.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 -
Here is some syntax taken from a real mathlib command
alias.syntax (name := our_alias) (docComment)? "our_alias " ident " ← " ident* : commandWe want
alias hi ← hello yesto print out the identifiers after←- that is, "hello" and "yes".Please add these semantics:
a) using
syntax+@[command_elab alias] def elabOurAlias : CommandElab. b) usingsyntax+elab_rules. c) usingelab. -
Here is some syntax taken from a real mathlib tactic
nth_rewrite.open Parser.Tactic syntax (name := nthRewriteSeq) "nth_rewrite " (config)? num rwRuleSeq (ppSpace location)? : tacticWe want
nth_rewrite 5 [←add_zero a] at hto print out"rewrite location!"if the user provided location, and"rewrite target!"if the user didn't provide location.Please add these semantics:
a) using
syntax+@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic. b) usingsyntax+elab_rules. c) usingelab.
Embedding DSLs By Elaboration
In this chapter we will learn how to use elaboration to build a DSL. We will not
explore the full power of MetaM, and simply gesture at how to get access to
this low-level machinery.
More precisely, we shall enable Lean to understand the syntax of IMP, which is a simple imperative language, often used for teaching operational and denotational semantics.
We are not going to define everything with the same encoding that the book does. For instance, the book defines arithmetic expressions and boolean expressions. We, will take a different path and just define generic expressions that take unary or binary operators.
This means that we will allow weirdnesses like 1 + true! But it will simplify
the encoding, the grammar and consequently the metaprogramming didactic.
Defining our AST
We begin by defining our atomic literal value.
import Lean
open Lean Elab Meta
inductive IMPLit
| nat : Nat → IMPLit
| bool : Bool → IMPLit
This is our only unary operator
inductive IMPUnOp
| not
These are our binary operations.
inductive IMPBinOp
| and | add | less
Now we define the expressions that we want to handle.
inductive IMPExpr
| lit : IMPLit → IMPExpr
| var : String → IMPExpr
| un : IMPUnOp → IMPExpr → IMPExpr
| bin : IMPBinOp → IMPExpr → IMPExpr → IMPExpr
And finally the commands of our language. Let's follow the book and say that "each piece of a program is also a program":
inductive IMPProgram
| Skip : IMPProgram
| Assign : String → IMPExpr → IMPProgram
| Seq : IMPProgram → IMPProgram → IMPProgram
| If : IMPExpr → IMPProgram → IMPProgram → IMPProgram
| While : IMPExpr → IMPProgram → IMPProgram
Elaborating literals
Now that we have our data types, let's elaborate terms of Syntax into
terms of Expr. We begin by defining the syntax and an elaboration function for
literals.
declare_syntax_cat imp_lit
syntax num : imp_lit
syntax "true" : imp_lit
syntax "false" : imp_lit
def elabIMPLit : Syntax → MetaM Expr
-- `mkAppM` creates an `Expr.app`, given the function `Name` and the args
-- `mkNatLit` creates an `Expr` from a `Nat`
| `(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
Elaborating expressions
In order to elaborate expressions, we also need a way to elaborate our unary and binary operators.
Notice that these could very much be pure functions (Syntax → Expr), but we're
staying in MetaM because it allows us to easily throw an error for match
completion.
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
Now we define the syntax for expressions:
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
Let's also allow parentheses so the IMP programmer can denote their parsing precedence.
syntax "(" imp_expr ")" : imp_expr
Now we can elaborate our expressions. Note that expressions can be recursive.
This means that our elabIMPExpr function will need to be recursive! We'll need
to use partial because Lean can't prove the termination of Syntax
consumption alone.
partial def elabIMPExpr : Syntax → MetaM Expr
| `(imp_expr| $l:imp_lit) => do
let l ← elabIMPLit l
mkAppM ``IMPExpr.lit #[l]
-- `mkStrLit` creates an `Expr` from a `String`
| `(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))
Elaborating programs
And now we have everything we need to elaborate our IMP programs!
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
And we can finally test our full elaboration pipeline. Let's use the following syntax:
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))))
Tactics
Tactics are Lean programs that manipulate a custom state. All tactics are, in
the end, of type TacticM Unit. This has the type:
-- from Lean/Elab/Tactic/Basic.lean
TacticM = ReaderT Context $ StateRefT State TermElabM
But before demonstrating how to use TacticM, we shall explore macro-based
tactics.
Tactics by Macro Expansion
Just like many other parts of the Lean 4 infrastructure, tactics too can be declared by lightweight macro expansion.
For example, we build an example of a custom_sorry_macro that elaborates into
a sorry. We write this as a macro expansion, which expands the piece of syntax
custom_sorry_macro into the piece of syntax sorry:
import Lean.Elab.Tactic
macro "custom_sorry_macro" : tactic => `(tactic| sorry)
example : 1 = 42 := by
custom_sorry_macro
Implementing trivial: Extensible Tactics by Macro Expansion
As more complex examples, we can write a tactic such as custom_tactic, which
is initially completely unimplemented, and can be extended with more tactics.
We start by simply declaring the tactic with no implementation:
syntax "custom_tactic" : tactic
/-- error: tactic 'tacticCustom_tactic' has not been implemented -/
example : 42 = 42 := by
custom_tactic
sorry
We will now add the rfl tactic into custom_tactic, which will allow us to
prove the previous theorem
macro_rules
| `(tactic| custom_tactic) => `(tactic| rfl)
example : 42 = 42 := by
custom_tactic
-- Goals accomplished 🎉
We can now try a harder problem, that cannot be immediately dispatched by 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
We extend the custom_tactic tactic with a tactic that tries to break And
down with apply And.intro, and then (recursively (!)) applies custom_tactic
to the two cases with (<;> trivial) to solve the generated subcases 43 = 43,
42 = 42.
macro_rules
| `(tactic| custom_tactic) => `(tactic| apply And.intro <;> custom_tactic)
The above declaration uses <;> which is a tactic combinator. Here, a <;> b
means "run tactic a, and apply "b" to each goal produced by a". Thus,
And.intro <;> custom_tactic means "run And.intro, and then run
custom_tactic on each goal". We test it out on our previous theorem and see
that we dispatch the theorem.
example : 43 = 43 ∧ 42 = 42 := by
custom_tactic
-- Goals accomplished 🎉
In summary, we declared an extensible tactic called custom_tactic. It
initially had no elaboration at all. We added the rfl as an elaboration of
custom_tactic, which allowed it to solve the goal 42 = 42. We then tried a
harder theorem, 43 = 43 ∧ 42 = 42 which custom_tactic was unable to solve.
We were then able to enrich custom_tactic to split "and" with And.intro, and
also recursively call custom_tactic in the two subcases.
Implementing <;>: Tactic Combinators by Macro Expansion
Recall that in the previous section, we said that a <;> b meant "run a, and
then run b for all goals". In fact, <;> itself is a tactic macro. In this
section, we will implement the syntax a and_then b which will stand for
"run a, and then run b for all goals".
-- 1. We declare the syntax `and_then`
syntax tactic " and_then " tactic : tactic
-- 2. We write the expander that expands the tactic
-- into running `a`, and then running `b` on all goals produced by `a`.
macro_rules
| `(tactic| $a:tactic and_then $b:tactic) =>
`(tactic| $a:tactic; all_goals $b:tactic)
-- 3. We test this tactic.
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 }
Exploring TacticM
The simplest tactic: sorry
In this section, we wish to write a tactic that fills the proof with sorry:
example : 1 = 2 := by
custom_sorry
We begin by declaring such a tactic:
elab "custom_sorry_0" : tactic => do
return
example : 1 = 2 := by
custom_sorry_0
-- unsolved goals: ⊢ 1 = 2
sorry
This defines a syntax extension to Lean, where we are naming the piece of syntax
custom_sorry_0 as living in tactic syntax category. This informs the
elaborator that, in the context of elaborating tactics, the piece of syntax
custom_sorry_0 must be elaborated as what we write to the right-hand-side of
the => (the actual implementation of the tactic).
Next, we write a term in TacticM Unit to fill in the goal with sorryAx α,
which can synthesize an artificial term of type α. To do this, we first access
the goal with Lean.Elab.Tactic.getMainGoal : Tactic MVarId, which returns the
main goal, represented as a metavariable. Recall that under
types-as-propositions, the type of our goal must be the proposition that 1 = 2.
We check this by printing the type of goal.
But first we need to start our tactic with Lean.Elab.Tactic.withMainContext,
which computes in TacticM with an updated context.
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
To sorry the goal, we can use the helper 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
And we no longer have the error unsolved goals: ⊢ 1 = 2.
The custom_assump tactic: Accessing Hypotheses
In this section, we will learn how to access the hypotheses to prove a goal. In
particular, we shall attempt to implement a tactic custom_assump, which looks
for an exact match of the goal among the hypotheses, and solves the theorem if
possible.
In the example below, we expect custom_assump to use (H2 : 2 = 2) to solve
the goal (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
When we do not have a matching hypothesis to the goal, we expect the tactic
custom_assump to throw an error, telling us that we cannot find a hypothesis
of the type we are looking for:
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
We begin by accessing the goal and the type of the goal so we know what we
are trying to prove. The goal variable will soon be used to help us create
error messages.
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
Next, we access the list of hypotheses, which are stored in a data structure
called LocalContext. This is accessed via Lean.MonadLCtx.getLCtx. The
LocalContext contains LocalDeclarations, from which we can extract
information such as the name that is given to declarations (.userName), the
expression of the declaration (.toExpr). Let's write a tactic called
list_local_decls that prints the local declarations:
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
Recall that we are looking for a local declaration that has the same type as the
hypothesis. We get the type of LocalDecl by calling
Lean.Meta.inferType on the local declaration's expression.
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
We check if the type of the LocalDecl is equal to the goal type with
Lean.Meta.isExprDefEq. See that we check if the types are equal at eq?, and
we print that H1 has the same type as the goal
(local decl[EQUAL? true]: name: H1), and we print that H2 does not have the
same type (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
Finally, we put all of these parts together to write a tactic that loops over
all declarations and finds one with the correct type. We loop over declarations
with lctx.findDeclM?. We infer the type of declarations with
Lean.Meta.inferType. We check that the declaration has the same type as the
goal with Lean.Meta.isExprDefEq:
elab "custom_assump_1" : tactic =>
Lean.Elab.Tactic.withMainContext do
let goalType ← Lean.Elab.Tactic.getMainTarget
let lctx ← Lean.MonadLCtx.getLCtx
-- Iterate over the local declarations...
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
Now that we are able to find the matching expression, we need to close the
theorem by using the match. We do this with Lean.Elab.Tactic.closeMainGoal.
When we do not have a matching expression, we throw an error with
Lean.Meta.throwTacticEx, which allows us to report an error corresponding to a
given goal. When throwing this error, we format the error using m!"..." which
builds a MessageData. This provides nicer error messages than using f!"..."
which builds a Format. This is because MessageData also runs delaboration,
which allows it to convert raw Lean terms like
(Eq.{1} Nat (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
into readable strings like(2 = 2). The full code listing given below shows how
to do this:
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
Tweaking the context
Until now, we've only performed read-like operations with the context. But what if we want to change it? In this section we will see how to change the order of goals and how to add content to it (new hypotheses).
Then, after elaborating our terms, we will need to use the helper function
Lean.Elab.Tactic.liftMetaTactic, which allows us to run computations in
MetaM while also giving us the goal MVarId for us to play with. In the end
of our computation, liftMetaTactic expects us to return a List MVarId as the
resulting list of goals.
The only substantial difference between custom_let and custom_have is that
the former uses Lean.MVarId.define and the later uses 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
"Getting" and "Setting" the list of goals
To illustrate these, let's build a tactic that can reverse the list of goals.
We can use Lean.Elab.Tactic.getGoals and 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
In this section, we collect common patterns that are used during writing tactics, to make it easy to find common patterns.
Q: How do I use goals?
A: Goals are represented as metavariables. The module Lean.Elab.Tactic.Basic
has many functions to add new goals, switch goals, etc.
Q: How do I get the main goal?
A: Use 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
Q: How do I get the list of goals?
A: Use 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
Q: How do I get the current hypotheses for a goal?
A: Use Lean.MonadLCtx.getLCtx which provides the local context, and then
iterate on the LocalDeclarations of the LocalContext with accessors such as
foldlM and forM.
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
Q: How do I evaluate a tactic?
A: Use Lean.Elab.Tactic.evalTactic: Syntax → TacticM Unit which evaluates a
given tactic syntax. One can create tactic syntax using the macro
`(tactic| ⋯).
For example, one could call try rfl with the piece of code:
Lean.Elab.Tactic.evalTactic (← `(tactic| try rfl))
Q: How do I check if two expressions are equal?
A: Use Lean.Meta.isExprDefEq <expr-1> <expr-2>.
#check Lean.Meta.isExprDefEq
-- Lean.Meta.isExprDefEq : Lean.Expr → Lean.Expr → Lean.MetaM Bool
Q: How do I throw an error from a tactic?
A: Use 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
Q: What is the difference between Lean.Elab.Tactic.* and Lean.Meta.Tactic.*?
A: Lean.Meta.Tactic.* contains low level code that uses the Meta monad to
implement basic features such as rewriting. Lean.Elab.Tactic.* contains
high-level code that connects the low level development in Lean.Meta to the
tactic infrastructure and the parsing front-end.
Exercises
-
Consider the theorem
p ∧ q ↔ q ∧ p. We could either write its proof as a proof term, or construct it using the tactics. When we are writing the proof of this theorem as a proof term, we're gradually filling up_s with certain expressions, step by step. Each such step corresponds to a tactic.There are many combinations of steps in which we could write this proof term - but consider the sequence of steps we wrote below. Please write each step as a tactic. The tactic
step_1is filled in, please do the same for the remaining tactics (for the sake of the exercise, try to use lower-level apis, such asmkFreshExprMVar,mvarId.assignandmodify fun _ => { goals := ~).-- [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 -
In the first exercise, we used lower-level
modifyapi to update our goals.liftMetaTactic,setGoals,appendGoals,replaceMainGoal,closeMainGoal, etc. are all syntax sugars on top ofmodify fun s : State => { s with goals := myMvarIds }. Please rewrite theforkertactic with:a)
liftMetaTacticb)setGoalsc)replaceMainGoalelab "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 -
In the first exercise, you created your own
introinstep_2(with a hardcoded hypothesis name, but the basics are the same). When writing tactics, we usually want to use functions such asintro,intro1,intro1P,introNorintroNP.For each of the points below, create a tactic
introductor(one per each point), that turns the goal(ab: a = b) → (bc: b = c) → (a = c):a) into the goal
(a = c)with hypotheses(ab✝: a = b)and(bc✝: b = c). b) into the goal(bc: b = c) → (a = c)with hypothesis(ab: a = b). c) into the goal(bc: b = c) → (a = c)with hypothesis(hello: a = b).example (a b c : Nat) : (ab: a = b) → (bc: b = c) → (a = c) := by introductor sorryHint: "P" in
intro1PandintroNPstands for "Preserve".
Lean4 Cheat-sheet
Extracting information
-
Extract the goal:
Lean.Elab.Tactic.getMainGoalUse as
let goal ← Lean.Elab.Tactic.getMainGoal -
Extract the declaration out of a metavariable:
mvarId.getDeclwhenmvarId : Lean.MVarIdis in context. For instance,mvarIdcould be the goal extracted usinggetMainGoal -
Extract the type of a metavariable:
mvarId.getTypewhenmvarId : Lean.MVarIdis in context. -
Extract the type of the main goal:
Lean.Elab.Tactic.getMainTargetUse as
let goal_type ← Lean.Elab.Tactic.getMainTargetAchieves the same as
let goal ← Lean.Elab.Tactic.getMainGoal
let goal_type ← goal.getType
-
Extract local context:
Lean.MonadLCtx.getLCtxUse as
let lctx ← Lean.MonadLCtx.getLCtx -
Extract the name of a declaration:
Lean.LocalDecl.userName ldeclwhenldecl : Lean.LocalDeclis in context -
Extract the type of an expression:
Lean.Meta.inferType exprwhenexpr : Lean.Expris an expression in contextUse as
let expr_type ← Lean.Meta.inferType expr
Playing around with expressions
-
Convert a declaration into an expression:
Lean.LocalDecl.toExprUse as
ldecl.toExpr, whenldecl : Lean.LocalDeclis in contextFor instance,
ldeclcould belet ldecl ← Lean.MonadLCtx.getLCtx -
Check whether two expressions are definitionally equal:
Lean.Meta.isDefEq ex1 ex2whenex1 ex2 : Lean.Exprare in context. Returns aLean.MetaM Bool -
Close a goal:
Lean.Elab.Tactic.closeMainGoal exprwhenexpr : Lean.Expris in context
Further commands
- meta-sorry:
Lean.Elab.admitGoal goal, whengoal : Lean.MVarIdis the current goal
Printing and errors
-
Print a "permanent" message in normal usage:
Lean.logInfo f!"Hi, I will print\n{Syntax}" -
Print a message while debugging:
dbg_trace f!"1) goal: {Syntax_that_will_be_interpreted}". -
Throw an error:
Lean.Meta.throwTacticEx name mvar message_datawherename : Lean.Nameis the name of a tactic andmvarcontains error data.Use as
Lean.Meta.throwTacticExtac goal (m!"unable to find matching hypothesis of type ({goal_type})")where them!formatting builds aMessageData` for better printing of terms
TODO: Add?
- Lean.LocalContext.forM
- Lean.LocalContext.findDeclM?
Extra: Options
Options are a way to communicate some special configuration to both
your meta programs and the Lean compiler itself. Basically it's just
a KVMap
which is a simple map from Name to a Lean.DataValue. Right now there
are 6 kinds of data values:
StringBoolNameNatIntSyntax
Setting an option to tell the Lean compiler to do something different
with your program is quite simple with the set_option command:
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
You can furthermore limit an option value to just the next command or term:
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`
If you want to know which options are available out of the Box right now
you can simply write out the set_option command and move your cursor
to where the name is written, it should give you a list of them as auto
completion suggestions. The most useful group of options when you are
debugging some meta thing is the trace. one.
Options in meta programming
Now that we know how to set options, let's take a look at how a meta program
can get access to them. The most common way to do this is via the MonadOptions
type class, an extension to Monad that provides a function getOptions : m Options.
As of now, it is implemented by:
CoreMCommandElabMLevelElabM- all monads to which you can lift operations of one of the above (e.g.
MetaMfromCoreM)
Once we have an Options object, we can query the information via Options.get.
To show this, let's write a command that prints the value of 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
Note that the real implementation of getting pp.explicit, Lean.getPPExplicit,
uses whether pp.all is set as a default value instead.
Making our own
Declaring our own option is quite easy as well. The Lean compiler provides
a macro register_option for this. Let's see it in action:
register_option book.myGreeting : String := {
defValue := "Hello World"
group := "pp"
descr := "just a friendly greeting"
}
However, we cannot just use an option that we just declared in the same file it was declared in because of initialization restrictions.
Extra: Pretty Printing
The pretty printer is what Lean uses to present terms that have been
elaborated to the user. This is done by converting the Exprs back into
Syntax and then even higher level pretty printing datastructures. This means
Lean does not actually recall the Syntax it used to create some Expr:
there has to be code that tells it how to do that.
In the big picture, the pretty printer consists of three parts run in the
order they are listed in:
- the delaborator
this will be our main interest since we can easily extend it with our own code.
Its job is to turn
Exprback intoSyntax. - the parenthesizer
responsible for adding parenthesis into the
Syntaxtree, where it thinks they would be useful - the formatter
responsible for turning the parenthesized
Syntaxtree into aFormatobject that contains more pretty printing information like explicit whitespaces
Delaboration
As its name suggests, the delaborator is in a sense the opposite of the
elaborator. The job of the delaborator is to take an Expr produced by
the elaborator and turn it back into a Syntax which, if elaborated,
should produce an Expr that behaves equally to the input one.
Delaborators have the type Lean.PrettyPrinter.Delaborator.Delab. This
is an alias for DelabM Syntax, where DelabM is the delaboration monad.
All of this machinery is defined here.
DelabM provides us with quite a lot of options you can look up in the documentation
(TODO: Docs link). We will merely highlight the most relevant parts here.
- It has a
MonadQuotationinstance which allows us to declareSyntaxobjects using the familiar quotation syntax. - It can run
MetaMcode. - It has a
MonadExceptinstance for throwing errors. - It can interact with
ppoptions using functions likewhenPPOption. - You can obtain the current subexpression using
SubExpr.getExpr. There is also an entire API defined around this concept in theSubExprmodule.
Making our own
Like so many things in metaprogramming the elaborator is based on an attribute,
in this case the delab one. delab expects a Name as an argument,
this name has to start with the name of an Expr constructor, most commonly
const or app. This constructor name is then followed by the name of the
constant we want to delaborate. For example, if we want to delaborate a function
foo in a special way we would use app.foo. Let's see this in action:
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
This is obviously not a good delaborator since reelaborating this Syntax
will not yield the same Expr. Like with many other metaprogramming
attributes we can also overload delaborators:
@[delab app.foo]
def delabfoo2 : Delab := do
`(2)
#check foo -- 2 : Nat → Nat
The mechanism for figuring out which one to use is the same as well. The
delaborators are tried in order, in reverse order of registering, until one
does not throw an error, indicating that it "feels unresponsible for the Expr".
In the case of delaborators, this is done using failure:
@[delab app.foo]
def delabfoo3 : Delab := do
failure
`(3)
#check foo -- 2 : Nat → Nat, still 2 since 3 failed
In order to write a proper delaborator for foo, we will have to use some
slightly more advanced machinery though:
@[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
Can you extend delabFooFinal to also account for non full applications?
Unexpanders
While delaborators are obviously quite powerful it is quite often not necessary
to use them. If you look in the Lean compiler for @[delab or rather @[builtin_delab
(a special version of the delab attribute for compiler use, we don't care about it),
you will see there are quite few occurrences of it. This is because the majority
of pretty printing is in fact done by so called unexpanders. Unlike delaborators
they are of type Lean.PrettyPrinter.Unexpander which in turn is an alias for
Syntax → Lean.PrettyPrinter.UnexpandM Syntax. As you can see, they are
Syntax to Syntax translations, quite similar to macros, except that they
are supposed to be the inverse of macros. The UnexpandM monad is quite a lot
weaker than DelabM but it still has:
MonadQuotationfor syntax quotations- The ability to throw errors, although not very informative ones:
throw ()is the only valid one
Unexpanders are always specific to applications of one constant. They are registered
using the app_unexpander attribute, followed by the name of said constant. The unexpander
is passed the entire application of the constant after the Expr has been delaborated,
without implicit arguments. Let's see this in action:
def myid {α : Type} (x : α) := x
@[app_unexpander myid]
def unexpMyId : Unexpander
-- hygiene disabled so we can actually return `id` without macro scopes etc.
| `(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
For a few nice examples of unexpanders you can take a look at NotationExtra
Mini project
As per usual, we will tackle a little mini project at the end of the chapter.
This time we build our own unexpander for a mini programming language.
Note that many ways to define syntax already have generation of the required
pretty printer code built-in, e.g. infix, and notation (however not macro_rules).
So, for easy syntax, you will never have to do this yourself.
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
]
As you can see, the pretty printing output right now is rather ugly to look at. We can do better with an 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
]
That's much better! As always, we encourage you to extend the language yourself
with things like parenthesized expressions, more data values, quotations for
term or whatever else comes to your mind.
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