LEAN

类

structure:类
inductive:递归定义类
class:类型类:方法

构造主义

Lean（以及 Coq 等）本身只是“形式化数学的工具/平台”，它的底层逻辑“天然支持”构造性逻辑，但——

  • Lean 内部确实默认使用构造主义（你写出来的函数、证明都要求是具体的/可以检查的对象）。
  • Lean 也可以引入经典公理（如排中律），此时系统本身逻辑就“升格”为经典逻辑环境，且用户可以自由选择是否采用构造/经典逻辑。
    • mathlib（Lean 的数学库）专注于数学实际工作，往往默认会局部引入排中律等经典公理，以便和大多数数学文献一致。
    • 你可以在 Lean 里使用 open classical 或加公理 axiom em : ∀ P : Prop, P ∨ ¬P

因此，Lean 是构造性基础的，但对经典逻辑“兼容并蓄”，可以按需切换。

类型论

degree & universe

sort type term
Prop (Sort 0) True True.intro
Type (Sort 1) Bool true
Type 1 (Sort 2) Nat → Type fun n => Fin n
Type 2 (Sort 3) Type → Type 1 fun (_ : Type) => Type
… … …
→度（degree）上升
↓宇宙（universe）的变化

polymorphic

1
2
3
4
5
6
#check List
-- List.{u} (α : Type u) : Type u
universe u
def F (α : Type u) : Type u := Prod α α
#check F
--

实际上这里的u不是目标语言的项，应该把 Type u 看成一个整体

dependent

types can depend on parameters
如果类型签名写Type → α → List α → List α α的指代不清晰
建议写cons (α : Type) (a : α) (as : List α) : List α
/fu_language cons α : Type : α → List α → List α
在 Haskell 中，cons 的类型是隐式多态的：cons :: α -> [α] -> [α]: 类型变量 α 由类型推断自动填充，无需显式传递 Type 参数。

dependent function type, or dependent arrow type, Pi-type:
α : Type and β : α → Type i.e. β: (a : α) → β a also writen as $\prod _{a :\alpha} ~\beta ~a$

dependent Cartesian product types (a : α) × β a also writen as $\sum _{a :\alpha} ~\beta ~a$
eg.godown := Sigma (λ n : Nat => Fin n) <2,1>:godown

Implicit Arguments

def bs : Lst Nat := Lst.cons _ 5 (Lst.nil _)
def Lst.cons {α : Type u} (a : α) (as : Lst α) : Lst α := List.cons a as

Lean 为了类型推断和后续泛化方便，在你没有指定具体类型参数时，用 ?m.n 这种形式“占位”。

1
2
3
4
5
6
#check (ident)
-- @ident ?m.403 → ?m.403
#check ident
-- ident.{u} {α : Type u} (x : α) : α
#check @ident
-- @ident : {α : Type u_1} → α → α

括号减少 “signature 损耗/粉饰” i.e. (ident) 的括号阻止了 Lean 自动展开 ident 的定义，因此只显示其未实例化的类型, Lean 仅检查 部分应用 的 ident（未提供隐式参数 α），因此类型暂时无法确定
@ident（显式化所有隐式参数）

1
2
3
4
#check (List.nil)
-- [] : List ?m.2
#check (List.nil : List Nat)
-- [] : List Nat

The process of instantiating these “holes,” or “placeholders,” in a term is often known as elaboration.细化

structures, typeclasses, sigma/record types

structures, typeclasses and sigma/record types are the same thing semantically, but typeclasses have a special role in automation and interface design
下面详细对比和举例 Lean 中三种相关的语法：structure、typeclass（class）、sigma/record types。

1. structure

定义一个结构体，类似于数学中的记录类型（record）。所有字段都要初始化。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
-- 定义结构体 Point，有两个字段
structure Point :=
(x : ℕ)
(y : ℕ)

-- 使用结构体
def p : Point := { x := 1, y := 2 }         -- 记录语法
def px : ℕ := p.x                          -- 点的 x 坐标

-- 也可以用 tuple 风格
def q : Point := ⟨3, 4⟩

-- 传递字段
def sum (pt : Point) : ℕ := pt.x + pt.y

2. typeclass（class）

用 class 关键字声明一个类型类，Lean 自动把它视作结构体，加上类型类自动推断机制。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
class MyGroup (G : Type) :=
(op   : G → G → G)
(one  : G)
(inv  : G → G)
(op_assoc : ∀ a b c : G, op (op a b) c = op a (op b c))
(one_op   : ∀ a : G, op one a = a)
(op_one   : ∀ a : G, op a one = a)
(op_inv   : ∀ a : G, op a (inv a) = one)

