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?

[rudynicolop]

Can we delete this section?

[Lysxia]

Sure!

[rudynicolop]

I may have spoken too soon 😅. I have some proposed helper lemmas for ITree.bind and rutt reasoning in coinduction proofs here: rogerburtonpatel#2

Admittedly, my proposed changes to Eq/Rutt.v may not be the most efficient.

This relates to the zulip discussion here: https://rocq-prover.zulipchat.com/#narrow/channel/394939-Interaction-Trees/topic/coinduction.20plugin/near/608963250

[YaZko]

What "efficiency" issue do you have in mind? From a quick glance that looks reasonable, Thanks for the contribution!

[rudynicolop]

I wasn't sure if/how there was a way to move the parameters for rutt_ and rutt_mon without breaking up the RuttF section?

[YaZko]

Ah I see I didn't notice this issue, indeed that forces the swap between the quantification on REv/RAns and R1/R2. That being said I would rather say that this swap is welcome and should be propagated to rutt rather than swap the order between ruttF and rutt as you did.

[rudynicolop]

If the parameter order for rutt is swapped could this complicate the signature for some of the Proper instances, such as rutt_Proper_R: https://rocq-prover.zulipchat.com/#narrow/channel/394939-Interaction-Trees/topic/coinduction.20plugin/near/609032183

(My apologies, I may be misunderstanding something, just double-checking).

[YaZko]

Ah I'm actually understanding the problem you were pointing at only now, that's indeed a bit annoying. Presumably you could simply split that into two lemmas, one Proper (eq_REv ==> eq_RAns ==> eq ==> eq ==> eq ==> eq ==> eq ==> iff) .. and then one Proper (@eq_rel R1 R2 ==> ....) (@rutt E1 E2 REv RAns R1 R2)?