Using the rocq-coinduction library

[rogerburtonpatel]

PR to pull the port of ITrees from paco to enhanced coinduction.

Of note, the ITreePredicatesExamples.v file needs to be rewritten.

[YaZko]

Thanks Roger!

@Lysxia : This PR by @rogerburtonpatel should superseed both partial starts at substituting paco for Damien Pous's library.

It will need significant reviewing, cleaning, and discussion as to whether it should eventually lead to a new main release for the library, or as a parallel branch for now.

At a very rough grain, the changes can be abstracted as:

• the classes for complete lattices and monotone functions are structured a bit differently from paco's
• we naturally now use the gfp construct, see for instance eqit and hence the coinduction tactic that comes with it
• some care must be taken to properly unfold and fold definitions of gfp. The perfect balance for this is still slightly in flux, Roger has coded some convenient and convincing tactics to work around it.
• up-to are overall nicer. There is no need for the old transitive closure and wiggling around it, we straightforwardly prove universal properties of the chain
• related, we push the quantification over return types and relations under the fixpoint to strengthen the up-to bind
• euttG is currently unplugged. This removes the layer of abstraction it provided, arguably because things are now clean enough to not need it. It however also removes the ability to rewrite eutt equations in a weak bisimulation proof provided we store no information guarded by Taus. This was very rarely used, and required a lot of machinery: if we want to recover it, I suggest fitting it in Biernarki's diacritical framework rather than trying to rebuild euttG.

[rudynicolop]

Thanks @rogerburtonpatel!

I opened a PR to change the dependency (e.g. in dune-project) from coq-paco to rocq-coinduction. (Forgive me I wasn't sure how to suggest this change more directly 😅).

I wasn't sure whether coq-paco is still used or if it makes sense for the deps to be changed this way so feel free to ignore ofc if my suggested change doesn't make sense.

[rudynicolop]

Should mentions of coq-paco be replaced with rocq-coinduction?