跳到主要内容

Lean 命题与定理

在Lean中，**命题（Proposition）和定理（Theorem）**是数学逻辑的核心概念。它们用于表达数学中的陈述，并通过形式化证明来验证其正确性。本文将逐步介绍如何在Lean中定义命题、构造定理，并通过实际案例展示其应用。

什么是命题？​

在数学中，命题是一个可以被判断为真或假的陈述。例如，“2 + 2 = 4”是一个命题，因为它可以被明确地判断为真。在Lean中，命题通常表示为类型为 Prop 的表达式。

定义命题​

在Lean中，我们可以使用 def 关键字来定义一个命题。例如：

def is_even (n : ℕ) : Prop := n % 2 = 0

这里，is_even 是一个命题，它接受一个自然数 n 并返回一个 Prop 类型的值，表示 n 是否为偶数。

什么是定理？​

定理是一个已经被证明为真的命题。在Lean中，定理是通过构造一个证明来定义的。定理的证明是一个类型为命题的函数，它展示了命题为真的证据。

定义定理​

在Lean中，我们可以使用 theorem 关键字来定义一个定理。例如：

theorem two_is_even : is_even 2 :=
begin
  show 2 % 2 = 0,
  exact rfl
end

这里，two_is_even 是一个定理，它证明了命题 is_even 2 为真。begin ... end 块中的代码是定理的证明。

逐步讲解​

1. 定义命题​

首先，我们需要定义一个命题。例如，我们可以定义一个命题 is_prime，表示一个数是否为素数：

def is_prime (n : ℕ) : Prop :=
  n > 1 ∧ ∀ m : ℕ, m ∣ n → m = 1 ∨ m = n

这个命题表示 n 大于1，并且对于所有能整除 n 的数 m，m 要么是1，要么是 n 本身。

2. 构造定理​

接下来，我们可以构造一个定理来证明某个数是素数。例如，我们可以证明2是素数：

theorem two_is_prime : is_prime 2 :=
begin
  split,
  { exact nat.succ_pos 1 },
  { intros m h,
    have h_le : m ≤ 2 := nat.le_of_dvd (nat.succ_pos 1) h,
    interval_cases m,
    { left, refl },
    { right, refl },
    { contradiction } }
end

在这个证明中，我们首先证明了2大于1，然后证明了对于所有能整除2的数 m，m 要么是1，要么是2。

3. 实际案例​

让我们通过一个实际案例来展示命题与定理的应用。假设我们想要证明“所有偶数的平方都是4的倍数”。

首先，我们定义命题：

def square_of_even_is_multiple_of_four (n : ℕ) : Prop :=
  is_even n → (n^2) % 4 = 0

然后，我们构造定理：

theorem square_of_even_is_multiple_of_four_proof : ∀ n : ℕ, square_of_even_is_multiple_of_four n :=
begin
  intros n h,
  rw is_even at h,
  rw nat.pow_two,
  rw nat.mul_mod,
  rw h,
  rw zero_mul,
  exact rfl
end

在这个证明中，我们假设 n 是偶数，然后证明了 n^2 是4的倍数。

总结​

在Lean中，命题和定理是数学逻辑的基础。通过定义命题和构造定理，我们可以形式化地表达和证明数学陈述。本文通过逐步讲解和实际案例，展示了如何在Lean中定义命题、构造定理，并通过证明验证其正确性。

附加资源与练习​

  • 练习1：定义一个命题 is_odd，表示一个数是奇数，并证明3是奇数。
  • 练习2：定义一个命题 is_multiple_of_three，表示一个数是3的倍数，并证明6是3的倍数。
  • 附加资源：阅读Lean官方文档中关于命题和定理的更多内容，深入理解其应用和证明技巧。

通过不断练习和探索，你将能够熟练掌握Lean中的命题与定理，并在形式化证明中游刃有余。