介绍

本书英文原文：Metaprogramming in Lean 4

本书的目的

本书的目的是教你 Lean 4 元编程，你将学会：

• 构建自己的元助手（定义新的 Lean 符号，如「∑」，构建新的 Lean 命令，如#check，编写策略，如use等）
• 阅读和讨论元编程API，如Lean 4 core和Mathlib4中的API

我们绝不打算对整个 Lean 4 元编程API进行详尽的解释。我们也不涉及单子（Monad）化编程的主题。我们希望示例足够简单，不太熟悉单子化编程也能跟上。强烈推荐 Lean 中的函数式编程作为这个主题的参考。

本书的结构

本书试着为DSL和策略建立足够的上下文来使你理解它们。章节依赖关系如下：

• 「表达式」=>「MetaM」
• 「语法」=>「宏」
• 「语法」+「MetaM」=>「繁饰」=>「DSL」
• 「宏」+「繁饰」=>「证明策略」

证明策略一章之后是包括关键概念和功能概述的备忘录。那之后，是一些章节的额外内容，展示了 Lean 4 元编程的其他应用。大多数章节的末尾都有习题，书的最后是习题答案。

本章的其余部分将简要介绍什么是元编程，并提供一些小示例开胃菜。

注意：代码片段不是自包含的。它们应该从每章的开头开始，以增量方式运行/读取。

译注：本书一律将Syntax译为语法，Grammar译为文法。

「元」是什么?

当我们用Python、C、Java或Scala等大多数编程语言编写代码时，通常遵循预定义的语法，否则编译器或解释器将无法理解代码。在Lean中，这些预定义语法是定义归纳类型、实现函数、证明定理等。然后，编译器必须解析代码，构建一个AST（抽象语法树），并将其语法节点阐释为语言内核可以处理的项。我们说编译器执行的这些活动是在元层面中完成的，这是本书的内容。我们还说，语法的常见用法是在对象层面中完成的。

在大多数系统中，元层面活动是用与我们当前用来编写代码的语言不同的语言完成的。在Isabelle中，元层面语言是ML和Scala。在Coq中，它是OCaml。在Agda中，是Haskell。在 Lean 4 中，元代码主要是用 Lean 本身编写的，还有一些用C++编写的组件。

Lean 的一个很酷且方便的地方是，它允许我们用日常在对象层面写 Lean 的方式自定义语法节点，并实现元层面例程。例如，可以编写记号来实例化某种类型的项，并在同一个文件中立即使用它！这个概念通常被称为反射。我们可以说，在Lean中，元层面被「反射」到对象层面。

用Ruby、Python或Javascript等语言做元编程的方式可能是使用预定义的元编程方法来即时定义一些东西。例如，在Ruby中你可以使用 Class.new 和 define_method 用于在程序执行时即时定义一个新类及其新方法（其中包含新代码！）。

在Lean中，我们通常不需要「即时地」定义新的命令或策略，但是在Lean元编程中能做类似的事，并且同样直接，例如，你可以使用简单的一行 elab "#help" : command => do ...normal Lean code...。

然而，在Lean中，我们经常想要直接操作Lean的CST（具体语法树，Lean的 Syntax 类型）和Lean的AST（抽象语法树，Lean的 Expr 类型），而不是使用「正常的Lean代码」，特别是当我们编写证明策略（Tactic）时。因此，Lean元编程更难掌握。本书的大部分内容都是为了研究这些类型以及我们如何操作它们。

元编程示例

下面这些例子仅作为展示。如果您现在不了解细节，请不要担心。

引入符号（定义新语法）

通常，人们希望引入新的符号，例如更适合数学（的某分支）的符号。例如，在数学中，人们会将给一个自然数加 2 的函数写为 x : Nat ↦ x + 2 或简单地写为 x ↦ x + 2 ，如果可以推断出定义域是自然数。相应的 Lean 定义 fun x : Nat => x + 2 和 fun x => x + 2 使用 =>，这在数学中表示蕴涵，因此可能会让一些人感到困惑。

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 中运行。然后我们使用 liftTermElabM 来访问单子 TermElabM，这使我们能够使用 elabType 和 elabTermEnsuringType 从语法节点 typeStx 和 termStx 构建表达式。

首先，我们繁饰预期的类型 tp : Expr，然后使用它来繁饰项表达式。该项应具有类型 tp，否则将引发错误。然后我们丢弃生成的项表达式，因为它对我们来说并不重要 - 我们调用 elabTermEnsuringType 作为健全性检查。

我们还添加了 synthesizeSyntheticMVarsNoPostponing，它强制 Lean 立即繁饰元变量。如果没有该行，#assertType [] : ?_ 将导致 success。

如果到现在为止没有抛出任何错误，则繁饰成功，我们可以使用 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           -- 常量
  | var : String → Arith        -- 变量

现在我们声明一个语法类别（declare syntax category）来描述我们将要解析的文法。我们通过为 + 语法赋予比 * 语法更低的优先级权重来控制 + 和 * 的优先级，这表明乘法比加法绑定得更紧密（数字越高，绑定越紧密）。

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 -- 带括号表达式

-- 将 arith 翻译为 term 的辅助符号
syntax " ⟪ " arith " ⟫ " : term

-- 我们的宏规则执行「显然的」翻译：
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" ⟫ -- 优先级
-- Arith.add (Arith.var "x") (Arith.mul (Arith.var "y") (Arith.var "z")) : Arith

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

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

编写我们自己的策略

让我们创建一个策略，将一个给定名称的新假设添加到语境中，并将其证明推迟到最后。它类似于 Lean 3 中的 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     -- 证明主目标
  rw [Nat.zero_add]; rfl -- 证明 `add_comm`

我们首先将主要目标存储在 mvarId 中，并将其用作 withMVarContext 的参数，以确保我们的繁饰能够适用于依赖于语境中其他变量的类型。

这次我们使用 mkFreshExprMVar 为 t 的证明创建一个元变量表达式，我们可以使用 intro1P 和 assert 将其引入语境。

为了要求将新假设的证明作为目标，我们调用 replaceMainGoal，并在头部传递一个带有 p.mvarId! 的列表。然后我们可以使用 rotate_left 策略将最近添加的顶部目标移到底部。

概述

在本章中，我们将概述 Lean 编译过程中涉及的主要步骤，包括解析（parsing）、繁饰（elaboration）和求值（evaluation）。正如介绍中提到的，Lean 中的元编程需要深入这个过程的核心。我们将探索所涉及的基本对象 Expr 和 Syntax，了解它们的含义，并发现如何将一个对象转换为另一个对象（并转换回来！）。

后面的章节会介绍细节，你可以之后回顾本章，以提醒自己这些组件是如何组合在一起的。

与编译器的连接

Lean 中的元编程密切关系到编译步骤 -- 解析、语法分析、转换和代码生成。

Lean 4 是用 Lean 本身重新实现的 Lean 定理证明器。新的编译器生成 C 代码，用户现在可以在 Lean 中实现高效的证明自动化，将其编译为高效的 C 代码，并将其作为插件加载。在 Lean 4 中，用户只需导入 Lean 包即可访问用于实现 Lean 的所有内部数据结构。

Leonardo de Moura、Sebastian Ullrich (Lean 4 定理证明器和编程语言)

Lean 编译过程可以总结为下图：

首先从字符串形式的 Lean 代码开始。然后它变成 Syntax 对象，然后是 Expr 对象。最后执行它。

因此，编译器看到一串 Lean 代码，例如 "let a := 2"，然后展开以下过程：

1. 应用相关语法规则 ("let a := 2" ➤ Syntax)

在解析步骤中，Lean 尝试将一串 Lean 代码与声明的语法规则之一进行匹配，以便将该字符串转换为 Syntax 对象。语法规则基本上是美化的正则表达式 -- 当您编写与某个语法规则的正则表达式匹配的 Lean 字符串时，该规则将用于处理后续步骤。

2. 循环应用所有宏 (Syntax ➤ Syntax)

在繁饰步骤中，每个宏只是将现有的 Syntax 对象转换为某个新的 Syntax 对象。然后，新的 Syntax 以类似的方式处理（重复步骤 1 和 2），直到没有更多宏可应用。

3. 应用单个 elab (Syntax ➤ Expr)

最后，是时候为你的语法注入意义了 -- Lean 通过 name 参数找到与相应语法规则匹配的 elab（语法规则、宏 和 elabs 都有此参数，并且它们必须匹配）。新发现的 elab 返回特定的 Expr 对象。

这样就完成了繁饰步骤。​​

然后，表达式（Expr）在求值步骤中转换为可执行代码 -- 我们不必以任何方式指定，Lean 编译器将为我们处理此操作。

繁饰和反繁饰

繁饰（elaboration）是 Lean 中一个被重载的术语。例如，您可能会遇到以下用法，其意图是「采用部分指定的表达式并推断出剩下的隐含内容」：

当您输入一个表达式，如 λ x y z, f (x + y) z 供 Lean 处理时，您隐含了一些信息。例如，必须从上下文中推断出 x、y 和 z 的类型，符号 + 可能被重载，并且 f 可能有需要补全的隐参数。

「采用部分指定的表达式并推断出剩下的隐含内容」的过程称为繁饰。Lean 的繁饰算法功能强大，但同时又微妙而复杂。在依值类型论系统中工作需要知道繁饰器可以可靠地推断哪些类型的信息，以及知道如何响应繁饰器失败时引发的错误消息。为此，了解 Lean 的繁饰器如何工作会很有帮助。

当 Lean 解析表达式时，它首先进入预处理阶段。首先，Lean 为隐参数插入「洞」。如果项 t 的类型为 Π {x : A}, P x，则 t 在所有地方都将被 @t _ 替换。然后，项中的洞（无论是在上一步中插入的洞还是用户明确编写的洞）由元变量 ?M1、?M2、?M3 等实例化。每个重载符号都与一个选项列表相关联，即可能的解释。类似地，Lean 尝试检测在一个应用 s t 中可能需要插入强制转换的点，以使推断出的 t 类型与 s 的参数类型相匹配。这些也成为选择点。如果繁饰过程的一个可能结果是不需要强制转换，那么列表中的选择之一就是恒等式。

(Lean 2 中的定理证明)

另一方面，我们只是将繁饰定义为将 Syntax 对象转换为 Expr 对象的过程。

这些定义并不相互排斥。此处定义繁饰是将 Syntax 转换为 Expr，只是为了实现这种转换，我们需要很多技巧。我们需要推断隐式参数、实例化元变量、执行统一、解析标识符等。其他地方只是把这些繁饰操作的一部分也称为繁饰。

在 Lean 中，还存在一个与繁饰相反的反繁饰（delaboration）过程。在反繁饰过程中，一个 Expr 被转换成一个 Syntax 对象；然后格式化程序将其转换成一个 Format 对象，该对象可以在 Lean 的信息视图中显示。每次您将某些内容记录到屏幕上，或者将鼠标悬停在 #check 上时看到一些输出，这都是反繁饰器的工作。

本书中，您将看到对繁饰器的引用；在「附加内容：美观打印」一章中，您可以阅读有关反繁饰器的内容。

3个必要命令及其语法糖

现在，当你阅读 Lean 源代码时，你会看到 11 (或更多) 条命令指定解析/繁饰/求值过程：

在上图中，您可以看到 notation、prefix、infix 和 postfix -- 所有这些都是 syntax 和 @[macro xxx] def ourMacro 的组合，就像 macro 一样。这些命令与 macro 不同，因为您只能用它们定义特定形式的语法。

所有这些命令都在 Lean 和 Mathlib 源代码中广泛使用，最好记住。然而，它们中的大多数都是语法糖，您可以通过研究以下 3 个低级命令的行为来了解它们的行为：syntax（语法规则）、@[macro xxx] def ourMacro（宏）和 @[command_elab xxx] def ourElab（elab，繁饰 elaborate 的简写）。

举一个更具体的例子，假设我们正在实现一个 #help 命令，也可以写成 #h。然后我们可以按如下方式编写我们的语法规则、宏和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 参数。

如果我们定义的不是命令，我们可以写 : term、: tactic 或任何其他语法类别来替换 : command。 elab 函数也可以是不同的类型，例如用于实现 #help 的 CommandElab 还有 TermElab 和 Tactic:

• TermElab 代表 Syntax → Option Expr → TermElabM Expr，因此 elab 函数应该返回 Expr 对象。
• CommandElab 代表 Syntax → CommandElabM Unit，因此它不应该返回任何内容。
• Tactic 代表 Syntax → TacticM Unit，因此它不应该返回任何内容。

这对应于我们对 Lean 中的项、命令和策略的直观理解 -- 项在执行时返回特定值，命令修改环境或打印某些内容，策略修改证明状态。

执行顺序：语法规则、宏、elab

上面是这三个基本命令的执行流程，现在明确地阐述一下。执行顺序遵循以下伪代码模板：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 / 可执行代码之间的手动转换

如果您使用 syntax、macro 和 elab 命令，Lean 将自动为您执行上述 解析/繁饰/求值 步骤，但是，当您编写策略时，您也经常需要手动执行这些转换。您可以使用以下函数来实现：

请注意，所有允许我们将 Syntax 转换为 Expr 的函数都以「elab」开头；所有允许我们将 Expr（或 Syntax）转换为 actual code 的函数都以「eval」（求值 evaluation 的简写）开头。

赋予含义：宏 VS 繁饰？

原则上，您可以使用 macro 执行（几乎？）任何可以使用 elab 函数执行的操作。只需将您在 elab 主体中的内容写成 macro 中的语法即可。但是，这里的经验法则是，仅当转换足够简单基本，几乎仅需重命名操作时才使用 macro。正如 Henrik Böving 所说：「一旦涉及类型或控制流，宏可能就不再合理了」（出自Zulip)。

因此，使用 macro 来创建语法糖、符号和快捷方式，并优先使用 elab 来编写带有一些编程逻辑的代码，即使它可能可以在 macro 中实现。

附加内容

打印消息

在 #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` 的蓝色下划线输出：dbg_trace: [[0, 1, 2], [0, 1, 2]]

  traces -- 现在 `traces` 的蓝色下划线输出：logInfo: [[0, 1, 2], [0, 1, 2]]

  trivial

类型正确性

由于元层面中定义的对象不是我们最感兴趣的证明定理的对象，因此证明它们的类型正确有时可能过于繁琐。例如，我们不关心证明遍历表达式的递归函数是否合理。因此，如果我们确信函数终止，我们可以使用 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抽象 lambda abstraction
  | forallE : Name → Expr → Expr → BinderInfo → Expr  -- (依值) 箭头(dependent) arrow
  | letE    : Name → Expr → Expr → Expr → Bool → Expr -- let 表达式
  -- 没那么必要的构造器：
  | lit     : Literal → Expr                          -- 字面量 literals
  | mdata   : MData → Expr → Expr                     -- 元变量 metadata
  | proj    : Name → Nat → Expr → Expr                -- 投影 projection

end Playground

这些构造函数各自在做什么？

• bvar 是一个 绑定变量。例如，fun x => x + 2 或 ∑ x, x² 中的 x。这是表达式中变量的任何出现，其中有一个绑定器。为什么参数是 Nat？这称为 de Bruijn 索引，稍后将解释。您可以通过查看绑定变量的绑定器来确定绑定变量的类型，因为绑定器始终具有其类型信息。
• fvar 是一个 自由变量。这些是不受绑定器绑定的变量。一个例子是 x + 2 中的 x。请注意，您不能只看一个自由变量 x 并知道它的类型是什么，需要有一个包含 x 及其类型的声明的语境。自由变量有一个 ID，它会告诉您在 LocalContext 中查找它的位置。在 Lean 3 中，自由变量也被称为「局部变量」。
• mvar 是一个 元变量。稍后将有更多关于它的内容，但您可以将其视为表达式中的占位符或「洞」，需要在稍后填充。
• sort 用于 Type u、Prop 等。
• const 是 Lean 文件中先前定义的常量。
• app 是一个函数应用。多参数是用部分应用（partial application）实现的，例如：f x y ↝ app (app f x) y。
• lam n t b 是一个 lambda 表达式（fun ($n : $t) => $b）。b 参数称为 函数体。请注意，您必须提供要绑定的变量的类型。
• forallE n t b 是一个依值箭头表达式（($n : $t) → $b）。这有时也称为 Π 类型或 Π 表达式，并且通常写为 ∀ $n : $t, $b。请注意，非依值箭头 α → β 是 (a : α) → β 的一个特例，其中 β 不依赖于 a。forallE 末尾的 E 是为了将其与 forall 关键字区分开来。
• letE n t v b 是一个 let 绑定器（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。这是出于效率原因（[todo] 引证）。

另外，您可以编写许多没有明显对应的 Expr 的 Lean 程序。例如， match 语句、do 块或 by 块等等。这些构造确实必须通过繁饰器首先转换为表达式，在后面的章节讨论。这种设置的好处是，一旦完成到 Expr的转换，我们就可以使用相对简单的结构。（缺点是从 Expr 返回到高级 Lean 程序可能具有挑战性。）

繁饰器还会填充您可能从 Lean 程序中省略的任何隐式或类型类实例参数。因此，在 Expr 级别，常量始终应用于所有参数，无论是否隐式。这样做的好处是可以获得大量从源代码中不明显的信息，坏处是构建 Expr 时，您必须自己提供任何隐式或实例参数）。

De Bruijn 索引

