paco => rocq-coinduction

[rudynicolop]

Description

Replaces coq-paco with rocq-coinduction. This draft PR anticipates this dependency change in the ITree library: PR 285. These changes are largely internal to the proof development, not exposed on the OCaml side. These changes /are visible/ to users of the Jasmin Rocq codebase. These changes largely only affect proofs by coinduction.

Zulip discussions:

• ITree channel
• Jasmin channel

Dependency changes:

• coq-paco replaced by rocq-coinduction version >= 1.21
• Only tested so far on rocq-core version 9.1.1 (but should still be compatible with versions 9.0 and 9.2 I hope)

Changes

Moving to rocq-coinduction largely affects the definition and use of coinductive relations/predicates:

• To define a coinductive relation/predicate, one must provide a mon definition for the monotonic endofunctor, then take the greatest fixpoint gfp on that mon definition (xrutt is now defined this way).
• For starting coinduction proofs, no choice between pcofix, gcofix, nor ecofix. Now there is only coinduction.
• Bind laws, especially within coinduction proofs no longer rely upon "clo" patterns/infrastructure. Instead, lemmas of the form of eqit_bind_chain must be used.
• punfold H is larged replaced with step in H
• Simplification with simpl is too aggressive on the new definitions, unfolding coinductive defintions and exposing observe and pattern matching, preventing use of Proper instances for rewriting. For various coinductive relations, there's often a custom "cbn" tactic to avoid this issue. There's icbn, bcbn for eqit, rcbn for rutt and xrcbn for xrutt.
• In coinductive proofs, there is no need to "choose" left or right branches of a "paco" goal, nor is there an analogue to "clearing constraints" with pclearbot, resulting in some simpler proofs.
• The ITree library now has generalized tactics for coinductive eqit goals, especially new eret, etau, evis, and ebind tactics which are for any eqit-based goal, not just eutt.

Some definitions/notations of rocq-coinduction clash with standard library names, such as id, const, leq, and "=<".

There were some collisions with the new rocq-coinduction-based definitions and ssreflect tactics, some of which may be due to version issues on my mind:

• Introducing with > is too aggressive on some coinductive goals, exposing the underlying "tower" definition. Instead using * seems to work.
• Some instances of chains of apply/H1/H2/... or exact/H1 failed. This may be a rocq-core version issue, or some other dependency issue.

Checklist

• Add a changelog entry in changes if the PR is a user-visible change
• Add one or several tests to compiler/tests if it makes sense, especially if it is a bug fix
• Update the documentation if needed

Draft Notes

Until ITree PR 285 is merged and there's a new ITree release, this will remain a draft:

• The coq-itree dependency is only temporarily pinned to the PR source branch or my fork of the PR branch.