more on commutator subgroups

[Alizter]

This PR was originally about some extra results on commutator subgroups but ended up introducing a definitionally involutive opposite groups and various improvements to groups.

[jdchristensen]

I reviewed the latest commits, but I'll want to make one more pass over the whole thing another day.

[jdchristensen]

(The build error seems to be a glitch.)

[Alizter]

Coq is undergoing renaming (to rocq) and the docker images have some teething problems it seems. I think this is known upstream, but I'm unsure if it will be fixed or if we have to do something.

[Alizter]

I've made groups definitionally involutive. I was in a bit of a rush so some of the naming and choices could be improved. The equiv_path_group lemma is very sensitive to changes, and it caused a lot of perf problems. Hopefully these are fixed now, but needs further more careful review.

[jdchristensen]

I've made groups definitionally involutive.

Great! I'm about to push a commit that takes advantage of this in one spot. Not sure if there are other places as well.

I was in a bit of a rush so some of the naming and choices could be improved.

We now have five constructors for groups: Build_Group, Build_Group', Build_Group_internal, Build_Group_internal_opp, and Build_Group_with_opp. I can't figure out any pattern to the naming or what _opp is supposed to indicate. And now one or both of the "internal" ones are used in many places. Can we reduce this to two or three variants with clearer names?

[Alizter]

I just pushed a commit clearing up the confusing naming for the constructors. The summary is as follows:

There are 3 constructors

• Build_Group_internal, this is the actual record constructor and contains the extra redundant info. This shouldn't really be used outside of Groups/Group.v.
• Build_Group is the main constructor, it doesn't have the redundant associativity axiom, and still uses IsGroup. There is a technical reason for this, which is that a completely unbundled version becomes extremely slow since axioms (with huge proofs) become arguments.
• Build_Group' is the "smart" constructor where all the redundancy has been removed and is unbundled. It is used sparingly throughout the library for the reason mentioned above. However it can be convenient for building groups that you don't wish to unfold.

[Alizter]

I've pruned some more changes that turned out to be unnecessary. I think this is in a good spot for a more thorough review. I'm interested if the build time has been affected in some files for instance. AbExt is a good place to check.

I had some previous experiments with changing around group constructors and they negatively impacted performance which is why I have chosen this setup. Hopefully, we have a balance of clarity, ease-of-use and utility (like with grp_op).

[Alizter]

Another trick I did that is worth mentioning was to encode the opposite associativity axiom as Associative (flip op) and add an instance so that this can be inferred from Associative op. Previously, we didn't use typeclasses which meant we couldn't just do exact _. This won't affect general use since it is hidden behind Build_Group, but it is something we could use for rings also. I'll take a look.

[jdchristensen]

Nice!

Can you squash 7 commits into one: starting from "improve group constructors" and including the 6 "revert ..." commits? You could also include the "clarify comment for Build_Group'" change if you want.

I'll check things over today or tomorrow.

[jdchristensen]

Can you squash 7 commits into one

Actually, if you can squash "definitionally involutive grp_op" as well, that would mean that files like FreeProduct.v don't get changed at all by this PR, which makes their history cleaner.

[Alizter]

@jdchristensen I've squashed the commits related to definitional grp_op into one. THat should be clearer now.

[jdchristensen]

Since the proof here is found by typeclass search, can we avoid needing this lemma at all by making IsUnitPreserving transparent for typeclass search? Or some similar idea? (And the same for the many results that use the same idiom.)

[Alizter]

I would rather not mark classes as being transparent for typeclass search or else Coq will spend time unfolding classes and trying to search each class it finds. I agree that this is a bit verbose, but I'm not sure if I can make the proof any slicker.

[jdchristensen]

Is there something like Hint Unfold that will only do it in limited cases?

[jdchristensen]

Ok, I've finished a full pass through and it looks good to me. But I haven't done any timing tests. Are you able to do some? If not, I'll try tomorrow.

[jdchristensen]

The build error is a glitch.

[Alizter]

Ok, I've finished a full pass through and it looks good to me. But I haven't done any timing tests. Are you able to do some? If not, I'll try tomorrow.

