deprecated folder -- deleting lemmas?

Stream: general

[Kevin Buzzard]

I am always a bit annoyed by the deprecated directory, and so I spent some time over the last few weeks changing all the main classes in there (is_submonoid, is_subgroup etc, and is_group_hom, is_ring_hom etc) to structures (my understanding is that we still want these things around but not in the typeclass system). My undeprecate branch just compiled for the first time the other day; I changed 87 files. It's #8178 .

There are still some loose ends here however, and I thought that maybe I should get some community input. What I would imagine the next step would be is to start removing imports of deprecated files. I had it in my head that there were a few places where these structures were really useful, however I am now less sure about this. The main examples where you see the advantage of the unbundled approach is in the rare-but-they-do-exist cases where R is, say, a ring, and (in the middle of a long tactic proof) you define some S : add_subgroup R and then do some stuff with it and then later on manage to show that it's closed under R's multiplication. With the deprecated system you had S : set R with [is_add_subgroup S] and you just add an instance of [is_add_subring S] and keep going. With the new system you need to make a new S' : subring R and all your hypotheses about S now need to be beefed up to apply to S' or else you can't rewrite with them. This turns out to be only a minor annoyance.

But the real reason I'm bringing this up is that once this change is made, there are some definitions and results in mathlib which are much harder to state, or rather can in theory be stated but only in a convoluted way. An example is subtype.monoid, which looks like this in master (clean, but using the fact that is_submonoid is a class) and like this on the branch where is_submonoid becomes a structure. Notice the weird [fact (is_submonoid s)]. Why is this here? Well, if I just wrote (hs : is_submonoid s) then I could get subtype.monoid compiling no problem, but the problems all start later when we're doing things like

lemma is_submonoid.coe_mul [fact (is_submonoid s)] (a b : s) :
 ((a * b : s) : M) = a * b := rfl

This is the version on my branch, which works fine. But without using fact Lean has no way of figuring out what the multiplication is, because M is a monoid but s : set M so it's hard to get the _statement_ to typecheck.

As I say, the branch compiles right now, so one can look through the changed files and see the facts I've added. There aren't that many, and I know for sure that these results cannot really be used anywhere because these facts will not be in the typeclass system in general, I didn't make an instance of fact (is_submonoid s)] anywhere. So one way forward would be simply to delete lemmas like is_submonoid.coe_mul completely. Basically they have become unusable because of the change, and I see little point in keeping them. I'm aware that deleting lemmas is not something which is usually done so this is why I wanted to ask about it.

