haskellで帰納的証明を設定するには？

Question

私は、xsはintの有限リストであるwhenver

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

を証明する必要があります。

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