How to unfold/rewrite `bind` as a `X.bind` from a monad?

Stream: new members

[Edward Zhang]

Hi! I am writing some exercises for Monad. I dont know how to unfold bind just like ReaderOption.bind It is polymorphic and will turn to Monad.toBind.1.

def ReaderOption (ρ : Type) (α : Type) : Type := ρ → Option α
-- Monad function with option return
def readOption : ReaderOption ρ ρ := fun env => some env
def ReaderOption.pure (x : α) : ReaderOption ρ α := fun _ => some x
def ReaderOption.bind (result : ReaderOption ρ α) (next : α → ReaderOption ρ β) : ReaderOption ρ β :=
  fun env => match result env with
    | none => none
    | some x => next x env
instance : Monad (ReaderOption ρ) where
  pure := ReaderOption.pure
  bind := ReaderOption.bind

theorem leftIdentityReaderOption (x : α) (f : α → ReaderOption ρ β) : bind (pure x) f = f x := by rfl
theorem rightIdentityReaderOption' (m : ReaderOption ρ α) : ReaderOption.bind m ReaderOption.pure = m := by
  funext env
  unfold ReaderOption.pure
  unfold ReaderOption.bind
  cases m env with
  | none => simp
  | some y => simp
theorem rightIdentityReaderOption (m : ReaderOption ρ α) : bind m pure = m := by
  -- `Monad.toBind.1` appears
  unfold bind
  funext env
  cases m env with
  | none => sorry
  | some x => sorry

[Edward Zhang]

As with the example code, I can prove the first rightIdentityReaderOption' but sorry not the second. For some basic Monad instances, it is easy to prove by rfl directly, but this time it doesn't work :( I prefer to write without X. prefix (use bind/pure directly) . Could anyone help me? How to provide extra information to make bind open as X.bind.

[Edward Zhang]

Can you give me some advice?