[WIP] Consolidate monad definitions to extlib

[laelath]

Removes the monad definitions in theories/Basics/Basics.v, and adapts all uses of stateT and writerT to instead use the ones defined in the extlib.

TODO:

• update theories/Events/FailFacts.v to use optionT from the extlib.
• update extra/
• update tests/
• update examples/
• update tutorial/

The changes are currently very not-backwards-compatible. I'm not entirely sure if it is possible to make them backwards compatible without copying every single lemma that uses the monads.

Closes #258

[laelath]

I had some trouble updating the proof of print_mults_sat_spec in extra/StateIOTrace.v. Either something is getting unfolded too much by the dependent induction earlier, or the monad change requires an extra proof of Proper for the setoid rewrite.

[Lysxia]

This is very helpful, thanks! I'll take a closer look at the proof you mention tomorrow.

[laelath]

Something about the switch to a record makes controlling unfolding a lot more annoying. I marked interp_state as simpl never as a cludgy fix but it also causes some issues.

[Lysxia]

The root cause of the failure is still mysterious to me but I managed to fix the proof. dependent induction does too much unfolding now. We want to keep interp_state handleIOState folded as long as possible, so I abstract it away with remember then revert the equation into the goal because dependent induction was still trying to use the equation to undo the remember.

[laelath]

when updating the tutorial, there seems to be a somewhat significant decision to make about whether the interp_asm and interp_imp functions should expose the stateT or produce an interface like the current one that returns a function that takes the state like they currently do.

[Lysxia]

I don't think I rely on the stateT abstraction in the tutorial, so try removing it from the result of interp_asm and interp_imp.