Lean 证明重用

在Lean中，证明重用是一种强大的技术，它允许我们避免重复编写相同的证明逻辑，从而提高代码的效率和可维护性。本文将逐步介绍如何在Lean中重用证明，并通过实际案例展示其应用场景。

什么是证明重用？

证明重用是指在不同的上下文中使用已经完成的证明，而不需要重新编写相同的逻辑。这在Lean中尤为重要，因为Lean是一个交互式定理证明器，编写证明可能会非常耗时。通过重用证明，我们可以节省时间并减少错误。

在Lean中，证明重用通常通过定义引理（lemma）或定理（theorem）来实现。这些引理或定理可以在后续的证明中被调用，从而避免重复编写相同的逻辑。

假设我们有一个简单的命题 P → Q → P，我们可以先证明这个命题，然后在后续的证明中重用这个证明。

lemma imp_trans : P → Q → P :=
begin
  intros hP hQ,
  exact hP,
end

在这个例子中，我们定义了一个名为 imp_trans 的引理，它证明了 P → Q → P。现在，我们可以在其他证明中重用这个引理。

example : P → Q → P :=
begin
  apply imp_trans,
end

在这个例子中，我们使用了 apply imp_trans 来重用之前定义的引理，而不需要重新编写证明逻辑。

首先，我们需要定义一个引理，它包含我们希望重用的证明逻辑。引理的定义通常包括一个名称和一个类型签名。

lemma my_lemma : P → Q → R :=
begin
  -- 证明逻辑
end

一旦定义了引理，我们可以在其他证明中通过名称调用它。调用引理的方式取决于引理的类型签名。

example : P → Q → R :=
begin
  apply my_lemma,
end

如果引理需要参数，我们可以在调用时传递这些参数。

example (hP : P) (hQ : Q) : R :=
begin
  apply my_lemma hP hQ,
end

假设我们需要证明一个关于自然数加法的交换律的命题。我们可以先定义一个引理来证明交换律，然后在其他证明中重用这个引理。

lemma add_comm : ∀ (n m : ℕ), n + m = m + n :=
begin
  intros n m,
  induction n with d hd,
  { simp },
  { simp [hd] },
end

现在，我们可以在其他证明中重用这个引理。

example : ∀ (n m : ℕ), n + m = m + n :=
begin
  apply add_comm,
end

证明重用是Lean中提高代码效率和可维护性的重要技术。通过定义引理并在后续证明中调用它们，我们可以避免重复编写相同的逻辑，从而节省时间并减少错误。

通过这些练习，你将更好地理解如何在Lean中有效地重用证明。