证明等价

重写为使用尾递归和累加器的程序可能看起来与原始程序非常不同。 原始递归函数通常更容易理解，但它有在运行时耗尽栈的风险。 在用示例测试程序的两个版本以排除简单错误后，可以使用证明来一劳永逸地证明二者是等价的。

证明 sum 相等

要证明 sum 的两个版本相等，首先用桩（stub）证明编写定理的陈述：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  skip

正如预期，Lean 描述了一个未解决的目标：

unsolved goals
⊢ NonTail.sum = Tail.sum

rfl 策略无法在此处应用，因为 NonTail.sum 和 Tail.sum 在定义上不相等。 然而，函数除了定义相等外还存在更多相等的方式。还可以通过证明两个函数对相同输入产生相等输出， 来证明它们相等。换句话说，可以通过证明「对于所有可能的输入 \( x \)， 都有 \( f(x) = g(x) \)」来证明 \( f = g \)。此原理称为 函数外延性（Function Extensionality）。 函数外延性正是 NonTail.sum 等于 Tail.sum 的原因：它们都对数字列表求和。

在 Lean 的策略语言中，可使用 funext 调用函数外延性，后跟一个用于任意参数的名称。 任意参数会作为假设添加到语境中，目标变为证明应用于此参数的函数相等：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs

unsolved goals
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sum xs

此目标可通过对参数 xs 进行归纳来证明。当应用于空列表时，sum 函数都返回 0，这是基本情况。 在输入列表的开头添加一个数字会让两个函数都将该数字添加到结果中，这是归纳步骤。 调用 induction 策略会产生两个目标：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  induction xs with
  | nil => skip
  | cons y ys ih => skip

unsolved goals
case h.nil
⊢ NonTail.sum [] = Tail.sum []

unsolved goals
case h.cons
y : Nat
ys : List Nat
ih : NonTail.sum ys = Tail.sum ys
⊢ NonTail.sum (y :: ys) = Tail.sum (y :: ys)

nil 的基本情况可以使用 rfl 解决，因为当传递空列表时，两个函数都返回 0：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  induction xs with
  | nil => rfl
  | cons y ys ih => skip

解决归纳步骤的第一步是简化目标，要求 simp 展开 NonTail.sum 和 Tail.sum：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  induction xs with
  | nil => rfl
  | cons y ys ih =>
    simp [NonTail.sum, Tail.sum]

unsolved goals
case h.cons
y : Nat
ys : List Nat
ih : NonTail.sum ys = Tail.sum ys
⊢ y + NonTail.sum ys = Tail.sumHelper 0 (y :: ys)

展开 Tail.sum 会发现它直接委托给了 Tail.sumHelper，它也应该被简化：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  induction xs with
  | nil => rfl
  | cons y ys ih =>
    simp [NonTail.sum, Tail.sum, Tail.sumHelper]

在结果目标中，sumHelper 执行了一步计算并将 y 加到累加器上：

unsolved goals
case h.cons
y : Nat
ys : List Nat
ih : NonTail.sum ys = Tail.sum ys
⊢ y + NonTail.sum ys = Tail.sumHelper y ys

使用归纳假设重写会从目标中删除所有 NonTail.sum 的引用：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  induction xs with
  | nil => rfl
  | cons y ys ih =>
    simp [NonTail.sum, Tail.sum, Tail.sumHelper]
    rw [ih]

unsolved goals
case h.cons
y : Nat
ys : List Nat
ih : NonTail.sum ys = Tail.sum ys
⊢ y + Tail.sum ys = Tail.sumHelper y ys

这个新目标表明，将某个数字加到列表的和中与在 sumHelper 中使用该数字作为初始累加器相同。 为了清晰起见，这个新目标可以作为独立的定理来证明：

theorem helper_add_sum_accum (xs : List Nat) (n : Nat) :
    n + Tail.sum xs = Tail.sumHelper n xs := by
  skip