I won't have time until tomorrow evening.

[jdchristensen]

I did some timing tests of -j8 builds of four commits: master, the HEAD of this PR, and two in between. All took the same time within the noise.

I also did a -j1 file-by-file comparison of the HEAD of this PR vs master and got the following:

   After |  Peak Mem | File Name                                     |   Before |  Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
0m50.20s | 600588 ko | Total Time / Peak Mem                         | 0m48.40s | 600752 ko || +0m01.80s ||      -164 ko |   +3.73% |         -0.02%
0m00.20s | 386344 ko | Classes/interfaces/abstract_algebra.vo        | 0m00.59s | 390148 ko || -0m00.38s ||     -3804 ko |  -66.10% |         -0.97%
0m01.60s | 468968 ko | Algebra/AbSES/Pushout.vo                      | 0m01.43s | 469736 ko || +0m00.17s ||      -768 ko |  +11.88% |         -0.16%
0m00.63s | 450480 ko | Algebra/AbGroups/AbPushout.vo                 | 0m00.46s | 450056 ko || +0m00.17s ||       424 ko |  +36.95% |         +0.09%
0m01.01s | 470772 ko | Homotopy/HomotopyGroup.vo                     | 0m00.84s | 469752 ko || +0m00.17s ||      1020 ko |  +20.23% |         +0.21%
0m01.37s | 463256 ko | Algebra/AbGroups/TensorProduct.vo             | 0m01.22s | 462648 ko || +0m00.15s ||       608 ko |  +12.29% |         +0.13%
0m00.96s | 482056 ko | Homotopy/PinSn.vo                             | 0m00.82s | 482188 ko || +0m00.14s ||      -132 ko |  +17.07% |         -0.02%
0m00.86s | 440892 ko | Algebra/Groups/Group.vo                       | 0m00.74s | 441348 ko || +0m00.12s ||      -456 ko |  +16.21% |         -0.10%
0m03.12s | 464720 ko | Classes/implementations/natpair_integers.vo   | 0m03.00s | 462544 ko || +0m00.12s ||      2176 ko |   +4.00% |         +0.47%
0m01.43s | 465968 ko | Algebra/AbSES/Core.vo                         | 0m01.32s | 466608 ko || +0m00.10s ||      -640 ko |   +8.33% |         -0.13%
0m01.24s | 466256 ko | Algebra/AbSES/Pullback.vo                     | 0m01.16s | 464852 ko || +0m00.08s ||      1404 ko |   +6.89% |         +0.30%
0m00.07s | 240056 ko | test/Algebra/Groups/Group.vo                  |   N/A    |    N/A    || +0m00.07s ||    240056 ko |        ∞ |              ∞
0m01.82s | 469096 ko | Algebra/Groups/FreeProduct.vo                 | 0m01.76s | 469004 ko || +0m00.06s ||        92 ko |   +3.40% |         +0.01%
0m00.75s | 445940 ko | Algebra/Groups/Subgroup.vo                    | 0m00.68s | 446096 ko || +0m00.06s ||      -156 ko |  +10.29% |         -0.03%
0m00.55s | 446304 ko | Algebra/Groups/QuotientGroup.vo               | 0m00.49s | 446404 ko || +0m00.06s ||      -100 ko |  +12.24% |         -0.02%
0m00.62s | 478516 ko | Algebra/AbSES/SixTerm.vo                      | 0m00.56s | 477876 ko || +0m00.05s ||       640 ko |  +10.71% |         +0.13%
0m01.11s | 483644 ko | Homotopy/ClassifyingSpace.vo                  | 0m01.06s | 484028 ko || +0m00.05s ||      -384 ko |   +4.71% |         -0.07%
0m00.42s | 453940 ko | Algebra/Groups/Commutator.vo                  | 0m00.37s | 454032 ko || +0m00.04s ||       -92 ko |  +13.51% |         -0.02%
0m00.41s | 439256 ko | Algebra/Groups/GrpPullback.vo                 | 0m00.36s | 439420 ko || +0m00.04s ||      -164 ko |  +13.88% |         -0.03%
0m01.40s | 472820 ko | Algebra/AbSES/PullbackFiberSequence.vo        | 0m01.35s | 472696 ko || +0m00.04s ||       124 ko |   +3.70% |         +0.02%