-- 提供实例内容
instance int_mygroup : MyGroup ℤ :=
{ op := (+),
  one := 0,
  inv := λ x, -x,
  op_assoc := by simp,
  one_op := by simp,
  op_one := by simp,
  op_inv := by simp }

-- 使用时 Lean 支持自动填充 typeclass instance
def double [MyGroup G] (a : G) : G := MyGroup.op a a

-- 下面可以直接 double 3，因为 ℤ 有实例
#eval double 3      -- Lean 会自动填入 int_mygroup

说明：

  • class 语法跟 structure 基本一致，但 Lean 给它加了类型类机制。
  • 用方括号 [MyGroup G] 可让 Lean 自动找实例。

3. sigma/record types

Sigma 类型（dependent pair），Lean 语法是 Σ x : A, B x 或 Sigma A B，手写比较多用于某些依赖类型场景。
通常，structure 就是 record type，Sigma 是依赖记录。

1
2
3
4
5
6
7
8
9
10
11
12
-- 普通 record 就是 structure Point
-- 依赖型记录例子：

def S : Type := Σ n : ℕ, Fin n → ℝ
-- 解释：一个自然数 n，加上一个数组（函数）从 Fin n 到 ℝ

-- 构造一项
def example : S := ⟨3, λ i, 2.0 * ↑i⟩

-- 取出字段
def len : ℕ := example.1
def data : Fin len → ℝ := example.2

λ-calculus

1
2
(λ x : Nat => x + 5) 10
#check (λ x  => x + 1 : Nat → Nat)

x: bound variable

def
let : Lean also allows you to introduce “local” definitions using the let keyword. The expression let a := t1; t2 is definitionally equal to the result of replacing every occurrence of a in t2 by t1.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
variable (x : α)
def  f :=  x + x

section useful
  variable (α β γ : Type)
  variable (g : β → γ) (f : α → β) (h : α → α)
  variable (x : α)

  def compose := g (f x)
  def doTwice := h (h x)
  def doThrice := h (h (h x))
end useful

namespace Foo
  def a : Nat := 5
  def f (x : Nat) : Nat := x + 7
end Foo

open Foo

#check a
-- Foo.a : Nat

Curry-Howard 同构

 the type Prop is syntactic sugar for Sort 0(类型中的一种), Type u is also just syntactic sugar for Sort (u+1)
命题即类型

  • 而Prop是类型的类型
  • 依赖变量的Prop依然是Prop
    Theorem,Lemma,Colloray本身是某个Prop的项, 证明即程序
  • 一个Prop如果有项则为真

we can use the usual function space constructor p → q from dependent type theory as our notion of implication.

A是B A:B
对p : Prop i.e. Sort 0 , t1 t2 : p , 认为 t1 t2 是定义等价的 , sort 0 的性质, 即更低的层级没有意义, 即只是形式上的东西.语法|语义
From the constructive point of view, proofs are abstract mathematical objects that are denoted by suitable expressions in dependent type theory.
we will slip back and forth between these two ways of talking, at times saying that an expression “==constructs==” or “produces” or “returns” a proof of a proposition, and at other times simply saying that it “is” such a proof. This is similar to the way that computer scientists occasionally blur the distinction between syntax and semantics by saying, at times, that a program “computes” a certain function, and at other times speaking as though the program “is” the function in question.
 To prove that assertion, we need to exhibit a term t : p.

head 名称 (输入:类型): 类型 := 值
theorem name : Prop:= Proof
example=Theorem foo
the #print command will show you the proof of a theorem:

