haskell - フリーモナドの Functor 法則の証明; 私はそれを正しくやっていますか？

Question

フリーモナドのFunctorと法則を証明する方法を理解するのに少し苦労しています。Monadまず、私が使用している定義を挙げましょう。

data Free f a = Pure a | Free (f (Free f a))

instance Functor f => Functor (Free f) where
    fmap f (Pure a) = Pure (f a)
    fmap f (Free fa) = Free (fmap (fmap f) fa)

instance Functor f => Monad (Free f) where
    return = Pure
    Pure a >>= f = f a
    Free fa >>= f = Free (fmap (>>=f) fa)

{-

Functor laws:
(1) fmap id x == x
(2) fmap f (fmap g x) = fmap (f . g) x

Monad laws:
(1) return a >>= f   ==  f a
(2) m >>= return     ==  m
(3) (m >>= f) >>= g  ==  m >>= (\x -> f x >>= g)

-}

私が物事を正しく理解していれば、方程式の証明には共導仮説へのアピールが必要であり、多かれ少なかれ次の例のようになります。

Proof: fmap id == id

Case 1: x := Pure a
fmap id (Pure a)
  == Pure (id a)   -- Functor instance for Free
  == Pure a        -- id a == a

Case 2: x := Free fa
fmap id (Free fa)
  == Free (fmap (fmap id) fa)  -- Functor instance for Free f
  == Free (fmap id fa)         -- By coinductive hypothesis; is this step right?
  == Free fa                   -- Functor f => Functor (Free f), + functor law 

正しいことをしているかどうか確信が持てないステップを強調しました。

その証明が正しければFree、第 2 法則のコンストラクタの場合の証明は次のようになります。

fmap f (fmap g (Free fa))
  == fmap f (Free (fmap (fmap g) fa))
  == Free (fmap (fmap f) (fmap (fmap g) fa))
  == Free (fmap (fmap f . fmap g) fa)
  == Free (fmap (fmap (f . g)) fa)           -- By coinductive hypothesis
  == fmap (f . g) (Free fa)