Lean4

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

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

工具链

gentoo安装

emege -v sci-mathematics/lean

Lean4有很多交互式函数

和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后面

闭包的形式为

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

在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在Lean中用于处理证明任务通过tactics来控制证明过程

example : 1 + 1 = 2 := by
	rfl

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

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

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