如何在haskell中建立归纳证明？ [关闭]答案

【问题标题】：How to set up an inductive proof in haskell? [closed]如何在haskell中建立归纳证明？ [关闭]
【发布时间】：2017-04-24 22:44:08
【问题描述】：

我需要证明

f (g xs) == g (f xs)

当 xs 是 Ints 的有限列表时。

假设 f 和 g 的类型都是 [Int]->[Int]

【问题讨论】：

这是针对特定的f 和g，对吧？（对于任意的f 和g 它不成立。）
它们都是 [Int]->[Int] 类型并且都采用有限整数列表。

标签： haskell proof induction

【解决方案1】：

反例反驳：

f xs = []
g xs = [1]

如果您希望保留此属性，则需要对 f 和 g 进行更具体的限制。

你可能在想法律

(map f . map g) == map (f . g)

确实可以证明。

【讨论】：

【解决方案2】：

从某处发现的

Theorem: (map f . map g) xs = map (f . g) xs
       - Proof is by induction on xs
    *** Base Case, xs = []
        - Left side: (map f . map g) [] = map f (map g []) = map f [] = []
        - Right side: map (f . g) [] = []
    *** Inductive Case, xs = k:ks
        - Inductive Hypothesis: (map f . map g) ks = map (f . g) ks
        - Left Side
          + (map f . map g) xs
          + map f (map g (k:ks))
          + map f ((g k) : (map g ks))
          + (f (g k)) : (map f (map g ks))
          + ((f . g) k) : ((map f . map g) ks)  i.e. change from bracket form back to point form
          + ((f . g) k) : (map (f . g) ks) by inductive hypothesis
          + map (f . g) (k:ks) by definition of map
          + map (f . g) xs

【讨论】：

这与说f (g xs) == g (f xs) 非常不同，正如其他人指出的那样，这通常是错误的。