考虑以下 lambda 表达式 (λ 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

现在我们在执行β-规约时不需要重命名变量。我们还可以轻松检查两个包含绑定表达式的 Expr 是否相等。这就是为什么 bvar 的类型签名是 Nat → Expr 而不是 Name → Expr。

如果 de Bruijn 指标对于其前面的绑定器数量来说太大，我们说它是一个 松弛的 bvar；否则我们说它是 绑定的。例如，在表达式 lam `x _ (app #0 #1) 中，bvar #0 由前面的绑定器绑定，而 #1 是松弛的。 Lean 将所有 de Bruijn 索引称为 bvar（「绑定变量」），这隐含了一种理念：除了一些非常低级的函数之外，Lean 期望表达式不包含任何松弛的 bvar。相反，每当我们想要引入一个松弛的 bvar 时，我们都会立即将其转换为 fvar（「自由变量」）。下一章将讨论其具体工作原理。

如果表达式中没有松弛的 bvar，我们称该表达式为 闭的。用 Expr 替换所有松弛的 bvar 实例的过程称为 实例化（instantiation）。反之称为抽象化（abstraction）。

如果您熟悉变量的标准术语，Lean 的术语可能会令人困惑，对应关系：Lean 的bvar通常被称为「变量」；Lean 的「松弛」通常称为「自由」；而 Lean 的fvar或许可以被称为「局部假设」。

宇宙等级

一些表达式涉及宇宙等级，由 Lean.Level 类型表示。宇宙等级是一个自然数、一个宇宙参数（通过 universe 声明引入）、一个宇宙元变量或两个宇宙中的最大值。它们与两种表达式相关。

首先，sort由 Expr.sort u 表示，其中 u 是 Level。Prop 是 sort Level.zero；Type 是 sort (Level.succ Level.zero)。

其次，宇宙多态常量具有宇宙参数。宇宙多态常量是其类型包含宇宙参数的常量。例如，List.map 函数是宇宙多态的，如 pp.universes 美观打印选项所示：

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

List.map 后面的 .{u_1,u_2} 后缀表示 List.map 有两个宇宙参数，u_1 和 u_2。List（本身是一个宇宙多态常量）后面的 .{u_1} 后缀表示 List 应用于宇宙参数 u_1，.{u_2} 也是如此。

事实上，每当您使用宇宙多态常量时，都必须将其应用于正确的宇宙参数。此应用由 Expr.const 的 List Level 参数表示。当我们编写常规 Lean 代码时，Lean 会自动推断宇宙，因此我们不需要过多考虑它们。但是当我们构造 Expr 时，我们必须小心将每个宇宙多态常量应用于正确的宇宙参数。

构造表达式

常量

我们可以构造的最简单的表达式是常量。我们使用 const 构造器并为其指定一个名称和一个宇宙等级列表。我们的大多数示例仅涉及非宇宙多态常量，在这种情况下宇宙等级列表为空。

反引号标识 Name 类型的项，也就是一个名称。名称可以任取，但有时你需要引用已定义的常量，此时可以用双反引号写名称。双反引号可以检查名称是否真的引用了已定义的常量，有助于避免拼写错误。

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 []

双反引号还可以解析给定的名称。下例演示了这种机制。第一个表达式 z₁ 是不安全的：如果我们在 Nat 命名空间未开放的上下文中使用它，Lean 会抱怨环境中没有名为 zero 的常量。相比之下，第二个表达式 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 构造器构建，其中第一个参数是函数表达式，第二个参数是表示函数的参数的表达式。

以下是两个示例。第一个只是将一个常量应用于另一个常量。第二个是递归定义，给出一个作为自然数函数的表达式。

def one := Expr.app (.const ``Nat.succ []) z -- Expr.const可以省略为.const
#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)

app 的变体 mkAppN 支持多参数应用。

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

最后两个函数的 #eval 输出表达式非常大，您可以自己试试看。

lambda 抽象

接下来，我们使用构造器 lam 来构造一个简单的函数，该函数接受任何自然数 x 并返回 Nat.zero。回忆一下lam构造器的类型是Name → Expr → Expr → BinderInfo → Expr，第一个Expr是Name对应的参数的变量类型，第二个Expr是函数体。参数 BinderInfo.default 表示 x 是一个显式参数（而不是隐式BinderInfo.implicit或类型类参数）。

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)

下面是更复杂的例子，还涉及到宇宙级别，这里是表示 List.map (λ x => Nat.add x 1) [] 的 Expr（分成几个定义以使其更具可读性）：

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. 利用 Expr.app 创建表达式 1 + 2
2. 利用 Lean.mkAppN 创建表达式 1 + 2
3. 创建表达式 fun x => 1 + x
4. [De Bruijn 索引] 创建表达式 fun a, fun b, fun c, (b * a) + c
5. 创建表达式 fun x y => x + y
6. 创建表达式 fun x, String.append "hello, " x
7. 创建表达式 ∀ x : Prop, x ∧ x
8. 创建表达式 Nat → String
9. 创建表达式 fun (p : Prop) => (λ hP : p => hP)
10. [Universe levels] 创建表达式 Type 6

MetaM

Lean 4 元编程 API 围绕着一系列单子（Monad）组织起来。主要有四个：

• CoreM 允许访问 环境，即程序当前点已声明或导入的事物集。
• MetaM 允许访问 元变量语境，即当前声明的元变量集及其赋值（如果有）。
• TermElabM 允许访问在繁饰过程中使用的各种信息。
• TacticM 允许访问当前目标列表。

这些单子相互扩展，因此 MetaM 操作也可以访问环境，而 TermElabM 计算可以使用元变量。还有其他单子不能很好地适应这个层次结构，例如CommandElabM 扩展了 MetaM，但与 TermElabM 没有扩展或被扩展的关系。

本章演示了 MetaM 单子中的许多有用操作。MetaM 特别重要，因为它允许我们为每个表达式赋予意义：环境（来自 CoreM）为 Nat.zero 或 List.map 等常量赋予意义，而元变量的语境为元变量和局部假设赋予意义。

import Lean

open Lean Lean.Expr Lean.Meta

元变量

概述

MetaM 中的「Meta」指的是元变量，所以我们应该先讨论一下。Lean 用户通常不会与元变量进行太多交互--至少不是主动为之--但它们在元程序中随处可见。有两种方式看待它们：作为表达式中的洞或作为目标。

首先从目标角度来看。当我们在 Lean 中证明事物时，我们总是围绕目标进行操作，例如

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

这些目标在内部由元变量表示。因此，每个元变量都有一个包含假设的局部语境（此处为[n : Nat, m : Nat]）和一个目标类型（此处为n + m = m + n）。元变量还有一个唯一的名称，比如 m，我们通常将它们呈现为 ?m。

要证成目标，我们必须给出目标类型的表达式 e。该表达式可能包含来自元变量局部语境的自由变量fvar，但不包含其他变量。在内部，以这种方式证成目标相当于指派元变量，写作 ?m := e。

元变量的第二个互补观点是它们表示表达式中的洞。例如，应用 Eq.trans 可能会生成两个如下所示的目标：

n m : Nat
⊢ n = ?x

n m : Nat
⊢ ?x = m

这里的 ?x 是另一个元变量 -- 是两个目标类型中的一个空洞，在证明过程中会被填充。?x 的类型是 Nat，它的局部语境是 [n : Nat, m : Nat]。现在，如果我们通过 rfl 解决第一个目标，那么 ?x 必须是 n，因此我们会赋值 ?x := n。关键是，这同样会影响第二个目标：它的目标将被“更新”为 n = m（实际上并不是完全更新，后续会说明）。元变量 ?x 在它出现的所有地方都代表相同的表达式。

通过元变量进行策略通信

策略通过元变量来传递当前的目标。为了理解这一点，我们来看一个简单（但稍显刻意）的证明例子：

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

进入策略模式后，我们的最终目标是生成一个类型为 f (f a) = a 的表达式，这个表达式可能会涉及假设 α、a、f 和 h。因此，Lean 生成了一个目标类型为 f (f a) = a 的元变量 ?m1，它的局部语境包含了这些假设。这个元变量被传递给第一个 apply 策略作为当前目标。

apply 策略尝试应用 Eq.trans 并成功，生成了三个新的元变量：

...
⊢ 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 现在是当前的目标。

此时，第二个 apply 策略接手。它接收 ?m2 作为当前目标，并将 h 应用于它。这成功了，并且策略赋值 ?m2 := h (f a)。这个赋值意味着 ?b 必须是 f a，因此策略也对 ?b := f a 进行赋值。被赋值的元变量不再被视为开放目标，所以剩下的唯一目标是 ?m3。

接着第三个 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)

这个例子还显示了元变量的两种视角 -- 作为表达式中的洞或作为目标 -- 是如何关联的：中间目标是最终证明项中的洞。

基本操作

让我们具体化这些概念。当我们在 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：元变量的种类。参见元变量种类（通常默认值是正确的）。
• userName：新元变量的用户可见名称。这是当元变量出现在目标中时会显示的名称。与 MVarId 不同，这个名称不需要唯一。

返回的 Expr 始终是一个元变量。我们可以使用 Lean.Expr.mvarId! 来提取唯一的 MVarId。（可以说，mkFreshExprMVar 应该只返回 MVarId。）

新元变量的局部语境继承自当前的局部语境，更多细节将在下一节介绍。如果你想要提供不同的局部语境，可以使用 Lean.Meta.mkFreshExprMVarAt。

元变量最初是未赋值的。要为它们赋值，可以使用 Lean.MVarId.assign，其类型如下：

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

这会使用赋值 ?mvarId := val 来更新 MetavarContext。你必须确保 mvarId 尚未被赋值（或者旧的赋值与新的赋值是定义相等的）。你还必须确保赋值的值 val 具有正确的类型。这意味着 (a) val 必须具有 mvarId 的目标类型，并且 (b) val 必须只包含 mvarId 局部语境中的自由变量。

如果你 #check Lean.MVarId.assign，你会看到它的实际类型比我们上面显示的更通用：它适用于任何可以访问 MetavarContext 的单子。但 MetaM 是其中最重要的单子，所以在本章中，我们专门讨论 assign 和类似函数的类型。

要获取关于已声明的元变量的信息，使用 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，其中 ?m 恰好被赋值为 0 = n，代表一个等式。换句话说，instantiateMVars 使我们的表达式与当前的元变量状态保持同步。

实例化元变量需要完整遍历输入表达式，所以它可能会有些昂贵。但如果输入表达式不包含任何元变量，instantiateMVars 基本上是免费的。由于这是常见情况，在大多数情况下广泛使用 instantiateMVars 是可以的。

在我们继续之前，这里有一个合成示例，展示了基本的元变量操作的使用。更自然的示例出现在接下来的部分中。

#eval show MetaM Unit from do
  -- 创建两个新元变量，类型为 `Nat`
  let mvar1 ← mkFreshExprMVar (Expr.const ``Nat []) (userName := `mvar1)
  let mvar2 ← mkFreshExprMVar (Expr.const ``Nat []) (userName := `mvar2)
  -- 创建一个新元变量，类型为 `Nat → Nat`。`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 "最初，所有的元变量都没被赋值："
  printMVars

  -- 赋值 `mvar1 : Nat := ?mvar3 ?mvar2`.
  mvar1.mvarId!.assign (.app mvar3 mvar2)
  IO.println "赋值mvar1之后："
  printMVars

  -- 赋值 `mvar2 : Nat := 0`.
  mvar2.mvarId!.assign (.const ``Nat.zero [])
  IO.println "赋值mvar2之后："
  printMVars

  -- 赋值 `mvar3 : Nat → Nat := Nat.succ`.
  mvar3.mvarId!.assign (.const ``Nat.succ [])
  IO.println "赋值mvar3之后："
  printMVars
-- 最初，所有的元变量都没被赋值：
--   meta1: ?_uniq.1
--   meta2: ?_uniq.2
--   meta3: ?_uniq.3
-- 赋值mvar1之后：
--   meta1: ?_uniq.3 ?_uniq.2
--   meta2: ?_uniq.2
--   meta3: ?_uniq.3
-- 赋值mvar2之后：
--   meta1: ?_uniq.3 Nat.zero
--   meta2: Nat.zero
--   meta3: ?_uniq.3
-- 赋值mvar3之后：
--   meta1: Nat.succ Nat.zero
--   meta2: Nat.zero
--   meta3: Nat.succ

局部语境

考虑表达式 e，它引用了唯一名称为 h 的自由变量：

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

这个表达式的类型是什么？答案取决于解释 e 的局部语境。一个局部语境可能声明 h 是类型为 Nat 的局部假设；另一个局部语境可能声明 h 是值为 List.map 的局部定义。

因此，表达式只有在为其设计的局部语境中解释时才有意义。如我们所见，每个元变量都有其自己的局部语境。因此，原则上，操作表达式的函数应该有一个附加的 MVarId 参数，指定解释表达式的目标。

这会很麻烦，所以 Lean 采用了稍微不同的方式。在 MetaM 中，我们始终可以访问一个环境局部语境，可以通过 Lean.getLCtx 函数获得，类型为：

getLCtx : MetaM LocalContext

所有涉及自由变量的操作都使用这个环境局部语境。

这种设置的缺点是我们始终需要更新环境局部语境以匹配当前处理的目标。为此，我们使用 Lean.MVarId.withContext，类型为

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

这个函数接受一个元变量 mvarId 和一个 MetaM 计算过程 c，功能是，设置环境语境为 mvarId 的局部语境，而后执行 c。典型的用例如下：

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

策略接收当前目标作为元变量 mvarId，并立即设置当前局部语境。do 块内的任何操作都会使用 mvarId 的局部语境。

一旦我们正确设置了局部语境，我们就可以操作自由变量。与元变量类似，自由变量由 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
  -- do something with the ldecl

循环在语境中的每个 LocalDecl 中迭代。isImplementationDetail 检查会跳过作为「实现细节」的局部假设，意味着它们是由 Lean 或策略为了记账引入的。它们不会显示给用户，策略应忽略它们。

此时，我们可以构建 assumption 策略的 MetaM 部分：

def myAssumption (mvarId : MVarId) : MetaM Bool := do
  -- 检查 `mvarId` 是否尚未被赋值。
  mvarId.checkNotAssigned `myAssumption
  -- 使用 `mvarId` 的局部语境。
  mvarId.withContext do
    -- 目标 target 是 `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 策略中使用了三个我们之前没有见过的函数：

• Lean.MVarId.checkNotAssigned：检查一个元变量是否尚未被赋值。myAssumption 参数是当前策略的名称，用于生成更友好的错误消息。
• Lean.Meta.isDefEq：检查两个定义是否在定义上相等。详细信息请参见定义等价部分。
• Lean.LocalDecl.toExpr：是一个辅助函数，用于构建对应于局部假设的 fvar 表达式。

延迟赋值

上述关于元变量赋值的讨论有一个遗漏：实际上有两种方式可以为元变量赋值。我们已经看到了一般的赋值方式，另一种称为延迟赋值（Delayed Assignments）。

这里我们不会详细讨论延迟赋值，因为它们对于编写策略并不常用。如果你想了解更多信息，可以参阅 Lean 标准库中的 MetavarContext.lean 文件中的注释。不过，它们带来了两个需要注意的复杂问题。

首先，延迟赋值使得 Lean.MVarId.isAssigned 和 getExprMVarAssignment? 成为可能导致问题的函数。这些函数只检查常规的赋值，因此你可能还需要使用 Lean.MVarId.isDelayedAssigned 和 Lean.Meta.getDelayedMVarAssignment?。

其次，延迟赋值打破了一种直观的约束。你可能假设在 instantiateMVars 的输出中仍然存在的元变量都是未赋值的，因为已赋值的元变量应该已经被替换掉了。但延迟赋值的元变量只有在其赋值的值不包含未赋值的元变量时才能被替换。因此，即使在 instantiateMVars 之后，延迟赋值的元变量仍然可能出现在表达式中。

元变量深度

元变量深度也是一个较为小众的特性，但有时会派上用场。每个元变量都有一个深度（一个自然数），并且 MetavarContext 也有一个相应的深度。Lean 只有在元变量的深度等于当前 MetavarContext 的深度时才会为其赋值。新创建的元变量继承 MetavarContext 的深度，因此默认情况下，每个元变量都是可赋值的。

这种机制在某些策略需要一些临时元变量，并且需要确保其他非临时元变量不会被赋值时会很有用。为了实现这一点，策略可以按照以下步骤进行：

1. 保存当前的 MetavarContext。
2. 增加 MetavarContext 的深度。
3. 执行必要的计算，可能会创建和赋值元变量。新创建的元变量位于当前 MetavarContext 的深度，因此可以被赋值。而旧的元变量位于较低的深度，因此不能被赋值。
4. 恢复保存的 MetavarContext，从而清除所有临时元变量并重置 MetavarContext 的深度。

这种模式封装在 Lean.Meta.withNewMCtxDepth 中。

计算

计算是依值类型理论的核心概念。项 2、Nat.succ 1 和 1 + 1 在计算出相同值的意义上是等价的。我们称它们为定义等价。从元编程的角度来看，问题在于定义等价的项可能由完全不同的表达式表示，但我们的用户通常期望适用于 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 构造函数的应用，它也可以是一个字面量。此外，注意 #eval 不仅可以用于计算项，还可以用于执行 MetaM 程序。

reduce 的可选填参数允许我们跳过表达式的某些部分。例如，reduce e (explicitOnly := true) 不会标准化表达式 e 中的任何隐式参数。这可以带来更好的性能：由于标准式可能非常庞大，跳过用户无须看到的表达式部分可能是个好主意。

#reduce 命令本质上就是 reduce 的一个应用：

#reduce someNumber
-- 5

透明度

Lean 4 元编程中的一个复杂但重要的细节是，任何给定的表达式都不只有一个标准式，而是根据给定的**透明度（transparency）**来确定其标准式。

透明度是 Lean.Meta.TransparencyMode 的一个枚举值，具有四个选项：reducible、instances、default 和 all。任何 MetaM 计算都可以访问一个环境透明度模式，使用 Lean.Meta.getTransparency 获取。

当前的透明度决定了在标准化过程中（如通过 reduce）哪些常量会被展开。（展开常量是指用其定义替换常量本身。）这四个设置逐步展开更多的常量：

• reducible：只展开带有 @[reducible] 属性的常量。注意，abbrev 是 @[reducible] def 的简写。
• instances：展开可归约 reducible 常量以及带有 @[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

我们从 reducible 透明度开始，它只展开 reducibleDef:

#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 可以在每种透明度下具有不同的标准式。

为什么要有这么多步骤？基本上是为了性能：如果我们允许标准化总是展开每个常量，诸如类型类搜索等操作的开销将变得无法接受。权衡在于我们必须为每个涉及标准化的操作选择适当的透明度。

弱头标准化（Weak Head Normalisation）

透明度解决了标准化中的一些性能问题。但更重要的是要认识到，对于许多情况，我们根本不需要完全标准化术语。假设我们正在构建一个自动拆分类型为 P ∧ Q 的假设的策略。如果 X 归约为 P ∧ Q，我们可能希望这个策略能够识别出假设 h : X。但是，如果 P 进一步归约为 Y ∨ Z，具体的 Y 和 Z 对我们来说并不重要，归约 P 就成了多余的工作。

这种情况非常常见，因此完全标准化的 reduce 实际上很少使用。Lean 中标准化的主力工具是 whnf，它将表达式简化为弱头标准式（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]

Lambda 表达式处于 WHNF：

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

全称量词（Foralls）处于 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  -- 假设元变量 `?x` 未被赋值，它处于 WHNF。
h 0 1   -- 假设 `h` 是一个局部假设，它处于 WHNF。

另一方面，以下是不处于 WHNF 的一些表达式。

如果当前透明度允许我们展开常量，那么常量的应用不处于 WHNF：

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

Lambda 表达式的应用不处于 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 -- 假设 `?x` 被赋值（例如赋值为 `Nat.add`），它的应用不处于 WHNF。
h 0 1  -- 假设 `h` 是一个局部定义（例如值为 `Nat.add`），它的应用不处于 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 调用。

定义等价

如前述，定义等价是基于计算的相等性。如果两个表达式 t 和 s 的标准式相等（在当前透明度下），它们就是定义等价（简写作defeq）的。

要检查两个表达式是否定义等价，可以使用 Lean.Meta.isDefEq，其类型签名为：

isDefEq : Expr → Expr → MetaM Bool

尽管定义等价是通过标准式定义的，但 isDefEq 实际上并不会计算参数的标准式，因为这代价太高。相反，它尝试以尽可能少的归约来「匹配」 t 和 s。这是一项启发式的任务，当启发式方法失效时，isDefEq 的计算代价可能非常高。在最坏的情况下，它可能不得不频繁地归约 s 和 t，最终它们仍会以标准式结束。不过，通常情况下，启发式方法是有效的，isDefEq 速度相对较快。

如果表达式 t 和 u 包含可赋值的元变量，isDefEq 可能会将这些元变量赋值，使得 t 与 u 定义等价。我们也可以说 isDefEq 合一（unify） 了 t 和 u；这种合一查询有时写作 t =?= u。例如，合一 List ?m =?= List Nat 成功并赋值 ?m := Nat。合一 Nat.succ ?m =?= n + 1 成功并赋值 ?m := n。合一 ?m₁ + ?m₂ + ?m₃ =?= m + n - k 失败，且没有元变量被赋值（尽管表达式之间存在「部分匹配」）。

isDefEq 是否将一个元变量视为可赋值由两个因素决定：

1. 元变量的深度必须等于当前 MetavarContext 的深度。参见元变量深度部分。
2. 每个元变量都有一个种类（kind）（MetavarKind 类型的值），其唯一目的是修改 isDefEq 的行为。可能的种类包括：
   • 自然：isDefEq 可以自由地赋值该元变量。这是默认值。
   • 合成：isDefEq 可以赋值该元变量，但如果可能，尽量避免赋值。例如，假设 ?n 是一个自然元变量，而 ?s 是一个合成元变量。当面对 ?s =?= ?n 的合一问题时，isDefEq 会赋值 ?n 而不是 ?s。
   • 合成不透明：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 还有一个变体 mkAppM'，它将第一个参数从 Name 改为 Expr，允许我们构造非常量表达式的应用。

不过，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 的函数。

Lambdas 和 Foralls

另一个常见的任务是构造涉及 λ 或 ∀ 绑定的表达式。假设我们想创建表达式 λ (x : Nat), Nat.add x x。一种方法是直接写出 lambda：

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 中除了最低层的函数外，其他函数都期望表达式不包含「松弛的 bvar」，其中松弛的意思是，如果它没有被同一个表达式中的某个绑定器绑定。（在 Lean 之外，这样的变量通常被称为「自由变量」。名称 bvar —— "bound variable"（绑定变量） —— 已经表明 bvar 永远不应是自由的。）

因此，如果在上面的例子中，我们用稍微高层的 mkAppM 替换 mkAppN，会导致运行时错误。按照局部封闭的约定，mkAppM 期望任何传递给它的表达式都不包含松弛的绑定变量，而 .bvar 0 恰好就是这样的松弛变量。

因此，Lean 的做法是通过两步构造带有绑定变量的表达式，而不是直接使用 bvar：

1. 构造表达式的主体（在我们的例子中是 lambda 的主体），使用临时的局部假设（fvar）来代替绑定变量。
2. 将这些 fvar 替换为 bvar，同时添加相应的 lambda 绑定器。

这个过程确保我们不需要在任何时候处理带有松弛 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

这里有两个新函数。首先，Lean.Meta.withLocalDecl 的类型为：

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

给定一个变量名称、绑定器信息和类型，withLocalDecl 构造一个新的 fvar 并将其传递给计算 k。在执行 k 时，该 fvar 在局部上下文中可用，但在之后会被删除。

第二个新函数是 Lean.Meta.mkLambdaFVars，其类型（忽略一些可选填参数）为：

mkLambdaFVars : Array Expr → Expr → MetaM Expr

此函数接受一个 fvar 数组和一个表达式 e。然后为每个 fvar x 添加一个 lambda 绑定器，并将 e 中的每个 x 替换为与新 lambda 绑定器对应的绑定变量。返回的表达式不再包含 fvar，这是很好的，因为当我们离开 withLocalDecl 上下文时，fvar 就会消失。（尽管名称中有 fvar，但我们也可以将 mvar 传递给 mkLambdaFVars。）

以下是这些函数的有用变体：

• 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 做一些操作。例如，当给定一个表达式 e : ∀ ..., U 时，apply 策略会比较 U 与当前目标，以确定是否可以应用 e。

为此，我们可以重复匹配类型表达式，逐步去除 ∀ 绑定器，直到得到 U。但这样会导致 U 包含未绑定的 bvar，如我们所见，这不是好事。相反，我们使用 Lean.Meta.forallTelescope，其类型为：

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

给定 type = ∀ (x₁ : T₁) ... (xₙ : Tₙ), U x₁ ... xₙ，此函数为每个 ∀ 绑定的变量 xᵢ 创建一个 fvar fᵢ，并在结论 U 中将每个 xᵢ 替换为 fᵢ。然后它调用计算 k，传递 fᵢ 和结论 U f₁ ... fₙ。在此计算中，fᵢ 会注册在局部语境中；计算结束后，它们会被删除（类似于 withLocalDecl）。

forallTelescope 有许多有用的变体：

• forallTelescopeReducing：与 forallTelescope 类似，但匹配是在计算后执行的。这意味着如果你有一个表达式 X，它不同于但定义等同于 ∀ x, P x，forallTelescopeReducing X 会将 X 解构为 x 和 P x。非归约的 forallTelescope 不会识别 X 为量化表达式。匹配是通过重复调用 whnf 来执行的，使用环境透明度。
• forallBoundedTelescope：类似于 forallTelescopeReducing（尽管名称中没有“reducing”），但在指定数量的 ∀ 绑定器之后停止。
• forallMetaTelescope，forallMetaTelescopeReducing，forallMetaBoundedTelescope：与相应的非 meta 函数类似，但绑定变量被替换为新的 mvar 而不是 fvar。与非 meta 函数不同，meta 函数在执行某些计算后不会删除新的元变量，因此这些元变量将无限期保留在环境中。
• lambdaTelescope，lambdaTelescopeReducing，lambdaBoundedTelescope，lambdaMetaTelescope：类似于相应的 forall 函数，但用于 λ 绑定器，而不是 ∀。

使用这些 telescope 函数之一，我们可以实现自己的 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} 无法应用于目标，目标类型为 {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 提供了两个基本操作：

• Lean.saveState : m s 返回当前状态的表示，其中 m 是我们所在的 monad，s 是状态类型。例如，对于 MetaM，saveState 返回一个包含当前环境、当前 MetavarContext 以及其他各种信息的 Lean.Meta.SavedState。
• Lean.restoreState : s → m Unit 接受先前保存的状态并恢复它。这实际上将编译器状态重置为之前的某个点。

通过这些操作，我们可以编写自己的 MetaM 版本的 try 策略：

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 局部语境的 fvars」。

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
   
     -- 创建 `mvar1` 类型为 `Nat`
     -- let mvar1 ← ...
     -- 创建 `mvar2` 类型为 `Nat`
     -- let mvar2 ← ...
     -- 创建 `mvar3` 类型为 `Nat`
     -- let mvar3 ← ...
   
     -- 指派 `mvar1` 为 `2 + ?mvar2 + ?mvar3`
     -- ...
   
     -- 指派 `mvar3` 为 `1`
     -- ...
   
     -- 实例化 `mvar1`，结果为表达式 `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. [元变量] 写一个策略 solve 来证明定理 red。

6. [计算] 写出下面表达式的一般形式： a) fun x => x 类型为 Bool → Bool b) (fun x => x) ((true && false) || true) 类型为 Bool c) 800 + 2 类型为 Nat

7. [计算] 说明 Expr.lit (Lean.Literal.natVal 1) 和 Expr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero []) 创建的 1 是定义等价的。

8. [计算] 确定下面的表达式是否是定义等价的。如果 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： a) 以非惯用方式：使用松弛绑定变量； b) 以惯用方式。 你可以在哪种方式中使用 Lean.mkAppN? 还有 Lean.Meta.mkAppM？

11. [构建表达式] 创建表达式 ∀ (yellow: Nat), yellow。

12. [构建表达式] 通过两种方式创建表达式 ∀ (n : Nat), n = n + 1： a) 以非惯用方式：使用松弛绑定变量； 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 是否定义等价（确保为你的元变量使用正确的类型或 Option.none）。使用 saveState 和 restoreState 来恢复元变量赋值。

语法

本章主要讨论在 Lean 中声明和操作语法的方法。由于操作语法的方式有很多种，我们不会在这里深入探讨，而是将相当一部分内容留到后续章节。

声明语法

声明辅助工具

有些读者可能熟悉 infix 或者 notation 命令，对于不熟悉的读者，以下是简要回顾：

import Lean

-- XOR, 输入 \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

-- 使用`notation`, "左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 命令声明一个左结合中缀二元运算符。此外 prefix 表示前缀。末尾的l表示左，对应地 infixr 意味着右结合。=>右侧表示符号所对应的二元函数。

notation 命令更自由：我们可以直接在语法定义中「提到」参数，并在右侧对它们进行操作。更棒的是，理论上我们可以通过 notation 命令创建从 0 到任意多个参数的语法，因此它也常被称为「mixfix」表示法。

留意：

• 我们在运算符周围留有空格：" ⊕ "，" LXOR "。这样做是为了当 Lean 以后漂亮打印我们的语法时，它也会在运算符周围使用空格，否则语法会显示为 l⊕r，而不是 l ⊕ r。

命令之后的 60 和 10 -- 这些表示运算符的优先级，意思是它们与参数绑定的强度，让我们来看看它的实际效果：

#eval true ⊕ false LXOR false -- false 这说明 ⊕ 符号的优先级比 LXOR 更高（60 > 10）
#eval (true ⊕ false) LXOR false -- false
#eval true ⊕ (false LXOR false) -- true

notation:precedence 的用法更能反映优先级具体实现的机制。例如：

#eval true LXOR false LXOR true -- true 这说明它也是左结合的
#eval (true LXOR false) LXOR true -- true
#eval true LXOR (false LXOR true) -- false

notation:10 代表 a LXOR b 一整块的优先级为10，也就是说可以看作 (a LXOR b):10 LXOR c。l:10 和 r:11 意为左侧参数的优先级必须至少为10，而右侧参数的优先级必须至少为11。这样就杜绝了右结合的可能，因为 a LXOR (b LXOR c):10 不满足 r:11。想要定义一个右结合符号，可以这样做：

notation:10 l:11 " LXORr " r:10 => (!l && r)
#eval true LXORr false LXORr true -- false

注意：如果符号没有显式指定优先级，它们会默认被赋予优先级0。

本节的最后一点说明：只要优先级允许, Lean 总是试图获得最长的匹配解析，这有三个重要的影响。首先，一个非常直观的例子，如果我们有一个右结合运算符 ^，Lean 看到类似 a ^ b ^ c 的表达式时，它会首先解析 a ^ b 成功，然后是 (a ^ b) ^ c 失败，最终解析为 a ^ (b ^ c) 成功。

其次，如果我们有一个符号，其优先级不足以确定表达式应如何加括号，例如：

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

像 a ~ b ~ c 这样的表达式将被解析为 a ~ (b ~ c)，因为 Lean 试图找到最长的解析方式。作为一条经验法则：如果优先级不明确，Lean 会默认为右结合。

#eval 5 ~ 3 ~ 3 -- 结果为 5，因为这被解析为 5 - (3 - 3)

最后，如果我们定义了重叠的符号，例如：

-- 定义 `a ~ b mod rel` 表示 a 和 b 在某种等价关系 rel 下是等价的
notation:65 a:65 " ~ " b:65 " mod " rel:65 => rel a b

Lean 会优先选择这种符号，而不是先解析为上面定义的 a ~ b，然后因为不知道如何处理 mod 和等价关系参数而报错。

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

这也是因为 Lean 正在寻找最长的解析方式，在这种情况下，还包括了 mod 和等价关系参数。

自由形式的语法声明

通过上面的 infix 和 notation 命令，你已经可以声明相当丰富的普通数学语法了。然而，Lean 也允许你引入任意复杂的语法。这是通过两个主要命令 syntax 和 declare_syntax_cat 实现的。syntax 命令允许你为已经存在的「语法类别」添加一个新的语法规则。最常见的语法类别有：

• term，这个类别将在繁饰章节中详细讨论，目前你可以将其理解为「任何可求值的东西」
• command，这是用于顶级命令的类别，如 #check、def 等。
• TODO: ...

让我们来看看它的实际效果：

syntax "MyTerm" : term

现在我们可以用 MyTerm 替代诸如 1 + 1 这样的表达式，它在语法上是有效的，但这并不意味着代码可以编译成功，这只是表示 Lean 解析器可以理解它：

#check_failure MyTerm
-- elaboration function for 'termMyTerm' has not been implemented  MyTerm
-- 尚未实现 'termMyTerm' 的繁饰函数

注意：#check_failure 命令允许以不报错的方式标记类型错误的表达式。

繁饰函数，即将这种语法转换为 Expr 类型，是繁饰章节的主题。

notation 和 infix 命令是一种方便的工具，将语法声明与宏定义捆绑在一起（关于宏的更多内容，请参见宏章节），其中 => 左侧的内容声明了语法。 之前提到的关于优先级的所有原则同样适用于 syntax。

当然，我们也可以在自己的声明中涉及其他语法，以构建语法树。例如，我们可以尝试构建一个简单的布尔表达式语言：

namespace Playground2

-- `scoped` 修饰符确保语法声明仅在该 `namespace` 中有效，以便我们在本章中不断修改它
scoped syntax "⊥" : term -- ⊥ 表示 false
scoped syntax "⊤" : term -- ⊤ 表示 true
scoped syntax:40 term " OR " term : term
scoped syntax:50 term " AND " term : term
#check_failure ⊥ OR (⊤ AND ⊥) -- 繁饰函数尚未实现，但解析通过

end Playground2

当下 AND 和 OR 操作的左右侧可以使用任意的 term。如果我们希望限制操作的「定义域」，例如仅接受（我们当下定义的）布尔表达式，我们将需要额外声明自己的语法类别。这可以通过 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

现在我们正在使用自己的语法类别，已经完全与系统的其他部分断开连接。这些不再是 term 了：

#check ⊥ AND ⊤ -- 期望是 `term`

但我们希望 boolean_expr 仍是 term 的一部分，除非你想重新从头开始写一切。实际上通常我们需要使用新的语法扩展已有的语法类别。也就是把 boolean_expr 重新嵌入到 term 类别中：

syntax "[Bool|" boolean_expr "]" : term
#check_failure [Bool| ⊥ AND ⊤] -- 繁饰函数尚未实现，但解析通过

语法组合器

更复杂的语法通常需要系统内置一些基本的语法操作，包括：

• 无语法类别的辅助解析器（即不可扩展）
• 选择（A或B）
• 重复（AAAAAA……）
• 可选项（可有可无）

虽然所有这些操作都可以通过语法类别进行编码，但有时会显得非常冗杂，因此 Lean 提供了更简便的方式来实现这些操作。

为了展示这些操作的实际效果，我们将简要定义一个简单的二进制表达式语法。

无语法类别

首先，声明不属于任何语法类别的命名解析器与普通的 def 非常相似：

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

这些命名解析器可以像上面的语法类别一样在相同位置使用，唯一的区别是它们不可扩展。 即它们在语法声明中直接展开，而我们不能像定义语法类别那样为它们定义新的模式。 此外，Lean 内置了一些非常有用的命名解析器，最著名的是：

• str 表示字符串字面量
• num 表示数字字面量
• ident 表示标识符
• … TODO: 完善列表或链接到编译器文档

选择

接下来，我们希望声明一个能够理解数字的解析器，二进制数字要么是 0 要么是 1，因此我们可以这样写：

syntax binDigit := binZero <|> binOne

其中 <|> 运算符实现了「接受左侧或右侧」的行为。我们还可以将它们链式组合，以实现能够接受任意多个复杂解析器的组合。

重复

现在，我们将定义二进制数的概念，通常二进制数会直接写作一串数字，但为了展示重复特性，我们将使用逗号分隔的方式：

-- "+" 表示「一个或多个」，为了表示「零个或多个」，可以使用 "*"
-- "," 表示 `binDigit` 之间的分隔符，如果省略，则默认分隔符为一个空格
syntax binNumber := binDigit,+

由于我们可以将命名解析器用于语法类别，我们现在可以轻松地将其添加到 term 类别：

syntax "bin(" binNumber ")" : term
#check bin(Z, O, Z, Z, O) -- 繁饰函数尚未实现，但解析通过
#check bin() -- 解析失败，因为 `binNumber` 是「一个或多个」：期望 'O' 或 'Z'

syntax binNumber' := binDigit,* -- 注意 *
syntax "emptyBin(" binNumber' ")" : term
#check_failure emptyBin() -- 繁饰函数尚未实现，但解析通过

注意，我们并不限于每个解析器只能使用一个语法组合器，我们也可以一次性编写所有内容：

syntax "binCompact(" ("Z" <|> "O"),+ ")" : term --使用括号来组合
#check_failure binCompact(Z, O, Z, Z, O) -- 繁饰函数尚未实现，但解析通过

可选项

作为最后一个功能，让我们添加一个可选填的字符串注释，用来解释所声明的二进制字面量：

-- (...)? 表示括号中的部分是可有可无的
syntax "binDoc(" (str ";")? binNumber ")" : term
#check_failure binDoc(Z, O, Z, Z, O) -- 繁饰函数尚未实现，但解析通过
#check_failure binDoc("mycomment"; Z, O, Z, Z, O) -- 繁饰函数尚未实现，但解析通过

操作语法

如前所述，本章不会详细讨论如何教 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

我们逐个解释构造器：

• missing 用于表示 Lean 编译器无法解析的内容，这使得 Lean 能在文件的某个部分存在语法错误时，仍能从错误中恢复并继续解析其他部分。基本上，我们对这个构造器不太关心。
• node，顾名思义，是语法树中的一个节点。它有一个所谓的 kind : SyntaxNodeKind，其中 SyntaxNodeKind 就是一个 Lean.Name。基本上，每个 syntax 声明都会自动生成一个 SyntaxNodeKind（我们也可以通过 syntax (name := foo) ... : cat 明确指定名称），这样我们可以告诉 Lean「这个函数负责处理这个特定的语法构造」。此外，像所有树中的节点一样，它有子节点，在这种情况下是 Array Syntax。
• atom 表示语法层次结构中除一个例外的所有对象。例如，我们之前的操作符 ⊕ 和 LXOR 将被表示为 atom。
• ident 是前述规则的例外。ident 和 atom 的区别也很明显：标识符有一个 Lean.Name 而不是表示它的 String。为什么 Lean.Name 不是 String 这一点与一个叫做宏卫生的概念有关，我们将在宏章节中详细讨论。现在可以把它们看作基本等价。

构造新的 Syntax

现在我们知道了 Lean 中语法的表示方法，当然可以编写生成这些归纳树的程序，然而这样做会非常繁琐，显然不是我们想要的。幸运的是，Lean 中有相当大量的API隐藏在 Lean.Syntax 命名空间中，可以供我们探索：

open Lean
#check Syntax -- Syntax. autocomplete

用于创建 Syntax 的有趣函数是那些以 Syntax.mk* 开头的函数，它们允许我们创建非常基础的 Syntax 对象，如 ident，也可以创建更复杂的对象，比如 Syntax.mkApp，我们可以用它来创建 Syntax 对象，相当于将第一个参数中的函数应用于第二个参数中的参数列表（所有都作为 Syntax 传递）。让我们看一些例子：

-- 名字字面量使用反引号 ` 表示
#eval Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"] -- 这是 `Nat.add 1 1` 的语法
#eval mkNode `«term_+_» #[Syntax.mkNumLit "1", mkAtom "+", Syntax.mkNumLit "1"] -- 这是 `1 + 1` 的语法

-- 注意 `«term_+_»` 是自动生成的用于加法语法的 SyntaxNodeKind

大家都不喜欢这种创建 Syntax 的方式。然而，这样做涉及一些机器的工作，尤其是为了让它漂亮且正确（大部分是为了正确）。这些内容将在宏章节中详细解释。

Syntax 中的匹配

正如构造 Syntax 是一个重要主题，特别是对于宏而言，匹配语法同样（甚至更）有趣。幸运的是，我们不必直接在归纳类型本身上进行匹配：相反，我们可以使用所谓的「语法模式」。它们非常简单，其语法就是 `(我想匹配的语法)。我们来看一个例子：

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 的类型是 TSyntax term，而不是 Syntax。虽然我们正在对 Syntax 进行模式匹配，正如我们在构造函数中所看到的，Syntax 仅由不是 TSyntax 的类型组成，那么这里发生了什么？基本上，`() 语法足够智能，能够识别我们要匹配的语法可能来自的最通用的语法类别（在这个例子中是 term）。然后它将使用参数化为该语法类别名称的类型化语法类型 TSyntax。这不仅让程序员更容易看清正在发生的事情，还带来了其他好处。例如，如果我们在下一个例子中将语法类别限制为 num，Lean 将允许我们直接在结果的 TSyntax num 上调用getNat，而不需要模式匹配或担心潜在错误。

-- 现在我们还明确标记了函数以操作 term 语法
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`，对我们来说重要的是它允许我们使用 `` `(arith| (12 + 3) - 4) `` 符号来构造 `Syntax`，而不仅仅是能够像这样进行匹配。
def test : Elab.TermElabM Nat := do
  let stx ← `(arith| (12 + 3) - 4)
  pure (denoteArith stx)

#eval test -- 11

随意玩弄这个例子，并根据需要扩展它。接下来的章节主要会讨论以某种方式操作 Syntax 的函数。

更复杂的例子

使用类型类进行符号定义

我们可以使用类型类来添加通过类型而不是语法系统可扩展的符号，这正是 Lean 中 + 如何使用类型类 HAdd 和 Add 以及其他常见运算符被通用定义的方式。

例如，我们可能想要为子集符号定义一个通用符号。第一步是定义一个捕捉我们想要构建符号的函数的类型类。

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 -- 空集没有成员

绑定

由于在 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} 并省略绑定变量周围的括号，参考宏章节。

练习

1. 创建一个「紧急减法」符号💀，使得 5 * 8 💀 4 返回 20，而 8 💀 6 💀 1 返回 3。

   a) 使用 notation 命令。 b) 使用 infix 命令。 c) 使用 syntax 命令。

   提示：在 Lean 4 中，乘法定义为 infixl:70 " * " => HMul.hMul。

2. 考虑以下语法类别：term、command、tactic；以及下面给出的 3 个语法规则。利用这些新定义的语法。

     syntax "good morning" : term
     syntax "hello" : command
     syntax "yellow" : tactic
   

3. 创建一个 syntax 规则，可以接受以下命令：

   • red red red 4
   • blue 7
   • blue blue blue blue blue 18

   （所以，要么是所有的 red 后面跟着一个数字；要么是所有的 blue 后面跟着一个数字；red blue blue 5 - 不应该有效。）

   使用以下代码模板：

   syntax (name := colors) ...
   -- 繁饰函数将语法注入语义
   @[command_elab colors] def elabColors : CommandElab := λ stx => Lean.logInfo "success!"
   

4. 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) ...
   -- 繁饰函数将语法注入语义
   @[command_elab help] def elabHelp : CommandElab := λ stx => Lean.logInfo "success!"
   

5. 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) ...
   -- 繁饰函数将语法注入语义
   @[term_elab bigsumin] def elabSum : TermElab := λ stx tp => return mkNatLit 666
   

   提示：使用 Std.ExtendedBinder.extBinder 解析器。 提示：你需要在 Lean 项目中安装 Std4 才能使这些导入生效。

宏

什么是宏

Lean 中的宏是 Syntax → MacroM Syntax 类型的函数。MacroM 是宏的单子，它允许宏拥有一些静态保证，我们将在下一节中讨论这些保证，目前你可以暂时忽略它。

宏作为特定语法声明的处理器使用 macro 属性来声明。编译器会在实际分析输入之前自动将这些函数应用到语法上。这意味着我们只需声明一个特定名称的语法，并将一个类型为 Lean.Macro 的函数绑定到它上面。让我们尝试重现 Syntax 章节中的 LXOR 符号：

import Lean

open Lean

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

@[macro lxor] def lxorImpl : Macro
  | `($l:term LXOR $r:term) => `(!$l && $r) -- 我们可以使用引号机制在宏中创建 `Syntax`
  | _ => Macro.throwUnsupported

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

这非常简单！宏可以使用 Macro.throwUnsupported 函数表示它“不认为自己负责处理这种语法”。在这个例子中，它仅仅用于填充一个永远不应该被触发的通配符模式。

事实上，如果我们愿意，我们可以为相同的语法编写多个宏。它们将一个接一个地尝试（后编写的宏具有更高优先级）直到某个宏要么抛出真正的错误（使用 Macro.throwError），要么成功，也就是说它没有 Macro.throwUnsupported。让我们看看这个功能的实际效果：

@[macro lxor] def lxorImpl2 : Macro
  -- 处理左右两侧为这些特定标识符的特殊情况
  | `(true LXOR true) => `(true)
  | _ => Macro.throwUnsupported

#eval true LXOR true -- true，由新宏处理
#eval true LXOR false -- false，仍由旧宏处理

这种能力显然非常强大！在不经过深思熟虑的情况下不要轻易使用它，因为它可能在编写代码时引入奇怪的行为。以下例子展示了这种奇怪的行为：

#eval true LXOR true -- true，由新宏处理

def foo := true
#eval foo LXOR foo -- false，由旧宏处理，毕竟标识符的名字不同

如果不知道这个宏是如何实现的，那么调试这个问题的开发者可能会非常困惑。

关于何时应该使用宏而不是其他机制（如繁饰），经验法则是：当你开始构建真正的逻辑时，例如上面第二个宏中的逻辑，它很可能不应该是一个宏，而应该是一个繁饰器（繁饰器将在繁饰章节中进行讲解）。这意味着理想情况下，我们希望将宏用于简单的语法到语法的转换，人类也可以轻松地手动编写这些转换，但可能嫌麻烦。

简化宏声明

现在我们了解了宏的基础知识以及如何编写宏，我们可以来看一些稍微自动化的方式（事实上，接下来要介绍的所有方式都是通过宏自己实现的）。

首先是 macro_rules，它基本上是对我们上面编写的函数的语法糖，例如：

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

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

它自动完成了许多事情：

• 语法声明的名称
• macro 属性的注册
• throwUnsupported 的通配符

除此之外，它就像一个使用模式匹配语法的函数一样工作，理论上我们可以在右侧编写任意复杂的宏函数。

如果你觉得这还不够简短，可以使用 macro 语法糖：

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

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

如你所见，macro 已经非常接近 notation 了：

• 它为我们进行了语法声明
• 它自动生成了一个 macro_rules 风格的函数来匹配语法

当然，它们之间也有一些区别：

• notation 仅限于 term 语法类别
• notation 不能在右侧包含任意的宏代码

Syntax 引号

基础知识

到目前为止，我们使用了 `(foo $bar) 语法来创建和匹配 Syntax 对象，但现在是时候进行完整的解释了，因为它在进阶的语法中至关重要。

首先我们称 `() 语法为 Syntax 引号。当我们将变量插入到语法引号中，如：`($x)，我们称 $x 部分为反引号（anti-quotation）。当我们像这样插入 x 时，要求 x 的类型为 TSyntax y，其中 y 是某种语法类别的名称。Lean 编译器实际上足够智能，能够推断出允许在此处使用的语法类别。因此，你有时可能会看到如下形式的错误：

application type mismatch 应用类型不匹配
  x.raw
argument 参数
  x
has type 类型为
  TSyntax `a : Type
but is expected to have type 但期望的类型为
  TSyntax `b : Type

如果你确信来自 a 语法类别的元素可以用作 b，你可以声明如下形式的类型转换：

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

这将允许 Lean 自动执行类型转换。如果你发现你的 a 不能在此处替代 b，恭喜你，你刚刚发现了你的 Syntax 函数中的一个 bug。类似于 Lean 编译器，你还可以声明特定于某些 TSyntax 变体的函数。例如，如我们在语法章节中所见，已经存在如下函数：

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

此函数不会发生错误，因为我们知道传递给它的 Syntax 是一个数字字面量，因此可以自然地转换为 Nat。

如果我们在模式匹配中使用反引号语法，如前面提到的，它将为我们提供类型为 TSyntax y 的变量 x，其中 y 是适合我们模式匹配位置的语法类别名称。如果出于某种原因我们想要将字面量 $x 插入到 Syntax 中，例如用于创建宏的宏，我们可以使用 `($$x) 来取消反引号（类似C等语言中的两次反斜杠转义）。

如果我们希望指定 x 的语法类型，可以使用 `($x:term)，其中 term 可以替换为任何其他有效的语法类别（如 command）或解析器（如 ident）。

到目前为止，这只是对我们在语法章节中以及本章至今所见的直观概念的更正式解释，接下来我们将讨论一些更高级的反引号用法。

高级反引号

为了方便起见，我们还可以以类似格式字符串的方式使用反引号：`($(mkIdent `c)) 与 let x := mkIdent `c; `($x) 是等价的。