Some early work of Kenny on Galois theory used is_add_subgroup and because I knew the material well and was confident that analogous add_subgroup versions weren't there, I took the trouble to refactor them and remove a deprecated import. If there are any other areas of mathlib where people want me to make the refactor from is_X to X then I'm in quite a good position to work on this stuff now because I know the tricks (and by this time next month I'll have forgotten them). However another point of view might be that because I made a PR which touches 87 files it might be best to get it merged ASAP. However I can certainly work on completely deleting those deprecated lemmas today or tomorrow.

[Johan Commelin]

Wowowow! Thanks a lot for this massive effort!
My first reaction is: we should get rid of those fact-lemmas, and merge the rest ASAP.

[Kevin Buzzard]

OK I will remove the lemmas which cannot be being used because they have facty typeclasses; I can do it at Xena tonight.

[Floris van Doorn]

I think we should get rid of all these lemmas about is_submonoid (at least, if there is a submonoid alternative, which should be the case almost always). The only things we really want to keep are the translations between is_submonoid and submonoid: submonoid.of (which maybe should be renamed is_submonoid.submonoid to enable projection notation) and submonoid.is_submonoid.
All declarations foo about is_submonoid that can be proven by M.submonoid.foo should be removed.

[Kevin Buzzard]

Should this be done in this PR or in another one? Thanks for the input!

[Kevin Buzzard]

In general PR's which touch a huge number of files are really scary, but actually I'm only changing things which nobody else is working on so it's much less scary than you think.

[Floris van Doorn]

If you make separate PRs, you're changing the statement of a lot of lemmas in this PR that will be removed in the next PR.
So it will at least be easier to review if you decide to make a single PR. It also depends on how likely merge conflicts are (and your willingness to resolve them).

[Floris van Doorn]

If you think that a lot of proofs of lemmas that we want to keep use lemmas that we are removing, then it might be easier to make separate PRs.

[Reid Barton]

is_submonoid.coe_mul is an API lemma about some has_mul instance that you are also deleting, right?

[Reid Barton]

Oh that's the subtype.monoid you mentioned

[Reid Barton]

Oh I'm confused now. subtype.monoid used to be a def, but now it is an instance; how come?

[Floris van Doorn]

We want to remove subtype.monoid and instead use (hM : is_submonoid M).submonoid.monoid (if really needed).

[Kevin Buzzard]

Reid Barton said:

Oh I'm confused now. subtype.monoid used to be a def, but now it is an instance; how come?

My impression is that it used to be dangerous in some way to make it an instance; it was occasionally made a local instance IIRC.

[Reid Barton]

Like for example about 12 lines after its definition, on your branch :upside_down:

[Kevin Buzzard]

So just to be clear -- we have docs#is_subgroup.normal_in_normalizer stating in a deprecated way that a subgroup is normal in its normalizer, and this is never used in mathlib, and we also have docs#subgroup.normal_in_normalizer, which states this in the non-deprecated way, and the statement uses subtype.group which is going to be removed, and so I am also going to remove is_subgroup.normal_in_normalizer.

[Kevin Buzzard]

PS I think merge conflicts are highly unlikely unless there's some big refactor of algebra going on that I don't know about.

[Kevin Buzzard]

OK so that was less painful than expected -- all the facts I added are removed now.

[Kevin Buzzard]

@Floris van Doorn or anyone else who understands this stuff: right now ring_theory.subring imports deprecated.subring, but it's the other way around for submonoids. I propose switching this, having deprecated.subring import ring_theory.subring, and moving docs#set.to_subring into deprecated.subring and renaming it to is_subring.subring. This way I can work on removing all import deprecated.subring from undeprecated mathlib. I have already achieved this with deprecated.subfield.

[Johan Commelin]

Wouldn't it be easier to move deprecated.* back into the main tree? Because that's the end goal anyway, right?

[Floris van Doorn]

I agree with Johan that we eventually want to remove the deprecated folder entirely. My thought is to have 20-30 lines at the end of
https://github.com/leanprover-community/mathlib/blob/master/src/group_theory/submonoid/basic.lean
(or perhaps in a separate file) about is_submonoid, with just the results in
https://github.com/leanprover-community/mathlib/blob/468328daee53ea78e8522daa20893a434ce30b57/src/deprecated/submonoid.lean#L34-L59
and
https://github.com/leanprover-community/mathlib/blob/468328daee53ea78e8522daa20893a434ce30b57/src/deprecated/submonoid.lean#L410-L415
There might be a little bit more that we want to keep, if it doesn't have a good bundled analogue. But something like docs#is_submonoid.inter can be removed since we can take meets of bundled submonoids.

The same can be true about rings.

[Eric Wieser]

In the long run I'd be tempted to extract the proofs from things like submonoid.has_inf and move them back out to is_submonoid.inter

[Eric Wieser]

But right now we prove the same thing from scratch in both places, so we may as well throw out the one we don't use

[Kevin Buzzard]

so right now I have removed all import.deprecated.* from all mathlib files other than those in src/deprecated (and test), and a bunch of stuff has broken again, so in some sense I feel like I'm back to square one. I am now creating diffs like the following screenshot:

diff.png

There are random places all over mathlib where people prove is_group_hom for a map, and I'm replacing them with defs (if they don't seem to be there already) and adding a simp lemma. Am I going the right way? I could just add some deprecated imports back in and I'd have everything compiling again. So far I've added set.singleton_mul_hom to replace docs#set.singleton.is_mul_hom, multiset.map_add_monoid_hom to replace is_add_monoid_hom (multiset.map f), countp_add_monoid_hom to replace docs#multiset.countp.is_add_monoid_hom and so on. Should I cut my losses and stop or is this what we want?

