跳到主要内容

Lean 证明风格指南

介绍​

在Lean中，编写证明不仅仅是展示数学逻辑的正确性，还需要确保代码的可读性和可维护性。Lean的证明风格指南旨在帮助初学者理解如何编写清晰、简洁且易于维护的证明代码。通过遵循这些指南，你可以提高代码的质量，并使其更容易被他人理解和扩展。

1. 使用清晰的命名​

在编写证明时，使用清晰的命名是非常重要的。变量名、定理名和引理名应该能够清晰地表达其含义。避免使用过于简短或模糊的命名。

lean
-- 不好的命名
example : ∀ n : ℕ, n + 0 = n :=
begin
  intro x,
  rw add_zero,
end

-- 好的命名
example : ∀ n : ℕ, n + 0 = n :=
begin
  intro n,
  rw add_zero,
end

在第一个例子中，x 是一个模糊的命名，而在第二个例子中，n 清晰地表示了一个自然数。

2. 保持证明的简洁性​

Lean鼓励编写简洁的证明。避免不必要的步骤和冗长的代码。使用Lean的内置策略和库函数来简化证明。

lean
-- 冗长的证明
example : ∀ n : ℕ, n + 0 = n :=
begin
  intro n,
  induction n,
  { rw add_zero, },
  { rw add_zero, },
end

-- 简洁的证明
example : ∀ n : ℕ, n + 0 = n :=
begin
  intro n,
  rw add_zero,
end

在第一个例子中，使用了不必要的归纳法，而在第二个例子中，直接使用了 add_zero 策略来简化证明。

3. 使用注释解释复杂的步骤​

对于复杂的证明步骤，使用注释来解释其逻辑。这有助于他人理解你的思路，也方便你自己在以后回顾代码时快速理解。

lean
example : ∀ n : ℕ, n + 0 = n :=
begin
  intro n,
  -- 使用 add_zero 策略来简化加法中的零
  rw add_zero,
end

4. 避免重复代码​

在编写证明时，尽量避免重复代码。如果某个逻辑在多个地方出现，考虑将其提取为一个单独的引理或定理。

lean
-- 重复代码
example : ∀ n : ℕ, n + 0 = n ∧ n * 1 = n :=
begin
  intro n,
  split,
  { rw add_zero, },
  { rw mul_one, },
end

-- 提取重复逻辑
lemma add_zero_and_mul_one (n : ℕ) : n + 0 = n ∧ n * 1 = n :=
begin
  split,
  { rw add_zero, },
  { rw mul_one, },
end

example : ∀ n : ℕ, n + 0 = n ∧ n * 1 = n :=
begin
  intro n,
  exact add_zero_and_mul_one n,
end

在第一个例子中，add_zero 和 mul_one 的逻辑被重复使用，而在第二个例子中，这些逻辑被提取为一个单独的引理。

5. 使用适当的缩进和格式​

保持代码的缩进和格式一致，有助于提高代码的可读性。Lean社区通常使用两个空格作为缩进。

lean
-- 不好的缩进
example : ∀ n : ℕ, n + 0 = n :=
begin
intro n,
rw add_zero,
end

-- 好的缩进
example : ∀ n : ℕ, n + 0 = n :=
begin
  intro n,
  rw add_zero,
end

6. 实际案例​

以下是一个实际案例，展示了如何应用上述风格指南来编写一个复杂的证明。

lean
-- 实际案例：证明自然数的加法交换律
theorem add_comm : ∀ n m : ℕ, n + m = m + n :=
begin
  intros n m,
  induction n with k hk,
  { -- 基本情况：n = 0
    rw zero_add,
    rw add_zero,
  },
  { -- 归纳步骤：假设 n = k 时成立，证明 n = k + 1 时成立
    rw succ_add,
    rw hk,
    rw add_succ,
  }
end

在这个例子中，我们使用了清晰的命名、简洁的证明、注释解释、避免重复代码以及适当的缩进和格式。

总结​

通过遵循Lean的证明风格指南，你可以编写出清晰、简洁且易于维护的证明代码。这不仅有助于提高代码的质量，还能使你的代码更容易被他人理解和扩展。

附加资源与练习​

  • 练习：尝试编写一个证明，证明自然数的乘法交换律 ∀ n m : ℕ, n * m = m * n，并应用本指南中的风格建议。
  • 资源：阅读Lean官方文档中的证明风格指南以获取更多详细信息。
提示

记住，编写证明不仅仅是展示逻辑的正确性，还需要确保代码的可读性和可维护性。通过遵循这些指南，你可以成为一名更高效的Lean程序员。