Lean4-1 —— Lean4 的基本使用

上一篇：Lean4-0 —— Lean4 的安装

这里假定大家有一定C语言、Python基础。

注释：单行注释：-- 注释，多行注释：/- 多行注释 -/。下面的代码中会使用注释来标记代码的解释说明或者Lean的返回结果。Lean是很方便的，它往往能实时向我们返回结果。

1. Lean4 中的声明、检查与求值

下面先列出对应的关键字：

  • 声明（Define） def：用于声明一个新的常量
  • 检查（Check） #check：用于检查一个对象的类型
  • 求值（Evaluate） #eval：用于计算给出的表达式

以井号开头的都是用于向Lean系统询问信息的辅助命令，比如这里的 #check 和 #eval。

例子：

/- 定义常数 -/
def m : Nat := 1
def b : Bool := true
/- 检查类型 -/
#check m
#check b
/- 求值 -/
#eval m + 6
#eval b && false

2. Lean4 的基本使用

Lean中的任意表达式都有一个类型。 Lean是用于构建复杂表达式的工具，基于 依值类型论（Dependent Type Theory） 这一形式语言。

2.0 依值类型论

类型论是一类基于 λ\lambda 演算的形式理论的统称，所有数学对象都有各自的类型。而依值类型论是一种类型的定义可以依赖于值（由值所推断）的类型论，可以写成：

Γ⊢A type\Gamma \vdash A\text{ type}

依值类型论的一些概念并不容易理解，但是我们可以将依值类型论和我们熟知的数理逻辑作如下对应（但不能完全等同）：

数理逻辑 依值类型论
语境 语境
命题 类型
命题宇宙 宇宙
全称量词 Π\Pi 类型（积类型）
存在量词 Σ\Sigma 类型（和类型）
  • 语境：相继式 ⊢\vdash 左边的部分，也称上下文或先决条件。
  • 类型：类似于集合，但与集合不同。类型直接通过规则定义。
  • 宇宙：可以理解为“类型的类型”，虽然这样并不准确。
  • Σ\Sigma 类型：定义的一种新类型，类似于将类型合并整合成一个新类型。如C语言中的联合体。
  • Π\Pi 类型：定义的一种新类型，展现出来的类型随输入实例类型变化。如C语言中的结构体。

2.1 Lean4 编程基础

万物皆函数。

2.1.1 Lean4 的 “Hello, World!”

函数的形式

在我们学习C语言等高级语言时，函数往往都写成 func(x) 的形式，而在 Lean （或 Haskell、Lisp 等）语言中朋友们应当习惯直接将参数写在函数后面：

#eval String.append "Hello, " "World!"

实际上实现的效果就是：String.append("Hello, ", "World")，但是这样写语法并不正确，所以这里用一根删除线划掉

当然你也可以类似 Python 点号标记来调用函数的写法：

#eval "Hello, ".append "World!"

这样的函数也是有一定执行顺序的，比如对比下面两个语句：

-- #eval String.append String.append "Hello" ", " "world!" （不可执行）
#eval String.append (String.append "Hello" ", ") "world!"
-- #eval String.append "Hello" String.append ", " "world!" （不可执行）
#eval String.append "Hello" (String.append ", " "world!")

而这个函数的值就是这个表达式所计算出来的值。

条件表达式（ITE表达式）

ITE表达式即 If-Then-Else 表达式，实际上就类似于 C语言 中的三目运算符 ; ? 或 Python 中的 <statement1> if <condition> else <statement2> ，那么在Lean中就有：

#eval String.append "Oh! " (if 1 > 2 then "Yes!" else "No!")
-->
#eval String.append "Oh! " (if false then "Yes!" else "No!")
-->
#eval String.append "Oh! " "No!"
--> "Oh! No!"

定义

功能 例子 效果
定义常量 def YES := "Yes!" #eval String.append "Oh! " YES
定义函数（单元） def succ1 (n : Nat) : Nat := n + 1 #eval succ1 6
定义函数（多元） def succk (n : Nat) (k : Nat) : Nat := n + k #eval succk 3 6
定义类型（类似于 typedef ） def Str : Type := String def HELLO : Str := "Hello, World!"

注：Nat 表示自然数，Type 表示“类型的类型”

不过可能遇到下面这个问题，首先定义：

def NaturalNum : Type := Nat

那么下面这段代码就会报错：

def sixteen : NatrualNum := 16 -- Wrong!

