Applicative List composition law proof sketch

proof sketch.agda

proof

cmp
  → {A : Set la} {B : Set lb} {C : Set lc}
  → (B → C)
  → (A → B)
  → (A → C)
cmp g f x = g (f x)

  pure a = a ∷ []

  apply
    → {A B : Set lx}
    → List (A → B)
    → List A
    → List B
  apply [] xs = []
  apply (f ∷ fs) xs = append (map f xs) (apply fs xs)

append
  → {A : Set lx}
  → List A
  → List A
  → List A
append [] ys = ys
append (x ∷ xs) ys = x ∷ (append xs ys)

  map
    → {A B : Set lx}
    → (A → B)
    → List A
    → List B
  map f [] = []
  map f (x ∷ xs) = f x ∷ map f xs

  composition
    → {A B C : Set lx}
    → (tg : List (B → C))
    → (tf : List (A → B))
    → (ta : List A)
    → apply (apply (apply (pure cmp) tg) tf) ta ≡ apply tg (apply tf ta)

  composition (g ∷ tg) (f ∷ tf) (a ∷ ta)


apply (apply (apply (pure cmp) (g ∷ tg)) (f ∷ tf)) (a ∷ ta)
 ≡ 
apply (g ∷ tg) (apply (f ∷ tf) (a ∷ ta))


apply (apply (apply (pure cmp) (g ∷ tg)) (f ∷ tf)) (a ∷ ta)
 ≡ 
apply (g ∷ tg) (apply (f ∷ tf) (a ∷ ta))

 ≡ 
append (map g (apply (f ∷ tf) (a ∷ ta))) (apply gs (apply (f ∷ tf) (a ∷ ta)))

