Associativity of liftA2

liftA2-assoc.hs

-- op :: a -> a -> a
-- `op` associative

-- We wish to prove that 'liftA2 op' is associative.

-- x, y, z :: a
-- f such that Applicative f
-- fx, fy, fz :: f a

(op x . op y) z
-- definition of (.)
op x (op y z)
-- associativity
op (op x y) z

-- from the above, by ŋ-reduction:
op (op x y) = op x . op y

-- therefore, by the lemma for liftA2:
-- <https://hackage.haskell.org/package/base-4.11.1.0/docs/Control-Applicative.html#t:Applicative>

liftA2 op (liftA2 op fx fy) = liftA2 op fx . liftA2 op fy
-- ŋ-expand both sides
liftA2 op (liftA2 op fx fy) fz = (liftA2 op fx . liftA2 op fy) fz
-- RHS: inline (.) and β-reduce
liftA2 op (liftA2 op fx fy) fz = liftA2 op fx (liftA2 op fy fz)

-- QED.