Lean 2 Quick Reference

• 语言: 英语
• 格式: .pdf
• 来源: leanprover.github.io

摘要

文档是对Lean 2的快速参考指南，详细介绍了其命令、选项和策略。文档包括命令的使用方法，如检查表达式、评估表达式、打印信息等；常见选项如隐式参数、宇宙变量、强制显示等；策略如申请定理、介绍假设、等式推理、重写规则等。还介绍了Lean-mode在Emacs中的命令和输出Unicode符号的方法。

AI总结

《Lean 2 Quick Reference》速查指南由Jeremy Avigad、Leonardo de Moura和Soonho Kong编写，主要介绍了Lean 2的使用方法和命令选项。以下是文档的核心内容总结：

### 1. **信息显示**
- ``: 检查表达式类型。
- `eval `: 计算表达式。
- `print `: 显示信息。
- `print notation`：显示所有符号。
- `print prefix `: 显示名称空间中的声明。
- `print coercions`：显示强制转换。
- `print classes`：显示所有类。
- `print metaclasses`：显示元数据。
- `help commands/options`：显示所有命令或选项。

---

### 2. **常见选项**
通过`set_option `更改选项，支持Tab补全。
- `pp.implicit`：显示隐式参数。
- `pp.universes`：显示量 downfall 多变量。
- `pp.coercions`：显示强制转换。
- `pp.abbreviations`：显示缩写。
- `pp.full_names`：使用全名表示标识符。
- `pp.all`：禁用符号、隐式参数、全名和强制转换。
- `pp.beta`：在显示前对表达式进行β归一化。

---

### 3. **一般战术**
- **应用定理**：
- `apply `: 应用定理。
- `fapply `: 应用定理，创建子目标。
- `eapply `: 适用于递归定义。
- `exact `: 应用定理并关闭目标。
- `rexact `: 更宽松的`exact`版本。
- `refine `: 类似`exact`，但解决子目标。

- **假设管理**：
- `intro `: 引入变量或假设。
- `intros `: 同`intro`。
- `rename `: 重命名变量或假设。
- `generalize `: 概括表达式。
- `clear `: 移除变量或假设。
- `revert `: 将变量或假设移到目标。
- `assumption`和`eassumption`：尝试用上下文关闭目标。

---

### 4. **等式推理**
- `esimp`: 简化表达式。
- `unfold `: 展开定义。
- `fold `: 收起表达式。
- `beta`和`whnf`: β归一化和弱头归一化。
- `change `: 更改目标。
- `rewrite `: 应用重写规则。

---

### 5. **重写规则**
- `rewrite []`: 应用一系列重写规则。
- `krewrite`: 使用带键的重写，匹配相同头部。
- `xrewrite`: 更"激进"的重写版本。

---

### 6. **Emacs Lean模式命令**
- **执行命令**：
- `C-c C-e`: 执行Lean命令。
- `C-c C-x`: 在独立模式下执行。
- `C-c C-r`: 重新启动Lean进程。
- **错误处理**：
- `C-c ! n/p/l`: 显示下一个/上一个/错误列表。
- **信息查询**：
- `C-c C-p`: 显示光标处标识符的定义。
- `C-c C-g`: 显示当前目标。
- `C-c C-f`: 填充占位符。
- `C-c C-o`: 设置Lean选项。
- `C-c C-k`: 显示如何输入Unicode符号。

---

### 7. **Unicode符号**
列举了常用逻辑符号及其ASCII表示和输入方式。

---

### 总结
本指南涵盖了Lean 2的核心功能、常用命令、选项、战术和Emacs模式下的快捷键，旨在帮助用户更高效地使用Lean 2进行定理证明和开发。