Manually prove left identity `pure` of Monad Option

Stream: new members

[Edward Zhang]

Hi! I'm new to functional programming and just do some practice. Given the Monad contract that pure should always be left/right identity of bind and the associativity. I try to manually prove them with instances of Monad Id' Monad Option and Monad Result. And I dont know how to unfold the polymorphic functionpure/bind as I wish (or maybe I use the wrong tactic). E.g.

instance : Monad Option where
  pure x := some x
  bind opt f := match opt with
    | none => none
    | some x => f x

theorem left_identity_pure_for_option (x : α) (f: α → Option β) : bind (pure x) f = f x := by
  rw [Option.pure_def]
  unfold bind
  -- ⊢ Monad.toBind.1 (some x) f = f x
  sorry

I hope the goal after unfold step to be -- ⊢ f x = f x (just use the bind under Monad Option).

[Daniel Weber]

(deleted)

[Daniel Weber]

This is true by rfl

[Daniel Weber]

If you're using Mathlib you can also use unfold_projs to unfold it

[Edward Zhang]

Daniel Weber said:

This is true by rfl

Yep. I know it’s true to solve the goal directly by rfl. Just want to move step by step like manually proof on paper. So I wonder can I use other tactics ( not strong enough to solve immediately)