Proving that applicative functors compose

Question

For simplicity, here an applicative functor means (in a proof assistant based on dependent type theory) the Haskellian applicative functor, bundled with its equational laws.

This I can of course brute force in any proof assistant. Nevertheless, streamlining such a proof is an interesting challenge. The definition for pure and <*> is easy, as can be copied off any Haskell library. The equational reasoning however is very very tedious, which anyone would agree if they were to write it down on paper.

One thing to note is that you can mechanically prove all four laws by deciding on a set of appropriate rewriting directions, and apply laws whenever you can. I would like to know how this is actually carried out in a tactic-based approach, and also whether this strategy can be used in non-tactic based proofs. And if unfortunately not, what other techniques can be used to reduce the tedium?

Answer 1

I would like to know how this is actually carried out in a tactic-based approach

The theorem functor.comp.is_lawful_applicative in Lean's mathlib library is what you are looking for:

@[protected, instance]
def functor.comp.is_lawful_applicative
  {F : Type u → Type w} {G : Type v → Type u}
  [applicative F] [applicative G]
  [is_lawful_applicative F] [is_lawful_applicative G] :
is_lawful_applicative (functor.comp F G)

I think the proof basically follows the brute force approah you had in mind, but here are a few comments:

• The mathlib control library is very systematic, proving results for functors, applicative functors, monads, etc (both the lawful and non-lawful versions). This breaks up the work and likely helps to keep track of everything.
• The mathlib definition of a lawful applicative functor is a class (a structure which can be used as a type class):

  class is_lawful_applicative (f : Type u → Type v) [applicative f] extends is_lawful_functor f : Prop :=
  (seq_left_eq  : ∀ {α β : Type u} (a : f α) (b : f β), a <* b = const β <$> a <*> b . control_laws_tac)
  (seq_right_eq : ∀ {α β : Type u} (a : f α) (b : f β), a *> b = const α id <$> a <*> b . control_laws_tac)
  -- applicative laws
  (pure_seq_eq_map : ∀ {α β : Type u} (g : α → β) (x : f α), pure g <*> x = g <$> x)
  (map_pure        : ∀ {α β : Type u} (g : α → β) (x : α), g <$> (pure x : f α) = pure (g x))
  (seq_pure        : ∀ {α β : Type u} (g : f (α → β)) (x : α), g <*> pure x = (λ g : α → β, g x) <$> g)
  (seq_assoc       : ∀ {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)), h <*> (g <*> x) = (@comp α β γ <$> h) <*> g <*> x)
  -- default functor law
  (comp_map := begin intros; simp [(pure_seq_eq_map _ _).symm, seq_assoc, map_pure, seq_pure] end)
  

• I think the control library is one of the major successes of Lean's type class system. Many facts about instances of say applicative functors (such as that the composition of two lawful applicative functors like option and list are still lawful) is automatically derived by the type class system.
• Further, Lean provides some automation to make it easier to show that an applicative functor is lawful. For example, the first two fields seq_left_eq and seq_right_eq are automatically derived by default using the tactic control_laws_tac which is just a follow-your-nose sequence of steps: whnf_target >> intros >> to_expr ``(rfl) >>= exact.
• The proof of functor.comp.is_lawful_applicative is based on a number of lemmas. The lemma proof are short, often mostly relying on the simp tactic and various rewrite lemmas. Some of these rewrite rules are annotated with the label functor_norm so one can just do, e.g. simp [applicative.pure_seq_eq_map'] with functor_norm to apply them during simplification.
• mathlib has a separate category theory library which redefines the same objects, like functor and monad, but in the usual category theoretic manner (which is more useful for doing mathematics). For that library, I heard they developed the tidy tactic to do a lot of the tedious follow-your-nose sort of reasoning. (The tidy tactic tries a bunch of common tactics, like intros and simp, in sequence until one of them works. It then applies it and repeat the process, without ever backtracking.)