unsolved goals
xs : List Nat
n : Nat
⊢ n + Tail.sum xs = Tail.sumHelper n xs

这又是一次归纳证明，其中基本情况使用 rfl 证明：

theorem helper_add_sum_accum (xs : List Nat) (n : Nat) :
    n + Tail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil => rfl
  | cons y ys ih => skip

unsolved goals
case cons
n y : Nat
ys : List Nat
ih : n + Tail.sum ys = Tail.sumHelper n ys
⊢ n + Tail.sum (y :: ys) = Tail.sumHelper n (y :: ys)

由于这是一个归纳步骤，因此目标应该被简化，直到它与归纳假设 ih 匹配。 简化，然后使用 Tail.sum 和 Tail.sumHelper 的定义，得到以下结果：

theorem helper_add_sum_accum (xs : List Nat) (n : Nat) :
    n + Tail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil => rfl
  | cons y ys ih =>
    simp [Tail.sum, Tail.sumHelper]

unsolved goals
case cons
n y : Nat
ys : List Nat
ih : n + Tail.sum ys = Tail.sumHelper n ys
⊢ n + Tail.sumHelper y ys = Tail.sumHelper (y + n) ys

理想情况下，归纳假设可以用来替换 Tail.sumHelper (y + n) ys，但它们不匹配。 归纳假设可用于 Tail.sumHelper n ys，而非 Tail.sumHelper (y + n) ys。 换句话说，这个证明到这里被卡住了。

第二次尝试

与其试图弄清楚证明，不如退一步思考。为什么函数的尾递归版本等于非尾递归版本？ 从根本上讲，在列表中的每个条目中，累加器都会增加与递归结果中添加的量相同的值。 这个见解可以用来写一个优雅的证明。 重点在于，归纳证明必须设置成归纳假设可以应用于 任何 累加器值。

放弃之前的尝试，这个见解可以编码为以下陈述：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  skip

在这个陈述中，非常重要的是 n 是冒号后面类型的组成部分。 产生的目标以 ∀ (n : Nat) 开头，这是「对于所有 n」的缩写：

unsolved goals
xs : List Nat
⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs

使用归纳策略会产生包含这个「对于所有（for all）」语句的目标：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil => skip
  | cons y ys ih => skip

在 nil 情况下，目标是：

unsolved goals
case nil
⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n []

对于 cons 的归纳步骤，归纳假设和具体目标都包含「对于所有 n」：

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)

换句话说，目标变得更难证明，但归纳假设相应地更加有用。

对于以「对于所有 \( x \)」开头的陈述的数学证明应该假设存在任意的 \( x \)， 并证明该阐述。「任意」意味着不假设 \( x \) 的任何额外性质，因此结果语句将适用于 任何 \( x \)。 在 Lean 中，「对于所有」语句是一个依值函数：无论将其应用于哪个特定值，它都将返回命题的证据。 类似地，选择任意 \( x \) 的过程与使用 fun x => ... 相同。在策略语言中， 选择任意 \( x \) 的过程是使用 intro 策略执行的，当策略脚本完成后，它会在幕后生成函数。 intro 策略应当被提供用于此任意值的名称。

在 nil 情况下使用 intro 策略会从目标中移除 ∀ (n : Nat),，并添加假设 n : Nat：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil => intro n
  | cons y ys ih => skip

unsolved goals
case nil
n : Nat
⊢ n + NonTail.sum [] = Tail.sumHelper n []

此命题等式的两边在定义上等于 n，因此 rfl 就足够了：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil =>
    intro n
    rfl
  | cons y ys ih => skip

cons 目标也包含一个「对于所有」：

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)

这这里建议使用 intro。

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil =>
    intro n
    rfl
  | cons y ys ih =>
    intro n

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)

