[Iris-Club] Generalized bind rule

[Ralf Jung]

Hi all,

I had some really nice idea today :) . I showed that we can have a
generalized bind rule as follows

{P} e {v. Q}    \All v. {Q} ctx v {v'. R}
-----------------------------------------
           {P} ctx e {v'. R}

for any function `ctx` satisfying some axioms:

>       Definition IsCtx (ctx: expr -> expr): Prop :=
>         (forall e, is_value (ctx e) -> is_value e) /\
>         (forall e1 σ1 e2 σ2 ef, prim_step (e1, σ1) (e2, σ2) ef -> prim_step (ctx e1, σ1) (ctx e2, σ2) ef) /\
>         (forall e1 σ1 e2 σ2 ef, ~is_value e1 -> prim_step (ctx e1, σ1) (e2, σ2) ef ->
>                                 exists e2', e2 = ctx e2' /\ prim_step (e1, σ1) (e2', σ2) ef).

See <https://gitlab.mpi-sws.org/FP/iris-coq/issues/2#note_14587> for my
ramblings as I went on and implemented this in Coq.

In particular, this means that languages that do have evaluation
contexts don't even need to go into the model to prove their bind rule:
"fill K" for any evaluation context K satisfies above axioms. That's
proven in ectx_lang.v. Robbert, I assume a language with sequential
composition or other C/Java-like languages could use that general rule
above directly to obtain the sequential composition rule.

So, now Iris still has all the proof rules it used to have, but without
talking about evaluation contexts anywhere, significantly simplifying
the language interface. The user can control what fork does, and fork
can have an effect on the state. And the interface for languages that
like to provide evaluation contexts actually got much simpler. Yay :D

Kind regards,
Ralf