LawfulMonad

Stream: mathlib4

[Reid Barton]

The default definitions of seqLeft and seqRight have changed relative to Lean 3, which makes constructing instances of LawfulApplicative or LawfulMonad nontrivial. I posted a brief analysis at https://github.com/leanprover-community/mathlib4/pull/1178#issuecomment-1364114605

[Reid Barton]

I think we should add some lemmas somewhere that prove the seqLeft_eq and seqRight_eq laws, given sufficient lawfulness hypotheses -- not sure quite how they should look, yet.

[Mario Carneiro]

There is a smart constructor for LawfulMonad in std

[Mario Carneiro]

usage is like:

import Std.Classes.LawfulMonad

instance : LawfulMonad Option := LawfulMonad.mk'
  (id_map := fun x => by cases x <;> rfl)
  (pure_bind := fun x f => rfl)
  (bind_assoc := fun x f g => by cases x <;> rfl)
  (bind_pure_comp := fun f x => by cases x <;> rfl)

and the fields default in the same way as the lean 3 is_lawful_monad