structure piling up

Stream: general

[Patrick Massot]

From the beginning, we've known that the current type-class + structure inheritance setup would get out of control when moving to sophisticated mathematics. This is mentioned in Tom's famous blog post for instance. Today I see both a series of Lean4 commits mentioning structures and this PR featuring five lines of arguments to a structure command. @Sebastian Ullrich could you tell us if Lean 4 will make it easier to have abbreviations or other mechanisms that will keep this proliferation under control?

[Sebastian Ullrich]

It's not clear to me whether you're asking for mere syntactic shortcuts for managing the current approach, or for alternative approaches to hierarchy encoding that avoid the explosion to begin with. Though I guess your answer will be "either of them as long as it works" :) .

[Patrick Massot]

Either of them, as long as it works.

[Patrick Massot]

I was thinking about shortcuts here. Alternative approaches could be nice but that's a very different scale.

[Jalex Stark]

Just to bring the code reference out from behind the link, this is the very long structure invocation

structure Lie_add_group_morphism (I : model_with_corners 𝕜 E E) (I' : model_with_corners 𝕜 E' E')
(G : Type*) [topological_space G] [charted_space E G] [smooth_manifold_with_corners I G]
[add_group G] [topological_add_group G] [Lie_add_group I G]
(G' : Type*) [topological_space G'] [charted_space E' G'] [smooth_manifold_with_corners I' G']
[add_group G'] [topological_add_group G'] [Lie_add_group I' G'] extends add_monoid_hom G G' :=
  (smooth_to_fun : smooth I I' to_fun)

[Sebastian Ullrich]

It should come as no surprise that we are only implementing the "new" structure command in Lean 4, so if mathlib wants to keep the current encoding, someone else would have to implement that alternative command. But before someone starts working on that, I would really like to have a discussion on whether that approach is still the way to go. For example, I'm not sure if there has been any consensus on whether @Cyril Cohen's work on forgetful inheritance could be a better way forward for mathlib - especially when code has to be adapted to Lean 4 anyway.

[Patrick Massot]

What work by Cyril are you referring to?

[Sebastian Ullrich]

He talked about it at Lean Together, but the most recent revision should be https://math-comp.github.io/competing-inheritance-paths-in-dependent-type-theory/

[Patrick Massot]

Ok, then I don't understand why you say mathlib doesn't do that.

[Rob Lewis]

Are you thinking of the (related but different) hierarchy builder tool? https://hal.inria.fr/hal-02478907/file/hb.pdf

[Patrick Massot]

That would make more sense.

[Sebastian Ullrich]

I have no idea which one is more relevant and applicable at this point, haha. I haven't read the papers yet and hoped someone else would do that and tell us what they think...

[Patrick Massot]

I'd love to see something like their hierarchy builder used in Lean, and indeed this kind of layer should make the difference between old and new structure irrelevant. But I guess the adaptation wouldn't be straightforward, if only because of unification hint vs type class.

[Patrick Massot]

The conclusion is very optimistic about adapting their work to different targets.

[Sebastian Ullrich]

Coming back to syntactic shortcuts, there is a nice GHC extension that lets you define typeclass constraint synonyms such as

type Stringy a = (Read a, Show a)
foo :: Stringy a => ...
foo ...  -- can use both `Read a` and `Show a`

It's kind of like a macro (it doesn't declare an actual new typeclass), but not quite. I'm not sure how it should be implemented in Lean 4, or even what the syntax should be.

[Patrick Massot]

I sounds like what I had in mind (and of course I have no opinion on implementation).

[Kevin Buzzard]

The following was very noticeable in Sebastien's talk: he had a field k, a topological space X, and three or so other mathematical objects, and then for many of the subsets of his collection of objects he had another typeclass (like M being an R-module etc) and somehow the statement of the result took a long time coming. But on the other hand I'm assuming a lot of this is being done with variables if you actually look at the source code

[Gabriel Ebner]

typeclass constraint synonyms

We can already do this in Lean 4 because TC synthesis has loop checking, right?

class Stringy (A) extends Read A, Show A.
instance {A} [Read A] [Show A] : Stringy A := ⟨_, _⟩

[Gabriel Ebner]

But this kind of synonyms don't really help for the issues we have in mathlib. For example, if you want two vector spaces over the same field, then [VectorSpace V1] [VectorSpace V2] does not help you. You need to be able to say that they have the same field structure:

def foo {K V1 V2} [Field K] [VectorSpace K V1] [VectorSpace K V2] := ...

[Gabriel Ebner]

(deleted)

[Johan Commelin]

But will it help for [topological_ring R]?
Currently that is: {R : Type*} [ring R] [topological_space R] [topological_ring R]

[Gabriel Ebner]

Maybe we should say this explicitly: topological_ring R is actually @topological_ring R _inst_1 _inst_2.
Similarly vector spaces also have the field as an instance argument.

[Johan Commelin]

Right, but actually in your vector space example, it's similar. vector_space K V should only introduce the K if it isn't known yet. (Note that the K is an explicit argument right now, in mathlib.)

[Yury G. Kudryashov]

How should the basic algebraic hierarchy work with the new structure cmd?

[Yury G. Kudryashov]

E.g., currently src#comm_group extends src#group and src#comm_monoid

[Gabriel Ebner]

How about?

class monoid (α) extends has_mul α
class group (α) extends monoid α
class commutative (α) [has_mul α]

class comm_monoid (α) extends monoid α, commutative α
instance [monoid α] [commutative α] : comm_monoid α

class comm_group (α) extends group α, commutative α
instance [group α] [commutative α] : comm_group α

[Kevin Buzzard]

And how does topological ring look?

[Sebastien Gouezel]

A possibility would be to have the following:

• We have syntatic classes [has_zero α], [has_one α], [has_add α] and so on
• No class extends these, they take them as instance parameters. In other words, other algebraic classes only have Prop in them
• This would mean that to declare a ring R, we would need [has_zero R] [has_one R] [has_add R] [has_mul R] [ring R], which is unbearable. Introduce a new kind of instance declaration [[ring R]] (or with beautiful unicode) that adds missing instances to the context (but only missing instances, i.e., if there is already a [has_zero R] it wouldn't add it).

This would solve the old type/new type structure, as the problem with new type structures is only with shared data field, that would be (shared) instance parameters now. And it would be a progress over what we have even now: to define a topological group G, one needs currently to write [group G] [topological_space G] [topological_group G], and it could be replaced with [[topological_group G]]. The gain for Lie groups, as @Patrick Massot was mentioning, would be even bigger.

Of course, I have no idea how hard it would be to implement this, but it doesn't seem crazy: Lean can already can tell us which instances are missing.

[Jalex Stark]

I guess one can try to write the new kind of instance declaration already, without refactoring things into syntax and props

[Mario Carneiro]

My 2c: let's not radically change the entire algebraic hierarchy during the port

[Mario Carneiro]

see also https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/XenaProject.20blog.20posts/near/204514809

[Mario Carneiro]

I think we should just try to recreate old_structure_cmd, either manually (writing all the fields out) or via a tactic or attribute

[Mario Carneiro]

I don't think it deserved to get deprecated in the first place, much less removed

[Scott Morrison]

We could radically change the entire algebraic hierarchy _before_ the port. :-)

[Scott Morrison]

But let's finish the current bundled/unbundled project first.

[Sebastien Gouezel]

Wouldn't this also solve many problems with diamonds for which Lean has a hard time figuring out that they're defeq, as Prop diamonds are obviously defeq without unfolding anything?

[Sebastian Ullrich]

Mario Carneiro said:

I think we should just try to recreate old_structure_cmd, either manually (writing all the fields out) or via a tactic or attribute

Oh I agree completely; it might be sufficient to build a slighty more rudimentary version when switching away from it is planned anyway, but porting must be as automated as possible to succeed.

[Mario Carneiro]

I remain unconvinced that something much different than the current structure is going to solve mathlib's problems better than what we already have. Any alternatives need to be tested on at least medium scale (involving class definitions, generic theorems, instance constructions and applications of general theorems to specific instances) and quantitatively compared to the status quo. There are just too many ideas to try and a high switching cost, so I don't want to move in another direction until we have concrete evidence it's going to be better when we get there

[Patrick Massot]

Mario, did you read Cyril's paper (the hierarchy builder one, not the forgetful inheritance one)? I only had a very quick look at the pdf on my phone in addition to attending his Pittsburgh talk, but it seems very sensible. It really sounds right to me that we need an abstraction layer here, hiding the actual implementation as much as possible, and putting alternate constructors on the same footing as the constructors coming from the actual implementation. Going beyond that paper, I think all this tricky business of deciding what should be a parameter and what should be extended should be completely hidden from users. We should have some meta-program reading a mathematical description of structures and doing all the tricky stuff, including defining bundled versions, morphisms and subobjects.

[Patrick Massot]

Such a think is necessarily part of the future of proof assistants, together with the proof automation tools, if proofs assistants want to ever become a common and useful tool for mathematics.

[Mario Carneiro]

I think that ideas are cheap and effective implementation in the context of a real library is much more expensive

[Patrick Massot]

Do you really intended to write publicly that mathcomp is not a real library?

[Mario Carneiro]

A good idea is only the first stage. Compare it to a drug trial

[Patrick Massot]

Because it seems that Cyril's stuff has already been tested at this scale (or maybe I read too quickly).

[Patrick Massot]

And I never wrote this was easy. I wrote this is necessary. Maybe it will never happen, and then proof assistants will never be usable.

[Mario Carneiro]

Also keep in mind that these decisions are very sensitive to details of the underlying architecture. The fact that typeclass inference in lean 4 is going to be cheaper will already significantly change the calculus, and we may find some other approach, using more typeclasses, performing better

[Patrick Massot]

Cyril and his coauthors claim that there stuff is not even sensitive to whether you use unification hints or type classes (although their implementation is obviously full unification hints).

[Johan Commelin]

That means that you might choose a different implementation that translates the abstract description of the hierarchy to Lean 4 code

[Rob Lewis]

I don't think the hierarchy builder is used in mathcomp releases yet (which I don't say to make any claim about its effectiveness!).

