引入一个与证明无关的 Prop 并标记定理不可约表示了分离关注点的第一步。目的是类型为 p : Prop 的元素在计算中不应发挥任何作用，因此从这个意义上说，项 t : p 的特定构造是「无关的」。人们仍然可以定义包含类型为 Prop
的元素的计算对象；关键是这些元素可以帮助我们推理计算的影响，但在我们从项中提取「代码」时可以忽略。但是，Prop 类型的元素并非完全无害。它们包括任何类型 α 的方程 s = t : α，并且此类方程可以作为强制转换使用，以对项进行类型检查。在后面，我们将看到此类强制转换是如何阻碍系统中的计算的示例。但是，在擦除命题内容、忽略中间定型约束并归约项，直到它们达到正规形式的求值方案下，它们仍然可以进行计算。这正是 Lean 的虚拟机所做的。
在通过了证明无关的 Prop 之后，可以认为使用排中律 p ∨ ¬p 是合法的，其中 p 是任何命题。当然，这也可能根据 CIC 的规则阻止计算，但它不会阻止字节码求值，如上所述。仅在 :numref:choice
中讨论过的选择原则才能完全消除理论中与证明无关的部分和与数据相关部分之间的区别。
namespace Hidden
axiompropext {a b : Prop} : (a ↔ b) → a = b
end Hidden
它断言当两个命题互相蕴含时，二者实质相等。这与集合论的解释一致，即对于某个特定的元素 *，其中任何元素 a : Prop 要么为空集，要么是单元素集 {*}。此公理具有这样的效果，即等价的命题可以在任何语境中彼此替换：
theoremthm₁(a b c d e : Prop)(h : a ↔ b): (c ∧ a ∧ d → e) ↔ (c ∧ b ∧ d → e) :=
propext h ▸ Iff.refl _
theoremthm₂(a b : Prop)(p : Prop → Prop)(h : a ↔ b)(h₁ : p a): p b :=
propext h ▸ h₁
Similar to propositional extensionality, function extensionality
asserts that any two functions of type (x : α) → β x that agree on
all their inputs are equal.
universe u v
#check (@funext :
{α : Type u}
→ {β : α → Type u}
→ {f g : (x : α) → β x}
→ (∀ (x : α), f x = g x)
→ f = g)
#printfunext
defSet(α : Type u):= α → Propnamespace Set
defmem(x : α)(a : Set α):= a x
infix:50 (priority := high) "∈" => mem
theoremsetext{a b : Set α}(h : ∀ x, x ∈ a ↔ x ∈ b): a = b :=
funext (fun x => propext (h x))
end Set
我们可以继续定义例如空集和交集，并证明的集合恒等性：
defSet(α : Type u):= α → Propnamespace Set
defmem(x : α)(a : Set α):= a x
infix:50 (priority := high) "∈" => mem
theoremsetext{a b : Set α}(h : ∀ x, x ∈ a ↔ x ∈ b): a = b :=
funext (fun x => propext (h x))
defempty: Set α := fun x => False
notation (priority := high) "∅" => empty
definter(a b : Set α): Set α :=
fun x => x ∈ a ∧ x ∈ b
infix:70" ∩ " => inter
theoreminter_self(a : Set α): a ∩ a = a :=
setext fun x => Iff.intro
(fun ⟨h, _⟩ => h)
(fun h => ⟨h, h⟩)
theoreminter_empty(a : Set α): a ∩ ∅ = ∅ :=
setext fun x => Iff.intro
(fun ⟨_, h⟩ => h)
(fun h => False.elim h)
theoremempty_inter(a : Set α): ∅ ∩ a = ∅ :=
setext fun x => Iff.intro
(fun ⟨h, _⟩ => h)
(fun h => False.elim h)
theoreminter.comm(a b : Set α): a ∩ b = b ∩ a :=
setext fun x => Iff.intro
(fun ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩)
(fun ⟨h₁, h₂⟩ => ⟨h₂, h₁⟩)
end Set
以下是一个函数外延性阻碍了 Lean 核心中计算的示例：
deff(x : Nat):= x
defg(x : Nat):= 0 + x
theoremf_eq_g: f = g :=
funextfun x => (Nat.zero_add x).symm
defval: Nat :=
Eq.recOn (motive := fun _ _ => Nat) f_eq_g 0-- 无法归约为 0#reduce val
-- 求值为 0#eval val
首先，我们使用函数外延性来证明两个函数 f 和 g 相等，然后用 g 替换类型为 Nat 的 f，从而转换该类型。当然，转换是无意义的，因为 Nat 不依赖于 f。但这已经足够了：在系统的计算规则之下，我们现在有了 Nat 的一个封闭项，它不会归约为一个数值。在这种情况下，我们可能倾向于将该表达式归约为 0。但是，在非平凡的例子里，消除转换会改变该项的类型，这可能会导致周围的表达式类型不正确。然而，虚拟机将表达式求值为 0 则不会遇到问题。下面是一个类似的例子，展示了 propext 如何造成阻碍。
theoremtteq: (True ∧ True) = True :=
propext (Iff.intro (fun ⟨h, _⟩ => h) (fun h => ⟨h, h⟩))
defval: Nat :=
Eq.recOn (motive := fun _ _ => Nat) tteq 0-- does not reduce to 0#reduce val
-- evaluates to 0#eval val
当前的研究计划包括关于观测类型论（Observational Type Theory）和立方类型论（Cubical Type Theory）的研究，旨在扩展类型理论，以便允许对涉及函数外延、商，等等的强制转换进行归约。但解决方案并不明朗，而 Lean 的底层演算法则对此类归约也不支持。
设 α 为任意类型，且 r 为 α 上的等价关系。在数学中，常见的做法是形成「商（Quotient）」α / r，即 α 中元素的类型「模（modulo）」r。从集合论的角度，可以将 α / r 视为 α 模 r 的等价类的集合。若 f : α → β 是任意满足等价关系的函数，即对于任意 x y : α, r x y
蕴含 f x = f y, 则 f「提升（lift）」到函数 f' : α / r → β，其在每个等价类 ⟦x⟧ 上由 f' ⟦x⟧ = f x 定义。Lean 的标准库通过执行这些构造的附加常量来扩展构造演算，并将该最后的方程作为定义归约规则。
在最基本的表述形式中，商构造甚至不需要 r 成为一个等价关系。下列常量被内置在 Lean 中：
namespace Hidden
universe u v
axiom Quot : {α : Sort u} → (α → α → Prop) → Sort u
axiom Quot.mk : {α : Sort u} → (r : α → α → Prop) → α → Quot r
axiom Quot.ind :
∀ {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop},
(∀ a, β (Quot.mk r a)) → (q : Quot r) → β q
axiom Quot.lift :
{α : Sort u} → {r : α → α → Prop} → {β : Sort u} → (f : α → β)
→ (∀ a b, r a b → f a = f b) → Quot r → β
end Hidden
第一条公理根据任何二元关系 r 的类型 α 形成类型 Quot r。第二条公理将 α 映射到 Quot α，因此若 r : α → α → Prop 且 a : α，则 Quot.mk r a 是 Quot r 的一个元素。第三条公理 Quot.ind 是说 Quot.mk r a 的每个元素都属于此形式。至于 Quot.lift，给定函数 f : α → β，若 h 是一个「f
遵循关系 r」的证明，则 Quot.lift f h 是 Quot r 上的对应函数。其思想是对于 α 中的每个元素 a，函数 Quot.lift f h
将 Quot.mk r a（包含 a 的 r-类）映射到 f a，其中 h 表明此函数是良定义的。事实上，计算公理被声明为一个归约规则，如下方的证明所示。
defmod7Rel(x y : Nat):Prop :=
x % 7 = y % 7-- the quotient type#check (Quot mod7Rel : Type)
-- the class of a#check (Quot.mk mod7Rel 4 : Quot mod7Rel)
deff(x : Nat): Bool :=
x % 7 = 0theoremf_respects(a b : Nat)(h : mod7Rel a b): f a = f b := bysimp [mod7Rel, f] at *
rw [h]
#check (Quot.lift f f_respects : Quot mod7Rel → Bool)
-- the computation principleexample (a : Nat) : Quot.lift f f_respects (Quot.mk mod7Rel a) = f a :=
rfl
当然，当 r 是等价关系时，商集的结构是最常用的。给定上面的 r，如果我们根据法则 r' a b 当且仅当 Quot.mk r a = Quot.mk r b 定义 r'，那么显然 r' 就是一个等价关系。事实上，r' 是函数 a ↦ quot.mk r a
的核（Kernel）。公理 Quot.sound 表明 r a b 蕴含 r' a b。使用 Quot.lift 和 Quot.ind，我们可以证明 r' 是包含 r 的最小的等价关系，意思就是，如果 r'' 是包含 r 的任意等价关系，则 r' a b 蕴含 r'' a b。特别地，如果 r 开始就是一个等价关系，那么对任意 a 和 b，我们都有
r a b 等价于 r' a b。
namespace Hidden
classSetoid(α : Sort u)where
r : α → α → Prop
iseqv : Equivalence r
instance{α : Sort u}[Setoid α]: HasEquiv α :=
⟨Setoid.r⟩
namespace Setoid
variable {α : Sort u} [Setoid α]
theoremrefl(a : α): a ≈ a :=
iseqv.refl a
theoremsymm{a b : α}(hab : a ≈ b): b ≈ a :=
iseqv.symm hab
theoremtrans{a b c : α}(hab : a ≈ b)(hbc : b ≈ c): a ≈ c :=
iseqv.trans hab hbc
end Setoid
end Hidden
给定一个类型 α 和其上的关系 r，以及一个证明 p 证明 r 是一个等价关系，我们可以定义 Setoid.mk r p 为广集类的一个实例。
为了完成此示例，给定 a : α 和 u : uprod α，我们定义命题 a ∈ u，若 a 是无序对 u 的元素之一，则该命题应成立。首先，我们在（有序）对上定义一个类似的命题 mem_fn a u；然后用引理 mem_respects 证明 mem_fn 关于等价关系 eqv 成立。这是一个在 Lean 标准库中广泛使用的惯用法。
privatedefeqv(p₁ p₂ : α × α):Prop :=
(p₁.1 = p₂.1 ∧ p₁.2 = p₂.2) ∨ (p₁.1 = p₂.2 ∧ p₁.2 = p₂.1)
infix:50" ~ " => eqv
privatetheoremeqv.refl(p : α × α): p ~ p :=
Or.inl ⟨rfl, rfl⟩
privatetheoremeqv.symm: ∀ {p₁ p₂ : α × α}, p₁ ~ p₂ → p₂ ~ p₁
| (a₁, a₂), (b₁, b₂), (Or.inl ⟨a₁b₁, a₂b₂⟩) =>
Or.inl (by simp_all)
| (a₁, a₂), (b₁, b₂), (Or.inr ⟨a₁b₂, a₂b₁⟩) =>
Or.inr (by simp_all)
privatetheoremeqv.trans: ∀ {p₁ p₂ p₃ : α × α}, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inl (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inl ⟨a₁b₁, a₂b₂⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inr (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inl ⟨b₁c₁, b₂c₂⟩ =>
Or.inr (by simp_all)
| (a₁, a₂), (b₁, b₂), (c₁, c₂), Or.inr ⟨a₁b₂, a₂b₁⟩, Or.inr ⟨b₁c₂, b₂c₁⟩ =>
Or.inl (by simp_all)
privatetheoremis_equivalence: Equivalence (@eqv α) :=
{ refl := eqv.refl, symm := eqv.symm, trans := eqv.trans }
instanceuprodSetoid(α : Type u): Setoid (α × α) where r := eqv
iseqv := is_equivalence
defUProd(α : Type u):Type u :=
Quotient (uprodSetoid α)
namespace UProd
defmk{α : Type}(a₁ a₂ : α): UProd α :=
Quotient.mk' (a₁, a₂)
notation"{ " a₁ ", " a₂ " }" => mk a₁ a₂
theoremmk_eq_mk(a₁ a₂ : α): {a₁, a₂} = {a₂, a₁} :=
Quot.sound (Or.inr ⟨rfl, rfl⟩)
privatedefmem_fn(a : α): α × α → Prop
| (a₁, a₂) => a = a₁ ∨ a = a₂
-- auxiliary lemma for proving mem_respects-- 用于证明 mem_respects 的辅助引理privatetheoremmem_swap{a : α}:
∀ {p : α × α}, mem_fn a p = mem_fn a (⟨p.2, p.1⟩)
| (a₁, a₂) => byapplypropextapply Iff.intro
. intro
| Or.inl h => exact Or.inr h
| Or.inr h => exact Or.inl h
. intro
| Or.inl h => exact Or.inr h
| Or.inr h => exact Or.inl h
privatetheoremmem_respects: {p₁ p₂ : α × α} → (a : α) → p₁ ~ p₂ → mem_fn a p₁ = mem_fn a p₂
| (a₁, a₂), (b₁, b₂), a, Or.inl ⟨a₁b₁, a₂b₂⟩ => by simp_all
| (a₁, a₂), (b₁, b₂), a, Or.inr ⟨a₁b₂, a₂b₁⟩ => by simp_all; apply mem_swap
defmem(a : α)(u : UProd α):Prop :=
Quot.liftOn u (fun p => mem_fn a p) (fun p₁ p₂ e => mem_respects a e)
infix:50 (priority := high) " ∈ " => mem
theoremmem_mk_left(a b : α): a ∈ {a, b} :=
Or.inl rfltheoremmem_mk_right(a b : α): b ∈ {a, b} :=
Or.inr rfltheoremmem_or_mem_of_mem_mk{a b c : α}: c ∈ {a, b} → c = a ∨ c = b :=
fun h => h
end UProd
namespace Hidden
open Classical
theoremem(p : Prop): p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p
let V (x : Prop) : Prop := x = False ∨ p
have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
sorryend Hidden
当 p 为真时，Prop 的所有元素既在 U 中又在 V 中。当 p 为假时，U 是单元素的 true，V 是单元素的 false。
接下来，我们使用 some 从 U 和 V 中各选取一个元素：
namespace Hidden
open Classical
theoremem(p : Prop): p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p
let V (x : Prop) : Prop := x = False ∨ p
have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
let u : Prop := choose exU
let v : Prop := choose exV
have u_def : U u := choose_spec exU
have v_def : V v := choose_spec exV
sorryend Hidden
U 和 V 都是析取，所以 u_def 和 v_def 表示四种情况。在其中一种情况下，u = True 且 v = False，在所有其他情况下，p 为真。因此我们有：
namespace Hidden
open Classical
theoremem(p : Prop): p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p
let V (x : Prop) : Prop := x = False ∨ p
have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
let u : Prop := choose exU
let v : Prop := choose exV
have u_def : U u := choose_spec exU
have v_def : V v := choose_spec exV
have not_uv_or_p : u ≠ v ∨ p :=
match u_def, v_def with
| Or.inr h, _ => Or.inr h
| _, Or.inr h => Or.inr h
| Or.inl hut, Or.inl hvf =>
have hne : u ≠ v := bysimp [hvf, hut, true_ne_false]
Or.inl hne
sorryend Hidden
另一方面，若 p 为真，则由函数的外延性和命题的外延性，可得 U 和 V 相等。根据 u 和 v 的定义，这蕴含了它们也相等。
namespace Hidden
open Classical
theoremem(p : Prop): p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p
let V (x : Prop) : Prop := x = False ∨ p
have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
let u : Prop := choose exU
let v : Prop := choose exV
have u_def : U u := choose_spec exU
have v_def : V v := choose_spec exV
have not_uv_or_p : u ≠ v ∨ p :=
match u_def, v_def with | Or.inr h, _ => Or.inr h
| _, Or.inr h => Or.inr h
| Or.inl hut, Or.inl hvf =>
have hne : u ≠ v := bysimp [hvf, hut, true_ne_false]
Or.inl hne
have p_implies_uv : p → u = v :=
fun hp =>
have hpred : U = V :=
funextfun x =>
have hl : (x = True ∨ p) → (x = False ∨ p) :=
fun _ => Or.inr hp
have hr : (x = False ∨ p) → (x = True ∨ p) :=
fun _ => Or.inr hp
show (x = True ∨ p) = (x = False ∨ p) frompropext (Iff.intro hl hr)
have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := byrw [hpred]; intros; rflshow u = v from h₀ _ _
sorryend Hidden
将最后两个事实放在一起可以得出期望的结论：
namespace Hidden
open Classical
theoremem(p : Prop): p ∨ ¬p :=
let U (x : Prop) : Prop := x = True ∨ p
let V (x : Prop) : Prop := x = False ∨ p
have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩
let u : Prop := choose exU
let v : Prop := choose exV
have u_def : U u := choose_spec exU
have v_def : V v := choose_spec exV
have not_uv_or_p : u ≠ v ∨ p :=
match u_def, v_def with | Or.inr h, _ => Or.inr h
| _, Or.inr h => Or.inr h
| Or.inl hut, Or.inl hvf =>
have hne : u ≠ v := bysimp [hvf, hut, true_ne_false]
Or.inl hne
have p_implies_uv : p → u = v :=
fun hp =>
have hpred : U = V :=
funextfun x =>
have hl : (x = True ∨ p) → (x = False ∨ p) :=
fun _ => Or.inr hp
have hr : (x = False ∨ p) → (x = True ∨ p) :=
fun _ => Or.inr hp
show (x = True ∨ p) = (x = False ∨ p) frompropext (Iff.intro hl hr)
have h₀ : ∀ exU exV, @choose _ U exU = @choose _ V exV := byrw [hpred]; intros; rflshow u = v from h₀ _ _
match not_uv_or_p with
| Or.inl hne => Or.inr (mt p_implies_uv hne)
| Or.inr h => Or.inl h
end Hidden
namespace Hidden
open Classical
theorempropComplete(a : Prop): a = True ∨ a = False :=
match em a with
| Or.inl ha => Or.inl (propext (Iff.intro (fun _ => ⟨⟩) (fun _ => ha)))
| Or.inr hn => Or.inr (propext (Iff.intro (fun h => hn h) (fun h => False.elim h)))
end Hidden
namespace Hidden
classinductiveDecidable(p : Prop)where
| isFalse (h : ¬p) : Decidable p
| isTrue (h : p) : Decidable p
end Hidden
与 p ∨ ¬ p 不同，它只能消去到 Prop，类型 Decidable p 等效于和类型
Sum p (¬ p)，它可以消除至任何类型。这就是编写「if-then-else（若-则-否则）」表达式所需的数据。
作为经典推理的一个示例，我们使用 choose 来证明，若 f : α → β 是单射的，且 α 是可居的，则 f 是左逆的。为了定义左逆 linv，我们使用一个依值的
if-then-else 表达式。回忆一下，if h : c then t else e 是dite c (fun h : c => t) (fun h : ¬ c => e) 的记法。在 linv 的定义中，选择公理使用了两次：首先，为了证明 (∃ a : A, f a = b) 是「可判定的」，需要选择一个 a，使得 f a = b。请注意，propDecidable 是一个作用域实例，它通过 open Classical 命令激活。我们使用此实例来证明 if-then-else 表达式。（还可以参阅 可判命题一节中的讨论）。
open Classical
noncomputabledeflinv[Inhabited α](f : α → β): β → α :=
fun b : β => if ex : (∃ a : α, f a = b) then choose ex else default
theoremlinv_comp_self{f : α → β}[Inhabited α](inj : ∀ {a b}, fa = fb → a = b)
: linv f ∘ f = id :=
funextfun a =>
have ex : ∃ a₁ : α, f a₁ = f a := ⟨a, rfl⟩
have feq : f (choose ex) = f a := choose_spec ex
calc linv f (f a)
_ = choose ex := dif_pos ex
_ = a := inj feq