cutsat and grobner macro frontends to grind #29468

Stream: PR reviews

[Kim Morrison]

These are arriving with a non-macro implementation at the beginning on next week in v4.24.0, but then it will be a much longer cycle before I can easily tweak the settings in Mathlib. If this can be merged today I may still have time to verify that the settings are appropriate for Mathlib, by comparing places where omega / grind / cutsat and grind / grobner work.

[Kim Morrison]

Unfortunately this was not reviewed, so the built-in versions have arrived without having had the opportunity to test them thoroughly in Mathlib.

The PR has been updated so it now just includes the old polyrith tests as tests for the new grobner.

Please let me know if you find places where cutsat and grobner are doing something far beyond their spec. (It's easy to find trivial things they will do: for example currently if a proof was by intros; assumption then either of these tactics will close the goal. Personally I think this is okay, but happy to discuss.)