此外，有时我们处理的并不是基本的 Syntax，而是更复杂的数据结构中包含的 Syntax，最典型的是 Array (TSyntax c) 或 TSepArray c s。其中 TSepArray c s 是一个 Syntax 特定类型，它是当我们在使用分隔符 s 来分隔 c 类别的元素时通过模式匹配得到的。例如，如果我们使用 $xs,* 进行匹配，xs 的类型将是 TSepArray c ","。而匹配时没有特定分隔符（即空白）时，如 $xs*，我们将得到 Array (TSyntax c)。

如果我们正在处理 xs : Array (TSyntax c) 并且想要将其插入到引号中，有两种主要方法可以实现：

1. 使用分隔符插入，最常见的是逗号：`($xs,*)。这也是插入 TSepArray c ","" 的方式。
2. 直接无分隔符插入（TODO）：`()

-- 如果可能的话，在语法上从元组中切掉第一个元素
syntax "cut_tuple " "(" term ", " term,+ ")" : term

macro_rules
  -- 切掉一对中的一个元素是不可能的，因为这不会形成元组
  | `(cut_tuple ($x, $y)) => `(($x, $y))
  | `(cut_tuple ($x, $y, $xs,*)) => `(($y, $xs,*))

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

本节的最后一部分将介绍所谓的「反引号拼接」。反引号拼接有两种类型，首先是可选拼接。例如，我们可能会声明一个带有可选填参数的语法，比如我们自己的 let。（现实例子是，仿写另一种函数式语言中的 let）：

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

