級聯的民主基金和列表是民主基金 - 證明哈斯克爾

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