auto bundling

Stream: general

[Johan Commelin]

I'm wondering if we can somehow bridge the gap between bundled and unbundled classes. Let's take Top as an example. If I have X : Top, and I want to apply a lemma from the library to X, then this will usually work. The lemma is written with assumptions {X : Type*} [topological_space X], and Lean can figure out how to fill them in. It has a coe_to_sort that turns X into a type, and a type class search will figure out the topological_space instance.
The other direction is currently not so easy. If we have and X : Type* and an instance [topological_space X] it is not so user-friendly to apply a lemma that assumes a Top (for example a generic lemma from the category library). One has to manually bundle everything up using \< X, by apply_instance \>. I would like to be able to just write 🗃 X and move on. This becomes especially nice if the bundling takes more than one instance (for example topological groups). The 🗃 would flag to Lean that it should first infer the expected type of the argument. The user "promises" that this type is a structure that contains exactly one data field. In this field Lean should plug X. All the other fields will be Props, and Lean should figure them out using apply_instance.
I have no idea whether this proposal makes any sense. I fear that it is impossible to implement this in Lean 3.4.2. I hope it will be possible in some future version of Lean...

[Scott Morrison]

It's not that hard to build a Top. You can just write Top.of X, and typeclass resolution finds the instance.

[Johan Commelin]

I still think that we are drifting away from the beautiful and concise notation that we have in regular maths

[Johan Commelin]

I would like to stay as close as possible to that notation. Inserting a single crazy symbol (an arrow, or an emoji) that is the same for every category, seems to get closer to that ideal than having foo_bar.of for every category.

[Johan Commelin]

I would like to have a has_of class.

[Johan Commelin]

But that seems to be impossible with current tech.

[Scott Morrison]

Multiple typeclasses are not a problem:

noncomputable example : TopCommRing := TopCommRing.of ℂ

[Mario Carneiro]

Please don't replace useful words with emoji

[Johan Commelin]

Please don't replace useful words with emoji

Why do you replace coe with an arrow?

[Mario Carneiro]

I find myself peering closely at :archive: trying to figure out what it is

[Mario Carneiro]

Oh

[Johan Commelin]

Or int.add with +?

[Mario Carneiro]

Coe is supposed to be invisible, but when you need to know it's there it's best to have a minimally invasive symbol

[Johan Commelin]

That

[Mario Carneiro]

+ is not even a reasonable example

[Johan Commelin]

That is exactly how I want autobundling to behave

[Johan Commelin]

It should be invisible

[Mario Carneiro]

It should be coe

[Johan Commelin]

It can't be

[Mario Carneiro]

that's lean's fault

[Mario Carneiro]

the solution is not more crazy notation

[Johan Commelin]

Can we fix this in Lean 3.4.2 with crazy notation?

[Mario Carneiro]

not generically

[Johan Commelin]

Can we easily fix this in Lean 3.5c without crazy notation?

[Mario Carneiro]

it's not on the todo list

[Mario Carneiro]

changing how coe works would I think be worthwhile but would also change a lot of stuff

[Johan Commelin]

I want to be able to have (R : Top) [comm_ring R] [topological_ring R] and then write (R : TopCommRing), and Lean should just be able to figure out what I mean.

[Mario Carneiro]

I know

[Johan Commelin]

Is it reasonable to expect that this will become better in Lean 4?

[Mario Carneiro]

I don't think it's changed but I could be wrong

[Johan Commelin]

Because I think that bundling-unbundling and transfer are the two biggest hurdles to making Lean usable for advanced math

[Mario Carneiro]

It doesn't sound like it's so hard currently

[Reid Barton]

Replying to the original message in this thread: In my experience (which might depend on the subject domain), it's not actually that frequent that one needs to go in the bundling direction if the library is structured to work with bundled objects in general. (I mean your own constructions/lemmas should take as input a bundled (X : Top).) Basically you need to bundle once per primitive object (e.g., the reals) or construction (e.g., product space or subspace with the induced topology) and then you're set. In contrast, the other direction (coercing Top to Type*) gets used all over the place.
https://github.com/rwbarton/lean-homotopy-theory/search?q=mk_ob&unscoped_q=mk_ob should give some sense of what I mean