Elimination principles for GroupCoeq

[Alizter]

Needed for #2172

[jdchristensen]

I'm surprised by how slow the above is. I tried various things, and couldn't improve it. Even providing the term with exact_no_check and all implicit arguments is slow:

Time Definition freeproduct_ind_hprop {G H} (P : FreeProduct G H -> Type)
  `{forall x, IsHProp (P x)}
  (l : forall g, P (freeproduct_inl g))
  (r : forall h, P (freeproduct_inr h))
  (Hop : forall x y, P x -> P y -> P (x * y))
  : forall x, P x.
Proof.
  unfold FreeProduct in *.
  unfold freeproduct_inl, freeproduct_inr in *.
  Time exact_no_check (@amalgamatedfreeproduct_ind_hprop grp_trivial G H (grp_trivial_rec G) 
  (grp_trivial_rec H) P H0 l r Hop).  (* 0.075s *)
Time Defined. (* 0.075s *)

[jdchristensen]

I cleaned up and sped up a few things, but there are also some slow lines, some of which I marked with comments.

But here's a bigger question about GroupCoeq: would it be better to define the coequalizer of f g : G $-> H as the quotient of H by the normal subgroup generated by f(x) g(x)^ for x : G? The current definition involves two amalgamated products, which makes it quite complicated. With my proposal, the recursion and induction principles would be easier to see. It would also be obvious that the map from H to the coequalizer is surjective, making the _ind_hprop result trivial (and with fewer hypotheses).

My proposal would require us to define the normal subgroup generated by a subset, but that shouldn't be too bad, and is important to have in any case.

[jdchristensen]

Since the map from H to the coequalizer is surjective, the Hop assumption shouldn't be needed. But I'm not sure how to show that this map is surjective using the current definition of coequalizer.

[Alizter]

I cleaned up and sped up a few things, but there are also some slow lines, some of which I marked with comments.

Thanks, they were annoying me too.

But here's a bigger question about GroupCoeq: would it be better to define the coequalizer of f g : G $-> H as the quotient of H by the normal subgroup generated by f(x) g(x)^ for x : G? The current definition involves two amalgamated products, which makes it quite complicated. With my proposal, the recursion and induction principles would be easier to see. It would also be obvious that the map from H to the coequalizer is surjective, making the _ind_hprop result trivial (and with fewer hypotheses).

Yes, there is no real reason to define the coequalizer as an amalgamated free product. In fact, the reason I probably chose to do it this way was a blind application of coproducts + pushout gives coequalizers. Now thinking about it, this seems kind of backwards as pushouts are quite complicated compared to coequalizers. I would therefore be in favour of switching to a direct quotient, which seems like it would be easier to understand too

My proposal would require us to define the normal subgroup generated by a subset, but that shouldn't be too bad, and is important to have in any case.

Yes, this is something we would need anyway for other arguments in group theory.

[jdchristensen]

I would be ok with merging this as-is and leaving the job of redefining the coequalizer to another PR, if you want.

[Alizter]

I will need to rebase this before however.

I'm travelling at the moment, but I think I know how to formalize normal closures. We need to take the conjugates of all elements of a set S and then take the subgroup closure.

There will be a bit of work on various properties we expect normal closures to have, but it should be enough to replace the definition of the coequalizer. Not sure if it will fit in this PR however, so maybe it's a good idea to merge after rebasing.

[jdchristensen]

Yeah, I think it's probably best to merge this after rebasing, and then make a new PR with the new implementation.

[jdchristensen]

I just remembered that two of the slow lines could be sped up by closing and reopening the section, getting rid of the local instances that caused the slowdown there. It doesn't help freeproduct_ind_hprop, which is still a bit of a mystery to me.

While I was at it, I also improved various implicit arguments.

[Alizter]

I was not able to rebase this and ran out of time today. @jdchristensen Could you have a go?

[jdchristensen]

@Alizter I was able to rebase it, but it was a bit of a pain. I guess we should have worked through the backlog of PRs before doing library-wide changes. In any case, things work now. Can you give it a quick check before merging, to make sure I didn't mess up the rebase? (I just force-pushed a second time, moving my build-fix into the commit that broke the build, so now I think all commits should build without error. I'm done now.)