现在，证明目标包含应用于 y :: ys 的 NonTail.sum 和 Tail.sumHelper。 简化器可以使下一步更清晰：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil =>
    intro n
    rfl
  | cons y ys ih =>
    intro n
    simp [NonTail.sum, Tail.sumHelper]

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + (y + NonTail.sum ys) = Tail.sumHelper (y + n) ys

此目标非常接近于匹配归纳假设。它不匹配的方面有两个：

• 等式的左侧是 n + (y + NonTail.sum ys)，但归纳假设需要左侧是一个添加到 NonTail.sum ys 的数字。 换句话说，此目标应重写为 (n + y) + NonTail.sum ys，这是有效的，因为自然数加法满足结合律。
• 当左侧重写为 (y + n) + NonTail.sum ys 时，右侧的累加器参数应为 n + y 而非 y + n 以进行匹配。 此重写是有效的，因为加法也满足交换律。

The associativity and commutativity of addition have already been proved in Lean's standard library. The proof of associativity is named Nat.add_assoc, and its type is (n m k : Nat) → (n + m) + k = n + (m + k), while the proof of commutativity is called Nat.add_comm and has type (n m : Nat) → n + m = m + n. Normally, the rw tactic is provided with an expression whose type is an equality. However, if the argument is instead a dependent function whose return type is an equality, it attempts to find arguments to the function that would allow the equality to match something in the goal. There is only one opportunity to apply associativity, though the direction of the rewrite must be reversed because the right side of the equality in Nat.add_assoc is the one that matches the proof goal:

加法的结合律和交换律已在 Lean 的标准库中得到证明。结合律的证明名为 Nat.add_assoc， 其类型为 (n m k : Nat) → (n + m) + k = n + (m + k)， 而交换律的证明称为 Nat.add_comm， 其类型为 (n m : Nat) → n + m = m + n。 通常，rw 策略会提供一个类型为等式的表达式。但是，如果参数是一个返回类型为等式的相关函数， 它会尝试查找函数的参数，以便等式可以匹配目标中的某个内容。 虽然必须反转重写方向，但只有一种机会应用结合律， 因为 Nat.add_assoc 中等式的右侧是与证明目标匹配的：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil =>
    intro n
    rfl
  | cons y ys ih =>
    intro n
    simp [NonTail.sum, Tail.sumHelper]
    rw [←Nat.add_assoc]

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + y + NonTail.sum ys = Tail.sumHelper (y + n) ys

然而，直接使用 Nat.add_comm 重写会导致错误的结果。rw 策略猜测了错误的重写位置，导致了意料之外的目标：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil =>
    intro n
    rfl
  | cons y ys ih =>
    intro n
    simp [NonTail.sum, Tail.sumHelper]
    rw [←Nat.add_assoc]
    rw [Nat.add_comm]

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ NonTail.sum ys + (n + y) = Tail.sumHelper (y + n) ys

可以通过显式地将 y 和 n 作为参数提供给 Nat.add_comm 来解决此问题：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil =>
    intro n
    rfl
  | cons y ys ih =>
    intro n
    simp [NonTail.sum, Tail.sumHelper]
    rw [←Nat.add_assoc]
    rw [Nat.add_comm y n]

unsolved goals
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + y + NonTail.sum ys = Tail.sumHelper (n + y) ys

现在目标与归纳假设相匹配了。特别是，归纳假设的类型是一个依值函数类型。 将 ih 应用于 n + y 会产生刚好期望的类型。如果其参数具有期望的类型， exact 策略会完成证明目标：

theorem non_tail_sum_eq_helper_accum (xs : List Nat) :
    (n : Nat) → n + NonTail.sum xs = Tail.sumHelper n xs := by
  induction xs with
  | nil => intro n; rfl
  | cons y ys ih =>
    intro n
    simp [NonTail.sum, Tail.sumHelper]
    rw [←Nat.add_assoc]
    rw [Nat.add_comm y n]
    exact ih (n + y)

