Move `MonadTheory` into ext-lib

[Lysxia]

A necessary and sufficient condition is to solve coq-ext-lib/coq-ext-lib#31

[Lysxia]

ext-lib seems to be using PERs which makes things complicated.

[gmalecha]

What needs to happen with ExtLib? Do we need to drop the PERs?

[Lysxia]

I think unbundling equals and proper to start with might allow things to remain compatible with both PERs and ERs.

[Lysxia]

Actually, what I would want out of a monad library looks more and more like what is in math-classes.

• ret and bind should be singleton classes instead of a record, because they don't simplify immediately by cbn. We can still expect them to simplify in the right context, which rules out the following alternatives:

  • Arguments Monad_itree : simpl never. because it entirely blocks cbn. Alsounfold Monad_itree doesn't help in situations where Monad_itree does not even appear in the context. (to remember a concrete example, when I tried this approach, I could not use our tau_steps tactic to unfold the factorial 5 itree in tutorial/Introduction.v)
  • Opaque Monad_itree, because then you have to tell people to set Transparent Monad_itree, and that's not going to scale if you have to do something similar for every library

• Monads are equipped with a relation transformer (eutt : relation A -> relation (itree E A)), but I would like to keep our heterogeneous generalization eutt : forall A B, (A -> B -> Prop) -> (itree E A -> itree E B -> Prop) which does not appear in math-classes. We use it to rewrite under iter, and sometimes it's natural to want to relate computations with different return types (like in our compiler theorem).