[Patrick Massot]

I certainly don't expect such a tool to reach the mathcomp release stage in less than a couple of years. That's not really the mathcomp speed I think.

[Patrick Massot]

It doesn't mean they didn't recreate the full mathcomp hierarchy using it.

[Mario Carneiro]

Even if it gets deployed in mathcomp, that doesn't say much about whether it will do well in lean 3 mathlib, or lean 4 mathlib. These are different environments and need separate testing

[Mario Carneiro]

To emphasize, I'm not making any judgment of the effectiveness of the idea. I'm saying that we will not know whether it works in lean until we try it in lean

[Mario Carneiro]

I agree that alternate constructors should not be second class citizens. I see this as a flaw in lean 3 that can hopefully be addressed in lean 4, but it doesn't require any hierarchy changes

[Sebastien Gouezel]

Just having [[topological_group G]] mean "introduce all the instances that are missing to make sense of [topological_group G]" (here [group G] and [topological_space G]) would make things way less verbose, and it doesn't require any change to the current hierarchy.

[Mario Carneiro]

There was an old lean PR about this

[Mario Carneiro]

leanprover/lean#1522

[Patrick Massot]

Mario Carneiro said:

I think that ideas are cheap and effective implementation in the context of a real library is much more expensive

Mario, just in case Cyril or his coauthors ever read this thread, could you clarify whether this is a comment on my general assertion that something like their work is needed or your assessment of their published paper on this topic?

