LEAN

类

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

类型论

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

#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语言]] 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 这种形式“占位”。

#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（显式化所有隐式参数）

#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.细化

λ-calculus

(λ 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.

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（偶数类型），但它的 可居性 被解释为命题的真假。

class Even a where
  isEven :: a -> Bool

instance Even Integer where
  isEven n = n `mod` 2 == 0

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

证明策略(tactic)

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.

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

构造

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

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

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

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

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

元编程

宏

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