Add basic prove_refinement tactic

[m-yac]

This PR adds a prove_refinement tactic which can be used to prove goals of the form:

(a1:A1) -> ... (an:An) -> refinesS_eq ...

within a call to prove_extcore (the Prop version of prove_print). All of the existing MRSolver unit tests work with this new tactic, and prove_refinement versions of all tests in mr_solver_unit_tests.saw have been added to that file to reflect this.

Note this tactic hooks into the existing MRSolver machinery with no changes, so if MRSolver fails it will currently exit the SAW script instead of proving more useful feedback and/or leaving unsolved goals over for the user. There is also currently no way to use theorems proved using this tactic in subsequent proofs using this tactic. Both of these things will change in coming PRs as we adapt MRSolver to this new paradigm.

[m-yac]

Hunh, and now it looks like the CI refuses to run for some reason on this latest commit (that checkmark is bogus and appeared instantly). We should definitely make it sure it runs before merging, I had a GHC 9 issue on my previous commit that I should have fixed, but didn't actually check on my machine.

[RyanGlScott]

Huh, it is quite strange that the CI just straight-up didn't happen. Can you try pushing an empty commit to see if that kickstarts it?

[eddywestbrook]

Looks good, other than the few places I've asked for more comments in the SAW core. I'm marking as approved because those are minor, but please address those before merging.

[m-yac]

Okay, @eddywestbrook, I think I addressed your comments! Thank you for suggesting to add more docs, those definitions are definitely not intuitive at first glance.

Also thankfully the CI now appears to start when I commit now, not sure what that one failure was about ¯_(ツ)_/¯

[eddywestbrook]

Wuh oh, looks like the Coq translator doesn't want to translate the List1 recursor. The hack we use for all the other recursors is to define List1__rec and add a special case for it to the Coq special treatment. But please file a bug about this, if there isn't one already, because that shouldn't be necessary.

[m-yac]

No idea why mr_solver_unit_tests.saw suddenly failed on my last commit – the only changes I made were to saw-core-coq, which shouldn't affect that test, and on the previous commit that test passed. I also couldn't replicate the failure on my machine. So, I'm trying out pushing a merge commit and hoping that a new CI run somehow magically fixes it.

My only guess is that somehow it's running the test with an old version of saw that doesn't have test_fun0 removed from the Prelude. That would explain why the error is that test_fun0 is being added twice, but I have no idea why the CI wouldn't use the version of saw it built on this branch...