confusion about do notation

Stream: new members

[Jasper Ganten]

Hello,
I am a little confused why those two definitions are different:

import Mathlib

variable {α : Type}

namespace PMF

-- naive
noncomputable def pureDo (a : α) : (PMF α) := do
  return a

-- this enables the proof to work
noncomputable def pureDo' (a : α) : (PMF α) := PMF.pure a

-- this proof does not work since pureDo
theorem pureDo_eval (a : α) : (pureDo a) a = 1 := by
  rw [pureDo]
  -- Now goal: (Pure.pure a) a = 1 NOT PMF.pure -> but why?
  rw [PMF.pure_apply]
  exact if_pos rfl

-- this proof does work
theorem pureDo_eval' (a : α) : (pureDo' a) a = 1 := by
  rw [pureDo']
  -- Now goal: (PMF.pure a) a = 1 -> correct
  rw [PMF.pure_apply]
  exact if_pos rfl

end PMF

showing their equality since doesnt work aswell. But to my understanding return x in the Monad context is the same as the pure x?
Thanks a lot for the insights!

[Robin Arnez]

return x is not pure x but the special Pure.pure x that's provided by the Pure typeclass that's part of the Monad typeclass. What you need here is simp only [Pure.pure] to unfold this.

[Eric Wieser]

Is docs#PMF.pure not protected? It should be...