mathlib4#2122

Stream: mathlib4

[Thomas Browning]

I just opened mathlib4#2122 porting Tactic.Group
I'm pretty new to lean4, and this is my first PR to mathlib4, so any feedback would be much appreciated.
In particular, the tactic really should really keep alternating between two auxiliary tactics (simp and ring), but I'm not sure how to do this and am currently just running simp <;> ring <;> simp which works for the test cases.

[Jireh Loreaux]

I haven't looked at the PR yet, but can't you do it essentially the same way as mathlib3? It used a call to repeat I think.

[Thomas Murrills]

Nice work! :) I pulled the branch and tried using repeat, but it makes some applications of group very slow—e.g. when the target is some equality that group simplifies but does not prove. Is there some tactic of the form fail_if_no_progress tacs (or equivalent meta code)?

[Thomas Murrills]

also here's a convenient example that fails without an extra ring call:

example (n m : ℤ) (a b : G) : a^(m-n)*b^(m-n)*b^(n-m)*a^(n-m) = 1 := by group

[Thomas Murrills]

I wrote a quick one already that should do the trick (until/unless an existing version is found). :) @Thomas Browning is it ok if I commit on the PR?

[Thomas Browning]

@Thomas Murrills Yes, go for it!

[Thomas Murrills]

Maaaaaaybe that new tactic should have been a separate PR. :sweat_smile: But it's small and, I imagine, fairly low-use—and the port is chugging along—so maybe it's ok if we bundle it together with group.

Or I can split it out and we can make it a PR dependence; that wouldn't be a problem.

[Thomas Murrills]

Of course, we might still find that some tactic or functionality like fail_if_no_progress already existed and I just couldn't find it :upside_down: but it was a fun exercise in any case :)

[Thomas Browning]

Thanks for the help!

[Thomas Murrills]

No problem, happy to! And nice work porting group! :D

[Jireh Loreaux]

@Thomas Murrills is group with your failIfNoProgress relatively quick? If not, is it in part because we're in TacticM instead of MetaM and there's more overhead?

[Jireh Loreaux]

A good test case would be line 114 in the open PR !4#2143. If it works there and doesn't take forever then it's probably okay.

[Jireh Loreaux]

I just checked. It works.

[Thomas Murrills]

Good to hear! :) I’m also going to take another look at fail_if_no_progress today if I can, and maybe improve it a little further.

[Thomas Murrills]

I'm thinking we should:

• merge Tactic.Group as-is, bundled with the current version of fail_if_no_progress
• enhance fail_if_no_progress afterwards to use simpler checks

instead of perfecting fail_if_no_progress first, so that we don't slow down the port. Does that sound reasonable?

[Jireh Loreaux]

Agreed, but I don't have merge powers