这里涉及一个可选填参数 (" : " term)?，用户可以通过它定义左边项的类型。按照我们目前掌握的方法，我们需要编写两个 macro_rules，一个处理带可选填参数的情况，一个处理不带的情况。然而，语法翻译的其余部分在有无可选填参数的情况下完全相同，因此我们可以使用拼接来同时定义两种情况：

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

这里的 $[...]? 部分就是拼接，它的作用基本上是说「如果这部分语法不存在，那么就忽略右侧涉及的反引号变量」。所以现在我们可以在无论有无类型说明的情况下运行这个语法：

#eval mylet x := 5 in x - 10 -- 0，因为 `Nat` 的减法行为
#eval mylet x : Int := 5 in x - 10 -- -5，因为现在它是 `Int` 类型

第二种拼接可能会让读者联想到例如在 Python 中看到的列表推导式。演示：

-- 对每个列表元素执行函数
syntax "foreach " "[" term,* "]" term : term

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

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

在这种情况下，$[...],* 部分是拼接。在匹配部分，它会尝试根据我们定义的模式进行重复匹配（根据我们指定的分隔符）。然而，不同于常规的分隔符匹配，它不会返回 Array 或 SepArray，而是允许我们在右侧写另一个拼接，每次匹配到我们指定的模式时，该拼接都会被计算，并使用每次匹配中的特定值。

卫生问题及其解决方案

如果你熟悉其他语言（如 C）的宏系统，你可能已经听说过所谓的宏卫生问题。宏卫生问题指的是，当宏引入的标识符与它包含的某些语法中的标识符发生冲突时。例如:

-- 应用这个宏会生成一个绑定了新标识符 `x` 的函数。
macro "const" e:term : term => `(fun x => $e)

-- 但是 `x` 也可以由用户定义
def x : Nat := 42

-- 编译器在替换 `$e` 时应该使用哪个 `x`？
#eval (const x) 10 -- 42

鉴于宏只执行语法转换，你可能会预期上面的 eval 返回 10 而不是 42：毕竟，结果语法应该是 (fun x => x) 10。虽然这显然不是作者的本意，但在更原始的宏系统（如 C 语言的宏系统）中，这就是会发生的情况。那么 Lean 是如何避免这些宏卫生问题的呢？你可以在出色的论文 Beyond Notations 中详细阅读 Lean 的这个思想和实现。我们这里只做一个概述，因为具体细节对实际使用没有那么大的意义。

《Beyond Notations》提出的思想归结为一个叫做「宏作用域」（macro scopes）的概念。每当一个新的宏被调用时，一个新的宏作用域（基本上是一个唯一的数字）会被添加到当前所有活跃宏作用域的列表中。当目前的宏引入一个新标识符时，实际上被添加的是以下形式的标识符：

<实际名称>._@.(<模块名称>.<作用域>)*.<模块名称>._hyg.<作用域>

例如，如果模块名称是 Init.Data.List.Basic，名称是 foo.bla，宏作用域是 [2, 5]，我们得到的标识符是：

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

由于宏作用域是唯一的数字，附加在名称末尾的宏作用域列表将在所有宏调用中保持唯一，因此像上面那样的宏卫生问题是不可能出现的。

如果你想知道为什么除了宏作用域之外还有其他内容，那是因为我们可能需要组合来自不同文件/模块的作用域。当前处理的主模块总是最右边的一个。这种情况可能发生在我们执行从当前文件导入的文件中生成的宏时。例如：

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

末尾的 _hyg 分隔符只是为了提高 Lean.Name.hasMacroScopes 函数的性能 -- 这种格式没有它也能工作。

以上有很多技术细节。你不需要理解它们也可以使用宏，只需记住 Lean 不会允许像 const 示例中那样的名称冲突问题。

请注意，这适用于所有使用语法引用引入的名称，也就是说，如果你编写了一个生成以下代码的宏：

`(def foo := 1)

用户将无法访问 foo，因为这个名称会受到卫生规则的影响。幸运的是，有一种方法可以绕过这个问题。你可以使用 mkIdent 来生成一个原始标识符，例如：

`(def $(mkIdent `foo) := 1)

在这种情况下，它将不会受宏卫生规则影响，用户可以访问该名称。

MonadQuotation 和 MonadRef

基于上述宏卫生机制的描述，出现了一个有趣的问题：我们如何知道当前的宏作用域列表到底是什么？毕竟，在上面定义的宏函数中，并没有显式地传递这些作用域的过程。正如在函数式编程中常见的那样，当我们需要跟踪一些额外的状态（比如宏作用域）时，通常会使用一个单子来处理。在这里也是如此，不过有一点小小的不同。

这里并不是仅为单个 MacroM 单子实现这个功能，而是通过一个叫做 MonadQuotation 的类型类抽象出跟踪宏作用域的通用概念。这样，任何其他单子只需实现这个类型类，就可以轻松提供这种带有卫生性的 Syntax 创建机制。

