如何用结构归纳法证明Scala中sum与turn函数的等式成立？

好的，我们用结构归纳法一步步来证明这个等式对所有整数列表都成立。首先先明确目标命题：对于任意整数列表cs，sum(cs) == sum(turn(cs))恒成立。

先把你给出的Scala函数整理成更易读的格式：

def sum(ls: List[Int]): Int = ls match {
  case Nil => 0
  case l::ls => l + sum(ls)
}

def turn(ls: List[Int]): List[Int] = ls match {
  case Nil => List()
  case l::ls => append(turn(ls), List(l))
}

注：这里默认append是标准的列表拼接函数，定义为：

def append[A](a: List[A], b: List[A]): List[A] = a match {
  case Nil => b
  case x::xs => x::append(xs, b)
}

1. 基例：空列表Nil #

我们先验证最简单的情况——空列表：

• 左边：根据sum的定义，sum(Nil) = 0
• 右边：先看turn(Nil)，根据turn的定义返回空列表List()，所以sum(turn(Nil)) = sum(List()) = 0

显然0 == 0，基例成立。

2. 归纳假设 #

假设对于任意的整数列表xs，命题sum(xs) == sum(turn(xs))成立（这是归纳假设，我们假设这个等式对更短的列表xs是成立的）。

3. 归纳步骤：非空列表x::xs #

现在我们需要证明当列表为x::xs（即头部是整数x，尾部是列表xs）时，等式sum(x::xs) == sum(turn(x::xs))成立。

展开等式两边： #

• 左边：根据sum函数的定义，直接展开得到：
  sum(x::xs) = x + sum(xs)
• 右边：先展开turn(x::xs)，根据turn的定义：
  turn(x::xs) = append(turn(xs), List(x))
  所以右边变为sum(append(turn(xs), List(x)))

用到的辅助性质 #

这里我们需要先确认一个列表求和的基本性质：对于任意两个整数列表a和b，sum(append(a, b)) = sum(a) + sum(b)。如果这个性质你还不熟悉，我也用结构归纳法快速证明一下：

辅助性质证明：

• 基例：a = Nil，append(Nil, b) = b，所以sum(append(Nil, b)) = sum(b) = sum(Nil) + sum(b)，成立。
• 归纳假设：假设对列表as，sum(append(as, b)) = sum(as) + sum(b)成立。
• 归纳步骤：a = x::as，append(x::as, b) = x::append(as, b)，所以sum(append(x::as, b)) = x + sum(append(as, b)) = x + sum(as) + sum(b) = sum(x::as) + sum(b)，成立。

继续推导右边 #

根据辅助性质，右边可以拆解为：
sum(append(turn(xs), List(x))) = sum(turn(xs)) + sum(List(x))

而sum(List(x))根据sum的定义，就是x + sum(Nil) = x + 0 = x。再代入我们的归纳假设sum(xs) == sum(turn(xs))，右边就变成：
sum(xs) + x

等式两边对比 #

左边是x + sum(xs)，右边是sum(xs) + x，根据整数加法的交换律，两者完全相等。因此当列表为x::xs时，等式成立。

结论 #

通过结构归纳法，我们验证了基例成立，且在归纳假设成立的前提下，非空列表的情况也成立。因此，对于所有的整数列表cs，sum(cs) == sum(turn(cs))恒成立。

内容的提问来源于stack exchange，提问作者MBD