a simpler corres method

[lsf37]

This new corres method is similar to the corresK method and calculus, but much less ambitious. Its main purpose is to automate boilerplate proof steps in corres proofs and is specifically not trying to fully automate such proofs (although some few might be solved).

The idea is that the method will make some progress with obvious steps and leave over a proof state the user can operate on further.

I've tried to put in a lot of comments to document the design and some of the rationale, but there are no examples yet.

Implements #634 (see there for parts of the design discussion)

This is on top of #653, which renames the old Corres_Method to CorresK_Method

[lsf37]

I might try to replace some of the existing corresKsimp invocations and maybe add a file with examples. Depending on how fast that goes, this would either be a separate PR or another commit or two on top of this one.

[lsf37]

Have now deployed the method in a few places in RISCV64 Refine and fine tuned thing a bit from that experience.

Seems to be working relatively well, at least I was able to develop with it incrementally fairly nicely and then collapse things down. The real test will be if it works for others as well.

[Xaphiosis]

I'm impressed you did this only with Eisbach. I'd have gone down rabbit holes of examining terms for schematics, which would result in faster code, but definitely less comprehensible. The documentation is solid as well.

There was one thing I didn't comment on directly because I'm used to it, but not sure if it's confusing to others or not: inline etc in the docs, e.g. "rules such as moving asserts to guards etc when the user" can be a tad confusing.

[michaelmcinerney]

Looks very cool. I'm sure I don't understand many of the subtleties of the method setup, but corressimp is used a fair bit in MCS and if I am the one who handles the merge, then I'm sure it'll be a good opportunity to test this out a bit.

[lsf37]

Review feedback addressed and commits squashed.