scala - scala：用结构归纳证明两个函数

Question

我在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))
}

函数sum(ls)正在计算其元素的总和，并turn(ls)以相反的顺序返回给我一个元素列表。sum(List(2, 13, 4))是 19 并且turn(List(2, 13, 4))是List(4, 13, 2)

我怎样才能用（结构）归纳表明

sum(cs) == sum(turn(cs))

持有？

标签： scalainduction