And.intro h1 h2 | p And q

  • ∀ x, P(x) 对应依赖函数类型 (x : X) → P xi.e $\prod _{a :\alpha} ~\beta ~a$ 是指数对象的推广 $\beta ^\alpha$
  • ∃ x, P(x) 对应依赖对类型 {x : X // P x} i.e. $\sum _{a :\alpha} ~\beta ~a$ 是乘积对象的推广 $\alpha \times\beta$
    量词范围默认向右延伸到表达式结束

此时，Σ (n : ℕ), n % 2 = 0 的类型仍然是 Type（偶数类型），但它的 可居性 被解释为命题的真假。

1
2
3
4
5
class Even a where
  isEven :: a -> Bool

instance Even Integer where
  isEven n = n `mod` 2 == 0
1
2
3
4
5
6
7
8
9
10
class EvenProp (α : Type) where
  Even : α → Prop       -- 将性质定义为命题
  decide : ∀ n : α, Decidable (Even n)  -- 可判定性

instance : EvenProp Nat where
  Even n := n % 2 = 0
  decide n := inferInstance  -- 自动推断 Decidable (n % 2 = 0)

-- 判断 4 是否为偶数
#eval decide (EvenProp.Even 4)  -- 输出 true

Calculational Proofs

1
2
3
4
5
6
7
8
9
import Mathlib.Data.Nat.Basic

theorem nat_ineq (a b : ℕ) : a^2 + b^2 ≥ a * b := by
  calc
    a^2 + b^2
      = (a - b)^2 + 2 * a * b := by ring
  _ ≥ 0 + 2 * a * b           := by gcongr; apply sq_nonneg
  _ ≥ 0 + a * b               := by gcongr; linarith
  _ = a * b                   := by ring

证明策略(tactic)

We will describe proofs that consist of sequences of tactics as “tactic-style” proofs, to contrast with the ways of writing proof terms we have seen so far, which we will call “term-style” proofs. Each style has its own advantages and disadvantages. For example, tactic-style proofs can be harder to read, because they require the reader to predict or guess the results of each instruction. But they can also be shorter and easier to write. Moreover, tactics offer a gateway to using Lean’s automation, since automated procedures are themselves tactics.

Natural Number Game
[[lean4game-g_leanprover-community_nng4-2025_7_11.json]]

实际上本来就有这些参数, 只是lean可以结合上下文自动推断
默认作用在goal上, 可以用at 指定对象, ⊢指当前目标
注意名称中都是是下划线

rfl

exact: Now you could finish with rw [h] then rfl, but exact h does it in one line.

  • doesn’t just take hypotheses, it will eat any proof which exists in the system.
    exact succ_eq_add_one x相当于把(n : ℕ) : MyNat.succ n = n + 1反着用

trivial: If you can turn your goal into True, then the trivial tactic will solve it.

rw

  • repeat rw: 注意对 add_comm会带来死循环, 但是可以 add_comm n
  • rw [add_zero c]: 实际上本来就有这些参数, 只是lean可以结合上下文自动推断
  • rw [\l h]
  • nth_rewrite n [h] : 注意是下划线
  • rw [zero_add] at h

apply$\Rightarrow$

  • apply h1 at h2
  • apply h: p ->q will turn the goal q into p

symm: apply h: a = b -> b=a

intro h will turn the gaol p -> q into hypothesis p and goal q

induction n with d hd

  • d指归纳步骤里出现的前一个数（即n = d + 1时的d），
  • hd就是归纳假设（hypothesis of induction）在n = d时成立的假设。
  • …generalizing c将变量 c 也提升为归纳假设的通用参数

contrapose: 逆否,contrapose! h !表示自动化简

constructor

cases:存在命题同样需要cases引入，如cases h with c hc if h : a ≤ b
 if you have a hypothesis h : False then you are done, because a false statement implies any statement.
 cases hyz with b hb will turn x ≤ y into hb: x+b =y (or tauto)

left right:changes a goal of P ∨ Q into a goal of PorQ

have: The have tactic can be used to add new hypotheses

use:prove an “exists” statement

simp only [add_assoc, add_left_comm, add_comm]

decide: decide will attempt to solve a goal if it can find an algorithm which it can run to solve it.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
instance instDecidableEq : DecidableEq ℕ
| 0, 0 => isTrue <| by
  show 0 = 0
  rfl
| succ m, 0 => isFalse <| by
  show succ m ≠ 0
  exact succ_ne_zero m
| 0, succ n => isFalse <| by
  show 0 ≠ succ n
  exact zero_ne_succ n
| succ m, succ n =>
  match instDecidableEq m n with
  | isTrue (h : m = n) => isTrue <| by
    show succ m = succ n
    rw [h]
    rfl
  | isFalse (h : m ≠ n) => isFalse <| by
    show succ m ≠ succ n
    exact succ_ne_succ m n h

tauto:The tauto tactic will solve any goal which can be solved purely by logic (that is, by truth tables).

a ≠ b is notation for a = b → False so just intro h to use reductio ad absurdum

forward | backward

构造

1
2
3
4
def pred (n : Nat) : Nat :=
  match n with
  | zero => zero  -- 约定：0 的前驱仍是 0（或有时定义为 0 无前驱）
  | succ k => k   -- n = k + 1 的前驱是 k

实际上是(-1), 但是减法还没定义, 构造保证了良定义

1
2
3
4
def is_zero (n : Nat) : Bool :=
  match n with
  | zero => true
  | succ _ => false

实际上是(==0), 但是(==)还没定义

  • 设计语言避免不必要的转换：eg存在命题，蕴含与条件

元编程

宏

1
2
macro "simp_add" : tactic => `(tactic|(
  simp only [add_assoc, add_left_comm, add_comm]))

Lean4Align

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
:maxdepth: 2

type_conversion

Sets & Functions

Elementary Algebra

Group Theory

Ring Theory

Field Theory

Matrix Theory

LEAN
http://kaelvio.com/LEAN/
作者
采薇
发布于
2025年11月4日
许可协议