实际的证明只需要一些额外的工作即可使目标与辅助函数的类型相匹配。 第一步仍然是调用函数外延性：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs

unsolved goals
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sum xs

下一步是展开 Tail.sum，暴露出 Tail.sumHelper：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  simp [Tail.sum]

unsolved goals
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sumHelper 0 xs

完成这一步后，类型已经近乎匹配了。但是，辅助类型在左侧有一个额外的加数。 换句话说，证明目标是 NonTail.sum xs = Tail.sumHelper 0 xs， 但将 non_tail_sum_eq_helper_accum 应用于 xs 和 0 会产生类型 0 + NonTail.sum xs = Tail.sumHelper 0 xs。 另一个标准库证明 Nat.zero_add 的类型为 (n : Nat) → 0 + n = n。 将此函数应用于 NonTail.sum xs 会产生类型为 0 + NonTail.sum xs = NonTail.sum xs 的表达式， 因此从右往左重写会产生期望的目标：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  simp [Tail.sum]
  rw [←Nat.zero_add (NonTail.sum xs)]

unsolved goals
case h
xs : List Nat
⊢ 0 + NonTail.sum xs = Tail.sumHelper 0 xs

最后，可以使用辅助定理来完成证明：

theorem non_tail_sum_eq_tail_sum : NonTail.sum = Tail.sum := by
  funext xs
  simp [Tail.sum]
  rw [←Nat.zero_add (NonTail.sum xs)]
  exact non_tail_sum_eq_helper_accum xs 0

此证明演示了在证明「累加器传递尾递归函数等于非尾递归版本」时可以使用的通用模式。 第一步是发现起始累加器参数和最终结果之间的关系。 例如，以 n 的累加器开始 Tail.sumHelper 会导致最终的和被添加到 n 中， 而以 ys 的累加器开始 Tail.reverseHelper 会导致最终反转的列表被前置到 ys 中。 第二步是将此关系写成定理陈述，并通过归纳法证明它。虽然在实践中， 累加器总是用一些中性值（Neutral，即幺元，例如 0 或 []）初始化， 但允许起始累加器为任何值的更通用的陈述是获得足够强的归纳假设所需要的。 最后，将此辅助定理与实际的初始累加器值一起使用会产生期望的证明。 例如，在 non_tail_sum_eq_tail_sum 中，累加器指定为 0。 这可能需要重写目标以使中性初始累加器值出现在正确的位置。

练习

热身

使用 induction 策略编写你自己的 Nat.zero_add、Nat.add_assoc 和 Nat.add_comm 的证明。

更多累加器证明

反转列表

将 sum 的证明调整为 NonTail.reverse 和 Tail.reverse 的证明。 第一步是思考传递给 Tail.reverseHelper 的累加器值与非尾递归反转之间的关系。 正如在 Tail.sumHelper 中将数字添加到累加器中与将其添加到整体的和中相同， 在 Tail.reverseHelper 中使用 List.cons 将新条目添加到累加器中相当于对整体结果进行了一些更改。 用纸和笔尝试三个或四个不同的累加器值，直到关系变得清晰。 使用此关系来证明一个合适的辅助定理。然后，写下整体定理。 因为 NonTail.reverse 和 Tail.reverse 是多态的，所以声明它们的相等性需要使用 @ 来阻止 Lean 尝试找出为 α 使用哪种类型。一旦 α 被视为一个普通参数， funext 应该与 α 和 xs 一起调用：

theorem non_tail_reverse_eq_tail_reverse : @NonTail.reverse = @Tail.reverse := by
  funext α xs

这会产生一个合适的目标：

unsolved goals
case h.h
α : Type u_1
xs : List α
⊢ NonTail.reverse xs = Tail.reverse xs

阶乘

通过找到累加器和结果之间的关系并证明一个合适的辅助定理， 证明上一节练习中的 NonTail.factorial 等于你的尾递归版本的解决方案。