That indicates a general trend to be slightly slower with this PR, but nothing major. So I'm ok with merging this.

[Alizter]

@jdchristensen Fantastic.

Are there any more related things you would like while we are looking at this?

[jdchristensen]

Actually, taking a quick look at the timing output for AbPushout.v showed two lines that got slower. I'll indicate them and any others I find.

• The Defined. line in isequiv_ab_pushout_rec went from 0.15 to 0.25s.
• Line 136 (refine (_ o (path_ab_pushout f g (grp_prod_inl c0) (grp_prod_inl c1))^-1).) went from 0.08 to 0.12s.

And here are some slow lines from the Groups folder. I didn't compare to how they are in master.

./FreeProduct:                                 Chars 23455 - 23500 [(intros~x~y~p~q;~by~nrapply~gr...] 0.225 secs (0.225u,0.s)
./FreeProduct:                                 Chars 23501 - 23509 [Defined.] 0.153 secs (0.153u,0.s)
./FreeProduct:                                 Chars 22033 - 22049 [End~FreeProduct.] 0.136 secs (0.134u,0.001s)
./QuotientGroup:                               Chars 9283 - 9314 [srapply~isembedding_isinj_hset.] 0.091 secs (0.091u,0.s)
./Group:                                       Chars 30182 - 30209 [rapply~Build_Is1Cat_Strong.] 0.09 secs (0.09u,0.s)
./Group:                                       Chars 29249 - 29272 [by~rapply~Build_Is1Cat.] 0.085 secs (0.085u,0.s)
./FreeProduct:                                 Chars 11414 - 11422 [Defined.] 0.072 secs (0.072u,0.s)
./GroupCoeq:                                   Chars 1638 - 1646 [Defined.] 0.057 secs (0.056u,0.s)
./Commutator:                                  Chars 5391 - 5437 [(rewrite~!grp_inv_op,~!grp_inv...] 0.056 secs (0.056u,0.s)
./FreeProduct:                                 Chars 21975 - 22020 [(intros~x~y~p~q;~by~nrapply~gr...] 0.053 secs (0.053u,0.s)
./Commutator:                                  Chars 5502 - 5510 [Defined.] 0.051 secs (0.05u,0.s)
./Group:                                       Chars 2558 - 2613 [Definition~issig_group~:~_~<~>...] 0.05 secs (0.033u,0.016s)

[jdchristensen]

Besides maybe fixing a few slow lines, there's nothing else I can think of adding now.

[jdchristensen]

(In case it isn't clear, I edited a previous comment to give details of slow lines.)

[Alizter]

I'm not fully certain why those lines in AbPushout are slow. I tried rewriting some of the proofs but it seemed to make things worse. I'll see if I can have a better look soon.

[jdchristensen]

• The Defined. line in isequiv_ab_pushout_rec went from 0.15 to 0.25s.

My latest commit reduces the time to 0.08s, so better than it was before. The main benefit comes from removing one simpl.

But it doesn't explain why it got slower. Presumably something about the other changes in the PR makes some code slower, and it would be nice to know what causes it.

I didn't yet look at any of the other spots I mentioned above.

[jdchristensen]

• Line 136 (refine (_ o (path_ab_pushout f g (grp_prod_inl c0) (grp_prod_inl c1))^-1).) went from 0.08 to 0.12s.

My last commit gets this down to ~0.09s. But if I make the same change in master, that line only takes 0.04s, so there is still a discrepancy. Not a big deal, but it must be small slowdowns like this that are showing up in the -j1 results.

[jdchristensen]

The slowest line in freeproduct_ind_homotopy is just as slow in master, so it isn't because of this PR. I can't figure out why it is slow, as it looks like a trivial step. I made a minor improvement, but it's still slow, and nothing else I tried helped. In any case, I think this PR is good and can be merged when you are ready.

[Alizter]

As you said before, the slowdown is within the realm of acceptability so its probably not worth the effort of splitting hairs.