busywork

Stream: maths

[Kevin Buzzard]

I am not 100% sure I know what this word means, but I think it's interesting that three Imperial mathematician @Ashvni Narayanan @Amelia Livingston and @Jason KY. all cut their teeth in the PR process with work doing stuff like bundling subobjects or morphisms ("we've done subrings but now we want subsemirings" or whatever). Why do we have a folder called deprecated in mathlib? Might removing this folder become quite a good summer project for mathematicians beginners? The mathematical material there is all very familiar to them. What needs to be done? I know I've asked this before, but I have a bunch of people looking for summer projects right now and need training material.

[Johan Commelin]

deprecated/ shouldn't be removed. Instead, we need is_group_hom (and friends) to move from class to structure, and all the instances should become lemmas, etc...

[Johan Commelin]

After that, they should just become part of regular mathlib, instead of living a poor and uncomfy life in deprecated/

[Kevin Buzzard]

In subring.lean (non-deprecated) it says

Let `R` be a ring. This file defines the "bundled" subring type `subring R`, a type
whose terms correspond to subrings of `R`. This is the preferred way to talk
about subrings in mathlib. Unbundled subrings (`s : set R` and `is_subring s`)
are not in this file, and they will ultimately be deprecated.

So This means "unbundled subrings will still exist, they're just not in simp normal form"?

[Johan Commelin]

Yep, that's my understanding of what is the best design (as far as we can see now)

[Eric Wieser]

My impression is that after doing what Johan describes, there may be benefits to redefining abbreviation subring:= subtype is_subring, since that gives us the ability to generalize statements like docs#subring.coe_add.

[Kevin Buzzard]

So that would be a massive subring refactor?

[Kevin Buzzard]

I had not internalised this before

[Kevin Buzzard]

You think the fundamental object from the point of view of CS is is_subring, and subring should be built on top?

[Eric Wieser]

I think subtype gives us much more generalization power than building a new structure each time

[Eric Wieser]

The idea behind docs#set_like is to say "look, this is basically just a subtype of a set". The alternative would be to make our subobjects defeq to subtypes of sets.

[Eric Wieser]

I don't know to what extent that would pay off yet

[Kevin Buzzard]

Does dot notation work with abbreviations? S.to_add_subgroup_mono for S : subring R?

[Anne Baanen]

It does, abbreviation is basically the same as @[reducible] def so it sticks around in expressions:

abbreviation nat_abbr := nat

def nat_abbr.zero : nat_abbr := 0
def nat_abbr.foo : nat_abbr → nat_abbr → nat_abbr := (has_add.add : ℕ → ℕ → ℕ)

example : nat_abbr.zero.foo nat_abbr.zero = nat_abbr.zero := rfl

[Anne Baanen]

This is different from notation, which is only a parsing thing and doesn't appear in expressions:

notation `nat_notation` := nat

def nat_notation.zero : nat_notation := 0
def nat_notation.foo := (has_add.add : ℕ → ℕ → ℕ)

example : nat_notation.zero.foo nat_notation.zero = nat_abbr.zero := rfl -- error, `nat.foo` undefined

[Kevin Buzzard]

Do abbreviations also mean that you're now stuck with _every_ nat appearing as nat_abbr in the prettyprinter until you've finished with the abbreviation?

[Anne Baanen]

No, it really creates something new. So ideal R could have been defined as an abbreviation for submodule R R instead of @[reducible] def as it is now. There is still the distinction between ideal R and submodule R R.

[Kevin Buzzard]

So why aren't we using vector_space as an abbreviation for module? Then I could still use vector space in teaching materials and...oh, I then have to move over all of module.foo into vector_space.foo :-/

[Patrick Massot]

Damn, I'm always half confused when I need to talk about the difference between abbreviation and notation. That's why I hesitated to write anything at all in this discussion.

[Anne Baanen]

Kevin Buzzard said:

So why aren't we using vector_space as an abbreviation for module? Then I could still use vector space in teaching materials and...oh, I then have to move over all of module.foo into vector_space.foo :-/

That was exactly the old situation before #7322: vector_space K V is an abbreviation for semimodule K V with extra assumptions [field K] [add_comm_group V].

[Anne Baanen]

I can't find where it was discussed, but there was also the possibility of defining

abbreviation vector_space (K V : Type*) [semiring K] [add_comm_monoid V] := module K V

