跳到主要内容

Lean 引理与推论

在Lean中，**引理（Lemma）和推论（Corollary）**是数学证明中常用的工具。它们帮助我们组织和简化复杂的证明过程。本文将详细介绍什么是引理和推论，如何定义它们，以及如何在Lean中使用它们。

什么是引理与推论？​

引理（Lemma）​

引理是一个辅助性的命题，通常用于证明更复杂的定理。引理本身可能是一个小的、独立的命题，但它为证明主要定理提供了关键的步骤。

推论（Corollary）​

推论是从一个已经证明的定理或引理中直接得出的结论。它通常是定理的一个简单应用或特殊情况。

定义引理与推论​

在Lean中，引理和推论的定义方式与定理（Theorem）非常相似。它们都是通过lemma或corollary关键字来定义的。

定义引理​

lean
lemma my_lemma (n : ℕ) : n + 0 = n :=
begin
  induction n,
  { refl }, -- 基本情况
  { simp [nat.succ_add, n_ih] } -- 归纳步骤
end

在这个例子中，我们定义了一个名为my_lemma的引理，它证明了对于任何自然数n，n + 0 = n。这个引理可以通过归纳法来证明。

定义推论​

lean
corollary my_corollary (n : ℕ) : n + 1 = n.succ :=
begin
  exact nat.succ_eq_add_one n
end

这个推论my_corollary直接从nat.succ_eq_add_one定理中得出，证明了n + 1等于n的后继数。

使用引理与推论​

在证明中使用引理​

引理通常用于简化复杂的证明。例如，假设我们有一个定理需要证明n + 0 = n，我们可以直接引用之前定义的引理my_lemma，而不需要重新证明它。

lean
theorem my_theorem (n : ℕ) : n + 0 + 0 = n :=
begin
  rw my_lemma, -- 使用引理简化证明
  exact my_lemma n
end

在证明中使用推论​

推论的使用方式与引理类似。它们通常用于简化证明中的某些步骤。

lean
theorem another_theorem (n : ℕ) : n + 1 + 1 = n.succ.succ :=
begin
  rw my_corollary, -- 使用推论简化证明
  rw my_corollary,
  refl
end

实际案例​

案例1：证明加法交换律​

假设我们需要证明加法的交换律，即∀ n m : ℕ, n + m = m + n。我们可以先证明一个引理，然后再使用它来证明主要定理。

lean
lemma add_zero (n : ℕ) : n + 0 = n :=
begin
  induction n,
  { refl },
  { simp [nat.succ_add, n_ih] }
end

lemma add_succ (n m : ℕ) : n + m.succ = (n + m).succ :=
begin
  induction n,
  { refl },
  { simp [nat.succ_add, n_ih] }
end

theorem add_comm (n m : ℕ) : n + m = m + n :=
begin
  induction m,
  { rw add_zero },
  { rw [add_succ, m_ih] }
end

在这个例子中，我们首先定义了两个引理add_zero和add_succ，然后使用它们来证明加法的交换律add_comm。

案例2：证明乘法分配律​

另一个常见的例子是证明乘法的分配律。我们可以通过定义引理来简化证明过程。

lean
lemma mul_zero (n : ℕ) : n * 0 = 0 :=
begin
  induction n,
  { refl },
  { simp [nat.succ_mul, n_ih] }
end

lemma mul_succ (n m : ℕ) : n * m.succ = n * m + n :=
begin
  induction n,
  { refl },
  { simp [nat.succ_mul, n_ih] }
end

theorem mul_distrib (n m k : ℕ) : n * (m + k) = n * m + n * k :=
begin
  induction k,
  { rw [add_zero, mul_zero, add_zero] },
  { rw [add_succ, mul_succ, mul_succ, k_ih, add_assoc] }
end

在这个例子中，我们定义了两个引理mul_zero和mul_succ，然后使用它们来证明乘法的分配律mul_distrib。

总结​

引理和推论是Lean中非常重要的工具，它们帮助我们组织和简化复杂的证明过程。通过定义和使用引理与推论，我们可以将复杂的证明分解为更小、更易管理的部分。

附加资源​

练习​

  1. 定义一个引理，证明∀ n : ℕ, n * 1 = n。
  2. 使用你定义的引理，证明∀ n m : ℕ, n * m = m * n。

通过练习，你将更好地理解引理和推论的使用方法，并能够在自己的证明中灵活运用它们。