Splitting system calls into two transitions

[YaZko]

We define refinements and equivalences in terms of (bi)simulations built over an LTS induced by the structure itself.
Currently, a Vis e k node, representing a system call, can step by emitting the label obs e x for any x.

This situation has two major drawbacks:

• It allows for equating a little too many programs. Namely, given e : E bool, consider P = (e.(1 | 2)) + (e.(3 | 4)) and Q = (e.(1 | 4)) + (e.(3 | 2)). Both P and Q can take two transitions obs e true and obs e false. For each transition, they can non-deterministically step to ret 1/ret 3 (resp ret2/ret4). Hence P ~ Q. However this is not preserved by interpretation : for h(e) = e.e, we get interp h P not bisimilar to interp h Q.
• It does not allow for distinguishing internal and external stuckness. Namely, if e : E False, then Stuck ~ e

This in progress PR refines the LTS by having two transitions Vis e k -ask e> β_e k -rcv e x> k x.

Major tangential change:

• Changed the way relators and their generalization to external calls are defined. It used to take arbitrary relations on labels, externally constrained in lemmas such as cuts to well-formed ones. Instead, we parameterize the (bi)simulations by value and event relations in the style of rutt, and use their lifting to labels in the definition: this way, they are well-formed by construction.

Minor tangential changes:

• introduced a copy of the stdpp [Inhabited] type class rather than an adhoc notation.
• introduced a [not_stuck] predicate for a slightly cleaner definition of complete simulations.
• a lot of renaming of lemmas and restructuration to try to make things more systematic across relations, hopefully reducing risks of missing some. In turn, I risk to have killed some lemmas proved uniquely to some relations: will need to do a little bit of auditing down the line.

Difficulty to be resolved (in a different PR?):

• bisimulations exploited symmetry arguments provided by the coinduction library that rely on the endofunction to be syntactically defined a certain way. With the new parametrization, this formulation breaks: can we recover the symmetry argument nonetheless?
  Update: It might actually be smooth, was able to reprove sbisim_sym. Need to remind myself down the line how the tactic works once we get to it.

In progress:

• : transition system patched and theory fixed
• : strong simulation
• : complete simulation
• : Strong bisimulation in progress---Generalized [Seq] by parameterizing it by a value relation to be able to state more general monotony statements for sb and sbisim
• : other refinements and equivalences
• : meta-theory