Lean 策略编程指南

1. 从证明状态开始🔗

策略本质上是读取并改变证明状态的程序。本章是中文迁移格式的最小示范：正文、 内联 Lean 代码和可检查的代码块都与书一起编译。

1.1. 第一个策略程序🔗

下面的证明使用内建策略关闭目标。Verso 会在构建文档时检查它，而不是只做语法高亮。

example : True := ⊢ True All goals completed! 🐙

可以把 (show True from by trivial) 理解为一个最小的策略程序：输入是目标 True，输出是一个 不再含有未解决目标的证明状态。

1.2. 本书的三篇教程🔗

三个上游教程继续完整保存在仓库根目录，中文 Verso 版分别收入以下三章：

  • TacticProgrammingGuide.lean：策略编程入门；

  • CustomRw.lean：从零实现一次重写；

  • CustomSimp.lean：从零实现简化器。

教程中的故意错误和未完成练习会明确标注并隔离。其余代码由 Verso 或 Book.Support 支持模块实际编译，不能只靠语法高亮冒充可运行。