Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - chore(deprecated/*): Make deprecated classes into structures #8178

Closed
wants to merge 230 commits into from

Conversation

kbuzzard
Copy link
Member

@kbuzzard kbuzzard commented Jul 2, 2021

I make the deprecated classes is_group_hom, is_subgroup, ... into structures, and delete some deprecated constructions which become inconvenient or essentially unusable after these changes. I do not completely remove all deprecated imports in undeprecated files, however I push these imports much further towards the edges of the hierarchy.

More detailed comments about what is going on here:

In the src/deprecated/ directory, classes such as is_ring_hom and is_subring are defined (and the same for groups, fields, monoids...). These are predicate classes on functions and sets respectively, formerly used to handle ring morphisms and subrings before both were bundled. Amongst other things, this PR changes all the relevant definitions from classes to structures and then picks up the pieces (I will say more about what this means later). Before I started on this refactor, my opinion was that these classes should be turned into structures, but should be left in mathlib. After this refactor, I am now moving towards the opinion that it would be no great loss if these structures were removed completely -- I do not see any time when we really need them.

The situation I previously had in mind where the substructures could be useful is if one is (in the middle of a long tactic proof) defining an explicit subring of a ring by first defining it as a subset, or add_subgroup or whatever, and then doing some mathematics to prove that this subset is closed under multiplication, and hence proving that it was a subring after all. With the old approach this just involves some S : set R with more and more properties being proved of it and added to the type class search as the proof progresses. With the bundled set-up, we might have S : set R and then later on we get S_subring : subring R whose underlying subset equals S, and then all our hypotheses about S built up during the proof can no longer be used as rewrites, we need to keep rewriting or changeing x \in S_subring to x \in S and back again. This issue showed up only once in the refactor, in src/ring_theory/integral_closure.lean, around line 230, where I refactored a proof to avoid the deprecated structures and it seemed to get a bit longer. I can definitely live with this.

One could imagine a similar situation with morphisms (define f as a map between rings, and only later on prove that it's a ring homomorphism) but actually I did not see this situation arise at all. In fact the main issue I ran into with morphism classes was the following (which showed up 10 or so times): there are many constructions in mathlib which actually turn out to be, or (even worse) turn out under some extra assumptions to be, maps which preserve some structure. For example multiset.map (f : X -> Y) : multiset X -> multiset Y (which was in mathlib since it was born IIRC) turns out to be an add_group_hom, once the add_group structure is defined on multisets. So here I had a big choice to make: should I actually rename multiset.map to be private multiset.map_aux and then redefine multiset.map to be the add_monoid_hom? In retrospect I think that there's a case for this. In fact data.multiset.basic is the biggest source of these issues -- map and sum and countp and count are all add_monoid_homs. I did not feel confident about ripping out these fundamental definitions so I made four new ones, map_add_monoid_hom, sum_add_monoid_hom etc. The disadvantage with this approach is that again rewrites get a bit more painful: some lemma which involves map may need to be rewritten so that it involves map_add_monoid_hom so that one can apply add_monoid_hom.map_add, and then perhaps rewritten back so that one can apply other rewrites. Random example: line 43 of linear_algebra.lagrange, where I have to rewrite coe_eval_ring_hom in both directions. Let me say that I am most definitely open to the idea of renaming multiset.map_add_monoid_hom to multiset.map and just nuking our current multiset.map or making it private or map_aux or whatever but we're already at 92 files changed so it might be best to get this over with and come up with a TODO list for future tidy-ups. Another example: should the fields of complex be re' and im', and complex.re be redefined as the R-linear map? Right now in mathlib we only use the fact that it's an add_group_hom, and I define re_add_group_hom for this. Note however one can not always get away with this renaming trick, for example there are instances when a certain fundamental construction only preserves some structure under additional conditions -- for example has_inv.inv on groups is only a group homomorphism when the underlying group is abelian (and the same for pow and gpow). In the past this was dealt with by a typeclass is_group_hom on inv which fired in the presence of a comm_group but not otherwise; now this has to be dealt with by a second definition inv_monoid_hom whose underlying function is inv. You can't just get away with applying the proof of inv (a * b) = inv a * inv b when you need it, because sometimes you want to apply things like monoid_hom.map_prod which needs a monoid_hom as input, so won't work with inv: you need to rewrite one way, apply monoid_hom.map_prod and then rewrite back the other way now :-/ I would say that this was ultimately the main disadvantage of this approach, but it seems minor really and only shows up a few times, and if we go ahead with the renaming plan it will happen even fewer times.

I had initially played with the idea of just completely removing all deprecated imports in non-deprecated files, but there were times near the end when I just didn't feel like it (I just wanted it to be over, I was scared to mess around in control or test), so I removed most of them but added some deprecated imports higher up the tree (or lower down the tree, I never understand which way up this tree is, I mean nearer the leaves -- am I right in that computer scientists for some reason think the root of a tree is at the top?). It will not be too hard for an expert to remove those last few deprecated imports in src outside the deprecated directory in subsequent PR's, indeed I could do it myself but I might I might need some Zulip help. Note: it used to be the case that subring imported deprecated.subring; this is now the other way around, which is much more sensible (and matches with submonoid). Outside the deprecated directory, there are only a few deprecated imports: control.fold (which I don't really want to mess with),group_theory.free_abelian_group (there is a bunch of seq stuff which I am not sure is ever used but I just couldn't be bothered, it might be the sort of refactor which someone finds interesting or fun though), ring_theory.free_comm_ring (this file involves some definitional abuse which either needs to be redone "mathematically" or rewritten to work with bundled morphisms) and topology.algebra.uniform_group (which I think Patrick is refactoring?) and a test file.

If you look at the diffs you see that various things are deleted (lots of is_add_monoid_hom foo proofs), but many of these deletions come with corresponding additions (e.g. a new foo_group_hom definition if it was not there already, plus corresponding simp lemma, which is randomly either a coe or an apply depending on what mood I was in; this could all be done with @[simps] trickery apparently but I didn't read the thread carefully yet). Once nice achievement was that I refactored a bunch of basic ring and field theory to avoid the is_ classes completely, which I think is a step in the right direction (people were occasionally being forced to use deprecated stuff when doing stuff like Galois theory because some fundamental things used to use them; this is no longer the case -- in particular I think Abel-Ruffini might now be deprecated-free, or very nearly so).

finset.sum_hom and finset.prod_hom are gone. It is very funny to do a search for these files in mathlib current master as I write -- 98% of the time they're used, they're used backwards (with .symm or \l with a rewrite). The bundled versions (monoid_hom.map_prod etc) are written the other way around. I could have just left them and not bothered, but it seemed easier just to get rid of them if we're moving to bundled morphisms. One funny observation was that unary - seemed to be a special case: we
seem to prefer -\sum i, f i to \sum i, -(f i) . For almost every other function, we want it to go the other way.


Open in Gitpod

@bryangingechen bryangingechen added the WIP Work in progress label Jul 3, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jul 5, 2021
@bryangingechen bryangingechen changed the title chore(deprecated/*) Make deprecated classes into structures chore(deprecated/*): Make deprecated classes into structures Jul 6, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jul 9, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jul 28, 2021
@jcommelin
Copy link
Member

@kbuzzard I think that the long detailed story in the top post deserves to be preserved in the git history, by moving it above the fold. What do you think?

@kbuzzard kbuzzard added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 31, 2021
Copy link
Member

@fpvandoorn fpvandoorn left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This must have been a Herculean task. Thanks!

src/algebra/group_power/basic.lean Outdated Show resolved Hide resolved
src/data/dfinsupp.lean Outdated Show resolved Hide resolved
src/ring_theory/noetherian.lean Outdated Show resolved Hide resolved
kbuzzard and others added 6 commits August 1, 2021 13:26
Copy link
Member

@fpvandoorn fpvandoorn left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some suggestions to remove your "temporary" comments.

I'm fine with merging this is the current state. I didn't check everything carefully, but nothing looks much worse (and a lot of things look nicer).

bors d+

src/data/dfinsupp.lean Outdated Show resolved Hide resolved
Comment on lines +240 to +241
-- the below line causes the linter to complain :-/
-- attribute [simps] pow_monoid_hom nsmul_add_monoid_hom
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
-- the below line causes the linter to complain :-/
-- attribute [simps] pow_monoid_hom nsmul_add_monoid_hom

src/algebra/group_power/basic.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Aug 1, 2021

✌️ kbuzzard can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Aug 1, 2021
kbuzzard and others added 2 commits August 1, 2021 18:16
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@kbuzzard
Copy link
Member Author

kbuzzard commented Aug 1, 2021

Thanks!

bors r+

bors bot pushed a commit that referenced this pull request Aug 1, 2021
I make the deprecated classes `is_group_hom`, `is_subgroup`, ... into structures, and delete some deprecated constructions which become inconvenient or essentially unusable after these changes. I do not completely remove all deprecated imports in undeprecated files, however I push these imports much further towards the edges of the hierarchy. 

More detailed comments about what is going on here:

In the `src/deprecated/` directory, classes such as `is_ring_hom` and `is_subring` are defined (and the same for groups, fields, monoids...). These are predicate classes on functions and sets respectively, formerly used to handle ring morphisms and subrings before both were bundled. Amongst other things, this PR changes all the relevant definitions from classes to structures and then picks up the pieces (I will say more about what this means later). Before I started on this refactor, my opinion was that these classes should be turned into structures, but should be left in mathlib. After this refactor, I am now moving towards the opinion that it would be no great loss if these structures were removed completely -- I do not see any time when we really need them.

The situation I previously had in mind where the substructures could be useful is if one is (in the middle of a long tactic proof) defining an explicit subring of a ring by first defining it as a subset, or `add_subgroup` or whatever, and then doing some mathematics to prove that this subset is closed under multiplication, and hence proving that it was a subring after all. With the old approach this just involves some `S : set R` with more and more properties being proved of it and added to the type class search as the proof progresses. With the bundled set-up, we might have `S : set R` and then later on we get `S_subring : subring R` whose underlying subset equals S, and then all our hypotheses about `S` built up during the proof can no longer be used as rewrites, we need to keep rewriting or `change`ing `x \in S_subring` to `x \in S` and back again. This issue showed up only once in the refactor, in `src/ring_theory/integral_closure.lean`, around line 230, where I refactored a proof to avoid the deprecated structures and it seemed to get a bit longer. I can definitely live with this.

One could imagine a similar situation with morphisms (define f as a map between rings, and only later on prove that it's a ring homomorphism) but actually I did not see this situation arise at all. In fact the main issue I ran into with morphism classes was the following (which showed up 10 or so times): there are many constructions in mathlib which actually turn out to be, or (even worse) turn out under some extra assumptions to be, maps which preserve some structure. For example `multiset.map (f : X -> Y) : multiset X -> multiset Y` (which was in mathlib since it was born IIRC) turns out to be an add_group_hom, once the add_group structure is defined on multisets. So here I had a big choice to make: should I actually rename `multiset.map` to be `private multiset.map_aux` and then redefine `multiset.map` to be the `add_monoid_hom`? In retrospect I think that there's a case for this. In fact `data.multiset.basic` is the biggest source of these issues -- `map` and `sum` and `countp` and `count` are all `add_monoid_hom`s. I did not feel confident about ripping out these fundamental definitions so I made four new ones, `map_add_monoid_hom`, `sum_add_monoid_hom` etc. The disadvantage with this approach is that again rewrites get a bit more painful: some lemma which involves `map` may need to be rewritten so that it involves `map_add_monoid_hom` so that one can apply `add_monoid_hom.map_add`, and then perhaps rewritten back so that one can apply other rewrites. Random example: line 43 of `linear_algebra.lagrange`, where I have to rewrite `coe_eval_ring_hom` in both directions. Let me say that I am most definitely open to the idea of renaming `multiset.map_add_monoid_hom` to `multiset.map` and just nuking our current `multiset.map` or making it private or `map_aux` or whatever but we're already at 92 files changed so it might be best to get this over with and come up with a TODO list for future tidy-ups. Another example: should the fields of `complex` be `re'` and `im'`, and `complex.re` be redefined as the R-linear map? Right now in mathlib we only use the fact that it's an `add_group_hom`, and I define `re_add_group_hom` for this. Note however one can not always get away with this renaming trick, for example there are instances when a certain fundamental construction only preserves some structure under additional conditions -- for example `has_inv.inv` on groups is only a group homomorphism when the underlying group is abelian (and the same for `pow` and `gpow`). In the past this was dealt with by a typeclass `is_group_hom` on `inv` which fired in the presence of a `comm_group` but not otherwise; now this has to be dealt with by a second definition `inv_monoid_hom` whose underlying function is `inv`. You can't just get away with applying the proof of `inv (a * b) = inv a * inv b` when you need it, because sometimes you want to apply things like `monoid_hom.map_prod` which needs a `monoid_hom` as input, so won't work with `inv`: you need to rewrite one way, apply `monoid_hom.map_prod` and then rewrite back the other way now :-/ I would say that this was ultimately the main disadvantage of this approach, but it seems minor really and only shows up a few times, and if we go ahead with the renaming plan it will happen even fewer times.

I had initially played with the idea of just completely removing all deprecated imports in non-deprecated files, but there were times near the end when I just didn't feel like it (I just wanted it to be over, I was scared to mess around in `control` or `test`), so I removed most of them but added some deprecated imports higher up the tree (or lower down the tree, I never understand which way up this tree is, I mean nearer the leaves -- am I right in that computer scientists for some reason think the root of a tree is at the top?). It will not be too hard for an expert to remove those last few deprecated imports in src outside the `deprecated` directory in subsequent PR's, indeed I could do it myself but I might I might need some Zulip help. Note: it used to be the case that `subring` imported `deprecated.subring`; this is now the other way around, which is much more sensible (and matches with submonoid). Outside the deprecated directory, there are only a few deprecated imports: `control.fold` (which I don't really want to mess with),`group_theory.free_abelian_group` (there is a bunch of `seq` stuff which I am not sure is ever used but I just couldn't be bothered, it might be the sort of refactor which someone finds interesting or fun though), `ring_theory.free_comm_ring` (this file involves some definitional abuse which either needs to be redone "mathematically" or rewritten to work with bundled morphisms) and `topology.algebra.uniform_group` (which I think Patrick is refactoring?) and a test file.

If you look at the diffs you see that various things are deleted (lots of `is_add_monoid_hom foo` proofs), but many of these deletions come with corresponding additions (e.g. a new `foo_group_hom` definition if it was not there already, plus corresponding `simp` lemma, which is randomly either a `coe` or an `apply` depending on what mood I was in; this could all be done with `@[simps]` trickery apparently but I didn't read the thread carefully yet). Once nice achievement was that I refactored a bunch of basic ring and field theory to avoid the `is_` classes completely, which I think is a step in the right direction (people were occasionally being forced to use deprecated stuff when doing stuff like Galois theory because some fundamental things used to use them; this is no longer the case -- in particular I think Abel-Ruffini might now be deprecated-free, or very nearly so). 

`finset.sum_hom` and `finset.prod_hom` are gone. It is very funny to do a search for these files in mathlib current master as I write -- 98% of the time they're used, they're used backwards (with `.symm` or `\l` with a rewrite). The bundled versions (`monoid_hom.map_prod` etc) are written the other way around. I could have just left them and not bothered, but it seemed easier just to get rid of them if we're moving to bundled morphisms. One funny observation was that unary `-` seemed to be a special case: we
seem to prefer `-\sum i, f i` to `\sum i, -(f i)` . For almost every other function, we want it to go the other way.
@bors
Copy link

bors bot commented Aug 1, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(deprecated/*): Make deprecated classes into structures [Merged by Bors] - chore(deprecated/*): Make deprecated classes into structures Aug 1, 2021
@bors bors bot closed this Aug 1, 2021
@bors bors bot deleted the undeprecate branch August 1, 2021 19:11
@jcommelin jcommelin mentioned this pull request Aug 9, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

5 participants