这也是为什么我们虽然可以使用 `(syntax) 对语法进行模式匹配，但不能在纯函数中直接用相同的语法创建 Syntax 的原因：因为没有涉及到实现了 MonadQuotation 的 Monad 来跟踪宏作用域。

现在让我们简要看看 MonadQuotation 类型类：

namespace Playground

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

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

end Playground

由于 MonadQuotation 基于 MonadRef，我们先来看看 MonadRef。其核心思想非常简单：MonadRef 作为 Monad 类型类的扩展，它提供了以下功能：

• 通过 getRef 获取对 Syntax 值的引用。
• 使用 withRef 在新的 Syntax 引用下执行某个 monadic 操作 m α。

单独来看，MonadRef 并不是特别有趣，但一旦与 MonadQuotation 结合，它就有了意义。

如你所见，MonadQuotation 扩展了 MonadRef，并增加了三个新函数：

• getCurrMacroScope：获取最新创建的 MacroScope。
• getMainModule：获取主模块的名称。这两个函数用于创建上面提到的带有卫生性的标识符。
• withFreshMacroScope：计算下一个宏作用域，并运行某些执行语法引用的计算 m α，以避免名称冲突。虽然这主要用于内部在新宏调用发生时调用，但在我们编写自己的宏时有时也有用，比如当我们反复生成某些语法块时，想要避免名称冲突。

MonadRef 在这里的作用是 Lean 需要一种方式来向用户指示某些位置的错误。一个没有在 Syntax 章节介绍的内容是，类型为 Syntax 的值实际上携带了它们在文件中的位置信息。当检测到错误时，通常会绑定到一个 Syntax 值上，以便 Lean 能够在文件中准确指示错误位置。

当使用 withFreshMacroScope 时，Lean 会将 getRef 的结果位置应用到每个引入的符号上，从而生成更准确的错误位置信息，而不是没有位置信息。

为了看到错误定位的实际效果，我们可以写一个小的宏来展示这个功能：

syntax "error_position" ident : term

macro_rules
  | `(error_position all) => Macro.throwError "Ahhh"
  -- `%$tk` 语法给 `%` 之前的东西命名为 `tk`，本例中是 `error_position`。
  | `(error_position%$tk first) => withRef tk (Macro.throwError "Ahhh")

#check_failure error_position all -- 错误在 `error_position all` 处显示
#check_failure error_position first -- 错误仅在 `error_position` 处显示

显然，以这种方式控制错误的位置对提供良好的用户体验非常重要。

项目示例

作为本节的最终迷你项目，我们将以稍微更高级的方式重建语法章节中的算术 DSL，这次我们将使用宏来实现，从而可以将其完全集成到 Lean 语法中。

declare_syntax_cat arith

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

macro_rules
  | `([Arith| $x:num]) => `($x)
  | `([Arith| $x:arith + $y:arith]) => `([Arith| $x] + [Arith| $y]) -- 递归宏是可以实现的
  | `([Arith| $x:arith - $y:arith]) => `([Arith| $x] - [Arith| $y])
  | `([Arith| ($x:arith)]) => `([Arith| $x])

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

如果你想构建更复杂的内容，比如包含变量的表达式，或许可以考虑使用宏来构建一个归纳类型。一旦你将算术表达式作为归纳类型，你就可以编写一个函数，该函数接受某种形式的变量赋值并对给定表达式进行求值。你还可以尝试使用一些特殊的语法将任意 term 嵌入到你的算术语言中，或者发挥你的想象力做其他事情。

更复杂的示例

绑定（续）

正如在语法章节中所承诺的，这里是绑定 2.0。我们将从重新引入集合理论开始：

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

-- 集成到已经存在的成员符号类中
instance : Membership α (Set α) where
  mem := Set.mem

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

-- 基本的 "所有满足某条件的元素" 函数，用于符号表示法
def setOf {α : Type} (p : α → Prop) : Set α := p

本节的目标是允许 {x : X | p x} 和 {x ∈ X, p x} 的表示法。原则上，有两种方法可以实现：

1. 为每种可能的绑定变量的方式定义语法和宏
2. 定义一种可以在其他绑定构造（例如 Σ 或 Π）中复用的绑定符号语法类别，并为 { | } 的情况实现宏

在本节中，我们将采用方法 2，因为它更易于复用。

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

现在我们来定义两个我们感兴趣的绑定符号构造：

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

最后，我们为语法扩展定义宏：

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

以下是使用新语法的示例：

-- 旧示例，使用更好的语法：
#check { x : Nat | x ≤ 1 } -- setOf fun x => x ≤ 1 : Set Nat

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

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

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

拓展阅读

如果你想了解更多关于宏的信息，可以阅读：

• API 文档：待补充链接
• 源代码：Init.Prelude 的底层部分，如你所见，由于它们在构建语法中非常重要，因此在 Lean 中被很早声明
• 前面提到的论文 Beyond Notations

繁饰

繁饰器（Elaborator）是负责将面向用户的 Syntax 转换为编译器可以处理的内容的组件。大多数情况下，这意味着将 Syntax 转换为 Expr，但也有其他用例，例如 #check 或 #eval。因此，繁饰器是一大块代码，代码位于这里。

繁饰命令

命令（Command）是最高层级的 Syntax，一个 Lean 文件由一系列命令组成。最常用的命令是声明，例如：

• def
• inductive
• structure

但也有其他命令，最著名的是 #check、#eval 等。所有命令都属于 command 语法类别，因此要声明自定义命令，必须在该类别中注册其语法。

为命令赋予意义

下一步是为语法赋予语义。对于命令，这是通过注册一个所谓的命令繁饰器完成的。

命令繁饰器的类型是 CommandElab，或者说 Syntax → CommandElabM Unit。它们的作用是获取表示用户想要调用的命令的 Syntax，并在 CommandElabM 单子上产生某种副作用，毕竟返回值始终是 Unit。CommandElabM 单子有四种主要的副作用：

1. 通过 Monad 扩展 MonadLog 和 AddMessageContext 向用户记录消息，例如 #check。这是通过 Lean.Elab.Log 中的函数完成的，其中最著名的是：logInfo、logWarning 和 logError。
2. 通过 Monad 扩展 MonadEnv 与 Environment 交互。这里存储了编译器的所有相关信息，所有已知的声明、它们的类型、文档字符串、值等。当前环境可以通过 getEnv 获取，并在修改后通过 setEnv 设置。请注意，像 addDecl 这样的 setEnv 包装器通常是向 Environment 添加信息的正确方式。
3. 执行 IO，CommandElabM 能够运行任何 IO 操作。例如，从文件中读取内容并根据其内容执行声明。
4. 抛出错误，因为它可以运行任何类型的 IO，所以它自然可以通过 throwError 抛出错误。

此外，CommandElabM 还支持其他一系列 Monad 扩展：

• MonadRef 和 MonadQuotation 用于像宏中的 Syntax 引用
• MonadOptions 用于与选项框架交互
• MonadTrace 用于调试跟踪信息
• TODO：还有一些其他的扩展，虽然不确定它们是否相关，可以参见 Lean.Elab.Command 中的实例。

命令繁饰

现在我们已经了解了命令繁饰器的类型，接下来简要看看繁饰过程是如何实际工作的：

1. 检查是否有任何宏可以应用于当前的 Syntax。如果有适用的宏，并且没有抛出错误，那么生成的 Syntax 将再次作为命令递归繁饰。
2. 如果没有可用的宏，我们将使用 command_elab 属性，搜索为我们正在繁饰的 Syntax 的 SyntaxKind 注册的所有 CommandElab。
3. 然后依次尝试所有这些 CommandElab，直到其中一个没有抛出 unsupportedSyntaxException，Lean 用这种方式表示繁饰器对这个特定的 Syntax 结构「负有责任」。请注意，它仍然可以抛出常规错误，以向用户表明某些地方出了问题。如果没有找到负责的繁饰器，那么命令繁饰将以 unexpected syntax 错误消息终止。

如你所见，这个过程背后的总体思路与普通宏扩展非常相似。

创建我们自己的命令

现在我们已经知道什么是 CommandElab 以及它们的使用方式，我们可以开始编写自己的命令了。正如我们上面所学的，步骤如下：

1. 声明语法
2. 声明繁饰器
3. 通过 command_elab 属性要求繁饰器负责该语法。

例子：

import Lean

open Lean Elab Command Term Meta

syntax (name := mycommand1) "#mycommand1" : command -- 声明语法

@[command_elab mycommand1]
def mycommand1Impl : CommandElab := fun stx => do -- 声明并注册繁饰器
  logInfo "Hello World"

#mycommand1 -- Hello World

你可能认为这有点模板化，Lean 的开发者们也这么认为，所以他们为此添加了一个宏！

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

#mycommand2 -- Hello World

注意，由于命令繁饰支持为相同语法注册多个繁饰器，我们实际上可以在需要时重载语法。

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

#mycommand1 -- new!

此外，也可以仅重载部分语法，在我们希望默认处理器处理的情况下抛出 unsupportedSyntaxException，或者让 elab 命令处理它。

在以下示例中，我们并没有扩展原始的 #check 语法，而是为这个特定的语法结构添加了一个新的 SyntaxKind。不过，从用户的角度来看，效果基本相同。

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

这实际上是扩展了原始的 #check

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

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

项目示例

作为本节的最终迷你项目，让我们构建一个实用的命令繁饰器。它将接受一个命令，并使用与 elabCommand（命令繁饰的入口点）相同的机制，告诉我们哪些宏或繁饰器与我们给出的命令相关。

不过，我们不会费力去真正重新实现 elabCommand。

elab "#findCElab " c:command : command => do
  let macroRes ← liftMacroM <| expandMacroImpl? (←getEnv) c
  match macroRes with
  | some (name, _) => logInfo s!"下一步是一个宏: {name.toString}"
  | none =>
    let kind := c.raw.getKind
    let elabs := commandElabAttribute.getEntries (←getEnv) kind
    match elabs with
    | [] => logInfo s!"没有繁饰器可以处理你的语法"
    | _ => logInfo s!"你的语法也许可以被以下繁饰器处理: {elabs.map (fun el => el.declName.toString)}"

#findCElab def lala := 12 -- 你的语法也许可以被以下繁饰器处理:  [Lean.Elab.Command.elabDeclaration]
#findCElab abbrev lolo := 12 -- 你的语法也许可以被以下繁饰器处理:  [Lean.Elab.Command.elabDeclaration]
#findCElab #check foo -- 甚至你自己的语法！: 你的语法也许可以被以下繁饰器处理:  [mySpecialCheck, Lean.Elab.Command.elabCheck]
#findCElab open Hi -- 你的语法也许可以被以下繁饰器处理:  [Lean.Elab.Command.elabOpen]
#findCElab namespace Foo -- 你的语法也许可以被以下繁饰器处理:  [Lean.Elab.Command.elabNamespace]
#findCElab #findCElab open Bar -- 甚至它自己！: 你的语法也许可以被以下繁饰器处理:  [«_aux_lean_elaboration___elabRules_command#findCElab__1»]

TODO：也许我们还应该添加一个小型项目来演示非 # 风格的命令，即声明类命令，尽管目前没有想到什么。 TODO：定义一个 conjecture 声明，类似于 lemma/theorem，不同之处在于它会自动补充 sorry。该 sorry 可以是一个自定义的，以反映 conjecture 可能被期望为真。

项繁饰

一个项（term）是一个表示某种 Expr 的 Syntax 对象。项繁饰器是处理我们编写的大部分代码的核心。尤其是，它们负责繁饰定义的值、类型（因为这些也只是 Expr）等。

所有的项都属于 term 语法类别（我们在宏章节中已经看到它的作用）。因此，要声明自定义的项，它们的语法需要在该类别中注册。

为项赋予意义

与命令繁饰一样，下一步是为语法赋予语义。对于项，这是通过注册一个所谓的项繁饰器完成的。

项繁饰器的类型是 TermElab，或者说 Syntax → Option Expr → TermElabM Expr：

• 与命令繁饰一样，Syntax 是用户用于创建此项的内容
• Option Expr 是该项的预期类型，由于这一点不总是已知，所以它只是一个 Option 参数
• 不同于命令繁饰，项繁饰不仅仅是因为其副作用而执行——TermElabM Expr 的返回值确实包含感兴趣的内容，即表示 Syntax 对象的 Expr。

TermElabM 在各个方面基本上都是 CommandElabM 的升级版：它支持我们之前提到的所有功能，再加上两项新功能。第一项非常简单：除了运行 IO 代码之外，它还可以运行 MetaM 代码，因此可以很好地构建 Expr。第二项功能非常专门，适用于项繁饰循环。

项繁饰

项繁饰的基本思想与命令繁饰相同：展开宏并递归调用，或者运行通过 term_elab 属性为 Syntax 注册的项繁饰器（它们可能会进一步运行项繁饰），直到我们完成。不过，项繁饰器在执行过程中可以执行一项特殊的操作。

项繁饰器可能会抛出 Except.postpone，表示它需要更多信息才能继续工作。为了表示这些缺失的信息，Lean 使用了所谓的合成元变量。正如你之前知道的，元变量是 Expr 中等待填补的空洞。合成元变量有所不同，它们具有特殊的方法来解决它们，这些方法注册在 SyntheticMVarKind 中。目前有四种：

• typeClass，元变量应通过类型类推导解决
• coe，元变量应通过类型转换（类型类的特殊情况）解决
• tactic，元变量是一个策略项，应该通过运行策略解决
• postponed，这些是在 Except.postpone 时创建的

一旦创建了这样的合成元变量，下一个更高层级的项繁饰器将继续执行。在某些时刻，延迟的元变量的执行将由项繁饰器恢复，希望它现在能够完成其执行。我们可以通过以下示例来观察它的运行：

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

这里发生的事情是，函数应用的繁饰器从 List.foldr 开始展开。List.foldr 是一个通用函数，因此它为隐式类型参数创建了元变量。然后，它尝试繁饰第一个参数 .add。

如果你不清楚 .name 的工作原理，基本想法是，Lean 通常可以推断出函数的输出类型（在这种情况下为 Nat，即 Nat.add）。在这种情况下，.name 特性会在 Nat 命名空间中查找一个名为 name 的函数。这在你希望使用某个类型的构造函数而不引用或打开其命名空间时特别有用，也可以像上面那样使用。

回到我们的例子，虽然此时 Lean 已经知道 .add 需要的类型是：?m1 → ?m2 → ?m2（其中 ?x 表示元变量），但 .add 的繁饰器需要知道 ?m2 的实际值，因此项繁饰器推迟执行（通过内部创建一个合成元变量代替 .add），然后其他两个参数的繁饰结果表明 ?m2 必须是 Nat。一旦 .add 的繁饰器继续执行，它就可以利用这些信息完成繁饰。

我们也可以轻松引发无法正常工作的情况。例如：

#check_failure set_option trace.Elab.postpone true in List.foldr .add
-- [Elab.postpone] .add : ?m.5808 → ?m.5809 → ?m.5809
-- 无效的点号标识符表示法，预期类型不符合形式 (... → C ...) 其中 C 是一个常量 ?m.5808 → ?m.5809 → ?m.5809

在这种情况下，.add 首先推迟了执行，随后再次被调用，但没有足够的信息完成繁饰，因此失败了。

创建我们自己的项繁饰器

添加新的项繁饰器的工作方式与添加新的命令繁饰器基本相同，因此我们只会简要地看一下：

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

def mytermValues := [1, 2]

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

#eval myterm 1 -- 1

-- 用 `elab` 亦可
elab "myterm 2" : term => do
  mkAppM ``List.get! #[.const ``mytermValues [], mkNatLit 1] -- `MetaM` code

#eval myterm 2 -- 2

项目示例

作为本章的最终小型项目，我们将重现 Lean 中最常用的语法糖之一，即 ⟨a, b, c⟩ 表示法，用作单构造器类型的简写：

-- 使用稍微不同的表示法，以避免歧义
syntax (name := myanon) "⟨⟨" term,* "⟩⟩" : term

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

@[term_elab myanon]
def myanonImpl : TermElab := fun stx typ? => do
  -- 如果类型未知或是元变量，尝试推迟执行。
  -- 元变量被诸如函数繁饰器等用来填充隐式参数的值，
  -- 当它们尚未获得足够的信息来确定这些值时。
  -- 项繁饰器只能推迟执行一次，以避免陷入无限循环。
  -- 因此，我们只尝试推迟执行，否则可能会导致错误。
  tryPostponeIfNoneOrMVar typ?
  -- 如果推迟后还没有找到类型，则报错
  let some typ := typ? | throwError "expected type must be known"
  if typ.isMVar then
    throwError "expected type must be known"
  let Expr.const base .. := typ.getAppFn | throwError s!"type is not of the expected form: {typ}"
  let [ctor] ← getCtors base | throwError "type doesn't have exactly one constructor"
  let args := TSyntaxArray.mk stx[1].getSepArgs
  let stx ← `($(mkIdent ctor) $args*) -- syntax quotations
  elabTerm stx typ -- call term elaboration recursively

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

最后， 我们可以通过使用 elab 语法的额外语法糖来缩短推迟操作： As a final note, we can shorten the postponing act by using an additional syntax sugar of the elab syntax instead:

-- 这个 `t` 语法将有效地执行 `myanonImpl` 的前两行
elab "⟨⟨" args:term,* "⟩⟩" : term <= t => do
  sorry

练习

1. 考虑以下代码。使用 elab 重写 syntax + @[term_elab hi]... : TermElab 组合。

   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
   

2. 以下是从真实的 mathlib 命令 alias 中提取的语法。

   syntax (name := our_alias) (docComment)? "our_alias " ident " ← " ident* : command
   

   我们希望 alias hi ← hello yes 输出 ← 之后的标识符，也就是 "hello" 和 "yes"。

   请添加以下语义：

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

3. 以下是从真实的 mathlib 策略 nth_rewrite 中提取的语法。

   open Parser.Tactic
   syntax (name := nthRewriteSeq) "nth_rewrite " (config)? num rwRuleSeq (ppSpace location)? : tactic
   

   我们希望 nth_rewrite 5 [←add_zero a] at h 在用户提供位置时输出 "rewrite location!"，如果用户没有提供位置，则输出 "rewrite target!"。

   请添加以下语义：

   a) 使用 syntax + @[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic。 b) 使用 syntax + elab_rules。 c) 使用 elab。

通过繁饰嵌入 DSL

在本章中，我们将学习如何通过繁饰（elaboration）来构建一个领域特定语言（DSL）。我们不会全面探索 MetaM 的全部功能，而是简单地演示如何访问这个底层机制。

更具体地说，我们将使 Lean 理解 IMP 的语法。IMP 是一个简单的命令式语言，通常用于教学操作和指称语义。

我们不会完全按照书中的编码方式来定义所有内容。比如，书中定义了算术表达式和布尔表达式。而我们将走一条不同的路径，只定义接受一元或二元运算符的通用表达式。

这意味着我们将允许出现像 1 + true 这样的奇怪表达式！不过这会简化编码、语法以及元编程的教学过程。

定义抽象语法树（AST）

我们首先定义我们的原子字面量：

import Lean

open Lean Elab Meta

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

这是我们唯一的一个一元运算符：

inductive IMPUnOp
  | not

接下来是我们的二元运算符：

inductive IMPBinOp
  | and | add | less

现在我们定义我们要处理的表达式：

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

最后，我们定义语言中的命令。我们遵循书中的结构，表示「程序的每个部分也是一个程序」：

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

繁饰字面量

现在我们已经定义了数据类型，接下来我们将 Syntax 转换为 Expr 类型的项。我们从定义字面量的语法和繁饰函数开始。

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

def elabIMPLit : Syntax → MetaM Expr
  -- `mkAppM` 由给定函数 `Name` 和参数，创建一个 `Expr.app`，
  -- `mkNatLit` 由一个 `Nat` 创建一个 `Expr`
  | `(imp_lit| $n:num) => mkAppM ``IMPLit.nat  #[mkNatLit n.getNat]
  | `(imp_lit| true  ) => mkAppM ``IMPLit.bool #[.const ``Bool.true []]
  | `(imp_lit| false ) => mkAppM ``IMPLit.bool #[.const ``Bool.false []]
  | _ => throwUnsupportedSyntax

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

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

繁饰表达式

为了繁饰表达式，我们还需要繁饰一元和二元运算符：

请注意，这些实际上可以是纯函数（Syntax → Expr），但我们选择在 MetaM 中处理，因为这样可以更方便地抛出匹配完成的错误。

declare_syntax_cat imp_unop
syntax "not"     : imp_unop

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

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

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

现在我们定义表达式的语法：

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

我们还允许括号表示解析的优先级：

syntax "(" imp_expr ")" : imp_expr

最后，我们定义递归繁饰表达式的函数：注意，表达式可以是递归的。这意味着我们的 elabIMPExpr 函数需要是递归的！我们需要使用 partial，因为 Lean 不能仅凭 Syntax 的消耗来证明终止性。

partial def elabIMPExpr : Syntax → MetaM Expr
  | `(imp_expr| $l:imp_lit) => do
    let l ← elabIMPLit l
    mkAppM ``IMPExpr.lit #[l]
  -- `mkStrLit` 由一个 `String` 创建一个 `Expr`
  | `(imp_expr| $i:ident) => mkAppM ``IMPExpr.var #[mkStrLit i.getId.toString]
  | `(imp_expr| $b:imp_unop $e:imp_expr) => do
    let b ← elabIMPUnOp b
    let e ← elabIMPExpr e -- 递归!
    mkAppM ``IMPExpr.un #[b, e]
  | `(imp_expr| $l:imp_expr $b:imp_binop $r:imp_expr) => do
    let l ← elabIMPExpr l -- 递归!
    let r ← elabIMPExpr r -- 递归!
    let b ← elabIMPBinOp b
    mkAppM ``IMPExpr.bin #[b, l, r]
  | `(imp_expr| ($e:imp_expr)) => elabIMPExpr e
  | _ => throwUnsupportedSyntax

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

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

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

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

