Zulip Chat Archive

Stream: new members

Topic: Proof about monadic functions


view this post on Zulip Jannis Limperg (Jun 25 2020 at 11:42):

I'm struggling a little with a proof that two monadic functions are equal. I'll post the full proof for critique when it's done, but for now I just need this lemma:

import tactic

lemma bind_const {α β m} [monad m] [is_lawful_monad m] (ma : m α) (mb : m β) :
  (ma >>= λ _, mb) = mb := by library_search -- fails :(

view this post on Zulip Reid Barton (Jun 25 2020 at 11:45):

Isn't this false though?

view this post on Zulip Reid Barton (Jun 25 2020 at 11:47):

for example, [] >>= (\lam _, [1]) = []

view this post on Zulip Jannis Limperg (Jun 25 2020 at 11:50):

Meh, you're right. Back to the drawing board.


Last updated: May 15 2021 at 02:11 UTC