Twan van Laarhoven twanvl at gmail.com
Sun Dec 30 21:52:01 EST 2007

```Robin Green wrote:

> I am proving various statements relating to applicative functors, using
> the Coq proof assistant (I am considering only Coq terms, which always
> terminate so you don't have to worry about _|_). However, I'm not sure
> how to go about proving a certain conjecture, which, translated back
> looks like this (assuming Control.Applicative and Control.Arrow are
> imported):
>
> "For all applicative functors:
>
> \f x -> fmap second f <*> fmap ((,) (0::Int)) x
>
> is equivalent to
>
> \f x -> fmap ((,) (0::Int)) (f <*> x)"

Using the laws from the Control.Applicative haddock page, and some puzzling:

First of all, to avoid getting lost in parenthesis hell, define:
let g = (,) (0::Int)
let c = (.)

fmap second f <*> fmap g x
law: fmap*2
<=>  (pure second <*> f) <*> (pure g <*> x)
law: composition
<=>  (pure c <*> (pure second <*> f)) <*> pure g <*> x
law: interchange
<=>  pure (\$g) (pure c <*> (pure second <*> f)) <*> x
law: composition
<=>  pure c <\$> pure (\$g) <*> pure c <*> (pure second <*> f) <*> x
law: homomorphism*2
<=>  pure (c (\$g) c) <*> (pure second <*> f) <*> x
simplify
<=>  pure (. g) <*> (pure second <*> f) <*> x
law: composition
<=>  pure c <*> pure (. g) <*> pure second <*> f <*> x
law: homomorphism*2
<=>  pure (c (. g) second) <*> f <*> x
rewrite (unpl)
<=>  pure (\ d u -> (0,d u)) <*> f <*> x
rewrite some more
<=>  pure (c g) <*> f <*> x
law: homomorphism
<=>  pure c <*> pure g <*> f <*> x
law: composition
<=>  pure g <*> (f <*> x)
law: fmap
<=>  fmap g (f <*> x)

Q.E.D.

Twan
```