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 into Haskell and made more specific to make it easier to think about, 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