# Lean4
Lean4是一个完备的**编程语言** 侧重于**数学定理证明**

Lean是一种严格的**纯函数式语言**

## 工具链
gentoo安装
```bash
emege -v sci-mathematics/lean
```

- lake: 库依赖管理器 相当于Rust的Cargo
- lean: 编译器

## 交互
Lean4有很多交互式函数

- `#eval`: 执行后面的表达式
- `#check`: 类型检查
## 类型
和Rust一样 使用`:`作为类型标注 但是注意 
>在Lean中 `:`的优先级很低 所以必须这样写

```lean
#eval (1 : Nat) - (2 : Nat)
```

类型定义

- 结构体
```lean
structure Point where 
	x: Float
	y: Float
	z: Float
```

这里有一个语法糖

如果需要修改结构中的少量值 可以这么写
```lean
def zeroX (p : Point) :Point :=
	{p with x := 0}
```

也就是说 需要修改的值写在关键字`with`后面 

- 闭包与lambda

闭包的形式为 
```lean
f: Float → Float
```

lambda的形式为

```lean
(fun arg1 => expr)
```

举个例子
```lean
def _point (p: Point) (f: Float → Float) : Point :=
    {x := f p.x,y := f p.y}

#eval _point b (fun a => a + 0.1)
```

- 归纳数据类型

可以通过**数学归纳法**来证明它们的陈述的类型

Bool和Nat是经典的归纳数据类型

```lean
inductive Bool where
	| false : Bool
	| true : Bool
	
inductive Nat where
	| zero : Nat
	| succ (n : Nat) : Nat
```
其中 succ代表后继 
>任何Nat都可以表示为0的若干个后继

- 模式匹配
```lean
match Nat.zero with
	| Nat.zero => true
	| Nat.succ k => false
```
## 函数
在rust中函数定义为
```rust
fn a() -> String {
	"ok".to_string()
}
fn b(arg1: i32,arg2: i32) -> i32 {
	arg1 + arg2 + 1
}
```

在lean中
```lean
def a : String := "ok"
def b(arg1: Int)(arg2: Int): Int := arg1 + arg2 + 1
```
## 定理与命题
在Lean中 **命题是类型 证明是值**


## Tactics
Tactics在Lean中用于处理证明任务 通过tactics来控制证明过程

- `rfl`: 证明两边**定义相等** 注意是定义相等
```lean
example : 1 + 1 = 2 := by
	rfl
```
- `induction`: 递归证明 比如归纳法
```lean
induction n with d hd
rw [add_zero 0]
rfl
rw [add_succ 0 d]
rw [hd]
rfl
```

其中 n为要归纳的变量 d为归纳假设的变量名 hd为归纳假设的名称

hd相当于我们在数学归纳法中 假设的n=k时成立时的式子
- `intro`: 引入一个假设或目标
- `exact`: 提供一个具体的证明对象
- `apply`: 尝试应用一个定理或者引理来证明
- `assumption`: 若当前目标是某个假设的结论 就使用它来证明
- `refl`: 如果目标是一个等式 且相等
- `split`: 当目标是一个AND时 分解为两个子目标