繁饰程序

现在我们有了繁饰 IMP 程序所需的一切！

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

syntax imp_program ";;" imp_program : imp_program

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

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

然后我们就可以测试完整的繁饰流程了。遵循以下语法：

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

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

证明策略

证明策略(Tactic)是 Lean 程序，用于操纵自定义状态。最终，所有策略都属于 TacticM Unit 类型。其类型为：

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

但在演示如何使用 TacticM 之前，我们将探索基于宏的策略。

通过宏扩展的策略

与 Lean 4 基础架构的许多其他部分一样，策略也可以通过轻量级宏扩展来声明。

例如下面的 custom_sorry_macro 示例，该示例繁饰为 sorry。我们将其写为宏扩展，将语法片段 custom_sorry_macro 扩展为语法片段 sorry：

import Lean.Elab.Tactic

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

example : 1 = 42 := by
  custom_sorry_macro

实现 trivial：通过宏扩展实现可扩展的策略

作为更复杂的示例，我们可以编写一个类似 custom_tactic 的策略，该策略最初完全未实现，并且可以通过添加更多策略来扩展。我们首先简单地声明这个策略，而不提供任何实现：

syntax "custom_tactic" : tactic

/-- 错误：策略 'tacticCustom_tactic' 尚未实现 -/
example : 42 = 42 := by
  custom_tactic
  sorry

接下来我们将在 custom_tactic 中添加 rfl 策略，这将允许我们证明前面的定理。

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

example : 42 = 42 := by
   custom_tactic
-- Goals accomplished 🎉

测试一个稍难的例子，它不能直接被 rfl 证明：

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

我们通过一个策略扩展 custom_tactic，该策略尝试使用 apply And.intro 分解 And，然后递归地对两个子情况应用 custom_tactic，并使用 (<;> trivial) 解决生成的子问题 43 = 43 和 42 = 42。

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

上面的声明使用了 <;>，这是一种策略组合器（tactic combinator）。这里，a <;> b 的意思是「运行策略 a，并对 a 生成的每个目标应用 b」。因此，And.intro <;> custom_tactic 的意思是「运行 And.intro，然后在每个目标上运行 custom_tactic」。我们在前面的定理上测试它，并发现我们能够证明该定理。

example : 43 = 43 ∧ 42 = 42 := by
  custom_tactic
-- Goals accomplished 🎉

总结一下，我们声明了一个可扩展的策略，名为 custom_tactic。最初，它完全没有任何实现。我们将 rfl 作为 custom_tactic 的一个实现，这使它能够解决目标 42 = 42。然后我们尝试了一个更难的定理 43 = 43 ∧ 42 = 42，而 custom_tactic 无法解决。随后我们丰富了 custom_tactic，使其能够通过 And.intro 分解「AND」，并且在两个子情况下递归调用 custom_tactic。

实现 <;>：通过宏扩展实现策略组合器

在上一节中，我们提到 a <;> b 意味着「运行 a，然后对所有生成的目标运行 b」。实际上，<;> 本身是一个策略宏。在本节中，我们将实现 a and_then b 语法，它代表「运行 a，然后对所有目标运行 b」。

-- 1. 我们声明语法 `and_then`
syntax tactic " and_then " tactic : tactic

-- 2. 我们编写扩展器，将策略扩展为运行 `a`，然后对 `a` 生成的所有目标运行 `b`。
macro_rules
| `(tactic| $a:tactic and_then $b:tactic) =>
    `(tactic| $a:tactic; all_goals $b:tactic)

-- 3. 我们测试这个策略。
theorem test_and_then: 1 = 1 ∧ 2 = 2 := by
  apply And.intro and_then rfl

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

探索 TacticM

最简单的策略：sorry

本节我们实现sorry：

example : 1 = 2 := by
  custom_sorry

从声明策略开始：

elab "custom_sorry_0" : tactic => do
  return

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

这定义了一个 Lean 的语法扩展，我们将这个语法片段命名为 custom_sorry_0，属于 tactic 语法类别。这告诉繁饰器，在繁饰 tactic 时，custom_sorry_0 语法片段必须按照我们在 => 右侧编写的内容进行繁饰（也就是策略的实际实现）。

接下来，我们编写一个 TacticM Unit 类型的项，用 sorryAx α 填充目标，它可以生成一个类型为 α 的人工项。为此，我们首先使用 Lean.Elab.Tactic.getMainGoal : Tactic MVarId 获取目标，它返回一个表示为元变量的主目标。回顾类型即命题的原理，我们的目标类型必须是命题 1 = 2。我们通过打印 goal 的类型来验证这一点。

但首先，我们需要使用 Lean.Elab.Tactic.withMainContext 开始我们的策略，它在更新后的语境中计算 TacticM。

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

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

为了 sorry 这个目标，我们可以用 Lean.Elab.admitGoal：

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

theorem test_custom_sorry : 1 = 2 := by
  custom_sorry_2

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

我们不再出现错误 unsolved goals: ⊢ 1 = 2。

custom_assump 策略：访问假设

在本节中，我们将学习如何访问假设来证明目标。特别是，我们将尝试实现一个策略 custom_assump，它会在假设中寻找与目标完全匹配的项，并在可能的情况下解决定理。

在下面的例子中，我们期望 custom_assump 使用 (H2 : 2 = 2) 来解决目标 (2 = 2)：

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

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

当我们没有与目标匹配的假设时，我们期望 custom_assump 策略抛出一个错误，告知我们找不到我们正在寻找类型的假设：

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

#print assump_wrong
-- 策略 'custom_assump' 失败，找不到类型 (2 = 2) 的匹配假设
-- tactic 'custom_assump' failed, unable to find matching hypothesis of type (2 = 2)
-- H1 : 1 = 1
-- ⊢ 2 = 2

我们首先通过访问目标及其类型，来了解我们正在试图证明什么。goal 变量很快将被用于帮助我们创建错误信息。

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

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

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

接下来，我们访问存储在名为 LocalContext 的数据结构中的假设列表。可以通过 Lean.MonadLCtx.getLCtx 访问它。LocalContext 包含 LocalDeclaration，我们可以从中提取信息，如声明的名称（.userName）和声明的表达式（.toExpr）。让我们编写一个名为 list_local_decls 的策略，打印出局部声明：

elab "list_local_decls_1" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let ctx ← Lean.MonadLCtx.getLCtx -- 获取局部语境
    ctx.forM fun decl: Lean.LocalDecl => do
      let declExpr := decl.toExpr -- 找到声明的表达式
      let declName := decl.userName -- 找到声明的名称
      dbg_trace f!"+ local decl: name: {declName} | expr: {declExpr}"

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

回想一下，我们正在寻找一个具有与假设相同类型的局部声明。我们可以通过在局部声明的表达式上调用 Lean.Meta.inferType 来获取 LocalDecl 的类型。

elab "list_local_decls_2" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let ctx ← Lean.MonadLCtx.getLCtx -- 获取局部语境
    ctx.forM fun decl: Lean.LocalDecl => do
      let declExpr := decl.toExpr -- 找到声明的表达式
      let declName := decl.userName -- 找到声明的名称
      let declType ← Lean.Meta.inferType declExpr -- **新事件：** 找到类型
      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

我们使用 Lean.Meta.isExprDefEq 检查 LocalDecl 的类型是否与目标类型相等。可以看到，我们在 eq? 处检查类型是否相等，并打印出 H1 与目标类型相同（local decl[EQUAL? true]: name: H1），同时我们也打印出 H2 的类型不相同（local decl[EQUAL? false]: name: H2）：

elab "list_local_decls_3" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goalType ← Lean.Elab.Tactic.getMainTarget
    let ctx ← Lean.MonadLCtx.getLCtx -- 获取局部语境
    ctx.forM fun decl: Lean.LocalDecl => do
      let declExpr := decl.toExpr -- 找到声明的表达式
      let declName := decl.userName -- 找到声明的名称
      let declType ← Lean.Meta.inferType declExpr -- 找到类型
      let eq? ← Lean.Meta.isExprDefEq declType goalType -- **新事件：** 检查是否与目标类型等价
      dbg_trace f!"+ local decl[EQUAL? {eq?}]: name: {declName}"

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

最后，我们将这些部分组合在一起，编写一个遍历所有声明并找到具有正确类型的声明的策略。我们使用 lctx.findDeclM? 遍历声明。使用 Lean.Meta.inferType 推断声明的类型。使用 Lean.Meta.isExprDefEq 检查声明的类型是否与目标相同：

elab "custom_assump_1" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goalType ← Lean.Elab.Tactic.getMainTarget
    let lctx ← Lean.MonadLCtx.getLCtx
    -- 在局部证明中迭代...
    let option_matching_expr ← lctx.findDeclM? fun ldecl: Lean.LocalDecl => do
      let declExpr := ldecl.toExpr -- 找到声明的表达式
      let declType ← Lean.Meta.inferType declExpr -- 找到类型
      if (← Lean.Meta.isExprDefEq declType goalType) -- 检查是否与目标类型等价
      then return some declExpr -- 如果等价，成功！
      else return none          -- 未找到
    dbg_trace f!"matching_expr: {option_matching_expr}"

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

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

