Zulip Chat Archive

Stream: general

Topic: auto bundling


Johan Commelin (May 23 2019 at 06:55):

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 (May 23 2019 at 06:56):

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

Johan Commelin (May 23 2019 at 06:57):

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

Johan Commelin (May 23 2019 at 06:58):

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 (May 23 2019 at 06:58):

I would like to have a has_of class.

Johan Commelin (May 23 2019 at 06:58):

But that seems to be impossible with current tech.

Scott Morrison (May 23 2019 at 06:58):

Multiple typeclasses are not a problem:

noncomputable example : TopCommRing := TopCommRing.of â„‚

Mario Carneiro (May 23 2019 at 06:59):

Please don't replace useful words with emoji

Johan Commelin (May 23 2019 at 06:59):

Please don't replace useful words with emoji

Why do you replace coe with an arrow?

Mario Carneiro (May 23 2019 at 06:59):

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

Mario Carneiro (May 23 2019 at 07:00):

Oh

Johan Commelin (May 23 2019 at 07:00):

Or int.add with +?

Mario Carneiro (May 23 2019 at 07:01):

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 (May 23 2019 at 07:01):

That

Mario Carneiro (May 23 2019 at 07:01):

+ is not even a reasonable example

Johan Commelin (May 23 2019 at 07:01):

That is exactly how I want autobundling to behave

Johan Commelin (May 23 2019 at 07:01):

It should be invisible

Mario Carneiro (May 23 2019 at 07:02):

It should be coe

Johan Commelin (May 23 2019 at 07:02):

It can't be

Mario Carneiro (May 23 2019 at 07:03):

that's lean's fault

Mario Carneiro (May 23 2019 at 07:03):

the solution is not more crazy notation

Johan Commelin (May 23 2019 at 07:03):

Can we fix this in Lean 3.4.2 with crazy notation?

Mario Carneiro (May 23 2019 at 07:03):

not generically

Johan Commelin (May 23 2019 at 07:03):

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

Mario Carneiro (May 23 2019 at 07:04):

it's not on the todo list

Mario Carneiro (May 23 2019 at 07:04):

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

Johan Commelin (May 23 2019 at 07:04):

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 (May 23 2019 at 07:04):

I know

Johan Commelin (May 23 2019 at 07:05):

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

Mario Carneiro (May 23 2019 at 07:05):

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

Johan Commelin (May 23 2019 at 07:05):

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

Mario Carneiro (May 23 2019 at 07:06):

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

Reid Barton (May 23 2019 at 14:46):

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


Last updated: Dec 20 2023 at 11:08 UTC