Как настроить индуктивное доказательство в haskell?

Question

Мне нужно доказать

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

всякий раз, когда xs является конечным списком Ints.

Предположим, что f и g имеют тип [Int]->[Int]

Answer 1

Противопоказан контрпример:

f xs = []
g xs = [1]

Если вы хотите, чтобы это свойство сохранялось, вам нужны более конкретные ограничения на то, что f а также g являются.

Вы можете думать о законе, который

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

что действительно может быть доказано.

Answer 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