simp and do notation

Stream: new members

[Miguel Negrão]

Hi again,

Sometimes after calling simp the result is in do notation. At least for me, this make is it a bit more difficult to visualize what I need to prove. Is there a way to force simp not to display do notation and show me instead >>= and lambdas ?

[Kevin Buzzard]

Can you give a #mwe ?

[Miguel Negrão]

I think the do notation appeared in my goal from a function definition. So let's say what we are trying to prove is in do notation, but during proof, we would like to change into desugared form, to make it easier to see which theorems apply, how would one do that ? A very simple mwe below.

universe u v w
variable {m : Type u → Type v} [Monad m] [LawfulMonad m]
variable {α β γ : Type u}
theorem map_bind2 (x : m α) {g : α → m β} {f : β → γ} :
    f <$> (x >>= g) = (do
      let a <- x
      f <$> g a) := by
  _

unsolved goals
m: Type u → Type v
x: m α
g: α → m β
f: β → γ
⊢ f <$> (x >>= g) = do
  let a ← x
  f <$> g a

[Alex J. Best]

Does

attribute [-delab] Lean.PrettyPrinter.Delaborator.delabDo

do what you want?

[Eric Wieser]

What import does that need, Alex?

[Eric Wieser]

docs4#Lean.PrettyPrinter.Delaborator.delabDo

[Alex J. Best]

I would think nothing?

[Eric Wieser]

It doesn't work for me without import Lean.PrettyPrinter.Delaborator.Builtins

[Alex J. Best]

Hmm interesting, not sure I understand how that works to be honest

[Eric Wieser]

I think it's because it's builtin

[Miguel Negrão]

Alex J. Best disse:

Does

attribute [-delab] Lean.PrettyPrinter.Delaborator.delabDo

do what you want?

Yup, that does the trick !!! Great ! Indeed l report the same as @Eric Wieser , I need that import to make it work. Thanks all !

[Eric Wieser]

FWIW, I was able to prove your lemma with simp only [map_eq_pure_bind, bind_assoc]

[Miguel Negrão]

Thanks, but my example is from mathlib4. Just needed something to illustrate the point. :-)

theorem map_bind (x : m α) {g : α → m β} {f : β → γ} :
    f <$> (x >>= g) = x >>= fun a => f <$> g a := by
  rw [← bind_pure_comp, bind_assoc] <;> simp [bind_pure_comp]