Lean

安装

# linux, Ubuntu (会自动装vscode，如果你已经装了vscode，直接打开vscode去插件市场手动安装lean4插件就可以开始上手了)
wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

# MacOS
/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_macos.sh)" && source ~/.profile

# Windows
https://leanprover-community.github.io/install/windows.html

elan self update  # 以防你下载的不是最新版elan  
# 下载及应用最新的Lean4版本 (https://github.com/leanprover/lean4/releases) 
elan default leanprover/lean4:stable

#eval Lean.versionString

开启新项目

创建新Lean项目

最简新项目

lake init <your_project_name>

带mathlib的新项目

lake +leanprover-community/mathlib4:lean-toolchain new <your_project_name> math

require mathlib from git 
    "https://github.com/leanprover-community/mathlib4"

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake update
lake exe cache get

Lean4证明器正式版的安装教程 - 知乎 (zhihu.com)

教程

Lean4 是一个函数式语言

def addOne(x : Int) : Int := x + 1

def addOne(x : Int) := x + 1

多参数函数

# 这是 Python 代码
def add1(x : Int , y : Int):
  return x + y

# 这是 Python 代码
def add2(x : Int):
  return lambda y : x + y

def add (x : Int) (y : Int) := x + y

def add (x y : Int) := x + y

lambda 表达式

def add := fun (x y : Int) => x + y

def add : Int → Int → Int := fun x y => x + y

Lean4 是一个强类型语言

一些常用类型

3  : Int -- 整数
-2 : Int 
0 : Nat -- 自然数
1 : Nat
2 : Nat
3.14 : Float -- 浮点数
3.00 : Float
'c' : Char -- 字符
"Hello" : String -- 字符串
true : Bool -- 布尔
false : Bool 
() : Unit -- 单元类型, 这个类型只有一个元素 ()
fun (x : Int) => x + 1 : Int → Int

定义类型

structure Point2D where
  x : Float
  y : Float
deriving Repr

def origin : Point2D := Point2D.mk 0.0 0.0

def origin : Point2D := {x := 0.0, y := 0.0}

structure Point2D where
  point :: 
  x : Float
  y : Float
deriving Repr 
#check Point2D.point -- Point2D.point (x y : Float) : Point2D

#eval origin.x -- 0
#eval origin.y -- 0

归纳类型

inductive Bool where
  | false : Bool
  | true : Bool

Bool.true : Bool
Bool.false : Bool

// 这是 Rust
enum Bool {
  True, 
  False,
}

def myNot (b : Bool) :=
  match b with
  | Bool.true => Bool.false
  | Bool.false => Bool.true

def myNot : Bool → Bool 
| Bool.true => Bool.false
| Bool.false => Bool.true

inductive Shape where
  | rect (a b : Float) : Shape
  | circ (r : Float)   : Shape
deriving Repr

def area (s : Shape) := match s with
  | Shape.rect a b => a * b
  | Shape.circ r => 3.14 * r * r
#eval area (Shape.rect 2 3) -- 6.000000
#eval area (Shape.circ 1)   -- 3.140000

归纳的类型和递归

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

open Nat -- 打开Nat命名空间, 这样我们就可以直接写 zero 和 succ 而不是 Nat.zero ...
#check zero -- 这代表 0
#check succ zero -- 这代表 1
#check succ (succ zero) -- 这代表 2
...

def myAdd (m n : Nat) := match m with
  | zero    => n
  | succ pm => succ (myAdd pm n)

def checkCollatz (n : Nat) : Unit :=
  if n == 1 || n == 0 then
    ()
  else if Nat.mod n 2 == 0 then
    checkCollatz (Nat.div n 2)
  else
    checkCollatz (3 * n + 1)

partial def checkCollatz (n : Nat) : Unit :=
  if n == 1 || n == 0 then
    ()
  else if Nat.mod n 2 == 0 then
    checkCollatz (Nat.div n 2)
  else
    checkCollatz (3 * n + 1)

inductive List α where
  | nil : List α
  | cons (head : α) (tail : List α) : List α

inductive Sum (α : Type _) (β : Type _) where
  | inl (val : α) : Sum α β
  | inr (val : β) : Sum α β
structure Prd (α : Type _) (β : Type _) where
  fst : α
  snd : β

Lean4 是一个"命令式语言"

def main : IO Unit := do
  let stdin ← IO.getStdin
  if let [some a,some b] := Functor.map String.toNat? ((←stdin.getLine).split (· == ' ')) then
    IO.println (a + b)
  else
    IO.println "Read Error"

-- 计算 1 + 2 + ... + 100
def main : IO Unit := do
  let mut sum := 0
  for i in List.range 101 do
    sum := sum + i
  IO.println sum

-- 从一数到一百
def main : IO Unit := do
  let mut i := 1
  while True do
    if i > 100 then
      break
    IO.println i
    i := i + 1

Lean4 是一个依值类型语言

inductive Vec : Nat → Type _ → Type _ where
  | nil : Vec 0 α
  | cons : α → Vec n α → Vec (Nat.succ n) α

structure Key where
  user : String
inductive DoorState where 
  | SOpen (key : Key) | SClosed (key : Key) | SLocked
open DoorState
inductive DoorCmd : (before after : DoorState) -> Type _ → Type _ where
  | Open   : DoorCmd (SClosed key) (SOpen key) Unit
  | Close  : DoorCmd (SOpen key) (SClosed key) Unit
  | Lock   : DoorCmd (SClosed key) SLocked Unit
  | Unlock : (key : Key) → DoorCmd SLocked (SClosed key) Unit
  | GenKey : String → DoorCmd α α Key
  | pure   : α → DoorCmd β β α
  | bind   : DoorCmd α β T → (T → DoorCmd β γ S) → DoorCmd α γ S
open DoorCmd

def proc : DoorCmd SLocked SLocked Unit :=
  bind (GenKey "admin") fun key =>
  bind (Unlock key) fun _ =>
  bind Open  fun _ =>
  bind Close fun _ =>
  bind Lock  fun _ =>
  pure ()

def proc : DoorCmd SLocked SLocked Unit :=
  bind (GenKey "admin") fun key =>
  bind (Unlock key) fun _ =>
  bind Open fun _ =>
  bind Lock fun _ =>
  pure ()
-- application type mismatch
--   DoorCmd.bind Lock
-- argument
--   Lock
-- has type
--   DoorCmd (SClosed ?m.21251) SLocked Unit : Type 1
-- but is expected to have type
--   DoorCmd (SOpen key) ?m.21247 ?m.21248 : Type 1

def interpret : DoorCmd α β T → IO T
| Open (key := key) => IO.println s!"Door opened with {key.user}'s key."
| Close => IO.println "Door closed."
| Lock => IO.println "Door locked."
| Unlock ⟨ user ⟩ => IO.println s!"Door unlocked by {user}"
| GenKey user => do
    IO.println s!"Generated a key for {user}"
    return (Key.mk user);
| DoorCmd.pure x => do return x
| DoorCmd.bind m f => do
    let x <- interpret m
    interpret (f x)

#eval interpret proc
-- print:
--  Generated a key for admin
--  Door unlocked by admin
--  Door opened with admin's key.
--  Door closed.
--  Door locked.

notation "let " e " <- " exp "in" other => DoorCmd.bind exp (fun e => other)
notation e1 ";" e2 => (let _ <- e1 in e2)
notation e ";" => e ; pure ()
def proc' : DoorCmd SLocked SLocked Unit :=
  let key <- (GenKey "admin") in
  Unlock key;
  Open;
  Close;
  Lock;

Lean4 是一个定理证明器