我正在关注 Coursera 上的 Scala 函数式编程讲座,在视频 5.7 的结尾,Martin Odersky 要求通过归纳证明以下等式的正确性:
(xs ++ ys) map f = (xs map f) ++ (ys map f)
当涉及多个列表时如何处理归纳证明?
我检查了 xs 为 Nil 和 ys 为 Nil 的基本情况。我已经通过归纳证明,当 xs 被 x::xs 替换时,等式成立,但是我们是否还需要检查 ys 被 y::ys 替换的等式?
在那种情况下(不会过多地破坏练习......无论如何都没有评分)你如何处理:(xs ++ (y::ys)) map f
?
这是我在类似示例中使用的方法,以证明
(xs ++ ys).reverse = ys.reverse ++ xs.reverse
证明(省略基本情况和简单的 x::xs 情况):
(xs ++ (y::ys)).reverse
= (xs ++ (List(y) ++ ys)).reverse //y::ys = List(y) ++ ys
= ((xs ++ List(y)) ++ ys).reverse //concat associativity
= ys.reverse ++ (xs ++ List(y)).reverse //by induction hypothesis (proven with x::xs)
= ys.reverse ++ List(y).reverse ++ xs.reverse //by induction hypothesis
= ys.reverse ++ (y::Nil).reverse ++ xs.reverse //List(y) = y :: Nil
= ys.reverse ++ Nil.reverse ++ List(y) ++ xs.reverse //reverse definition
= (ys.reverse ++ List(y)) ++ xs.reverse //reverse on Nil (base case)
= (y :: ys).reverse ++ xs.reverse //reverse definition
这是正确的吗 ?