这是因为 16 被认为是歧义的，我们需要指定右边 16 的类型，即重载（Overload）：

def sixteen : NatrualNum := (16 : Nat) -- Right!

当然你也可以使用 abbrev 关键字来解决这个问题：

abbrev NNNNat : Type := Nat
def sixteen' : NNNNat := 16

而像 abbrev 生成的定义会被标记为可约（Reducible）定义，即可展开的定义，而当我们完全展开所有定义可能会产生十分大的类型（正如第一小节依值类型论所涉及到的），控制这种可约定义对 Lean 的灵活性有着关键作用。

2.1.2 柯里化（Currying）

柯里化指的是把接受多个参数的函数转换成接受单个参数的函数，可以理解为每接受一个参数就产生一个新函数，即逐个带入函数的参数（即使用返回函数的函数来实现多参数函数），以数学家哈斯克尔·柯里（Haskell Curry）命名。柯里化能够一定程度上解决重复传参问题，提高函数适用性。

在Python中考虑这样形式的函数（虽然我们并不建议使用Python中lambda表达式语法糖）：

add3 = lambda x, y, z: x + y + z

柯里化后会形如：

add3_ = lambda x: lambda y: lambda z: x + y + z

这里Python中 add3(1, 2, 3) 就与 add3_(1)(2)(3) 一致。

下面来谈谈 Lean 中的柯里化。观察下面这个多元输入函数：

def mycurrying (n : Nat) (k : String) :
    Int := n + (String.length k)

使用 #check 语句，用小括号来包裹住函数名称使其显示函数类型，得到如下结果：

#check (mycurrying)             -- mycurrying : Nat → String → Int
#check (mycurrying 3)           -- mycurrying 3 : String → Int
#check (mycurrying 3 "Hello")   -- mycurrying 3 "Hello" : Int
  • 第一行 mycurrying 是一个接受自然数和字符串，返回整数的函数。类型表示为 Nat → String → Int，表示函数依次接受一个自然数和字符串，最后返回一个整数。
  • 第二行 mycurrying 3 表达式整体被视为一个接受字符串，返回整数的函数。类型表示为 String → Int，表示函数依次接受一个字符串，最后返回一个整数。
  • 第三行 mycurrying 3 "Hello" 表示在提供了所有参数 3 和 "Hello" 之后，mycurrying 函数的类型。此时，它直接返回一个整数 Int。

Lean4 中，函数的柯里化是默认的，也就是说，函数的参数是从左到右的，而函数的返回值是从右到左即右结合的（即 Nat → String → Int 所表达的就是 Nat → (String → Int) ，即 Nat 返回一个 String → Int 的函数）。

如果我们把类型看做命题，那么只有接受了正确类型的值（类型由值推导），才能获得下一步的函数，也就是说我们可以把其中连接类型的箭头 → 看做蕴含或者推导符号。

2.1.3 数据类型

  • Lean 基本类型：Nat, Int, String, Char, Bool, Float, …
  • Lean 标准库内置类型：List（链表），Option（可选类型），Prod（积类型），Sum（和类型），Unit（单位类型），Empty（空类型）…
  • 自定义数据类型：Structure（结构体），Inductive（归纳类型）…

在这一篇中我们主要只介绍 structure 和 inductive 两种类型。更多内容，包括多态（Polymorphism），将在后续文章中进行介绍。

结构体（Structure）

下面以平面坐标的一个点为例。一个平面坐标中的点由 x和 y两个坐标唯一确定，因此可以通过下面的Lean代码构建这样的一个表示平面坐标中点的结构体：

structure Point where
  x : Float
  y : Float

structure 关键字定义了一个新的数据类型，其中 x 和 y 是结构体的字段，它们是结构体中包含的数据。如果你希望在 #eval 的时候能够显示求值结果，那么请在上述代码后面加上 deriving Repr（类似于Python 的 __repr__ 函数）。即：

structure Point where
  x : Float
  y : Float
deriving Repr

deriving Repr 是一个 Lean4 的关键字，它表示在结构体中定义的每个字段都会被自动生成一个 Repr 实例，即 Repr 实例会自动生成一个 toString 方法，该方法会将结构体中的每个字段转换为字符串，并使用逗号分隔。