-- (apply (f ∷ tf) (a ∷ ta)  ≡  append (map f (a ∷ ta)) (apply tf (a ∷ ta))


 ≡ 
append
  (map g (append (map f (a ∷ ta)) (apply tf (a ∷ ta))))
  (apply gs (append (map f (a ∷ ta)) (apply tf (a ∷ ta))))

-- (map f (a ∷ ta))
--  map f (a ∷ ta) = f a ∷ map f ta

 ≡ 
append
  (map g (append (f a ∷ map f ta) (apply tf (a ∷ ta))))
  (apply gs (append (map f (a ∷ ta)) (apply tf (a ∷ ta))))

-- (append (f a ∷ map f ta) (apply tf (a ∷ ta)))
--   append (x ∷ xs) ys = x ∷ (append xs ys)

-- (f a ∷ append (map f ta) (apply tf (a ∷ ta)))

 ≡ 
append
  (map g (f a ∷ append (map f ta) (apply tf (a ∷ ta))))
  (apply gs (append (map f (a ∷ ta)) (apply tf (a ∷ ta))))

-- (map g (f a ∷ append (map f ta) (apply tf (a ∷ ta))))
--    map f (x ∷ xs) = f x ∷ map f xs
-- (g (f a) ∷ map g (append (map f ta) (apply tf (a ∷ ta))))

 ≡ 
append
  (g (f a) ∷ map g (append (map f ta) (apply tf (a ∷ ta))))
  (apply gs (append (map f (a ∷ ta)) (apply tf (a ∷ ta))))

--  append (x ∷ xs) ys = x ∷ (append xs ys)

 ≡ 
g (f a) ∷
  append
    (map g (append (map f ta) (apply tf (a ∷ ta))))
    (apply gs (append (map f (a ∷ ta)) (apply tf (a ∷ ta))))




-- (apply (pure cmp) (g ∷ tg))  ≡  (apply (cmp ∷ []) (g ∷ tg))
-- (apply (cmp ∷ []) (g ∷ tg))  ≡  (append (map cmp (g ∷ tg)) (apply [] (g ∷ tg)))
-- (append (map cmp (g ∷ tg)) (apply [] (g ∷ tg)))  ≡  (append (map cmp (g ∷ tg)) [])
-- (append (map cmp (g ∷ tg)) [])  ≡  (map cmp (g ∷ tg))


apply (apply (apply (pure cmp) (g ∷ tg)) (f ∷ tf)) (a ∷ ta)
 ≡ 

apply (apply (map cmp (g ∷ tg)) (f ∷ tf)) (a ∷ ta)
 ≡ 


-- (map cmp (g ∷ tg) ≡ (cmp g ∷ map cmp tg)

-- (apply (map cmp (g ∷ tg)) (f ∷ tf))
-- (apply (cmp g ∷ map cmp tg) (f ∷ tf))
-- append
      (map (cmp g) (f ∷ tf))
      (apply (map cmp tg) (f ∷ tf))


apply
  (append
      (map (cmp g) (f ∷ tf))
      (apply (map cmp tg) (f ∷ tf)))
  (a ∷ ta)
 ≡ 


-- (map (cmp g) (f ∷ tf))
--     map f (x ∷ xs) = f x ∷ map f xs
-- (cmp g f ∷ map (cmp g) tf)

apply
  (append
      (cmp g f ∷ map (cmp g) tf)
      (apply (map cmp tg) (f ∷ tf)))
  (a ∷ ta)
 ≡ 

--  (append
--      (g (f x) ∷ map (cmp g) tf)
--      (apply (map cmp tg) (f ∷ tf)))
--    append (x ∷ xs) ys = x ∷ (append xs ys)
-- (g (f x) ∷ append (map (cmp g) tf) (apply (map cmp tg) (f ∷ tf))


apply
  (cmp g f ∷ append (map (cmp g) tf) (apply (map cmp tg) (f ∷ tf))
  (a ∷ ta)
 ≡ 

--   apply (f ∷ fs) xs = append (map f xs) (apply fs xs)

append
  (map (cmp g f) (a ∷ ta))
  (apply
    (append (map (cmp g) tf) (apply (map cmp tg) (f ∷ tf)))
    (a ∷ ta))
 ≡ 
g (f a) ∷
  append
    (map g (append (map f ta) (apply tf (a ∷ ta))))
    (apply gs (append (map f (a ∷ ta)) (apply tf (a ∷ ta))))


-- (map (cmp g f) (a ∷ ta))
--     map f (x ∷ xs) = f x ∷ map f xs
-- (cmp g f a) ∷ map (cmp g f) ta
-- g (f a) ∷ map (cmp g f) ta


append
  (g (f a) ∷ map (cmp g f) ta)
  (apply
    (append (map (cmp g) tf) (apply (map cmp tg) (f ∷ tf)))
    (a ∷ ta))
 ≡ 
g (f a) ∷
  append
    (map g (append (map f ta) (apply tf (a ∷ ta))))
    (apply gs (append (map f (a ∷ ta)) (apply tf (a ∷ ta))))

-- append (g (f a) ∷ map (cmp g f) ta) zs
--   append (x ∷ xs) ys = x ∷ (append xs ys)
-- g (f a) ∷ append (map (cmp g f) ta) zs

g (f a) ∷
  append
    (map (cmp g f) ta)
    (apply
      (append (map (cmp g) tf) (apply (map cmp tg) (f ∷ tf)))
      (a ∷ ta))
 ≡ 
g (f a) ∷
  append
    (map g (append (map f ta) (apply tf (a ∷ ta))))
    (apply gs (append (map f (a ∷ ta)) (apply tf (a ∷ ta))))

-- apply [] xs = []
-- apply (f ∷ fs) xs = append (map f xs) (apply fs xs)


--   map (cmp g f) x ≡ cmp (map g) (map f) x

append (append (map g (map f ta)) (map g (apply tf (a ∷ ta))))


(g (f a) ∷
 append (map g (map f ta))
 (apply
  (append (map (λ f₁ x → g (f₁ x)) tf)
   (apply (map (λ g₁ f₁ x → g₁ (f₁ x)) tg) (f ∷ tf)))
  (a ∷ ta)))
≡
(g (f a) ∷
 append (map g (map f ta))
 (append (map g (apply tf (a ∷ ta)))
  (apply tg (f a ∷ append (map f ta) (apply tf (a ∷ ta))))))


(g (f a) ∷
 append (map g (map f ta))
 (apply
  (append (map (cmp g) tf)
   (apply (map cmp tg) (f ∷ tf)))
  (a ∷ ta)))
≡
(g (f a) ∷
 append (map g (map f ta))
 (append (map g (apply tf (a ∷ ta)))
  (apply tg (f a ∷ append (map f ta) (apply tf (a ∷ ta))))))


(g (f a) ∷
 append (map g (map f ta))
 (apply
  (append
    (map (cmp g) tf)
    (apply (map cmp tg) (f ∷ tf)))
  (a ∷ ta)))
≡
(g (f a) ∷
 append (map g (map f ta))
 (append (map g (apply tf (a ∷ ta)))
  (apply tg (f a ∷ append (map f ta) (apply tf (a ∷ ta))))))