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 を参照してください（通常はデフォルト値が正しいです）。1
  • userName：新しいメタ変数のユーザが目にする名前。これはメタ変数がゴールに現れる際に表示されるものになります。MVarId と異なり、この名前は一意である必要はありません。

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

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

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

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

この関数は MetavarContext を割当 ?mvarId := val で更新します。ここでこの mvarId が割り当てられていないことを確認しなければなりません（もしくは古い割当と新しい割当が definitionally equal ことを確認する必要があります）。また、割り当てられた値 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
      -- もしこの仮定の型がターゲットの型と definitionally equal 場合：
      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つの定義が definitionally equal かどうかをチェックします。詳細は 定義上の等しさの節 を参照してください。
  • 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 の深さを継承するため、デフォルトではすべてのメタ変数が割り当て可能です。

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

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

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

計算

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

完全正規化

計算でできることの中で最も単純なものは項を正規形にすることです。数値型のいくつかの例外を除いて、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 は（現在の透過度において）正規形が等しい場合、 definitionally equal 、もしくは 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つの要素によって決まります：

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

式の構築

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

適用

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

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

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

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

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

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

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

mkAppM : Name → Array Expr → MetaM Expr

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

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

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

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

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

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

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

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

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

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

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

ラムダ式と forall

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

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

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

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

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

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

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

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

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

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

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

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

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

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

mkLambdaFVars : Array Expr → Expr → MetaM Expr

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

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

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

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

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

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

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

elab "someProp" : term => somePropExpr

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

式の分解

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

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

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

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

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

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

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

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

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

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

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

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

バックトラッキング

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

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

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

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

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

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

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

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

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

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

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

try
  doSomething
catch e =>
  doSomethingElse

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

try
  commitIfNoEx doSomething
catch e =>
  doSomethingElse

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

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

演習問題

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

  2. [メタ変数] instantiateMVars (Lean.mkAppN (Expr.const 'Nat.add []) #[mkNatLit 1, mkNatLit 2]) は何を出力するでしょうか？

  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 ← ...
  -- 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`
  ...

  4. [メタ変数] 下記の定理 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

  5. [メタ変数] 上記の定理 red を証明するタクティク solve を書いてください。

  6. [計算] 以下の式の正規形は何になるでしょうか？ a) Bool → Bool 型の fun x => x b) Bool 型の (fun x => x) ((true && false) || true) c) Nat 型の 800 + 2

  7. [計算] Expr.lit (Lean.Literal.natVal 1) で作られた 1 と Expr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero []) で作られた式が definitionally equal ことを示してください。

  8. [計算] 以下の式が definitionally equal かどうか判定してください。もし Lean.Meta.isDefEq が成功し、メタ変数の割り当てを導くなら、その割当も書き下してください。 a) 5 =?= (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z)) b) 2 + 1 =?= 1 + 2 c) ?a =?= 2、ここで ?a は String 型 d) ?a + Int =?= "hi" + ?b、ここで ?a と ?b は型を持ちません e) 2 + ?a =?= 3 f) 2 + ?a =?= 2 + 1

  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) -- ...

  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) -- ...

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

  11. [式の構築] 式 ∀ (yellow: Nat), yellow を構築してください。

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

  13. [式の構築] 式 fun (f : Nat → Nat), ∀ (n : Nat), f n = f (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 -- ...

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

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

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

1

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