Proving a simple equality in a code using IO monad

Stream: lean4

[Juneyoung Lee]

Hello all,

How can I prove the following simple statement?

theorem do_pure_bind (a : α) (f : α → IO β) :
  (do let x <- pure a; f x) = f a := by
  (?)

It seems the fact that the IO monad isn't a lawful monad makes the goal slightly more complicated than expected, but I could be wrong.

[Aaron Liu]

It's not possible to prove this I'm surprised I could prove this

theorem do_pure_bind (a : α) (f : α → IO β) :
    (do let x <- pure a; f x) = f a := by
  simp only [Bind.bind, Pure.pure]
  unfold EStateM.pure EStateM.bind
  dsimp

[Johannes Tantow]

import Std.Tactic.Do

set_option mvcgen.warning false

theorem do_pure_bind (a : α) (f : α → IO β) :
  (do let x <- pure a; f x) = f a := by
  mvcgen

If you are willing to use tactics that are under developement.

[Juneyoung Lee]

Thank you all! :)

[Robin Arnez]

import Batteries

theorem do_pure_bind (a : α) (f : α → IO β) :
    (do let x <- pure a; f x) = f a := by
  simp

If you have batteries

[Robin Arnez]

(or mathlib)

[Kyle Miller]

Maybe this is cheating, since it's surely unfolding some implementation details of IO:

theorem do_pure_bind (a : α) (f : α → IO β) :
    (do let x <- pure a; f x) = f a :=
  rfl

[Kyle Miller]

But IO implements LawfulMonad, so do_pure_bind is just pure_bind:

theorem do_pure_bind (a : α) (f : α → IO β) :
    (do let x <- pure a; f x) = f a :=
  pure_bind a f

[Aaron Liu]

you might need some imports

import Batteries.Lean.LawfulMonad

theorem do_pure_bind (a : α) (f : α → IO β) :
    (do let x <- pure a; f x) = f a :=
  pure_bind a f

[Kyle Miller]

I'm doing this with just import Lean, but I'm in a bleeding-edge build (edit: the instance was added in lean4#8995)

[Aaron Liu]

huh

[Aaron Liu]

https://github.com/leanprover/lean4/blob/2104fd7da90ce810ea66949634f68c4cc1a08484/src/Std/Do/WP/IO.lean#L43

[Aaron Liu]

neat

[Eric Wieser]

batteries#416 was where Aaron's instance came from

[Eric Wieser]

Interestingly I was told at the time not to add any instances for IO because it shouldn't be lawful