Reasoning about monad transformer

Stream: lean4

[Yicheng Qian]

How can I prove that "If m is a valid monad, then (EitherT m e) is a valid monad"?

class QMonad (inst : Monad m) where
  pure_l : ∀ (x : α) (f : α → m β), pure x >>= f = f x
  pure_r : ∀ (x : m α), x >>= pure = x
  bind_assoc : ∀ (ma : m α) (f : α → m β) (g : β → m γ),
      ma >>= (fun x => f x >>= g) = (ma >>= f) >>= g

def EitherT (m : Type _ → Type _) e a := m (a ⊕ e)

instance [H : Monad m] : Monad (EitherT m e) where
  -- pure : a -> m (a ⊕ e)
  pure := H.pure ∘ Sum.inl
  bind ma amb := H.bind ma (fun a =>
      match a with
      | Sum.inl a => amb a
      | Sum.inr e => H.pure (Sum.inr e))

instance [H : Monad m] [Q : QMonad H] :
  QMonad (instMonadEitherT (e:=e) (H:=H)) where
  pure_l := sorry
  pure_r := sorry
  bind_assoc := sorry

[Tomas Skrivan]

There is LawfulMonad class https://github.com/leanprover/lean4/blob/37252e5fa7eff2ce938b7b63f72c0f40cab7e878/src/Init/Control/Lawful.lean#L46 that has these rules.

And for example here is proof of lawfulness of StateT https://github.com/leanprover/lean4/blob/37252e5fa7eff2ce938b7b63f72c0f40cab7e878/src/Init/Control/Lawful.lean#L298

[Yicheng Qian]

Thanks. I'll try to figure it out.

[Yicheng Qian]

There is ExceptT which is essentially EitherT
https://github.com/leanprover/lean4/blob/37252e5fa7eff2ce938b7b63f72c0f40cab7e878/src/Init/Control/Lawful.lean#L101

And the proof of its lawfulness
https://github.com/leanprover/lean4/blob/37252e5fa7eff2ce938b7b63f72c0f40cab7e878/src/Init/Control/Lawful.lean#L163

[Jan-Mirko Otter]

I just tried to prove the first one, pure_l, by just "plugging in the definitions" and using the pure_l rule of the original monad.

I came up with the following behaviour which is kind of surprising for me:

-- same as above, stripped for clarity

instance [H : Monad m] [Q : QMonad H] :
  QMonad (instMonadEitherT (e:=e) (H:=H)) where
  pure_l := by
    intro U V x f
    conv =>
      lhs

      -- Why is this block necessary?
      change H.bind (pure x : EitherT m e U) (fun (a : U ⊕ e) =>
        match a with
          | Sum.inl a => f a
          | Sum.inr e => H.pure (Sum.inr e))

      change (H.pure (Sum.inl x) : EitherT m e U) >>= (fun (a : U ⊕ e) =>
        match a with
          | Sum.inl a => f a
          | Sum.inr e => H.pure (Sum.inr e))

      rw [QMonad.pure_l]
  pure_r := sorry
  bind_assoc := sorry

If instances and notations are involved, I find it very difficult to use unfold or whnf, so I basically have to plug in the defintions manually using change. However, while the proof above works, I do not understand why the first change block is necessary. If I remove it, the argument of the remaining change does not typecheck any more.

Any ideas?

[Yicheng Qian]

I also find it difficult to use rw, apply, unfold, etc. when instances and notations are involved.

I'm not very sure why the first block is necessary, but the three properties can be proved as follows:

instance [H : Monad m] [Q : QMonad H] :
  QMonad (instMonadEitherT (e:=e) (H:=H)) where
  pure_l := fun x f => Q.pure_l _ _
  pure_r := fun x =>
       by simp [bind]
          have : H.bind x pure = x := Q.pure_r _
          rw [←this]
          apply congr
          . rw [Q.pure_r]
          . apply funext; intro x
            cases x <;> rfl
  bind_assoc := fun ma f g =>
       by simp [bind]
          rw [←Q.bind_assoc]
          apply bind_congr; intros a
          cases a with
          | inl => rfl
          | inr => rw [Q.pure_l]

[Yicheng Qian]

I read the proof of the lawfulness of ExceptT at https://github.com/leanprover/lean4/blob/37252e5fa7eff2ce938b7b63f72c0f40cab7e878/src/Init/Control/Lawful.lean#L163, and found that in the proof there is ExceptT.mk and ExceptT.run, which seems to be useful. There also seems to be some tricks which I do not fully understand.

[Tomas Skrivan]

When notation gets confusing, try set_option pp.notation false. It can help to clear things up.

Also stylistic nitpick, the class QMonad should be declared as:

class QMonad (m : Type _ → Type _) [Monad m] where ...

and the instance:

instance {m} [Monad m] [QMonad m] : QMonad (EitherT m e) where

Only in rare cases it makes sense to ask for a class as an explicit argument, like (inst : Monad m).