现在我们能够找到匹配的表达式，需要使用匹配来证成定理。我们通过 Lean.Elab.Tactic.closeMainGoal 来完成这一操作。如果没有找到匹配的表达式，我们会使用 Lean.Meta.throwTacticEx 抛出一个错误，允许我们针对给定的目标报告错误。在抛出此错误时，我们使用 m!"..." 来格式化错误信息，这会生成一个 MessageData。与生成 Format 的 f!"..." 相比，MessageData 提供了更友好的错误信息，这是因为 MessageData 还会运行反繁饰，使其能够将像 (Eq.{1} Nat (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) 这样的原始 Lean 项转换为易读的字符串，例如 (2 = 2)。完整的代码示例如下：

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

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

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

调整语境

到目前为止，我们只对语境执行了类似读取的操作。但如果我们想要更改语境呢？在本节中，我们将看到如何更改目标的顺序以及如何向其添加内容（新的假设）。

然后，在繁饰我们的项之后，我们需要使用辅助函数 Lean.Elab.Tactic.liftMetaTactic，它允许我们在 MetaM 中运行计算，同时为我们提供目标 MVarId 以便操作。计算结束时，liftMetaTactic 期望我们返回一个 List MVarId，即目标列表的最终结果。

custom_let 和 custom_have 的唯一实质性区别是前者使用了 Lean.MVarId.define，而后者使用了 Lean.MVarId.assert：

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

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

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

「获取」和「设置」目标列表

为了说明这些操作，我们将构建一个可以反转目标列表的策略。我们可以使用 Lean.Elab.Tactic.getGoals 和 Lean.Elab.Tactic.setGoals：

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

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

常见问题

在本节中，我们收集了一些在编写策略时常用的模式，备查。

问题：如何使用目标？

回答：目标表示为元变量。模块 Lean.Elab.Tactic.Basic 提供了许多函数用于添加新目标、切换目标等。

问题：如何获取主要目标？

回答：使用 Lean.Elab.Tactic.getMainGoal。

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

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

问题：如何获取目标列表？

回答：使用 getGoals。

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

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

问题：如何获取目标的当前假设？

回答：使用 Lean.MonadLCtx.getLCtx 获取局部语境，然后使用诸如 foldlM 和 forM 之类的访问器，遍历 LocalContext 中的 LocalDeclaration。

elab "faq_get_hypotheses" : tactic =>
  Lean.Elab.Tactic.withMainContext do
  let ctx ← Lean.MonadLCtx.getLCtx -- 获取局部语境。
  ctx.forM (fun (decl : Lean.LocalDecl) => do
    let declExpr := decl.toExpr -- 找到声明的表达式。
    let declType := decl.type -- 找到声明的类型。
    let declName := decl.userName -- 找到声明的名称。
    dbg_trace f!"局部声明: 名称: {declName} | 表达式: {declExpr} | 类型: {declType}"
  )

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

问题：如何执行一个策略？

回答：使用 Lean.Elab.Tactic.evalTactic: Syntax → TacticM Unit 来执行给定的策略语法。可以使用宏 `(tactic| ⋯) 创建策略语法。

例如，可以使用以下代码调用 try rfl：

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

问题：如何检查两个表达式是否相等？

回答：使用 Lean.Meta.isExprDefEq <expr-1> <expr-2>。

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

问题：如何从一个策略中抛出错误？

回答：使用 throwTacticEx <tactic-name> <goal-mvar> <error>。

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

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

问题：Lean.Elab.Tactic.* 和 Lean.Meta.Tactic.* 有什么区别？

回答：Lean.Meta.Tactic.* 包含使用 Meta 单子实现的底层代码，用于提供诸如重写等基本功能。而 Lean.Elab.Tactic.* 包含连接 Lean.Meta 中的底层开发与策略基础设施及解析前端的高级代码。

练习

1. 考虑定理 p ∧ q ↔ q ∧ p。我们可以将其证明写为一个证明项，或者使用策略构建它。 当我们将该定理的证明写成证明项时，我们会逐步用特定的表达式填充 _，一步一步进行。每一步都对应一个策略。

   我们可以通过多种步骤组合来编写这个证明项，但请考虑我们在下面编写的步骤序列。请将每一步写为策略。 策略 step_1 已经填写，请对其余策略执行相同操作（为了练习，请尝试使用较底层的 API，例如 mkFreshExprMVar、mvarId.assign 和 modify fun _ => { goals := ~)）。

   -- [这是初始目标]
   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. 创建具有适当类型的新 `_`。
     let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red")
     let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue")
   
     -- 2. 将主目标分配给表达式 `Iff.intro _ _`。
     mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2])
   
     -- 3. 将新的 `_` 报告给 Lean，作为新的目标。
     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
   

以下是这段内容的翻译：

2. 在第一个练习中，我们使用了较底层的 modify API 来更新我们的目标。liftMetaTactic、setGoals、appendGoals、replaceMainGoal、closeMainGoal 等都是在 modify fun s : State => { s with goals := myMvarIds } 之上的语法糖。请使用以下方法重写 forker 策略：

a) liftMetaTactic b) setGoals c) replaceMainGoal

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

  let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId (m!"Goal is not of the form P ∧ Q")

  mvarId.withContext do
    let mvarIdP ← mkFreshExprMVar p (userName := "red")
    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")

    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
    mvarId.assign proofTerm

    modify fun state => { goals := [mvarIdP.mvarId!, mvarIdQ.mvarId!] ++ state.goals.drop 1 }

example (A B C : Prop) : A → B → C → (A ∧ B) ∧ C := by
  intro hA hB hC
  forker
  forker
  assumption
  assumption
  assumption

3. 在第一个练习中，你在 step_2 中创建了自己的 intro（假设名是硬编码的，但基本原理是相同的）。在编写策略时，我们通常会使用 intro、intro1、intro1P、introN 或 introNP 等函数。

对于下面的每一点，请创建一个名为 introductor 的策略（每一点对应一个策略），将目标 (ab: a = b) → (bc: b = c) → (a = c) 变为：

a) 包含假设 (ab✝: a = b) 和 (bc✝: b = c) 的目标 (a = c)。 b) 包含假设 (ab: a = b) 的目标 (bc: b = c) → (a = c)。 c) 包含假设 (hello: a = b) 的目标 (bc: b = c) → (a = c)。

example (a b c : Nat) : (ab: a = b) → (bc: b = c) → (a = c) := by
  introductor
  sorry

提示：intro1P 和 introNP 中的 "P" 代表 "Preserve"（保留）。

Lean4 速查表

读取信息

• 读取目标：Lean.Elab.Tactic.getMainGoal

  用法：let goal ← Lean.Elab.Tactic.getMainGoal

• 读取元变量外声明：mvarId.getDecl 当 mvarId : Lean.MVarId 在语境中 例如，mvarId 可以是被 getMainGoal 读取到的目标。

• 读取元变量的类型：mvarId.getType 当 mvarId : Lean.MVarId 在语境中

• 读取主目标的类型：Lean.Elab.Tactic.getMainTarget

  用法： let goal_type ← Lean.Elab.Tactic.getMainTarget

  等价实现：

let goal ← Lean.Elab.Tactic.getMainGoal
let goal_type ← goal.getType

• 读取局部语境：Lean.MonadLCtx.getLCtx

  用法：let lctx ← Lean.MonadLCtx.getLCtx

• 读取声明的名称：Lean.LocalDecl.userName ldecl 当 ldecl : Lean.LocalDecl 在语境中

• 读取表达式的类型 Lean.Meta.inferType expr 当 expr : Lean.Expr 是语境中的表达式

  用法：let expr_type ← Lean.Meta.inferType expr

操纵表达式

• 把声明转换为表达式：Lean.LocalDecl.toExpr

  用法：ldecl.toExpr，当 ldecl : Lean.LocalDecl 在语境中

  例如，ldecl 可以是 let ldecl ← Lean.MonadLCtx.getLCtx

• 检查两个表达式是否定义等价：Lean.Meta.isDefEq ex1 ex2 当 ex1 ex2 : Lean.Expr 在语境中。返回一个 Lean.MetaM Bool

• 选择一个目标：Lean.Elab.Tactic.closeMainGoal expr 当 expr : Lean.Expr 在语境中

更多命令

• meta-sorry: Lean.Elab.admitGoal goal，当 goal : Lean.MVarId 是当前目标

打印和显示报错

• 打印一句话：

  Lean.logInfo f!"Hi, I will print\n{Syntax}"

• 调试时打印：

  dbg_trace f!"1) goal: {Syntax_that_will_be_interpreted}".

• 抛出错误信息：Lean.Meta.throwTacticEx name mvar message_data 其中，name : Lean.Name 是策略名，mvar 包含错误信息

  用法：Lean.Meta.throwTacticEx tac goal (m!"unable to find matching hypothesis of type ({goal_type})") 其中，m!格式化用于构建MessageData`，以便更好地打印项。

TODO: Add?

• Lean.LocalContext.forM
• Lean.LocalContext.findDeclM?

额外内容：选项

选项（Option）是一种向元程序和 Lean 编译器传达一些特殊配置的方法。基本上它只是一个 KVMap，这是一个从 Name 到 Lean.DataValue 的简单映射。目前有 6 种数据值：

• String
• Bool
• Name
• Nat
• Int
• Syntax

通过 set_option 命令设置一个选项，告诉 Lean 编译器对程序做一些不同的处理是非常简单的：

import Lean
open Lean

#check 1 + 1 -- 1 + 1 : Nat

set_option pp.explicit true -- 在美观打印中不使用通常的语法

#check 1 + 1 -- @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) 1 1 : Nat

set_option pp.explicit false

你还可以将选项值限制为仅适用于下一个命令或表达式：

set_option pp.explicit true in
#check 1 + 1 -- @HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) 1 1 : Nat

#check 1 + 1 -- 1 + 1 : Nat

#check set_option trace.Meta.synthInstance true in 1 + 1 -- 显示类型类合成 `OfNat` 和 `HAdd` 的途径

如果你想知道目前有哪些选项可用，你可以直接码出 set_option 空一格然后编辑器会自动弹出代码建议。在调试某些元程序时，最有用的一类选项是 trace.。

元编程中的选项

现在我们已经知道如何设置选项了，接下来我们来看一下元程序如何访问这些选项。最常见的方法是通过 MonadOptions 类型类，这个类扩展了 Monad，提供了一个函数 getOptions : m Options。目前，它在以下类型中得到了实现：

• CoreM
• CommandElabM
• LevelElabM
• 所有可以提升上述某个类型操作的 monad（例如 MetaM 是从 CoreM 提升的）

一旦我们有了 Options 对象，我们就可以通过 Options.get 查询相关信息。 为了演示这一点，让我们编写一个命令来打印 pp.explicit 的值。

elab "#getPPExplicit" : command => do
  let opts ← getOptions
  -- defValue = default value 默认值
  logInfo s!"pp.explicit : {opts.get pp.explicit.name pp.explicit.defValue}"

#getPPExplicit -- pp.explicit : false

set_option pp.explicit true in
#getPPExplicit -- pp.explicit : true

注意到，获取 pp.explicit 的实际实现 Lean.getPPExplicit 使用了 pp.all 是否被设置作为默认值。

自定义选项

声明我们自己的选项也非常简单。Lean 编译器提供了一个宏 register_option 来实现这一功能。让我们来看一下它的用法：

register_option book.myGreeting : String := {
  defValue := "Hello World"
  group := "pp"
  descr := "just a friendly greeting"
}

然而，我们不能在声明选项的同一个文件中直接使用它，因为有初始化的限制。

额外内容：美观打印

Lean 的美观打印器用于向用户呈现已繁饰的术语。这是通过将 Expr 转换回 Syntax，然后再转换为更高级的美观打印数据结构来完成的。这意味着 Lean 实际上不会记住它用来创建某些 Expr 的 Syntax：必须有代码告诉它如何执行此操作。

从宏观角度来看，美观打印器由三个部分组成，按列出的顺序运行：

• 反繁饰器 这是我们主要感兴趣的部分，因为我们可以轻松地用自己的代码扩展它。它的任务是将 Expr 转换回 Syntax。
• 括号添加器 负责在 Syntax 树中添加括号，它认为在某些地方括号会有帮助。
• 格式化器 负责将加了括号的 Syntax 树转换为包含更多美观打印信息（如显式空格）的 Format 对象。

反繁饰

顾名思义，反繁饰器在某种意义上是繁饰器的反面。反繁饰器的任务是将由繁饰器生成的 Expr 转换回 Syntax，如果再次繁饰，应该生成一个与输入行为相同的 Expr。

反繁饰器的类型是 Lean.PrettyPrinter.Delaborator.Delab。这是 DelabM Syntax 的别名，其中 DelabM 是反繁饰 monad。所有这些机制都定义在这里。DelabM 为我们提供了很多选项，您可以在文档中查看（TODO：文档链接）。这里我们只强调最相关的部分。

• 它有一个 MonadQuotation 实例，允许我们使用熟悉的引用语法声明 Syntax 对象。
• 它可以运行 MetaM 代码。
• 它有一个 MonadExcept 实例用于抛出错误。
• 它可以使用 whenPPOption 等函数与 pp 选项交互。
• 您可以使用 SubExpr.getExpr 获取当前的子表达式。SubExpr 模块中还围绕这个概念定义了整个 API。

创建我们自己的反繁饰器

像元编程中的许多事情一样，反繁饰器基于属性，在这种情况下是 delab 属性。delab 期望以 Name 作为参数，这个名称必须以 Expr 构造函数的名称开头，最常见的是 const 或 app。此构造函数名称后面跟着我们想要反繁饰的常量名称。例如，如果我们想以特殊方式反繁饰函数 foo，我们将使用 app.foo。让我们来看一下实际操作：

import Lean

open Lean PrettyPrinter Delaborator SubExpr

def foo : Nat → Nat := fun x => 42

@[delab app.foo]
def delabFoo : Delab := do
  `(1)

#check foo -- 1 : Nat → Nat
#check foo 13 -- 1 : Nat, 整个应用同样被这样打印出来了

这显然不是一个好的反繁饰器，因为重新繁饰此 Syntax 不会产生相同的 Expr。像许多其他元编程属性一样，我们也可以重载反繁饰器：

@[delab app.foo]
def delabfoo2 : Delab := do
  `(2)

#check foo -- 2 : Nat → Nat

确定使用哪个反繁饰器的机制也是相同的。反繁饰器按照注册的相反顺序依次尝试，直到其中一个没有抛出错误，表明它「不对这个 Expr 负责」。在反繁饰器的情况下，这是通过使用 failure 来完成的：

@[delab app.foo]
def delabfoo3 : Delab := do
  failure
  `(3)

#check foo -- 2 : Nat → Nat, 还是 2 因为 3 失败了

为了为 foo 编写一个合适的反繁饰器，我们将不得不使用一些稍微高级一点的机制：

@[delab app.foo]
def delabfooFinal : Delab := do
  let e ← getExpr
  guard $ e.isAppOfArity' `foo 1 -- 只能像这样反繁饰整个应用
  let fn := mkIdent `fooSpecial
  let arg ← withAppArg delab
  `($fn $arg)

#check foo 42 -- fooSpecial 42 : Nat
#check foo -- 2 : Nat → Nat, 还是 2 因为 3 失败了

你能扩展 delabFooFinal 来处理非完整应用的情况吗？

反扩展器

虽然反繁饰器非常强大，但很多情况下并不需要使用它们。如果你查看 Lean 编译器中的 @[delab 或 @[builtin_delab（编译器使用的 delab 属性的特殊版本，我们对此不关心），你会发现它们的出现次数很少。这是因为大多数美观打印实际上是由所谓的反扩展器完成的。与反繁饰器不同，反扩展器的类型是 Lean.PrettyPrinter.Unexpander，这实际上是 Syntax → Lean.PrettyPrinter.UnexpandM Syntax 的别名。正如你所看到的，它们是 Syntax 到 Syntax 的转换，类似于宏，区别在于它们应该是宏的逆向操作。UnexpandM monad 比 DelabM 弱得多，但它仍然具有：

• 支持语法引用的 MonadQuotation
• 能够抛出错误，尽管错误信息并不十分详细：throw () 是唯一有效的错误

反扩展器始终针对一个常量的应用进行。它们通过 app_unexpander 属性注册，后面跟着该常量的名称。反扩展器在 Expr 经过反繁饰后被传递整个常量应用，而不包含隐式参数。让我们看看这个过程如何操作：

def myid {α : Type} (x : α) := x

@[app_unexpander myid]
def unexpMyId : Unexpander
  -- 禁用语法卫生，这样我们实际上可以返回 `id`，而不涉及宏范围等。
  | `(myid $arg) => set_option hygiene false in `(id $arg)
  | `(myid) => pure $ mkIdent `id
  | _ => throw ()

#check myid 12 -- id 12 : Nat
#check myid -- id : ?m.3870 → ?m.3870

关于一些反扩展器的不错示例，你可以查看 NotationExtra

项目示例

像往常一样，我们将在本章末进行一个迷你项目。这次我们将为一个迷你编程语言构建自己的反扩展器。请注意，许多定义语法的方法已经内置了生成所需的漂亮打印代码，例如 infix 和 notation（但不包括 macro_rules）。因此，对于简单的语法，你不需要自己手动编写这些代码。

declare_syntax_cat lang
syntax num   : lang
syntax ident : lang
syntax "let " ident " := " lang " in " lang: lang
syntax "[Lang| " lang "]" : term

inductive LangExpr
  | numConst : Nat → LangExpr
  | ident    : String → LangExpr
  | letE     : String → LangExpr → LangExpr → LangExpr

macro_rules
  | `([Lang| $x:num ]) => `(LangExpr.numConst $x)
  | `([Lang| $x:ident]) => `(LangExpr.ident $(Lean.quote (toString x.getId)))
  | `([Lang| let $x:ident := $v:lang in $b:lang]) => `(LangExpr.letE $(Lean.quote (toString x.getId)) [Lang| $v] [Lang| $b])

instance : Coe NumLit (TSyntax `lang) where
  coe s := ⟨s.raw⟩

instance : Coe Ident (TSyntax `lang) where
  coe s := ⟨s.raw⟩

-- LangExpr.letE "foo" (LangExpr.numConst 12)
--   (LangExpr.letE "bar" (LangExpr.ident "foo") (LangExpr.ident "foo")) : LangExpr
#check [Lang|
  let foo := 12 in
  let bar := foo in
  foo
]

正如你所见，目前的漂亮打印输出相当难看。我们可以通过使用反扩展器来改进它：

@[app_unexpander LangExpr.numConst]
def unexpandNumConst : Unexpander
  | `(LangExpr.numConst $x:num) => `([Lang| $x])
  | _ => throw ()

@[app_unexpander LangExpr.ident]
def unexpandIdent : Unexpander
  | `(LangExpr.ident $x:str) =>
    let str := x.getString
    let name := mkIdent $ Name.mkSimple str
    `([Lang| $name])
  | _ => throw ()

@[app_unexpander LangExpr.letE]
def unexpandLet : Unexpander
  | `(LangExpr.letE $x:str [Lang| $v:lang] [Lang| $b:lang]) =>
    let str := x.getString
    let name := mkIdent $ Name.mkSimple str
    `([Lang| let $name := $v in $b])
  | _ => throw ()

-- [Lang| let foo := 12 in foo] : LangExpr
#check [Lang|
  let foo := 12 in foo
]

-- [Lang| let foo := 12 in let bar := foo in foo] : LangExpr
#check [Lang|
  let foo := 12 in
  let bar := foo in
  foo
]

这样就好多了！一如既往，我们鼓励你自己扩展语言，比如添加带括号的表达式、更多的数据值、对 term 的引用，或其他你能想到的内容。

import Lean
open Lean Meta

Solutions

Expressions: Solutions

1.

def one : Expr :=
  Expr.app (Expr.app (Expr.const `Nat.add []) (mkNatLit 1)) (mkNatLit 2)

elab "one" : term => return one
#check one  -- Nat.add 1 2 : Nat
#reduce one -- 3

2.

def two : Expr :=
  Lean.mkAppN (Expr.const `Nat.add []) #[mkNatLit 1, mkNatLit 2]

elab "two" : term => return two
#check two  -- Nat.add 1 2 : Nat
#reduce two -- 3

3.

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

elab "three" : term => return three
#check three    -- fun x => Nat.add 1 x : Nat → Nat
#reduce three 6 -- 7

4.

def four : Expr :=
  Expr.lam `a (Expr.const `Nat [])
  (
    Expr.lam `b (Expr.const `Nat [])
    (
      Expr.lam `c (Expr.const `Nat [])
      (
        Lean.mkAppN
        (Expr.const `Nat.add [])
        #[
          (Lean.mkAppN (Expr.const `Nat.mul []) #[Expr.bvar 1, Expr.bvar 2]),
          (Expr.bvar 0)
        ]
      )
      BinderInfo.default
    )
    BinderInfo.default
  )
  BinderInfo.default

elab "four" : term => return four
#check four -- fun a b c => Nat.add (Nat.mul b a) c : Nat → Nat → Nat → Nat
#reduce four 666 1 2 -- 668

5.

def five :=
  Expr.lam `x (Expr.const `Nat [])
  (
    Expr.lam `y (Expr.const `Nat [])
    (Lean.mkAppN (Expr.const `Nat.add []) #[Expr.bvar 1, Expr.bvar 0])
    BinderInfo.default
  )
  BinderInfo.default

elab "five" : term => return five
#check five      -- fun x y => Nat.add x y : Nat → Nat → Nat
#reduce five 4 5 -- 9

6.

def six :=
  Expr.lam `x (Expr.const `String [])
  (Lean.mkAppN (Expr.const `String.append []) #[Lean.mkStrLit "Hello, ", Expr.bvar 0])
  BinderInfo.default

elab "six" : term => return six
#check six        -- fun x => String.append "Hello, " x : String → String
#eval six "world" -- "Hello, world"

7.

def seven : Expr :=
  Expr.forallE `x (Expr.sort Lean.Level.zero)
  (Expr.app (Expr.app (Expr.const `And []) (Expr.bvar 0)) (Expr.bvar 0))
  BinderInfo.default

elab "seven" : term => return seven
#check seven  -- ∀ (x : Prop), x ∧ x : Prop
#reduce seven -- ∀ (x : Prop), x ∧ x

8.

def eight : Expr :=
  Expr.forallE `notUsed
  (Expr.const `Nat []) (Expr.const `String [])
  BinderInfo.default

elab "eight" : term => return eight
#check eight  -- Nat → String : Type
#reduce eight -- Nat → String

9.

def nine : Expr :=
  Expr.lam `p (Expr.sort Lean.Level.zero)
  (
    Expr.lam `hP (Expr.bvar 0)
    (Expr.bvar 0)
    BinderInfo.default
  )
  BinderInfo.default

elab "nine" : term => return nine
#check nine  -- fun p hP => hP : ∀ (p : Prop), p → p
#reduce nine -- fun p hP => hP

10.

def ten : Expr :=
  Expr.sort (Nat.toLevel 7)

elab "ten" : term => return ten
#check ten  -- Type 6 : Type 7
#reduce ten -- Type 6

import Lean
open Lean Meta

MetaM: Solutions

1.

#eval show MetaM Unit from do
  let hi ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `hi)
  IO.println s!"value in hi: {← instantiateMVars hi}" -- ?_uniq.1

  hi.mvarId!.assign (Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero []))
  IO.println s!"value in hi: {← instantiateMVars hi}" -- Nat.succ Nat.zero

2.

-- It would output the same expression we gave it - there were no metavariables to instantiate.
#eval show MetaM Unit from do
  let instantiatedExpr ← instantiateMVars (Expr.lam `x (Expr.const `Nat []) (Expr.bvar 0) BinderInfo.default)
  IO.println instantiatedExpr -- fun (x : Nat) => x

3.

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

  -- Create `mvar1` with type `Nat`
  let mvar1 ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `mvar1)
  -- Create `mvar2` with type `Nat`
  let mvar2 ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `mvar2)
  -- Create `mvar3` with type `Nat`
  let mvar3 ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `mvar3)

  -- Assign `mvar1` to `2 + ?mvar2 + ?mvar3`
  mvar1.mvarId!.assign (Lean.mkAppN (Expr.const `Nat.add []) #[(Lean.mkAppN (Expr.const `Nat.add []) #[twoExpr, mvar2]), mvar3])

  -- Assign `mvar3` to `1`
  mvar3.mvarId!.assign oneExpr

  -- Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1`
  let instantiatedMvar1 ← instantiateMVars mvar1
  IO.println instantiatedMvar1 -- Nat.add (Nat.add 2 ?_uniq.2) 1

4.

elab "explore" : tactic => do
  let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
  let metavarDecl : MetavarDecl ← mvarId.getDecl

  IO.println "Our metavariable"
  -- [anonymous] : 2 = 2
  IO.println s!"\n{metavarDecl.userName} : {metavarDecl.type}"

  IO.println "\nAll of its local declarations"
  let localContext : LocalContext := metavarDecl.lctx
  for (localDecl : LocalDecl) in localContext do
    if localDecl.isImplementationDetail then
      -- (implementation detail) red : 1 = 1 → 2 = 2 → 2 = 2
      IO.println s!"\n(implementation detail) {localDecl.userName} : {localDecl.type}"
    else
      -- hA : 1 = 1
      -- hB : 2 = 2
      IO.println s!"\n{localDecl.userName} : {localDecl.type}"

theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
  explore
  sorry

5.

-- The type of our metavariable `2 + 2`. We want to find a `localDecl` that has the same type, and `assign` our metavariable to that `localDecl`.
elab "solve" : tactic => do
  let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
  let metavarDecl : MetavarDecl ← mvarId.getDecl

  let localContext : LocalContext := metavarDecl.lctx
  for (localDecl : LocalDecl) in localContext do
    if ← Lean.Meta.isDefEq localDecl.type metavarDecl.type then
      mvarId.assign localDecl.toExpr

theorem redSolved (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
  solve

6.

def sixA : Bool → Bool := fun x => x
-- .lam `x (.const `Bool []) (.bvar 0) (Lean.BinderInfo.default)
#eval Lean.Meta.reduce (Expr.const `sixA [])

def sixB : Bool := (fun x => x) ((true && false) || true)
-- .const `Bool.true []
#eval Lean.Meta.reduce (Expr.const `sixB [])

def sixC : Nat := 800 + 2
-- .lit (Lean.Literal.natVal 802)
#eval Lean.Meta.reduce (Expr.const `sixC [])

7.

#eval show MetaM Unit from do
  let litExpr := Expr.lit (Lean.Literal.natVal 1)
  let standardExpr := Expr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero [])

  let isEqual ← Lean.Meta.isDefEq litExpr standardExpr
  IO.println isEqual -- true

8.

-- a) `5 =?= (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))`
-- Definitionally equal.
def expr2 := (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))
#eval show MetaM Unit from do
  let expr1 := Lean.mkNatLit 5
  let expr2 := Expr.const `expr2 []
  let isEqual ← Lean.Meta.isDefEq expr1 expr2
  IO.println isEqual -- true

-- b) `2 + 1 =?= 1 + 2`
-- Definitionally equal.
#eval show MetaM Unit from do
  let expr1 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 2, Lean.mkNatLit 1]
  let expr2 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 1, Lean.mkNatLit 2]
  let isEqual ← Lean.Meta.isDefEq expr1 expr2
  IO.println isEqual -- true

-- c) `?a =?= 2`, where `?a` has a type `String`
-- Not definitionally equal.
#eval show MetaM Unit from do
  let expr1 ← Lean.Meta.mkFreshExprMVar (Expr.const `String []) (userName := `expr1)
  let expr2 := Lean.mkNatLit 2
  let isEqual ← Lean.Meta.isDefEq expr1 expr2
  IO.println isEqual -- false

-- d) `?a + Int =?= "hi" + ?b`, where `?a` and `?b` don't have a type
-- Definitionally equal.
-- `?a` is assigned to `"hi"`, `?b` is assigned to `Int`.
#eval show MetaM Unit from do
  let a ← Lean.Meta.mkFreshExprMVar Option.none (userName := `a)
  let b ← Lean.Meta.mkFreshExprMVar Option.none (userName := `b)
  let expr1 := Lean.mkAppN (Expr.const `Nat.add []) #[a, Expr.const `Int []]
  let expr2 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkStrLit "hi", b]
  let isEqual ← Lean.Meta.isDefEq expr1 expr2
  IO.println isEqual -- true

  IO.println s!"a: {← instantiateMVars a}"
  IO.println s!"b: {← instantiateMVars b}"

