Prove commutation of monads (categorical systems theory)

Stream: mathlib4

[André Muricy Santos]

Hi all, I'm kind of stuck in proving a basic fact about commutative monads. I'm following David Jaz Myers' categorical systems theory book and there, in definition 2.1.0.5, he defined a commutative monad. Since Lean4 is a dependent language, it should accomodate proofs about computation straightforwardly.

Here's my definition of a commutative monad, I'm just following what's in the book:

---- Auxiliary definitions ----
def η [Monad m] {A : Type} (a : A) : m A := pure a
def μ [Monad m] {A : Type} (a : m (m A)) : m A := a >>= id
notation "⟨" f:80 "×" g:80 "⟩" => Prod.map f g

def myswap : a × b × c → (a × b) × c := λ ⟨a, b, c⟩ => ⟨⟨a, b⟩, c⟩
def myunswap : (a × b) × c → a × b × c := λ ⟨⟨a, b⟩, c⟩ => ⟨a, b, c⟩
-------------------------------

class CommutativeMonad (m : Type → Type) extends Monad m where
  -- A morphism from a pair of "monadic values" into a monadic pair of values
  σ : m a × m b → m (a × b)
  -- Such that performing it on a `pure`'d Unit on the right and then taking the
  -- projection is the same as just performing the action on the left
  comm_l : let arr : m a × Unit → m a := Functor.map Prod.fst ∘ σ ∘ ⟨id × η⟩
           arr = Prod.fst
  -- The same for the left
  comm_r : let arr : Unit × m a → m a := Functor.map (f := m) Prod.snd ∘ σ ∘ ⟨η (m := m) × id⟩
           arr = Prod.snd
  -- And rearranging two of three paired monadic arguments does not affect
  -- the result
  assoc : let arrleft : m a × m b × m c → m (a × b × c) := σ ∘ ⟨id × σ⟩
          let arrright : m a × m b × m c → m (a × b × c) := Functor.map myunswap ∘ σ ∘ ⟨σ × id⟩ ∘ myswap
          arrleft = arrright
  -- and `pure`-ing a pair is the same as `pure`-ing each element then performing it
  relift : let arr : a × b → m (a × b) := σ ∘ ⟨η × η⟩
          arr = η
  -- and finally that performing it twice on a pair of nested monadic values
  -- then `join`-ing is the same as `join`-ing such a pair and then performing it
  rejoin : let arrleft : m (m a) × m (m b) → m (a × b) := μ ∘ Functor.map σ ∘ σ
           let arrright : m (m a) × m (m b) → m (a × b) := σ ∘ ⟨μ × μ⟩
           arrleft = arrright

Then what I want to do is just prove that actually executing these monadic actions out of order doesn't matter. Expressing this in code is super straightforward:

def f (m : Type → Type) (a : Type) (b : Type ): [CommutativeMonad m] → m a → m b → m (a × b) :=
  λ ma mb ↦ do
    let a ← ma
    let b ← mb
    return (a, b)

def g (m : Type → Type) (a : Type) (b : Type ) : [CommutativeMonad m] → m a → m b → m (a × b) :=
  λ ma mb ↦ do
    let b ← mb
    let a ← ma
    return (a, b)

theorem do_notation_equal [inst : CommutativeMonad m] : ∀ x y, f m x y = g m x y:= by
  sorry

But then already I have a bunch of questions:

1. Why is giving m explicitly needed?
2. Where do I go from here? I need to somehow convolve the left hand side of the equation into the right side, but I don't know what do notation in Lean is doing behind the scenes, so I don't even know what to apply and in what order.

[Somo S.]

1. If you re-define things in the manner shown in the code below, you actually do not (technically) have to provide m explicitly. The type inferencing for lean would otherwise need a bit more help for example by specifying the named argument (m:=m) (assuming the corresponding parameter is implicit).
2. I have provided exactly what the do notation is definitionally equal to below. Hope that helps.
   As for the rest of the proof, my guess is that if it makes sense to assume the monad is Lawful then I'd use propositions from the LawfulMonad class (and/or definition of bind/pure) and somehow get to the conclusion. Otherwise you have to somehow coax it out of the properties of CommutativeMonad. Due to my unfamilarity with the general subject, i'm not sure how that might be done say on paper, so i'm having trouble imagining how to do it via Lean as well.

/- ---- Re-define things like: ----- -/

def f' [CommutativeMonad m] (ma : m A) (mb : m B) : m (A × B) := do
  let a ← ma
  let b ← mb
  return (a, b)

def g' [CommutativeMonad m] (ma : m A) (mb : m B) : m (A × B) := do
  let b ← mb
  let a ← ma
  return (a, b)

theorem do_notation_equal' [CommutativeMonad m] {ma : m A} {mb : m B} : f' ma mb = g' ma mb := by
  unfold f'
  unfold g'

  change -- this line is redundunt but explains exactly what the `do` notation is doing
    (bind ma fun a => bind mb fun b => pure (a, b))
      =
    (bind mb fun b => bind ma fun a => pure (a, b))

  -- change (ma >>= λa ↦ mb >>= λ b ↦ pure (a, b)) = (mb >>= λb ↦ ma >>= λ a ↦ pure (a, b))

  sorry -- TODO

/- ---- Which is equivalent to: ----- -/

def f (m : Type → Type) (a : Type) (b : Type ): [CommutativeMonad m] → m a → m b → m (a × b) := -- f'
  λ ma mb ↦ do
    let a ← ma
    let b ← mb
    return (a, b)

def g (m : Type → Type) (a : Type) (b : Type ) : [CommutativeMonad m] → m a → m b → m (a × b) := -- g'
  λ ma mb ↦ do
    let b ← mb
    let a ← ma
    return (a, b)

theorem do_notation_equal [inst : CommutativeMonad m] : ∀ x y, f m x y = g m x y:= by
  intros ; ext ; apply @do_notation_equal'

example [CommutativeMonad m] : f m a b = f' := rfl
example [CommutativeMonad m] : g m a b = g' := rfl

[Adam Topaz]

It’s worth noting that we already have docs#CommApplicative