associativity of ideal product

[Alizter]

This was left as a TODO so I did a quick proof for it. It's possible it can be simplified.

Edit: This PR started as a simple lemma, but I've since hijacked it to do a big cleanup of Subgroup and Ideal. Notably, we introduce Basics/Predicate.v.

• Fixes introduce subgroup inclusions and equality #2202.

[Alizter]

@jdchristensen I managed to carry out the opposite argument you suggested, but it required a lot of refactoring in Ideal. Namely, exploding the Section IdealLemmas which is probably for the best. While the diff is big, it might be a good time to perform some more style changes like changing Lemma to Definition.

[jdchristensen]

I started reviewing this, but the change to the indentation made it impossible to see what changed later on in the file, as github got quite confused with the diff it displayed. It's better if large indentation changes can be moved to a separate commit. Maybe you can force push to fix this, replacing just the last commit? (I think the comments I already made should still be visible and understandable after this.)

[Alizter]

You're totally right about the diff being hard to read. I've gone ahead and separated that out. Sorry about that. I'll get to your other review suggestions later.

[jdchristensen]

I pushed three commits. The first two I think are clear benefits. And subgroup_generated_subset_subgroup can be used in other places in Ideal.v and probably in other places in Subgroup.v or maybe elsewhere. Look for places using ideal_in_zero and ideal_in_plus_negate.

The third commit is the thing I wrote a comment about. Feel free to revert if you think it is not worth it. Or maybe with the new approach to the assertion, it's not worth using opposite rings here?

I do think opposite rings help with ideals in other parts of the file, so that's great. Can you find more places where this helps?

I have to run and won't have time to look at this for a while, but hopefully you'll be able to use some of these ideas to clean things up further.

[Alizter]

@jdchristensen I've added some material on predicates of types. This generalises all the subset material we had in Ideal and makes it available for Subgroup.

[jdchristensen]

I've carefully looked at Classes.v and Predicate.v, but not at the rest of the PR. I'm about to push a lot of changes involving those two files, so I thought I should pause my review here and see if you like the changes. I broke the changes into small commits, and the library builds after each commit, so you can read them independently.

[Alizter]

Feel free to push ahead with this, I won't be able to take a look until the weekend.

[jdchristensen]

I just pushed a few more changes. I still want to think a bit more about this, hopefully tomorrow.

[jdchristensen]

I've finished my review and don't plan to push any more changes. There are still a number of comments, but none of them are very important, so some could be handled by just adding TODO items to the file.

A couple more I noticed: ideal_subset_extension_preimage could be simplified with a _rec lemma for ideal_generated. And subgroup_left_ideal_quotient is really the statement that an arbitrary intersection of subgroups is a subgroup, which could be proved in Subgroup.v and then used here. (Each I (_ * x) is a subgroup since (_ * x) is a group homomorphism, and we intersect these over all x satisfying J x.)

[Alizter]

@jdchristensen This is ready for another round of review.

[jdchristensen]

subgroup_leftideal_quotient: As I mentioned earlier, this just seems to be the fact that an arbitrary intersection of subgroups is a subgroup. My last commit makes this more clear, since J can be any predicate.

isleftideal_subgroup_leftideal_quotient: And this seems to be the fact that an arbitrary intersection of left ideals is a left ideal.

Both of these facts should be proved in general, and then used in these two places. (Or maybe both of these results can then be dropped, as you can just directly form the left ideal as the intersection.)

[Alizter]

@jdchristensen Good observation. I will try to do that today.

[Alizter]

This is not so straightforward due to the truncation. I can show that merely (forall i, H i) is a subgroup, but in this particular case we have merely (forall i, J i -> H i) which means the first isn't a more general version of the second (without funext).

[Alizter]

@jdchristensen I didn't manage to find a nice way to generalise it for the reasons I mentioned before. Did you want to have a go too or should we just merge this now?

[jdchristensen]