-- e) `2 + ?a =?= 3`
-- Not definitionally equal.
#eval show MetaM Unit from do
  let a ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `a)
  let expr1 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 2, a]
  let expr2 := Lean.mkNatLit 3
  let isEqual ← Lean.Meta.isDefEq expr1 expr2
  IO.println isEqual -- false

-- f) `2 + ?a =?= 2 + 1`
-- Definitionally equal.
-- `?a` is assigned to `1`.
#eval show MetaM Unit from do
  let a ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `a)
  let expr1 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 2, a]
  let expr2 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 2, Lean.mkNatLit 1]
  let isEqual ← Lean.Meta.isDefEq expr1 expr2
  IO.println isEqual -- true

  IO.println s!"a: {← instantiateMVars a}"

9.

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

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

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

  Meta.withTransparency Meta.TransparencyMode.reducible do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- [1, instanceDef, defaultDef, irreducibleDef]

  Meta.withTransparency Meta.TransparencyMode.instances do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- [1, 2, defaultDef, irreducibleDef]

  Meta.withTransparency Meta.TransparencyMode.default do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- [1, 2, 3, irreducibleDef]

  Meta.withTransparency Meta.TransparencyMode.all do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- [1, 2, 3, 4]

  -- Note: if we don't set the transparency mode, we get a pretty strong `TransparencyMode.default`.
  let reducedExpr ← Meta.reduce constantExpr
  dbg_trace (← ppExpr reducedExpr) -- [1, 2, 3, irreducibleDef]

10.

-- Non-idiomatic: we can only use `Lean.mkAppN`.
def tenA : MetaM Expr := do
  let body := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 1, Expr.bvar 0]
  return Expr.lam `x (Expr.const `Nat []) body BinderInfo.default

-- Idiomatic: we can use both `Lean.mkAppN` and `Lean.Meta.mkAppM`.
def tenB : MetaM Expr := do
  Lean.Meta.withLocalDecl `x .default (Expr.const `Nat []) (fun x => do
    -- let body := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 1, x]
    let body ← Lean.Meta.mkAppM `Nat.add #[Lean.mkNatLit 1, x]
    Lean.Meta.mkLambdaFVars #[x] body
  )

#eval show MetaM _ from do
  ppExpr (← tenA) -- fun x => Nat.add 1 x
#eval show MetaM _ from do
  ppExpr (← tenB) -- fun x => Nat.add 1 x

11.

def eleven : MetaM Expr :=
  return Expr.forallE `yellow (Expr.const `Nat []) (Expr.bvar 0) BinderInfo.default

#eval show MetaM _ from do
  dbg_trace (← eleven) -- forall (yellow : Nat), yellow

12.

-- Non-idiomatic: we can only use `Lean.mkApp3`.
def twelveA : MetaM Expr := do
  let nPlusOne := Expr.app (Expr.app (Expr.const `Nat.add []) (Expr.bvar 0)) (Lean.mkNatLit 1)
  let forAllBody := Lean.mkApp3 (Expr.const ``Eq []) (Expr.const `Nat []) (Expr.bvar 0) nPlusOne
  let forAll := Expr.forallE `n (Expr.const `Nat []) forAllBody BinderInfo.default
  return forAll

-- Idiomatic: we can use both `Lean.mkApp3` and `Lean.Meta.mkEq`.
def twelveB : MetaM Expr := do
  withLocalDecl `n BinderInfo.default (Expr.const `Nat []) (fun x => do
    let nPlusOne := Expr.app (Expr.app (Expr.const `Nat.add []) x) (Lean.mkNatLit 1)
    -- let forAllBody := Lean.mkApp3 (Expr.const ``Eq []) (Expr.const `Nat []) x nPlusOne
    let forAllBody ← Lean.Meta.mkEq x nPlusOne
    let forAll := mkForallFVars #[x] forAllBody
    forAll
  )

#eval show MetaM _ from do
  ppExpr (← twelveA) -- (n : Nat) → Eq Nat n (Nat.add n 1)

#eval show MetaM _ from do
  ppExpr (← twelveB) -- ∀ (n : Nat), n = Nat.add n 1

13.

def thirteen : MetaM Expr := do
  withLocalDecl `f BinderInfo.default (Expr.forallE `a (Expr.const `Nat []) (Expr.const `Nat []) .default) (fun y => do
    let lamBody ← withLocalDecl `n BinderInfo.default (Expr.const `Nat []) (fun x => do
      let fn := Expr.app y x
      let fnPlusOne := Expr.app y (Expr.app (Expr.app (Expr.const `Nat.add []) (x)) (Lean.mkNatLit 1))
      let forAllBody := mkApp3 (mkConst ``Eq []) (Expr.const `Nat []) fn fnPlusOne
      let forAll := mkForallFVars #[x] forAllBody
      forAll
    )
    let lam := mkLambdaFVars #[y] lamBody
    lam
  )

#eval show MetaM _ from do
  ppExpr (← thirteen) -- fun f => (n : Nat) → Eq Nat (f n) (f (Nat.add n 1))

14.

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

  let (_, _, conclusion) ← forallMetaTelescope expr
  dbg_trace conclusion -- And ?_uniq.10 ?_uniq.10

  let (_, _, conclusion) ← forallMetaBoundedTelescope expr 2
  dbg_trace conclusion -- (Or ?_uniq.14 ?_uniq.15) -> ?_uniq.15 -> (And ?_uniq.14 ?_uniq.14)

  let (_, _, conclusion) ← lambdaMetaTelescope expr
  dbg_trace conclusion -- forall (a.1 : Prop) (b.1 : Prop), (Or a.1 b.1) -> b.1 -> (And a.1 a.1)

15.

#eval show MetaM Unit from do
  let a ← Lean.Meta.mkFreshExprMVar (Expr.const `String []) (userName := `a)
  let b ← Lean.Meta.mkFreshExprMVar (Expr.sort (Nat.toLevel 1)) (userName := `b)
  -- ?a + Int
  let c := Lean.mkAppN (Expr.const `Nat.add []) #[a, Expr.const `Int []]
  -- "hi" + ?b
  let d := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkStrLit "hi", b]

  IO.println s!"value in c: {← instantiateMVars c}" -- Nat.add ?_uniq.1 Int
  IO.println s!"value in d: {← instantiateMVars d}" -- Nat.add String ?_uniq.2

  let state : SavedState ← saveState
  IO.println "\nSaved state\n"

  if ← Lean.Meta.isDefEq c d then
    IO.println true
    IO.println s!"value in c: {← instantiateMVars c}"
    IO.println s!"value in d: {← instantiateMVars d}"

  restoreState state
  IO.println "\nRestored state\n"

  IO.println s!"value in c: {← instantiateMVars c}"
  IO.println s!"value in d: {← instantiateMVars d}"

import Lean
import Lean.Parser.Syntax
import Std.Util.ExtendedBinder

open Lean Elab Command Term

Syntax: Solutions

1.

namespace a
  scoped notation:71 lhs:50 " 💀 " rhs:72 => lhs - rhs
end a

namespace b
  set_option quotPrecheck false
  scoped infixl:71 " 💀 " => fun lhs rhs => lhs - rhs
end b

namespace c
  scoped syntax:71 term:50 " 💀 " term:72 : term
  scoped macro_rules | `($l:term 💀 $r:term) => `($l - $r)
end c

open a
#eval 5 * 8 💀 4 -- 20
#eval 8 💀 6 💀 1 -- 1

2.

syntax "good morning" : term
syntax "hello" : command
syntax "yellow" : tactic

-- Note: the following are highlighted in red, however that's just because we haven't implemented the semantics ("elaboration function") yet - the syntax parsing stage works.

#check_failure good morning -- the syntax parsing stage works

/-- error: elaboration function for 'commandHello' has not been implemented -/
hello -- the syntax parsing stage works

/-- error: tactic 'tacticYellow' has not been implemented -/
example : 2 + 2 = 4 := by
  yellow -- the syntax parsing stage works

#check_failure yellow -- error: `unknown identifier 'yellow'`

3.

syntax (name := colors) (("blue"+) <|> ("red"+)) num : command

@[command_elab colors]
def elabColors : CommandElab := fun stx => Lean.logInfo "success!"

blue blue 443
red red red 4

4.

syntax (name := help) "#better_help" "option" (ident)? : command

@[command_elab help]
def elabHelp : CommandElab := fun stx => Lean.logInfo "success!"

#better_help option
#better_help option pp.r
#better_help option some.other.name

5.

-- Note: std4 has to be in dependencies of your project for this to work.
syntax (name := bigsumin) "∑ " Std.ExtendedBinder.extBinder "in " term "," term : term

@[term_elab bigsumin]
def elabSum : TermElab := fun stx tp =>
  return mkNatLit 666

#eval ∑ x in { 1, 2, 3 }, x^2

def hi := (∑ x in { "apple", "banana", "cherry" }, x.length) + 1
#eval hi

import Lean
open Lean Elab Command Term Meta

Elaboration: Solutions

1.

elab n:term "♥" a:"♥"? b:"♥"? : term => do
  let nExpr : Expr ← elabTermEnsuringType n (mkConst `Nat)
  if let some a := a then
    if let some b := b then
      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 3)
    else
      return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 2)
  else
    return Expr.app (Expr.app (Expr.const `Nat.add []) nExpr) (mkNatLit 1)

#eval 7 ♥ -- 8
#eval 7 ♥♥ -- 9
#eval 7 ♥♥♥ -- 10

2.

-- a) using `syntax` + `@[command_elab alias] def elabOurAlias : CommandElab`
syntax (name := aliasA) (docComment)? "aliasA " ident " ← " ident* : command

@[command_elab «aliasA»]
def elabOurAlias : CommandElab := λ stx =>
  match stx with
  | `(aliasA $x:ident ← $ys:ident*) =>
    for y in ys do
      Lean.logInfo y
  | _ =>
    throwUnsupportedSyntax

aliasA hi.hello ← d.d w.w nnn

-- b) using `syntax` + `elab_rules`.
syntax (name := aliasB) (docComment)? "aliasB " ident " ← " ident* : command

elab_rules : command
  | `(command | aliasB $m:ident ← $ys:ident*) =>
    for y in ys do
      Lean.logInfo y

aliasB hi.hello ← d.d w.w nnn

-- c) using `elab`
elab "aliasC " x:ident " ← " ys:ident* : command =>
  for y in ys do
    Lean.logInfo y

aliasC hi.hello ← d.d w.w nnn

3.

open Parser.Tactic

-- a) using `syntax` + `@[tactic nthRewrite] def elabNthRewrite : Lean.Elab.Tactic.Tactic`.
syntax (name := nthRewriteA) "nth_rewriteA " (config)? num rwRuleSeq (ppSpace location)? : tactic

@[tactic nthRewriteA] def elabNthRewrite : Lean.Elab.Tactic.Tactic := fun stx => do
  match stx with
  | `(tactic| nth_rewriteA $[$cfg]? $n $rules $_loc) =>
    Lean.logInfo "rewrite location!"
  | `(tactic| nth_rewriteA $[$cfg]? $n $rules) =>
    Lean.logInfo "rewrite target!"
  | _ =>
    throwUnsupportedSyntax

-- b) using `syntax` + `elab_rules`.
syntax (name := nthRewriteB) "nth_rewriteB " (config)? num rwRuleSeq (ppSpace location)? : tactic

elab_rules (kind := nthRewriteB) : tactic
  | `(tactic| nth_rewriteB $[$cfg]? $n $rules $_loc) =>
    Lean.logInfo "rewrite location!"
  | `(tactic| nth_rewriteB $[$cfg]? $n $rules) =>
    Lean.logInfo "rewrite target!"

-- c) using `elab`.
elab "nth_rewriteC " (config)? num rwRuleSeq loc:(ppSpace location)? : tactic =>
  if let some loc := loc then
    Lean.logInfo "rewrite location!"
  else
    Lean.logInfo "rewrite target!"

example : 2 + 2 = 4 := by
  nth_rewriteC 2 [← add_zero] at h
  nth_rewriteC 2 [← add_zero]
  sorry

import Lean.Elab.Tactic
open Lean Elab Tactic Meta

1.

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

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

  -- 1. Create new `_`s with appropriate types.
  let mvarId1 ← mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red")
  let mvarId2 ← mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue") 

  -- 2. Assign the main goal to the expression `Iff.intro _ _`.
  mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2])

  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }

elab "step_2" : tactic => do
  let some redMvarId ← (← get).goals.findM? (fun mvarId => do
    return (← mvarId.getDecl).userName == `red
  ) | throwError "No mvar with username `red`"
  let some blueMvarId ← (← get).goals.findM? (fun mvarId => do
    return (← mvarId.getDecl).userName == `blue
  ) | throwError "No mvar with username `blue`"

  ---- HANDLE `red` goal
  let Expr.forallE _ redFrom redTo _ := (← redMvarId.getDecl).type | throwError "Goal type is not of the form `a → b`"
  let handyRedMvarId ← withLocalDecl `hA BinderInfo.default redFrom (fun fvar => do
    -- 1. Create new `_`s with appropriate types.
    let mvarId1 ← mkFreshExprMVar redTo MetavarKind.syntheticOpaque `red
    -- 2. Assign the main goal to the expression `fun hA => _`.
    redMvarId.assign (← mkLambdaFVars #[fvar] mvarId1)
    -- just a handy way to return a handyRedMvarId for the next code
    return mvarId1.mvarId!
  )
  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [handyRedMvarId, blueMvarId] }

  ---- HANDLE `blue` goal
  let Expr.forallE _ blueFrom _ _ := (← blueMvarId.getDecl).type | throwError "Goal type is not of the form `a → b`"
  -- 1. Create new `_`s with appropriate types.
  -- None needed!
  -- 2. Assign the main goal to the expression `fun hB : q ∧ p => (And.intro hB.right hB.left)`.
  Lean.Meta.withLocalDecl `hB .default blueFrom (fun hB => do
    let body ← Lean.Meta.mkAppM `And.intro #[← Lean.Meta.mkAppM `And.right #[hB], ← Lean.Meta.mkAppM `And.left #[hB]]
    blueMvarId.assign (← Lean.Meta.mkLambdaFVars #[hB] body)
  )
  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [handyRedMvarId] }

elab "step_3" : tactic => do
  let mvarId ← getMainGoal
  let goalType ← getMainTarget
  let mainDecl ← mvarId.getDecl

  let Expr.app (Expr.app (Expr.const `And _) q) p := goalType | throwError "Goal type is not of the form `And q p`"

  -- 1. Create new `_`s with appropriate types.
  let mvarId1 ← mkFreshExprMVarAt mainDecl.lctx mainDecl.localInstances q (userName := "red1")
  let mvarId2 ← mkFreshExprMVarAt mainDecl.lctx mainDecl.localInstances p (userName := "red2")

  -- 2. Assign the main goal to the expression `And.intro _ _`.
  mvarId.assign (← mkAppM `And.intro #[mvarId1, mvarId2])

  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }

elab "step_4" : tactic => do
  let some red1MvarId ← (← get).goals.findM? (fun mvarId => do
    return (← mvarId.getDecl).userName == `red1
  ) | throwError "No mvar with username `red1`"
  let some red2MvarId ← (← get).goals.findM? (fun mvarId => do
    return (← mvarId.getDecl).userName == `red2
  ) | throwError "No mvar with username `red2`"

  ---- HANDLE `red1` goal
  -- 1. Create new `_`s with appropriate types.
  -- None needed!
  -- 2. Assign the main goal to the expression `hA.right`.
  let some hA := (← red1MvarId.getDecl).lctx.findFromUserName? `hA | throwError "No hypothesis with name `hA` (in goal `red1`)"
  red1MvarId.withContext do
    red1MvarId.assign (← mkAppM `And.right #[hA.toExpr])
  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [red2MvarId] }

  ---- HANDLE `red2` goal
  -- 1. Create new `_`s with appropriate types.
  -- None needed!
  -- 2. Assign the main goal to the expression `hA.left`.
  let some hA := (← red2MvarId.getDecl).lctx.findFromUserName? `hA | throwError "No hypothesis with name `hA` (in goal `red2`)"
  red2MvarId.withContext do
    red2MvarId.assign (← mkAppM `And.left #[hA.toExpr])
  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [] }

theorem gradual (p q : Prop) : p ∧ q ↔ q ∧ p := by
  step_1
  step_2
  step_3
  step_4

2.

elab "forker_a" : tactic => do
  liftMetaTactic fun mvarId => do
    let (Expr.app (Expr.app (Expr.const `And _) p) q) ← mvarId.getType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")

    let mvarIdP ← mkFreshExprMVar p (userName := "red")
    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")

    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
    mvarId.assign proofTerm

    return [mvarIdP.mvarId!, mvarIdQ.mvarId!]

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

  let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")

  mvarId.withContext do
    let mvarIdP ← mkFreshExprMVar p (userName := "red")
    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")

    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
    mvarId.assign proofTerm

    setGoals ([mvarIdP.mvarId!, mvarIdQ.mvarId!] ++ (← getGoals).drop 1)

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

  let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId ("Goal is not of the form P ∧ Q")

  mvarId.withContext do
    let mvarIdP ← mkFreshExprMVar p (userName := "red")
    let mvarIdQ ← mkFreshExprMVar q (userName := "blue")

    let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
    mvarId.assign proofTerm

    replaceMainGoal [mvarIdP.mvarId!, mvarIdQ.mvarId!]

example (A B C : Prop) : A → B → C → (A ∧ B) ∧ C := by
  intro hA hB hC
  forker_a
  forker_a
  assumption
  assumption
  assumption

3.

elab "introductor_a" : tactic => do
  withMainContext do
    liftMetaTactic fun mvarId => do
      let (_, mvarIdNew) ← mvarId.introN 2
      return [mvarIdNew]

elab "introductor_b" : tactic => do
  withMainContext do
    liftMetaTactic fun mvarId => do
      let (_, mvarIdNew) ← mvarId.intro1P
      return [mvarIdNew]

elab "introductor_c" : tactic => do
  withMainContext do
    liftMetaTactic fun mvarId => do
      let (_, mvarIdNew) ← mvarId.intro `wow
      return [mvarIdNew]

-- So:
-- `intro`   - **intro**, specify the name manually
-- `intro1`  - **intro**, make the name inacessible
-- `intro1P` - **intro**, preserve the original name
-- `introN`  - **intro many**, specify the names manually
-- `introNP` - **intro many**, preserve the original names

example (a b c : Nat) : (ab: a = b) → (bc: b = c) → (a = c) := by
  introductor_a
  -- introductor_b
  -- introductor_c
  sorry