Lean4

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

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

工具链

gentoo安装

emege -v sci-mathematics/lean

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

交互

Lean4有很多交互式函数

#eval: 执行后面的表达式
#check: 类型检查

类型

和Rust一样使用:作为类型标注但是注意

在Lean中 :的优先级很低所以必须这样写

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

类型定义

结构体

structure Point where 
	x: Float
	y: Float
	z: Float

这里有一个语法糖

如果需要修改结构中的少量值可以这么写

def zeroX (p : Point) :Point :=
	{p with x := 0}

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

闭包与lambda

闭包的形式为

f: Float → Float

lambda的形式为

(fun arg1 => expr)

举个例子

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是经典的归纳数据类型

inductive Bool where
	| false : Bool
	| true : Bool
	
inductive Nat where
	| zero : Nat
	| succ (n : Nat) : Nat

其中 succ代表后继

任何Nat都可以表示为0的若干个后继

模式匹配

match Nat.zero with
	| Nat.zero => true
	| Nat.succ k => false

Rat

有理数类型写为ℚ

实现为一对整数的分数其中: 分母为正数,且分子与分母互质

structure Rat where
  -- 通过各个组件构造一个有理数。 我们将构造函数重命名为 mk'，以避免与“智能构造函数”发生冲突
  -- 建议使用封装后的智能构造函数而不是mk'
  mk' :: -- 原始的构造函数
  num : Int -- 分子
  den : Nat := 1 -- 分母
  den_nz : den ≠ 0 := by decide -- 属性: 分母不为0
  reduced : num.natAbs.Coprime den := by decide -- 属性: 分子分母必须互质
  deriving DecidableEq, Hashable -- 类似Rust的#[derive]

关键字

let: 赋值
have: 提出一个假设或中间证明

函数

在rust中函数定义为

fn a() -> String {
	"ok".to_string()
}
fn b(arg1: i32,arg2: i32) -> i32 {
	arg1 + arg2 + 1
}

在lean中

def a : String := "ok"
def b(arg1: Int)(arg2: Int): Int := arg1 + arg2 + 1

定理与命题

在Lean中 命题是类型证明是值

Tactics

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

rfl: 证明两边定义相等 注意是定义相等

example : 1 + 1 = 2 := by
	rfl

Built-in

Lean4的内置Tatics

逻辑操作

intro: 引入一个假设或目标

假设命题成立为h

theorem two_not_square_rat : ¬ ∃ q : ℚ, q^2 = 2 := by
  intro h

cases: 对命题进行拆解分类讨论
induction: 递归证明比如归纳法

induction n with d hd
rw [add_zero 0]
rfl
rw [add_succ 0 d]
rw [hd]
rfl

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

hd相当于我们在数学归纳法中假设的n=k时成立时的式子

等式化简/转化

rw: 带入
refl: 证明自反性

Mathlib

Mathlib库的tatics

逻辑操作

rcases: 递归cases

把h拆开为 q: 若命题成立 q^2=2的q, hq: 证明q^2 = 2的证据

theorem two_not_square_rat : ¬ ∃ q : ℚ, q^2 = 2 := by
  intro h
  rcases h with ⟨q, hq⟩

等式化简/转化

norm_cast: 类型转换