A. 创建结构体类型值
  • 直接创建：def P1 : Point := { x := 1.0, y := 2.0 }
  • 构造子（Constructor）：收集要存储在新分配的数据结构中的数据，如上面 Point 结构体的构造子是 Point.mk 这个默认名称。上面直接创建的方式，就等价于 def P1 : Point := Point.mk 1.0 2.0。而若要覆盖默认名称 mk，则需要写成如下形式：
structure Point where
    newpoint ::
    x : Float
    y : Float
B. 访问结构体字段
  • 点号表记法：访问 x 和 y 字段：P1.x 和 P1.y
  • 例子，点的欧氏距离函数：
def distance (p1 p2 : Point) : Float :=
    Float.sqrt ((p2.x - p1.x) ^ 2.0 + (p2.y - p1.y) ^ 2.0)
C. 结构体更新

更新在 Lean 中其实与其在其他语言中含义并不太一样，在其他语言中这意味着对应的内存位置被新的值覆盖，但是Lean 是没有可变状态的，即说明 Lean 中的更新相当于分配了一个新的 Point （在此例中）。

使用 with 关键字来替换结构体中的一些字段，例子如下：

def updateX (p : Point) (x' : Float) : Point :=
  { p with x := x'}
-- 等价于
def updateX' (p : Point) (x' : Float) : Point :=
  { x := x', y := p.y }

再次注意，Lean 中结构体的更新并没有修改原有结构体实例的值。

和类型、递归类型（Recursive Type）、归纳类型（Inductive Type）

  • Σ\Sigma 类型/和类型：可以理解为可以选择的类型
  • 递归类型：可以包含自身实例的类型。
  • 归纳类型：递归类型 + 和类型

下面就是一个归纳类型的例子，它表示一个图形，可以是一个点，也可以是直线，也可以是圆。

inductive Shape where
  | point : Point → Shape
  | line : Point → Point → Shape
  | circle : Point → Float → Shape
deriving Repr -- 加上使得我们能够 #eval 它

下面是一个使用的例子：

#check Shape -- Shape : Type
#eval Shape.circle origin 3.0
-- 也相当于
#eval Shape.circle (Point.mk 0.0 0.0) 3.0

Lean 中使用**模式匹配（Pattern Matching）**来处理一些诸如类型判断，然后分别处理等任务。如下例子所示：

def area (s : Shape) : Float :=
  match s with
  | Shape.point _ => 0.0
  | Shape.line _ _ => 0.0
  | Shape.circle _ r => Pi * r * r
  where Pi := 3.141592653589793

match 关键字根据模式来匹配一个值，然后执行相应的代码块。这里代码的意义就是，match 判断 s 属于 Shape 中的哪一类：

  • Shape.point，则返回 0.0
  • Shape.line，则返回 0.0
  • Shape.circle，则返回 Pi * r * r，其中 Pi 是一个局部变量，r 是 Shape.circle 中的一个字段。

而这里的 _ 相当于一个参数的占位符，往往用于表示忽略该字段。where 关键字定义了一个局部变量，它只在当前函数内部可见。

值得一提的是，Lean 提供了不少简洁的写法，比如上面的 area 函数和下面这个 area' 函数是等价的：

def area' : Shape → Float
  | Shape.point _ => 0.0
  | Shape.line _ _ => 0.0
  | Shape.circle _ r => Pi * r * r
  where Pi := 3.141592653589793

你可以对多变元函数的某个变元进行匹配：

def PointOnCircle (c : Shape) (p : Point) : Prop :=
  match c with
  | Shape.circle o r =>
    (p.x - o.x) ^ 2 + (p.y - o.y) ^ 2 = r ^ 2
  | _ => false

也可以对多变元函数的多个变元进行匹配：

def PointOnLine (l : Shape) (p : Point) : Prop :=
  match l with
  | Shape.line p1 p2 =>
    (p.x - p1.x) * (p2.y - p1.y) - (p.y - p1.y) * (p2.x - p1.x) = 0
  | _ => false

这里的两个函数 PointOnCircle 和 PointOnLine 与我们刚刚定义的函数有点不同，它们是无法 #eval 的，这是因为它们返回的是一个 Proposition，即一个命题类型（Prop），而命题无法求值。

匿名函数

Lean中也允许函数不在顶层被定义，它允许定义一种被称为匿名函数（anonymous function）的东西，使用的是关键字 fun 或者 λ。

如下面这个例子：

#check fun x : Nat => x + 1  -- fun x => x + 1 : Nat → Nat
#check λ x : Nat => x + 1    -- fun x => x + 1 : Nat → Nat

事实上匿名函数的使用方式和一般的 def 所定义的函数完全一致，就是没有函数名的函数。

下面是一个更加复杂一点的例子：

#check λ hpc : PointOnCircle (Shape.circle origin 5.0) (Point.mk 3.0 4.0) => sorry

这里函数变量 hpc 的类型就是 PointOnCircle (Shape.circle origin 5.0) (Point.mk 3.0 4.0)的实例化，虽然后面使用了 sorry 来作为占位符，但实际上 =>后面我们就可以使用 hpc 这个变量，来表示 hpc 这个命题了。

证明一个定理

在上一部分中其实还有许许多多可以聊的内容，但是我想在这里可以聊一聊如何利用Lean 来证明一个定理。

回忆一下，我们说，Lean 中的类型与数理逻辑中的命题相对应，Lean 通过对类型的推断来证明定理。

在本篇内容的前半部分，我们定义了下面几个东西：

#check Point            -- Point : Type
#check Shape            -- Shape : Type
#check PointOnCircle    -- PointOnCircle (c : Shape) (p : Point): Prop
#check (PointOnCircle)  -- PointOnCircle : Shape → Point → Prop
#check PointOnLine      -- PointOnLine (l : Shape) (p : Point): Prop
#check (PointOnLine)    -- PointOnLine : Shape → Point → Prop

下面我们证明一个定理：

若一个点在一个圆上，且这个点也在一条直线上，则该点同时在直线和圆上。

注：其实这里就是一个重言式的例子，不过为了方便，我们给了它这样的一个情境。

定理的描述

将上述命题在 Lean 中表达出来即：

theorem PointOnCircleOnLine
    (c : Shape) (l : Shape) (p : Point) :
    PointOnCircle c p → PointOnLine l p →
    PointOnCircle c p ∧ PointOnLine l p := sorry

theorem 关键字定义了一个定理，它和 def 的区别在于，theorem 直接是一个不可求值的命题，而 def 是一个可求值的函数。

另外，sorry 是一个占位符，表示我们暂时还没有证明这个命题。

假设 theorem 的名字是 PointOnCircleOnLine，那么 PointOnCircleOnLine 的内容就被视为一个命题，而 PointOnCircleOnLine c l p 就是一个命题的实例。如下所示：

#check PointOnCircleOnLine

Lean Infoview中反馈到我们：

PointOnCircleOnLine (c l : Shape) (p : Point) :
  PointOnCircle c p → PointOnLine l p → PointOnCircle c p ∧ PointOnLine l p

传入一个参数 Shape.circle (Point.mk 0.0 0.0) 3.0：

#check PointOnCircleOnLine (Shape.circle (Point.mk 0.0 0.0) 3.0)

注：柯里化。

Lean Infoview中反馈到我们：

PointOnCircleOnLine
  (Shape.circle { x := 0.0, y := 0.0 }
    3.0) : ∀ (l : Shape) (p : Point),
  PointOnCircle (Shape.circle { x := 0.0, y := 0.0 } 3.0) p →
    PointOnLine l p → PointOnCircle (Shape.circle { x := 0.0, y := 0.0 } 3.0) p ∧ PointOnLine l p

定理的证明

数学上大致证明过程如下：

theorem PointOnCircleOnLine
    (c : Shape) (l : Shape) (p : Point) :
    PointOnCircle c p → PointOnLine l p →
    PointOnCircle c p ∧ PointOnLine l p :=
    -- 假设 p 在 c 上，并且 p 在 l 上
    -- 证明 p 在 c 和 l 上
    -- 证明完成
    sorry

在 Lean4 中它所对应的代码就如下所示：

theorem PointOnCircleOnLine
    (c : Shape) (l : Shape) (p : Point) :
    PointOnCircle c p → PointOnLine l p →
    PointOnCircle c p ∧ PointOnLine l p :=
  -- 假设 p 在 c 上，并且 p 在 l 上
  λ hpc : PointOnCircle c p =>
  λ hpl : PointOnLine l p =>
  have hp : PointOnCircle c p := hpc
  have hl : PointOnLine l p := hpl
  -- 证明 p 在 c 和 l 上
  show PointOnCircle c p ∧ PointOnLine l p -- 证明目标
    from And.intro hp hl -- 证明过程
  -- 证明完成
  • λ 关键字：表示一个 lambda 表达式/匿名函数，是Lean中未在顶层定义的函数，可以理解为就是一个表达式。Lean中 的 λ 关键字 和 fun 是一致的，虽然你常常看到的是 fun。
  • hpc 和 hpl：表示 hpc 是 PointOnCircle c p 的一个实例，表示对应的命题 PointOnCircle c p，而 hpl 是 PointOnLine l p 的一个实例，亦表示了对应的命题 PointOnLine l p。
  • have 关键字：用来引入一个新的局部假设或结论的关键字。在证明中，可以使用 have 来声明一个中间步骤，然后这个步骤就可以在后面被引用。比如这里的 have hp : PointOnCircle c p := hpc，hp 就是一个局部假设，它表示 hpc 的值。
  • show 关键字：用来明确指出证明的目标类型的关键字。这里 show PointOnCircle c p ∧ PointOnLine l p 就指出证明的目标是展示点同时在圆上和线上。
  • from 关键字：用来指定证明过程的关键字。这里 from And.intro hp hl 就使用 And.intro 证明了点同时在圆上和线上。
  • And.intro：用来构造一个 PointOnCircle c p ∧ PointOnLine l p 的值，同时也就证明了我们需要的命题。

让我们回顾一些理解关键点：

  • Lean 中 Prop 类型和数理逻辑中的命题相对应。值和类型可以看做是等价的（依值类型）。
  • 函数的参数（的类型）可以看做初始条件；函数的返回值（的类型）可以看做目标条件。比如上述例子中的 PointOnCircle c p → PointOnLine l p →，PointOnCircle c p 和 PointOnLine l p 都是初始条件，而 PointOnCircle c p ∧ PointOnLine l p 是目标条件。
  • 我们根据给到的传入参数值构造新的中间变量，这些中间变量的类型就是我们产生的中间命题。
  • have 关键字可以引入新的局部假设或结论，而 show 关键字可以明确指出证明的目标类型，from 关键字则可以指定证明过程。

更进一步

如果进一步定义两个图形的交点：

def Intersects (c1 c2 : Shape) (p : Point) : Prop :=
  match c1, c2 with
  | Shape.circle _ _, Shape.circle _ _ =>
    PointOnCircle c1 p ∧ PointOnCircle c2 p
  | Shape.circle _ _, Shape.line _ _ =>
    PointOnCircle c1 p ∧ PointOnLine c2 p
  | Shape.line _ _, Shape.circle _ _ =>
    PointOnCircle c2 p ∧ PointOnLine c1 p
  | Shape.line _ _, Shape.line _ _ =>
    PointOnLine c1 p ∧ PointOnLine c2 p
  | _, _ => false

前面证明的定理的描述可以转换为：

若一个点在一个圆上，且这个点也在一条直线上，则该点为直线和圆的交点。

类似地可以给出如下定理及其证明：

theorem PointOnCircleOnLine'
    (c : Shape) (l : Shape) (p : Point) :
    PointOnCircle c p → PointOnLine l p → -- 条件：假设 p 在 c 上，并且 p 在 l 上
    Intersects c l p :=                   -- 目标：证明 p 是 c 和 l 的交点
  λ hpc : PointOnCircle c p =>            -- 实例化条件 hpc：p 在 c 上
  λ hpl : PointOnLine l p =>              -- 实例化条件 hpl：p 在 l 上
  have hp : PointOnCircle c p := hpc      -- 引入新的局部假设 hp，由 hpc 诱导出
  have hl : PointOnLine l p := hpl        -- 引入新的局部假设 hl，由 hpl 诱导出
  match c, l with  -- 匹配 c 和 l 的类型，确保其在后续使用 Intersects 的时候具体类型是匹配的
  | Shape.circle o1 r1, Shape.line p1 p2 => -- 匹配到 c 和 l 的具体类型
  show Intersects (Shape.circle o1 r1) (Shape.line p1 p2) p from  -- 证明目标
    And.intro hp hl                     
    -- 证明过程，构造一个 PointOnCircle c p ∧ PointOnLine l p 的值，其与 Intersects c l p 类型一致，也就证明了这个命题

这里我们并不能直接使用 show Intersects c l p，因为 Lean4 的 show 关键字只能显式地指明目标类型，而 Intersects c l p 的类型是隐式地推导出来的，所以需要显示地指明。即 Lean4 会认为这里的 c, l 的类型是 Shape，而非期待的 Shape.circle 和 Shape.line。

 2024-12-07   Lean4   Coding  

上一篇  下一篇