Adapt to Rocq#21180

[Tragicus]

There are a few repeat split in definitions of groups, which causes split to try and solve equalities using reflexivity. This used to fail, but with rocq-prover/rocq#21180 the unification algorithm becomes powerful enough to find a solution, albeit not the required one.

[jdchristensen]

I guess an alternative is a custom `justsplit' tactic that does nothing on equality goals and does split on all other goals...

[jdchristensen]

I'm curious how reflexivity could possibly solve any of the goals here. That doesn't look possible to me. And it's a bit annoying to be unable to use `repeat split'.

Do either of the following work?

    snapply (Build_Group freegroup_type).
    4: repeat split.
    all: exact _.

or with the second line replaced with

    4: split.  4: split.  4: split.

[Tragicus]

One of the goals is the fact that inv x is the left-inverse of x. Since the unit and the operation are not yet instantiated, there is a solution that makes op the constant operation returning the unit.
Oh, good catch, 4: repeat split causes the issue, but 4: split. 4: repeat split does work, thank you.

[jdchristensen]

I'd also prefer something more concise here.

[Tragicus]

I can do that, if you prefer. I just need to know where to put the tactic.

[jdchristensen]

I think this looks fine now, without needing a custom tactic. I think we should only merge it if the Coq change is definitely going to be merged. Do we know that yet or should I wait to find out?

[Tragicus]

There is no hurry, I still need to make a few overlays (or fix bugs).

[jdchristensen]

@Tragicus , is it possible to tell Coq to run a tactic like split but to not instantiate any evars while doing so? Essentiallly, we want a limited form of split.

Also, based on your diagnosis, I suspect that this single line would work for the first hunk:

    snapply (Build_Group freegroup_type sgop_freegroup); repeat split; exact _.

(I'm not sure why srapply (Build_Group freegroup_type) (with an r to allow typeclass search) doesn't find this sgop_freegroup instance, as that would be an even cleaner way to avoid the issue.)

[jdchristensen]

(I'm not sure why srapply (Build_Group freegroup_type) (with an r to allow typeclass search) doesn't find this sgop_freegroup instance, as that would be an even cleaner way to avoid the issue.)

(I think the reason is that other arguments depend on this one, and it doesn't know how to solve them. So while it finds the sgop_freegroup instance, it backtracks, and doesn't keep that solution. I can see why, but it does suggest that a greedy typeclass search option might be nice. Anyways, this is an aside from the main discussion here.)

[Tragicus]

I do not think so, but your fix also works. Which one do you prefer?

[jdchristensen]

I like the latest version the most. It's more robust, as once you've specified the operation, the remaining things are properties.