make bind into notation

[Zdancewic]

Remove the definition of bind from ITree.v and replace it with notation. This simplifies certain rewriting proofs since there's no longer a distinction between bind and bind'.

[gmalecha]

What if you just make everyone use bind? You could even write the cofix inline if you want to remove the definition of bind' entirely.

[Lysxia]

Steve and I were discussing about this this morning. The issue comes up when doing proofs by simplification, you want to prove some equation eq_itree eq (bind t k) u, so one way is to start is to rewrite itree_eta; cbn. to simplify, but then the bind goes away and you have bind' instead, that you need to refold if all the lemmas talk about bind.

[gmalecha]

Ok. I think the thing to note with this change is it will make it even harder to integrate with any typeclass libraries for monads (ext-lib or otherwise). Alternatives would be to opt for something like rewrite_strat.

[gmalecha]

I guess this is one instance where rewrite-based simplification is more principled than reduction-based simplification.

[Zdancewic]

@gmalecha -- why will this make it harder to integrate with typeclass libraries for monads? Won't those be defined purely in terms of the (generic) monad bind?

[gmalecha]

They will be, but aren't you removing bind as a definition and replacing it with a notation?

[Lysxia]

I think that the breakage to integrate with a general monad interface would be significant either way, and the main difference with this change is that you would need to write bind := fun _ _ t k => ITree.bind t k instead of bind := ITree.bind, but otherwise I don't expect the proofs to really be affected. If there's no objection to that, let's fix and merge this PR.

[Zdancewic]

I'm ok with that. (Though maybe this is less pressing now that we are trying to avoid using cbn for proofs like the one in factorial_correct?)

[Lysxia]

Gil's PR is adding bind_fold again because of bind currently being a definition, and itree_eta+cbn might still be a tempting combination for various unforeseen reasons.

[Zdancewic]

OK -- it seems like it doesn't hurt that much to make this change, and it should improve some proofs. Let's go ahead and merge it.