State facts

[Zdancewic]

This pull request completes some of the missing proofs in MorphismsFacts.v that have to do with interp_state. It also adds a Proper morphism declaration for interp_state to enable rewriting.

[Zdancewic]

I just checked in some more work on some examples with reasoning about the state monad. (See the experiments/Reasoning.v file.)

• It might be a bit cleaner if functions like interp_state didn't introduce a Tau node for Vis constructors that they don't handle. The way things are now, nesting monads introduces extra Taus when the unhandled visible even propagates through the interpreter.

• I tried for a while to get some automation to work with the `(embed e) way of lifting subeffects, but the embedding tags got in the way of convenient pattern matching.

• At the top of Reasoning.v I define a class of MonadTransformers and show that works with stateT. I also liked using ExtLib's MonadState class, which can clean up examples a bit.

• For the "state2E" examples of using two state monads simultaneously, I haven't yet shown that the events from different instances commute: x <- get1 ;; y <- get2 ;; k x y ~~ y <- get2 ;; x <- get1 ;; k x y, etc.

-- The runboth lemmas were mostly boilerplate. It would be good to think about how to abstract over these: lemmas that combine two separate run functions and show that their operations commute generically, as well as "lifting" properties (such as get_law) from one monad's interpretation into an interpeter combined with another.

[Lysxia]

It might be a bit cleaner if functions like interp_state didn't introduce a Tau node for Vis constructors that they don't handle. The way things are now, nesting monads introduces extra Taus when the unhandled visible even propagates through the interpreter.

interp1_state has a notion of "unhandled" events for which it avoids the extra Tau.

[Zdancewic]

Good point about interp1! I modified the examples to use that instead. (Along the way, I added Proper inter1_state and accompanying lemmas). It seems to me that we probably want to use the "interp1" version of interpreters whenever we can.