Lean 简单证明示例

Lean是一个交互式定理证明器，它允许用户通过编写代码来形式化数学证明。对于初学者来说，理解Lean的基本证明结构是迈向更复杂证明的第一步。本文将介绍一些简单的证明示例，帮助你快速上手Lean。

什么是Lean证明？

在Lean中，证明是通过编写代码来完成的。Lean的核心思想是将数学命题转化为类型，而证明则是构造这些类型的实例。通过这种方式，Lean能够验证你的证明是否正确。

让我们从一个非常简单的例子开始：证明 1 + 1 = 2。在Lean中，这个命题可以表示为 1 + 1 = 2，而证明则是构造这个等式的一个实例。

lean
example : 1 + 1 = 2 :=
begin
  refl
end

在这个例子中，refl 是“自反性”（reflexivity）的缩写，它表示等式两边的值是相等的。Lean会自动计算 1 + 1 并验证它是否等于 2。

接下来，我们来看一个稍微复杂一点的例子：证明对于所有自然数 n，n + 0 = n。这个命题可以表示为 ∀ n : ℕ, n + 0 = n。

lean
example : ∀ n : ℕ, n + 0 = n :=
begin
  intro n,
  induction n with d hd,
  { refl },
  { simp [hd] }
end

在这个证明中，我们使用了归纳法。首先，我们引入一个自然数 n，然后对 n 进行归纳。基础情况是 n = 0，此时 0 + 0 = 0 显然成立。归纳步骤假设对于某个自然数 d，d + 0 = d 成立，然后证明 d.succ + 0 = d.succ 也成立。

最后，我们来看一个逻辑命题的证明：证明 ¬(false)，即“假命题的否定为真”。

lean
example : ¬(false) :=
begin
  intro h,
  cases h
end

在这个证明中，我们假设 false 成立，然后通过 cases 策略推导出矛盾，从而证明了 ¬(false)。

Lean的证明能力不仅仅局限于简单的数学命题。它在形式化数学、计算机科学、甚至硬件验证中都有广泛的应用。例如，Lean可以用来验证算法的正确性，或者证明复杂的数学定理。

通过本文的简单示例，你已经初步了解了如何在Lean中进行基础证明。Lean的证明过程虽然一开始可能看起来有些抽象，但随着练习的深入，你会发现它非常强大且灵活。

通过这些练习，你将进一步巩固对Lean证明的理解。继续探索Lean的世界，你会发现更多有趣且强大的功能！