More invariants

[MarkusKL]

Improvements made by this PR:

• Introduces rel_app as a general relation invariant over any number of sided locations. Closes Generalize relations between locations in the invariant. #71
• Re-defines existing semi-invariants: couple_lhs, coupls_rhs, triple_rhs.
• Trivially adds more automation-enabled semi-invariants: single_lhs, single_rhs, triple_lhs, couple_cross`.
• Handle cases in ssprove_invariant when locations in a relation have not been put and/or remembered.
• Strict simplification of proofs for affected examples.
• Less lines of code overall :)

TODO:

• Write issue description.
• Consolidate side and lhs definitions.
• Add invariant variations.
• Rename some of the new definitions (rel-).
• Update documentation.

[MarkusKL]

This is ready for review. I will have another look at the failing builds. I am using 8.19 locally, so it is strange that it fails in the pipeline.

[spitters]

Thanks! These are nice simplifications.
Feel free to merge once CI is happy.

[4ever2]

I will have another look at the failing builds. I am using 8.19 locally, so it is strange that it fails in the pipeline.

I think that it is the math-comp version causing problems.

It might also be time to stop supporting Coq 8.18-8.19 and some older math-comp versions.
@spitters @MarkusKL any thoughts on this?

[spitters]

Yes, I think it's fine to drop support for them. I guess it will break the jasmin part, which was broken already.
It would be nice to keep Hax working. I forgot the precise dependencies for that.

[4ever2]

We already have a branch of Hax that works with Rocq 9.0.

[spitters]

Feel free to drop the other versions then, if it simplifies things...

[MarkusKL]

I made an ugly fix that maybe applies a rewrite rule, so that it both works with the flake (that I am using locally) and the pipeline.
@4ever2 Dropping versions would not fix the issues for me I think. I would rather like if we could figure out how to synchronize the pipeline and the flake setup once and for all.

[MarkusKL]

Build succeeded. It may be better to use something like nix-shell --argstr bundle "8.20" when developing SSProve instead of the flake. This invokes the coq-toolbox directly and most packages are cached (unlike 8.19). However, this discussion should probably be taken elsewhere.

[4ever2]

@MarkusKL The comment about versions was just a general comment and not related to this issue.
I dropped support for 8.18 and prepared a PR for 8.19. I won't merge it yet, as you are still using the 8.19 flake.
I agree that we need to find a better solution with the Nix flake.

The changes look good to me, so let's merge.