[Yakov Pechersky]

Shouldn't simps take care of making the simp lemma for you?

[Kevin Buzzard]

I don't understand simps. Is this what it does?

[Kevin Buzzard]

attribute#simps

[Kevin Buzzard]

I'm not very good at attributes.

[Yakov Pechersky]

Simps makes the boilerplate lemmas for equivs and I think bundled homs

[Eric Rodriguez]

I didn't get it before but I just put @[simps?] before any definition and if the lemmas look reasonable I keep it in

[Kevin Buzzard]

Right now my question is whether I should be going down this rabbithole at all. I've changed 86 files, got mathlib compiling, then I deleted a few imports and now it's all broken again.

[Eric Rodriguez]

works fine most of the time, you can also make it simp the RHS before making a lemma (I can't remember how though)

[Yakov Pechersky]

simps {rhs := true} iirc

[Yakov Pechersky]

(deleted)

[Patrick Massot]

Kevin, if you manage to convince some maintainer to merge #8317 then you'll have less deprecated group homs to handle.

[Kevin Buzzard]

Apparently you should be tagging to_compl with simps

[Patrick Massot]

Me? Why?

[Kevin Buzzard]

Because above I was replacing is_monoid_hom (foo : X -> Y) := ... with foo_monoid_hom : X ->* Y := ... and then @[simp] lemma foo_monoid_hom_coe : (foo_monoid_hom : X -> Y) = foo := rfl and Yakov told me I should be using @[simps].

[Kevin Buzzard]

Yakov Pechersky said:

Shouldn't simps take care of making the simp lemma for you?

Wait a minute. I'm now doing this simps thing and I've noticed that it's not making coe lemmas, it's making apply lemmas. For example in the deprecated days we had multiset.map_is_add_monoid_hom (a proof that map f : multiset α → multiset β preserves 0 and addition) and I'm changing it to

def multiset.map_add_monoid_hom (f : α → β) : multiset α →+ multiset β := ...

If I @[simps] this I get

multiset.map_add_monoid_hom_apply: ⇑(map_add_monoid_hom f) s = map f s

whereas I was proposing

@[simp] lemma map_add_monoid_hom_coe (f : α → β) :
  (map_add_monoid_hom f : multiset α → multiset β) = map f := rfl

and of course the linter doesn't like both. Which one should be in mathlib? Or isn't it as simple as that?

[Eric Wieser]

simps hasn't been taught to distinguish coe from apply (yet)

[Eric Wieser]

IMO we should teach it to though

[Floris van Doorn]

You can get those lemmas with @[simps {fully_applied := ff}]. See docs#simps_cfg for more info.
There is no way yet to tell simps that for certain projections you should always have {fully_applied := ff}.

[Kevin Buzzard]

Thanks! I don't know whether they are good simp lemmas in practice but if we're moving away from the is_ structures completely then one of them at least seems to be necessary

[Eric Wieser]

Can you tell it to call the unapplied lemmas coe_foo rather than foo_apply though Floris?

[Patrick Stevens]

A piece of GitHub usage you might not have known: if you are deciding whether or not to use two PRs, A and then B (which depends on A), one option is to make PR A, then raise PR B with a base of A rather than a base of master. (That is, it is a pull request for merging B into A, not into master.) That way, both PRs can be reviewed independently, with PR B being reviewed as though A had already been merged into master, but really you haven't actually merged A into master. When the whole stack of PRs is ready to merge, you can merge B into A, and then Bors squash-merge A into master. See https://blog.logrocket.com/using-stacked-pull-requests-in-github/ for a longer-form explanation with screenshots. (This workflow may or may not be any use for what you want to do here; I just saw some words upthread which suggested this might be appropriate.)

[Eric Wieser]

Was that intended for a different thread?

[Floris van Doorn]

Eric Wieser said:

Can you tell it to call the unapplied lemmas coe_foo rather than foo_apply though Floris?

Currently the setup is

initialize_simps_projections add_hom (to_fun → apply)

If you want the coe naming uniformly, you can replace it with

initialize_simps_projections add_hom (to_fun → coe as_prefix)

Not sure if that is preferred throughout the whole library, though.

[Eric Wieser]

Sure, but what I'm asking is how to make @[simps apply] output f_hom_apply : ⇑f_hom x = f x and @[simps coe] output coe_f_hom : ⇑f_hom = f

[Eric Wieser]

Or at least, a way to get both via simps, the exact spelling needed doesn't matter, only the lemmas it generates

[Floris van Doorn]

This is possible, as long as you write the coe projection as [simps? coe {fully_applied := ff}]
You have to change the initialization to the following:

/-- See Note [custom simps projection] -/
def add_hom.simps.coe (e : α →+ β) : α → β := e

initialize_simps_projections add_hom (to_fun → apply, to_fun → coe, -coe as_prefix)

(apparently you have to give the coercion explicitly for the second name of the to_fun projection)

Here is a full example:

import tactic.simps

structure equiv (α : Sort*) (β : Sort*) :=
(to_fun    : α → β)

local infix ` ≃ `:25 := equiv

variables {α β γ : Sort*}

instance : has_coe_to_fun $ α ≃ β := ⟨_, equiv.to_fun⟩

/-- See Note [custom simps projection] -/
def equiv.simps.coe (e : α ≃ β) : α → β := e

initialize_simps_projections? equiv (to_fun → apply, to_fun → coe, -coe as_prefix)

/-- Composition of equivalences `e₁ : α ≃ β` and `e₂ : β ≃ γ`. -/
protected def equiv.trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
⟨e₂ ∘ e₁⟩

attribute [simps? coe {fully_applied := ff}] equiv.trans
/-
[simps] > adding projection equiv.coe_trans:
        > ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e₁ : α ≃ β) (e₂ : β ≃ γ),
  ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