If we have H : I -> Subgroup G, then the intersection will be defined as fun g => merely (forall i, H i g) (so that we don't need to use Funext to know that it is hprop-valued). So there are two ways to proceed. One is to change the definition of the ideal intersection to

exact (fun r => merely (forall x : sig J, subgroup_preimage (grp_homo_rng_left_mult r) I x.1)).

Here sig J plays the role of the indexing type I, and this is exactly expressed as an intersection of subgroups, so it should work fine. However, with this change, some later proofs need to change, which might be a bit annoying.

An alternative is to use the same predicate we currently have, but then use issubgroup_equiv to convert the predicate to the other form. This is how it would start:

Definition subgroup_leftideal_quotient {R : Ring} (I : Subgroup R) (J : R -> Type)
  : Subgroup R.
Proof.
  snapply Build_Subgroup.
  1: exact (fun r => merely (forall x, J x -> subgroup_preimage (grp_homo_rng_left_mult r) I x)).
  snapply issubgroup_equiv.
  - exact (fun r => merely (forall (x : sig J), subgroup_preimage (grp_homo_rng_left_mult r) I x.1)).
  - intro r.
    apply ReflectiveSubuniverse.equiv_O_functor. (* Need to add an import. *)
    symmetry.
    napply equiv_sig_ind.
  - (* Remaining goal: use that intersections of subgroups are subgroups. *)
Admitted.

(This just shows that it is possible. But probably we want to have a general proof that an intersection of ideals is an ideal, and use that, so this result wouldn't appear in this form.)

[jdchristensen]

Another option, which ties in to things I've been suggesting about subgroups, is to allow subgroups to be defined by non-hprop-predicates. We'd probably need two kinds of subgroups. Maybe the kind I'm talking about could be called "presubgroups". Then we would have a result that says that if H : G -> Type is a presubgroup, then fun g => (W -> H g) is a presubgroup. And another result that says that if H : I -> Presubgroup G is a family of presubgroups, then fun g => forall i, H i g is a presubgroup. And finally if H is a presubgroup, then fun g => merely (H g) is a subgroup. Those could be instances, and from that Coq could automatically infer that fun r => merely (forall x, J x -> subgroup_preimage (grp_homo_rng_left_mult r) I x) is a subgroup.

[Alizter]

I like the idea of showing it is equivalent to an uncurried version. I won't be able to finish it tonight, but that's probably the direction we should go in. I had some stuff on showing intersections are subgroups and ideals that I wrote today, so its just going to require some more time.

[jdchristensen]

@Alizter It would be nice to get this last step finished, as it would be handy to have this in the library. (E.g. Predicate.v will be useful.)

[Alizter]

@jdchristensen I sank too much time into trying to fix the Rocq master build last week. I am not sure when I will have enough time to look at this again. In the meantime, if you feel like pushing ahead with this, I don't mind.

[jdchristensen]

I merged with master. No conflicts and no changes required. I'll see if I can simplify those last two results.

[jdchristensen]

The first of the two recent commits introduces intersections of families of subgroups, and uses that to simplify subgroup_leftideal_quotient using issubgroup_equiv as discussed above. With this approach, I didn't see a good way to simplify isleftideal_subgroup_leftideal_quotient. The second commit adds things about intersections of families of ideals, but they aren't used.

I also experimented with simply defining subgroup_leftideal_quotient to be the intersection of the sig J indexed family. Then isleftideal_subgroup_leftideal_quotient can also be simplified slightly, using the results about intersections of ideals. And in most of the file, very little needs to change. But near the end there were two or three results that seemed a bit trickier to prove using that definition, so I went with the first approach.

I haven't looked over the rest of this PR recently, but I think this was the only remaining thing I had asked about, so I think we can merge this if you agree, @Alizter .

[Alizter]

LGTM, thanks for taking this on @jdchristensen. Feel free to merge. Let's not worry about the failures on master for now.

[JasonGross]

I started reviewing this, but the change to the indentation made it impossible to see what changed later on in the file, as github got quite confused with the diff it displayed. It's better if large indentation changes can be moved to a separate commit.

Very belatedly, https://github.blog/news-insights/product-news/ignore-white-space-in-code-review/ might help with such issues