NEComonadApplyProof.hs

import Data.List.NonEmpty
--These are the definitions I'll use in my proof:

fmap :: (a -> b) -> NonEmpty a -> NonEmpty b
fmap f (a :| as) = f a :| Prelude.fmap f as

extract :: NonEmpty a -> a
extract (a :| _) = a

duplicate :: NonEmpty a -> NonEmpty (NonEmpty a)
duplicate l@(_ :| as) = l :| go_dupe as
  where
    go_dupe (x:xs) = (x :| xs) : go_dupe xs
    go_dupe _ = []


-- zipped = zipWith id
zipped :: NonEmpty (a -> b) -> NonEmpty a -> NonEmpty b
zipped (f :| fs) (a :| as) = f a :| go_zipped fs as
  where
    go_zipped (f' : fs') (a' : as') = f' a' : go_zipped fs' as'
    go_zipped _          _          = []

{-
(<@>) = zipped
is a valid ComonadApply instance for NonEmpty.

PROOF:

Associativity for `zipWith id` is already known.

extract (ff <@> fa) === extract ff $ extract fa

  extract (ff <@> fa)
      -- let ff = (f :| fs)
      -- let fa = (a :| as)
      -- definition of (<@>)
    === extract (f a :| go_zipped fs as)
      -- definition of extract
    === f a

  extract f $ extract a
      -- let ff = (f :| fs)
      -- let fa = (a :| as)
    === extract (f :| fs) $ extract (a :| as)
      -- definition of extract
    === f $ a
    === f a


duplicate (f <@> a) === (<@>) <$> duplicate ff <@> duplicate fa

duplicate (ff <@> fa)
    -- let ff = (f :| fs)
    -- let fa = (a :| as)
    -- definition of (<@>)
  === duplicate (f a :| go_zipped fs as)
    -- definition of duplicate
  === (ff <@> fa) :| go_dupe (go_zipped fs as)

(<@>) <$> duplicate ff $ duplicate fa
    -- (<$>) = fmap
  === (fmap (<@>) (duplicate ff)) <@> duplicate fa
    -- let ff = (f :| fs)
    -- definition of duplicate
  === (fmap (<@>) (ff :| go_dupe fs)) <@> duplicate fa
    -- definition of fmap
  === ((ff <@>) :| fmap (<@>) (go_dupe fs)) <@> duplicate fa
    -- let fa = (a :| as)
    -- definition of duplicate
  === ((ff <@>) :| fmap (<@>) (go_dupe fs)) <@> (fa :| go_dupe as)
    -- definition of (<@>)
  === (ff <@> fa) :| go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as)

For:

duplicate (f <@> a) === (<@>) <$> duplicate ff <@> duplicate fa

to be proven equal, we must show that:

go_dupe (go_zipped fs as) === go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as)

Proof by induction:

Base case:
fs and/or as is []

  go_dupe (go_zipped fs as)
      -- definition of go_zipped:
      -- go_zipped [] as === go_zipped fs [] === []
    === go_dupe []
      -- definition of go_dupe
    === []


  go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as)

    If fs === []:
      go_zipped (fmap (<@>) (go_dupe [])) (go_dupe as)
          -- definition of go_dupe
        === go_zipped (fmap (<@>) []) (go_dupe as)
          -- definition of fmap
        === go_zipped [] (go_dupe as)
          -- definition of go_zipped
        === []

    If as === []:
      go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe [])
          -- definition of go_dupe
        === go_zipped (fmap (<@>) (go_dupe fs)) []
          -- definition of go_zipped
        === []

  we have:
    go_dupe (go_zipped fs as) === go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as)



Induction step:
let fs = (f' : fs')
let as = (a' : as')
And assume:
go_dupe (go_zipped fs' as') === go_zipped (fmap (<@>) (go_dupe fs')) (go_dupe as')


  go_dupe (go_zipped fs as)
      -- definition of go_zipped
    === go_dupe (f' a' : go_zipped fs' as')
      -- definition of go_dupe
    === (f' a' :| go_zipped fs' as') : go_dupe (go_zipped fs' as')


  go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as)
      -- definition of go_dupe
    === go_zipped (fmap (<@>) ((f' :| fs') : go_dupe fs')) ((a' :| as') : go_dupe as')
      -- definition of fmap
    === go_zipped (((f' :| fs') <@>) : fmap (<@>) (go_dupe fs')) ((a' :| as') : go_dupe as')
      -- definition of go_zipped
    === ((f' :| fs') <@> (a' :| as')) : go_zipped (fmap (<@>) (go_dupe fs')) (go_dupe as')
      -- definition of (<@>)
    === (f' a' :| go_zipped fs' as') : go_zipped (fmap (<@>) (go_dupe fs')) (go_dupe as')

  per our assumption,
    go_dupe (go_zipped fs' as') === go_zipped (fmap (<@>) (go_dupe fs')) (go_dupe as')

  we have:
    go_dupe (go_zipped fs as) === go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as)




Thus,
go_dupe (go_zipped fs as) === go_zipped (fmap (<@>) (go_dupe fs)) (go_dupe as)

Thus,

duplicate (f <@> a) === (<@>) <$> duplicate ff <@> duplicate fa


-}