Commit 2021-08-01 17:17 f961b280

chore(deprecated/*): Make deprecated classes into structures (#8178) 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.