Remove aloop

[Lysxia]

Removes the weirdly typed aloop with a more normal-looking iter + some renaming.

The problem I'm running into is that it breaks strong bisimulations about interp and mrec. I managed to fix them for interp, but now mrec is giving me trouble, in particular with the "unfolding equations" which reexpress mrec as interp (interp_mrec_as_interp, mrec_as_interp). I'm not sure yet how much work that will take.

The best outcome would be to come up with a variant of mrecursive with a few more taus here and there so that these equations hold up to strong bisimulation.

In the current state of things, I made those into weak bisimulations instead to see what happens. It turns out that the HandlerFacts proofs for the properties of iter operation are coinduction proofs, which require those equations to be strong bisimulations (and the extra taus for that would be dealt with in the coinduction proofs themselves).

Some ideas to try to get taus in different places so that strong bisimulations may be easier to establish:

• Make ITree.iter smarter about taus, in particular so that interp trigger : itree E ~> itree E is strongly bisimilar to the identity function. A useful thing for this would be a version of bind which guards the continuation, but without inserting a Tau if its first argument is already a Vis.

• Define ITree.ana : (A -> itreeF E R A) -> A -> itree E R and mrec using it.

[Lysxia]

The proofs in the library are fixed, though they could use some refactoring. AsmOptimizations is the only remaining one to fix otherwise.

In a separate branch (aloop-iter-gbind) I experimented with a Guarded version of bind, but it actually composes quite weirdly (for example there is nothing interesting to rewrite gbind (bind u k) h to).

In HandlerFacts, I'm using a trick where, to prove a bisimulation, I first prove a version where the handlers are transformed to insert an extra Tau, enough to obtain two at the front for an initial guarded step, and then I can use tau_eutt (which is really a euttge) to cut down the other Taus. I had used a similar trick before, but the difference was that I proved strong bismulation before, but now it's directly eutt, and the possibility of using tau_eutt really takes away a lot of headaches.

[Lysxia]

T_T

There seems to be a universe inconsistency blocking test/unit/Unit.v and possibly test/extraction/Extract.v.

And examples/Nimp.v tries to rewrite using eutt under euttG. @YaZko @Grain do you have some idea how to fix that proof.

[Grain]

I fixed the example, you need to use edrop to put it in a specific form (euttG rH rH rH gH) to apply up to (undirected) transitivity.

[Lysxia]

Thanks Paul! So edrop allows you to rewrite with eutt but steps must now be guarded by Vis... that's interesting.

[Lysxia]

Fixed the inconsistency. (2e8d194cb6ac123df6bb029e14265f1f63408792)