Lean 中的证明如何终止
类型论只有一个核心概念：类型。命题也是一种类型。证明一个命题就是构造一个类型的对象的过程。
Lean 中命题的类型就是 Prop。如果 P 的类型是 Prop，而 Q 的类型是 P，则 Q 是 P 的一个证明。使用 #check 表达式 即可检查表达式的类型。
证明的标准写法：theorem 类型A : 类型B := 类型A 的定义，这可以想象成 theorem 证法A : 命题 B := 证法A 的内容。
要省略一个证明，可以用 sorry，就像这样：theorem 这太难了 : 费马大定理 := sorry。
Lean 如何检查证明
example (a b c : ℝ) : (a * b) * c = b * (a * c) :=
begin
rw mul_comm a b,
rw mul_assoc b a c
end
在上述证明中，要证明的目标（goal）是“对任意实数 $a,b,c$ 都有 $(a* b) * c=b* (a* c)$”。Lean 检查证明的过程，就是逐行执行位于 begin 与 end 之间的代码，而执行每一行代码都意味着把当前目标变换为新的目标。
目标（goal）由语境（context）和靶（target）构成。例如，如果你在 Lean infoview 看到：
1 goal
x y : ℕ,
h₁ : prime x,
h₂ : ¬even x,
h₃ : y > x
⊢ y ≥ 4
那么 x y : ℕ, h₁ : prime x, h₂ : ¬even x, h₃ : y > x 是语境，而 y ≥ 4 是靶；在这个语境中，x y : ℕ 指明涉及的对象，而 h₁ : prime x, h₂ : ¬even x, h₃ : y > x 列举了三个假设（assumption）。
如何输入符号
注意有很多都是 LaTeX 中的写法。
数字下标：使用 h\1 得到 h₁
实数集 ℝ：\R 或 \real
左箭头 ←：\l
右箭头 →：\r 或 \to
希腊字母：就用 LaTeX 中的写法，例如 ε 就是 \epsilon
∀：\forall
∃：\exists
¬ ：\not
∧：\and
∨：\or
↔：\iff 或 \lr
局部变量
section
variables a b c : ℝ
end
这里 section ... end 声明了局部环境，把 variables 的作用范围约束其中；在这个 section 中，variables 的声明会被其他所有命令捕获。
用反证法与逆否命题
import data.real.basic -- 涉及实数需要它
import tactic.push_neg -- 它收录了这里用到的 push_neg 与 contrapose!
open_locale classical -- 用反证法（by_contradiction）需要它，因为要有排中律
variables a b c : Prop -- 约定 a, b, c 都是命题
variables ε δ : ℝ -- 约定 ε与δ 都是实数
variables x : ℝ -- 约定 x 也是实数，其实可以合并到上一行去
variable f : ℝ → ℝ -- 约定 f 是定义在实数集上的实值函数
-- 下面这个名叫 f_0 的“引理”说 f 在原点连续。在 Lean 中，关键字 lemma 与关键字 theorem 是一回事。
-- 这里的写法是 lemma 引理名 (引理条件被省略了) : 引理的结论 :=
-- 此引理的结论的写法是：任意ε (满足名叫h1的假设 : ε > 0), 存在δ (满足名叫h2的假设 : δ > 0) , （使得对）任意 x (满足名叫h3的假设 : x 的绝对值 < δ) , （成立）f x < ε
lemma f_0 : ∀ ε (h1 : ε > 0) , ∃ δ (h2 : δ > 0) , ∀ x (h3 : abs x < δ) , f x < ε :=
begin
by_contradiction H, -- 原本的靶（作为命题）的否定在这里被命名为 H，这是一条新增的假设，然后靶会被替换成 false （意味着最终必须推出矛盾）。
push_neg at H, -- 进一步把 H 左边的 ¬ 一直推到最右边，得到我们熟悉的反证法的第一步。
sorry,
end
-- 下面是一个省略了名字与条件、只有结论的例题（example）
example : ¬ (a → b) → a ∧ ¬ b ∨ c :=
begin
contrapose!, -- 转为证明逆否命题
sorry,
end
参考文献
Jeremy Avigad, Type Theory and Practical Foundations
Mathematics in Lean, https://leanprover-community.github.io/mathematics_in_lean/index.html
HoTT学习笔记1：类型论基础, https://zhuanlan.zhihu.com/p/33483631
最后修改于 2021-06-23