unf和list的连接是unf - 证明Haskell

Question

如何证明以下每个列表xs都是如此:

undefined ++ xs = undefined

Answer 1

没有太多要证明的.只有一个规则(不能解释或分解成更小的规则)case试图匹配undefined构造函数的语句导致undefined.一旦你接受这个规则,我们就可以观察到

undefined ++ ys
= { by definition of ++ }
case undefined of
    [] -> ys
    x:xs -> x : (xs ++ ys)
= { case that matches undefined against a constructor }
undefined