Programming in Lean Release 3.4.2

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

摘要

文档介绍了Lean 3.4.2作为一个多功能系统的使用方式，包括作为编程语言、程序属性验证系统和元程序写作平台。它详细描述了Lean的类型系统、基本编程概念、输入输出机制以及高级功能如元变量和统一。文档还展示了如何通过具体示例理解和应用这些功能，如依赖类型的使用、函数定义和策略的编写。

AI总结

《Programming in Lean Release 3.4.2》文档总结：

1. **Lean的多重用途**：
- **编程语言**：支持一般的程序开发。
- **程序验证系统**：用于验证程序的性质。
- **元程序系统**：允许编写扩展Lean自身功能的程序。

2. **元程序与`meta`关键字**：
- 使用`meta`关键字可以编写元程序。
- 特性：
* 允许任意递归调用，无需担心终止。
* 可以访问元常量（即实现于Lean内部的原始函数和对象）。

3. **输入与输出（IO）**：
- `io`指令用于处理输入输出操作。
- `io`指令在逻辑基础中是不透明的。
- 这种设计允许验证不依赖具体输入输出结果的程序。

4. **函数与类型**：
- **函数定义**：
* 隐式参数（使用花括号`{}`）可以由Lean自动生成。
* 显式参数需要在函数调用时明确提供。
- **类型系统**：
* 基于Calculus of Inductive Constructions（CIC）。
* 类型是对象，函数可以依赖类型。
* 例如：多态恒等函数`id`的定义与使用。
- **基础类型**：
* 包括自然数`nat`、整数`int`、列表`list`和布尔值`bool`等。
* 使用`#check`、`#print`等指令可以查询类型和定义。
* 例如：

       #check nat
       #print nat

       #check int
       #print int

5. **元变量与统一（Unification）**：
- **元变量**：
* 用于表示尚未确定的术语。
* 目标列表中的目标实际上是元变量。
- **策略**：
* `get_goals`和`set_goals`用于操作目标列表。
* `unify`策略用于统一元变量。

6. **基本操作与数据类型**：
- **表达式操作**：
* `#reduce`用于归约表达式。
* `#eval`用于计算表达式的结果。
* 例如：

       #reduce (λ x, x + 3) 2
       #eval (λ x, x + 3) 2

- **集合与对**：
* 例如：

       variables (a b : α) (n : N)
       #check (a1, a2)
       #check (n, b)
       #reduce (n, b).1
       #eval (n, b).1

- **隐式参数**：
* 某些参数可以由Lean自动生成。
* 使用双花括号`{{`可以强制隐式参数的生成。

7. **标准库功能**：
- 支持的数据类型和操作包括加法`has_add.add`、乘法`has_mul.mul`、列表操作`append`等。
- 例如：

     #check @has_add.add
     #check @has_mul.mul
     #check @append

8. **CIC基础**：
- Lean的基础逻辑系统是一个版本的Calculus of Inductive Constructions（CIC）。
- 支持定义各种数学对象（如自然数、整数、复数等）和数据类型。
- 支持写数据类型和程序的同时，也支持数学证明。