[Mario Carneiro]

Neither, it's even more general than that. Any idea at all that has aspirations to replace mathlib's algebraic hierarchy requires evidence that it is going to work beforehand because it's a huge project

[Mario Carneiro]

and evidence that it works in Coq doesn't suffice here because Coq is not lean, it differs in many technical details that matter for the determination

[Mario Carneiro]

Looking at Cyril et al's hierarchy builder paper, it looks like a boilerplate elimination tactic for declaring a mathcomp style hierarchy. We could certainly have a boilerplate elimination tactic for declaring a mathlib style hierarchy, but this seems to have a large overlap with what lean's native structure command already does, and I don't think that the mathlib hierarchy actually has all that much boilerplate to eliminate

[Mario Carneiro]

If we start writing flat structures by hand because leo doesn't want to support them anymore, well that will be some boilerplate that we will want to eliminate (although actually we already know that it's not as simple as this because subclasses can often prove fields of superclasses)

[Yury G. Kudryashov]

It would be nice to have some meta program generating sub* structures, or at least boilerplate theory (complete_lattice, map, comap).

[Mario Carneiro]

I think there is a general theory of such structures (universal algebra? varieties?) that can be put into a tactic to do this kind of thing

[Mario Carneiro]

It might be good to define the general theory even if it's a little hard to instantiate (for example, you provide a signature for the language and a family of equations) so that we can apply it manually and then eventually with tactics

[Johan Commelin]

Note that @Fabian Glöckle wrote a large part of such a meta program already

[Johan Commelin]

It can generate bundled homs and concrete category instances as well.

[Yury G. Kudryashov]

Note that we want to reuse our bundled homs for groups.

[Mario Carneiro]

it's little things like that that make me dubious about boilerplate eliminating tactics in general

[Mario Carneiro]

because when you look carefully, it's not actually boilerplate, it's just slightly lower entropy text

[Mario Carneiro]

and capturing the patterns while allowing all the variations can be much more complicated than the original boilerplate

[Utensil Song]

Scott Morrison said:

But let's finish the current bundled/unbundled project first.

Where can I learn more about "the current bundled/unbundled project"?

[Jalex Stark]

see e.g. #3321

[Scott Morrison]

The basic goal is to delete the files under src/deprecated/. That's too much to do all in one go, so that idea is to find places where we can reduce dependencies on these files.

[Scott Morrison]

Additionally, someone still needs to write subring, folllowing the model of subsemiring, and move the current file about is_subring into deprecated/.

[Yury G. Kudryashov]

And subfield!

[Kevin Buzzard]

I might have a student working on subring -- I'll report back today

[Patrick Massot]

I haven't been paying attention to this bundling fashion. Is there any place to read about the goals of all this? In particular, how does the bundled subgroup perform in the third isomorphism grand challenge?

[Kevin Buzzard]

If the challenge is just to formalise the 3rd isom theorem, we have it now (using bundled subgroups and bundled normal subgroups) in the group theory game (which is not a game at all right now, it's just an independent formalisation of the basics of group theory in Lean). It's here