which should have a lot less drawbacks, although it's mathematically slightly lying.

[Kevin Buzzard]

So maybe notation would be perfect for vector_space, let it apply in all situations, the point being that what we are trying to do with vector_space is shield a beginner UG from the word module completely because it sounds intimidating.

[Kevin Buzzard]

The moment they start using modules and vector spaces you just disable the notation because they're not scared of modules any more. Isn't this a perfect thing to do in localised notation? It seems to me that it might solve all the issues I had with the disappearance of vector_space.

[Anne Baanen]

I think that would be perfect, i.e. localized "notation `vector_space` := module" in vector_space

[Kevin Buzzard]

I try and explain all my code, but perhaps heuristically, when I'm teaching. I tend to minimise imports and say "we need this one for subgroups" or whatever. But when it comes to open X I just say "we'll be using results about Xs" and I can dismiss open_locale X in just the same way.

[Filippo A. E. Nuccio]

Patrick Massot said:

Damn, I'm always half confused when I need to talk about the difference between abbreviation and notation. That's why I hesitated to write anything at all in this discussion.

@Patrick Massot But is all this somewhere documented?

[Anatole Dedecker]

Just wondering, what were the original motivations for switching to bundled subgroups/subrings/... ?

[Eric Wieser]

I'm not sure either - perhaps it was to make map and comap easier in some way?

[Eric Wieser]

That is, maybe is_subring (f '' s) couldn't be found by typeclass search

[Kevin Buzzard]

My memory was that people were complaining that type class inference was not doing all the things which people wanted it to do, and the problem was diagnosed and my understanding was that the conclusion was that it was hard to fix in Lean 3, so we switched to a bundled approach which seems to have worked fine.

[Anne Baanen]

From the mathlib paper:

• It is important for compositions of homs to be a hom, but problems of the form is_hom (f ◦ g) can be difficult for type class inference. With bundled homs, one instead defines a custom composition operator Hom(A, B) × Hom(B, C) → Hom(A, C) that is used explicitly, obviating the need to search for is_hom (f ◦ g).
• The type Hom(A, B) itself often has interesting structure. For example, the type M →l [R] N of R-linear maps from M to N is an R-module where the zero element is the constant zero map, and addition and scalar multiplication work pointwise (Section 5.1). Bundling the type makes it easier to reason about this structure.

[Anne Baanen]

(In particular, if we have an instance is_hom (f ◦ g) and is_hom id, you have to be very careful with reducibility etc that searching for is_hom f doesn't go through is_hom (id ◦ f), is_hom (id ◦ id ◦ f), is_hom (id ◦ id ◦ id ◦ f), ...)

[Eric Wieser]

That's the one I had internalized too - but was there a similar argument for not using is_submonoid as a typeclass?

[Anne Baanen]

Presumably the same for is_submonoid s, is_submonoid (id '' s), is_submonoid (id '' id '' s), ...?

[Johan Commelin]

We also have a bunch of results about the lattice structure on is_sub_X

[Johan Commelin]

And X.quotient for X = ideal/subgroup/submodule etc...

[Eric Wieser]

I don't think dot notation working is a particularly convincing argument

[Johan Commelin]

Of course the latter is just a convenience, but not a crucial feature.

[Eric Wieser]

Since if we found a new design, we would probably be motivated to adjust lean core to make notation nice like last time when we expanded dot notation

[Anne Baanen]

My informal/unscientific intuition is that typeclasses are much easier to work with when there is a "trivial theory of equalities" on the arguments. Basically, you never have to use the fact that zmod 0 = ℤ in the way you would use the fact that smul_alg_hom 1 = id. As soon as you need a nontrivial equality, you need to make things reducible to infer well, and then you have a global condition on "everything that reduces in typeclass search" + "every instance declared" for termination of typeclass search.

[Reid Barton]

I agree. Type classes work well when the proof of P x is usually/always determined by a kind of structural recursion on the syntactic form of x. But if x is a something like a real number or a set int or a function then a very common way to prove P x is to prove that x = y and P y, and if P is a type class then this becomes much more awkward.
This doesn't arise for types because we don't have any general way to reason about isomorphism-invariance (such as univalence)--so the strategy "x is isomorphic to y and P y" isn't very convenient, and most proofs end up being of the structural form.