-/
attribute [simps?] equiv.trans
/-
[simps] > adding projection equiv.trans_apply:
        > ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e₁ : α ≃ β) (e₂ : β ≃ γ) (ᾰ : α),
  ⇑(e₁.trans e₂) ᾰ = (⇑e₂ ∘ ⇑e₁) ᾰ
-/

This is assuming that with @[simps] (without options) you want to generate the apply lemma and not the coe lemma.

[Eric Wieser]

I guess the only thing that would be left to ask for would be for coe to imply fully_applied:=ff

[Floris van Doorn]

That's a todo in #5489

[Kyle Miller]

I was just thinking about ways the ways we tend to attach properties to terms.

• Typeclasses let you associate data to a term more or less syntactically: if a term has a particular form, then you can provide some additional structure. A downside is that rewriting an expression tends to break the connection.
• "Bundling" the property by defining a structure along with coercions to the underlying data. This solves the rewrite problem, but the structure isn't literally the data. Attaching multiple different kinds of data can require a carefully designed hierarchy.

One that doesn't seem to be used much is tagging. This is a general tagging function I was just playing with:

@[reducible] def attach {α : Sort*} (β : α → Sort*) (x : α) (h : β x) : α := x

You can use this to define sets with an attached proof that they are subgroups:

abbreviation the_subgroup {α : Type*} [group α] (s : set α) (h : is_subgroup s) :=
attach is_subgroup s h

Then, for example,

