Basic theory of rutt

[lephe]

This PR expands the theory of rutt by basically following eqit.

Context: While working on proving abstract semantics correct with Yannick, I figured we needed equality for ITrees with different (concrete and abstract) event types, and landed on a design that turned out to be equivalent to rutt. Since there was no theory for it at the time I expanded it to match eqit.

None of this is particularly exciting; it's just required for convenient work with rutt. Maybe one property that stands out is compatibility with eutt, which is a fairly intricate coinductive proof involving two concurrent inductions on ruttF and euttF (and at one point three).

Changes:

• theories/Eq/Eqit.v:
  • Helper tactic fold_eqitF that applies fold_eqitF more consistently by eta-expanding arguments that don't have the expected syntactic structure.
  • Extra inversion lemmas eutt_inv_Ret_l and eutt_inv_Ret_r, used later to prove compatibility of rutt with eutt. These couldn't go under eutt_inv_Ret because some required congruences aren't yet available.
• theories/Eq/Rutt.v:
  • Inversion lemmas for ruttF: ruttF_inv_VisF_r, ruttF_inv_VisF (with dependent destruction, that's the best I can do).
  • unfold_rutt tactic, fold_ruttF lemma and tactic.
  • Remaining construction and inversion lemmas for rutt: rutt_Ret, rutt_inv_Ret, rutt_inv_Ret_l, rutt_inv_Ret_r, rutt_Vis, rutt_inv_Vis, rutt_inv_Vis_l, rutt_inv_Vis_r.
  • Specialized up-to principles for eq_itree and euttge, which typeclasses eauto cannot infer from the general versions.
• theories/Eq/RuttFacts.v (new file):
  • Higher-level construction lemmas: just rutt_trigger.
  • Morphisms for quantified equality over REv and RAns.
  • Morphisms for flipping REv and RAns, ending with rutt_flip (closest thing to symmetry we have).
  • Proper instances culminating in an eutt compatibility lemma. The most general rewrite available is:
  • Rewrite REv for eq_REv, RAns for eq_RAns and RR for eq_rel.
  • Rewrite t1 and t2 for eutt.
  • Outline for the up-to closure for bind.
  • Bind lemma rutt_bind.

Unfinished wishlist:

• Properly finish the bind closure
• Have bind inversion lemmas

I tried to imitate the code style; let me know if anything needs fixing.

Tested with Coq 8.15.2.

[Lysxia]

Thanks @lephe This looks good!

I will make a release shortly before Christmas. Are the bind lemmas on your wishlist something you were planning to look at soon?

@YaZko Does Damien Pous's library have something equivalent to what paco provides for bind closure?

[lephe]

Cool! I'm afraid I won't have time to come back to this in the near future. I PR'd it because Yannick mentioned it would be useful in Vellvm soonish. Are the bind lemmas required for the next version of the library?

[Lysxia]

Not at all! I only asked to know whether to expect more PRs on top of this in the near future. No pressure if not!

[YaZko]

@YaZko Does Damien Pous's library have something equivalent to what paco provides for bind closure?

Well I would argue that paco does not provide much: nothing in the vanilla version, and with the gpaco version the valid up-to principles are derived by proving that they are below a "main" closure proved to be weakly compatible.

So specifically in itrees, we define the closure and prove that it is below eqitC here: https://github.com/DeepSpec/InteractionTrees/blob/master/theories/Eq/Eqit.v#L1100 .

I would argue that the companion provides significantly better support: there is no need for picking this weird "larger" closure that eqitC incarnates, valid principles are principles below the companion, which in particular contain all compatible functions.

So specifically in ctrees, I defined a generic up-to bind function bind_ctx here: https://github.com/vellvm/ctrees/blob/master/theories/Eq/Equ.v#L545. And it is specialized to the various relations we are interested in, for instance coinductive equality (the same as eq_itree essentially) a little lower in this same file: bind_ctx_equ for the definition and bind_ctx_equ_t for the proof of validity.

[lephe]

Not at all! I only asked to know whether to expect more PRs on top of this in the near future. No pressure if not!

Right, I see. I still have ~350 lines of lemmas like inversion principles for iter, a non-trivial theorem that x ∈ interp h t → x ∈ t, and misc stuff. I can try and PR that too for the next version if that's of interest to you.

[Lysxia]

If that's not too much trouble for you, that would be lovely!