级联的民主基金和列表是民主基金 - 证明哈斯克尔

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