Lean 2 Quick Reference

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

摘要

文档《Lean 2 Quick Reference》提供了Lean 2编程语言的快速参考指南，涵盖了各种命令和战术的使用方法。内容包括检查和评估表达式、打印信息、设置选项、目标管理、组合战术、等价推理、归纳与情况处理以及特殊用途战术等。文档还介绍了与Lean集成的Emacs模式命令和Unicode符号的使用方法。

AI总结

《Lean 2 Quick Reference》是一份关于Lean 2的快速参考指南，主要介绍了Lean 2的基本命令、战术、选项以及一些高级功能。以下是文档的核心内容总结：

### 1. **显示信息**
- `check `：检查表达式的类型。
- `eval `：评估表达式。
- `print `：打印标识符的相关信息。
- `print notation`：显示所有定义的符号。
- `print axioms`：显示假设公理。
- `print options`：显示用户或Emacs模式设置的选项。

### 2. **常见选项**
- `set_option `：更改选项。
- `pp.implicit`：显示隐式参数。
- `pp.universes`：显示宇宙变量。
- `pp.notation`：使用定义的符号显示输出。
- `pp.full_names`：使用全限定名显示标识符。
- `beta`：在显示前对项进行beta归约。

### 3. **组合战术**
- `and_then `：执行`tac1`后执行`tac2`，支持回溯。
- `or_else `：如果`tac1`失败，则执行`tac2`。
- `par `：并行执行`tac1`和`tac2`。
- `repeat `：重复执行`tac`，直到失败。
- `at_most `：最多执行`tac` ``次。

### 4. **目标管理**
- `focus_at `：专注于第`i`个目标，若未解决则失败。
- `focus `：等同于`focus_at 0`。
- `rotate_left `：将目标向左旋转``次。
- `rotate_right `：将目标向右旋转``次。
- `all_goals `：对所有目标执行`tac`。

### 5. **信息与调试**
- `state`：显示当前证明状态。
- `trace `：显示当前字符串。
- `with_options [] `：使用不同选项执行单个战术。

### 6. **通用战术**
- `apply `：应用定理，生成子目标。
- `fapply `：类似`apply`，但生成更多子目标。
- `eapply `：用于应用前导定义。
- `exact `：应用表达式以解决目标。
- `intro `：引入变量或假设。
- `clear `：移除变量或假设。
- `assumption`：尝试用上下文中的内容解决目标。

### 7. **等式推理**
- `esimp`：简化目标中的表达式。
- `unfold `：展开定义。
- `rewrite `：应用重写规则。
- `change `：如果可转换，则将目标改为``。

### 8. **归纳与情况分解**
- `cases `：分解归纳类型。
- `induction `：使用归纳法。
- `constructor`：应用第一个成功构造器。
- `split`：仅适用于单构造归纳类型。

### 9. **特殊用途战术**
- `contradiction`：解决矛盾目标。
- `exfalso`：实现“从假到任意”逻辑。
- `congruence`：解决形式为`f a_1 ...a_n = f' b_1 ...b_n`的目标。

### 10. **其他**
- 提供了与Lean集成的Emacs命令和一些Unicode符号的输入方法。
- 包含了对Lean特定命令的简要说明，如显示当前目标、设置选项等。

这份文档为使用Lean 2提供了全面的参考，涵盖了从基本命令到高级战术的使用方法。