lemma the_subgroup.mem_inter_iff
  (s : set α) (h : is_subgroup s) (s' : set α) (h' : is_subgroup s') (x : α)
  (h'' : is_subgroup (s ∩ s')) :
  x ∈ the_subgroup (s ∩ s') h'' ↔ x ∈ the_subgroup s h ∧ x ∈ the_subgroup s' h' :=
by rw set.mem_inter_iff

Theoretically, the the_subgroup terms in an expression are able to help you apply lemmas that need a proof of is_subgroup, but otherwise the tags will be ignored.

Here are some basic examples (sorry, it's for an older version of mathlib, before @Kevin Buzzard's recent changes...). I haven't really tested the idea, but I thought I'd throw it out there in case it's somehow interesting.

import data.int.parity
import deprecated.subgroup
import tactic

@[reducible]
def attach {α : Sort*} (β : α → Sort*) (x : α) (h : β x) : α := x

abbreviation the_even (n : ℤ) (h : even n) := attach even n h
abbreviation the_odd (n : ℤ) (h : odd n) := attach odd n h

lemma the_even_add_one_eq (n : ℤ) (h : even n) :
  the_even n h + 1 = the_odd (n + 1) (by simp [int.even_add_one, h]) :=
rfl

abbreviation the_subgroup {α : Type*} [group α] (s : set α) (h : is_subgroup s) :=
attach is_subgroup s h

variables {α : Type*} [group α]

instance (s : set α) (h : is_subgroup s) : is_subgroup (the_subgroup s h) := h

lemma the_subgroup_attach (s : set α) [is_subgroup s] : s = the_subgroup s infer_instance := rfl

lemma the_subgroup.inter (s : set α) (h : is_subgroup s) (s' : set α) (h' : is_subgroup s') :
  the_subgroup s h ∩ the_subgroup s' h' = the_subgroup (s ∩ s') infer_instance :=
rfl

lemma subgroup.of_eq (s : set α) [h : is_subgroup s] : (subgroup.of s : set α) = the_subgroup s h :=
rfl

lemma the_subgroup.mem_inter_iff
  (s : set α) (h : is_subgroup s) (s' : set α) (h' : is_subgroup s') (x : α)
  (h'' : is_subgroup (s ∩ s')) :
  x ∈ the_subgroup (s ∩ s') h'' ↔ x ∈ the_subgroup s h ∧ x ∈ the_subgroup s' h' :=
by rw set.mem_inter_iff

[Yakov Pechersky]

Aren't these just subtypes of "set X"?

[Kyle Miller]

@Yakov Pechersky A term with attached data is definitionally equal to that term -- there aren't any new types here -- for the subgroup example, the_subgroup s h is trivially defeq to s. It's true that the terms for which you can write a the_subgroup term correspond to terms of a subtype (in particular, {s : set α // is_subgroup s}), but nothing is explicitly constructed. This lets you manipulate tagged terms easier, I think. For example you can sort the attached data:

lemma attach_swap
  {α : Sort*} (β β' : α → Sort*) (x : α) (h : β x) (h' : β' x) :
  attach β (attach β' x h') h = attach β' (attach β x h) h' := rfl

In principle, you can also attach data other than proofs, and then they would in a sense "just" be sigma types. One difference from a sigma type is that the additional data is sort of discarded, and it's only used to help fill in implicit arguments during elaboration or when proving things.

[Yakov Pechersky]

So your attach is like constructing a term of a subtype then instantly coercing it back to the original type

[Kyle Miller]

Sure, if you want there to be a type involved to explain it. (Are you suggesting it would be better that way? This is just meant add some data to the AST that's easy to access and easy to ignore. Also, if it were using subtypes, it would have to be done in a way that that coercion you describe doesn't get simped away.)

[Yakov Pechersky]

I'm saying that attach is fine for constructing such tagged terms. What about requiring such tagged terms, as an argument for a def or a proof? Then you are proving the data and the proof separately, to be able to say lemma ex (x : X) (h : P x) : Q (attach x h) := .... I guess I'm not fully understanding what attach gives you that subtypes do not.

[Yakov Pechersky]

I am not saying that subtypes are the solution to the problem, but rather, I want to appreciate what you propose!

[Yakov Pechersky]

Ah, here's a difference where your approach is "trivially defeq" but the subtype one isn't:

import deprecated.subgroup
import tactic

abbreviation the_subgroup {α : Type*} [group α] (s : set α) (h : is_subgroup s) : set α :=
(⟨s, h⟩ : subtype is_subgroup)

attribute [class] is_subgroup

variables {α : Type*} [group α]

lemma the_subgroup.mem_inter_iff
  (s : set α) (h : is_subgroup s) (s' : set α) (h' : is_subgroup s') (x : α)
  (h'' : is_subgroup (s ∩ s')) :
  x ∈ the_subgroup (s ∩ s') h'' ↔ x ∈ the_subgroup s h ∧ x ∈ the_subgroup s' h' :=
-- by rw set.mem_inter_iff
begin
  rw set.mem_inter_iff, -- fails
  sorry
end

@[reducible]
def attach {α : Sort*} (β : α → Sort*) (x : α) (h : β x) : α := x

abbreviation the_subgroup' {α : Type*} [group α] (s : set α) (h : is_subgroup s) : set α :=
attach is_subgroup s h

lemma the_subgroup'.mem_inter_iff
  (s : set α) (h : is_subgroup s) (s' : set α) (h' : is_subgroup s') (x : α)
  (h'' : is_subgroup (s ∩ s')) :
  x ∈ the_subgroup' (s ∩ s') h'' ↔ x ∈ the_subgroup' s h ∧ x ∈ the_subgroup' s' h' :=
by rw set.mem_inter_iff -- works

[Yakov Pechersky]

The subtype approach requires a by convert set.mem_inter_iff _ _ _

[Kyle Miller]

This is all very untested, but the design constraints I was going for are (1) that rewrites should work with tagged data, and (2) that the tags don't unintentionally disappear (I suspect simp will gobble them up if they were subtypes). Using subtypes is an interesting idea, but I think things tend to work out better following the principle "if a function could take a sigma type, existential, or subtype, make it take the components separately."

[Yakov Pechersky]

Another way tagged data works is, of course, with structures.

[Yakov Pechersky]

Which are inherently even more opaque than subtypes.

[Kyle Miller]

A place tags are sort of used already in mathlib is to create "new" types for having a different collection of instances. There's a variation I haven't seen (though it's possible it's there somewhere, mathlib is big!) where there are additional unused arguments whose purpose is to parameterize instances. One example might be where you want to take a docs#add_torsor, choose an origin, and treat it like an additive group.

[Kyle Miller]

This could potentially also be a way to have a set remember that it comes from a set_like, which might be an alternative to things like is_subgroup.

def sets (α : Type*) {β : Type*} [set_like α β] : set (set β) :=
{s : set β | ∃ (x : α), s = (x : set β)}

abbreviation the (α : Type*) {β : Type*} [set_like α β] (s : set β)
  (h : s ∈ sets α) := attach _ s h

lemma some_set {α : Type*} {β : Type*} [set_like α β] {s : set β} (h : s ∈ sets α) :
  (h.some : set β) = s := h.some_spec.symm

lemma the_subgroup.inter {α : Type*} [group α] (s t : set α)
  (h : s ∈ sets (subgroup α)) (h' : t ∈ sets (subgroup α)) :
  the (subgroup α) s h ∩ the (subgroup α) t h' =
    the (subgroup α) (s ∩ t) (by { use h.some ⊓ h'.some, simp [some_set]}) := rfl

[Kyle Miller]

(There's probably some way to not have to write lemmas like the_subgroup.inter. I just chose it for demonstration.)