Name collisions

Stream: Equational

[Mario Carneiro]

Currently you can't import Mathlib in equational_theories because of a name conflict on FreeMagma. Perhaps we can use namespaces more consistently?

[Terence Tao]

Huh, I had no idea FreeMagma already existed in Mathlib. Perhaps we can refactor our current code to use the Mathlib version? The label names are slightly different but its essentially the identical concept.

Perhaps it's time to have the broader discussion of how/whether to import our magma machinery to Mathlib. It seems like for the FreeMagma code at least we would need to perform the above refactoring first.

[Pietro Monticone]

Here is the related topic.

[Mario Carneiro]

I'm guessing that the FreeMagma definition in ET is incompatible with mathlib's, since it uses a different Magma definition with a custom operator instead of *

[Mario Carneiro]

src#FreeMagma

[Terence Tao]

We could import Mathlib's FreeMagma and give it an instance of Magma (which would be identical except for the operator symbol to the instance of Mul that it already has).

[Bhavik Mehta]

Mario Carneiro said:

I'm guessing that the FreeMagma definition in ET is incompatible with mathlib's, since it uses a different Magma definition with a custom operator instead of *

I think this isn't an incompatibility - as Terence says we can provide the (other) Magma instance, and because of the scopes here, there shouldn't be any problems unless those scopes are opened

[Shreyas Srinivas]

Unless someone is really willing to get into all the autogenerated folders, refactoring everything to Mathlib's variant could be a bit painful. Instead I suggest we follow what Terence says. This doesn't solve the namespace clash for which there are two solutions in greatly decreasing order of preference:

1. Namespace all project files into a namespace like EqTheories.
2. Namespace Mathlib's FreeMagma in the Mathlib namespace. I know this one is less likely to be accepted, but in general I feel Mathlib leaks too many names and symbols into the global namespace.

[Shreyas Srinivas]

I think taking every opportunity to put more Mathlib things into the Mathlib namespace makes mathlib more easily usable in the long run.

[Eric Wieser]

Terence Tao said:

We could import Mathlib's FreeMagma and give it an instance of Magma (which would be identical except for the operator symbol to the instance of Mul that it already has).

This is going to be a bit annoying, because then you need to decide whether the simp-normal form is * or the notation Magma currently uses; or you have to repeat every lemma from one spelling for the other

[Mario Carneiro]

Equational leaks quite a lot, I don't think people are following good naming practices here (because it wasn't a priority, which is fine)

[Shreyas Srinivas]

Equational is a downstream project

[Mario Carneiro]

downstream is relative

[Shreyas Srinivas]

Fwiw, I am in favour of every project being namespaced by the project's name by default.

[Mario Carneiro]

I think you mean to say it's an "endpoint project" i.e. no one is expected to be able to import it

[Shreyas Srinivas]

Mario Carneiro said:

I think you mean to say it's an "endpoint project" i.e. no one is expected to be able to import it

Yes. This is what I mean.

[Mario Carneiro]

it's generally better for endpoint projects to just use some uniform namespacing convention, because it doesn't matter as much as for mathlib

[Shreyas Srinivas]

I can open a PR to namespace mathlib's FreeMagma later in the evening. I have a talk to record now.

[Mario Carneiro]

I don't think ET has a better global claim to the name than mathlib

[Shreyas Srinivas]

Yeah, but as you said, it's an endpoint project. I just see every chance to namespace something in mathlib as an opportunity

[Mario Carneiro]

it's not though, that's a decision for mathlib maintainers

[Mario Carneiro]

and I at least would be opposed to it

[Shreyas Srinivas]

If someone wants to namespace this project that's a task I can just put up for claiming.

[Shreyas Srinivas]

Mario Carneiro said:

it's not though, that's a decision for mathlib maintainers

Agreed. But I am hoping that after the last mathlib meeting some might support it. Just a fleeting hope

[Shreyas Srinivas]

Shreyas Srinivas said:

If someone wants to namespace this project that's a task I can just put up for claiming.

This task could be a pain because all the scripts and tools that are not lean based also need fixing. I don't know how some of the visualisation tools like equation explorer andGraphiti handle errors and declaration names.

[Shreyas Srinivas]

Mario Carneiro said:

I don't think ET has a better global claim to the name than mathlib

upstream libraries being namespaced properly makes downstream use easier.

[Terence Tao]

As a narrow short term patch for the "can't import Mathlib" problem, we could just namespace Equational's FreeMagma specifically, which I think impacts relatively few Lean files and almost no autogenerated files. This could be a down payment for a more comprehensive namespacing later.

In retrospect, when we were debating what foundational definition to use for magmas, perhaps it would have had been good to go with the option to have both [Magma] and [Mul], with API to convert back and forth, and appropriate namespacing for the former, and have all the "front end" theorems of the project (such as EquationX_implies_EquationY or Facts) use our custom class [Magma] with no intention of upstreaming them to Mathlib (in particular allowing for isolating those results as standalone Lean statements with minimal imports), but all the "back end" theorems (such as the theory of free magmas) use [Mul] and other Mathlib classes, with the intention of upstreaming them to Mathlib at the end. At the time, that sounded like an overengineered option, but perhaps it would have saved us some future upstreaming headaches.

[Vlad Tsyrklevich]

Shreyas Srinivas said:

don't know how some of the visualisation tools like equation explorer andGraphiti handle errors and declaration names

They don't even see the declarations, they consume graph edges directly from lake exe extract_implications. As long as EquationXYZ isn't renamed Equational.EquationXYZ in the output I don't think anything changes for them. (Also many individual implications/non-implications are already namespaced as is.)

[Terence Tao]

Yeah, it was a good idea to have all the secondary analytic tools pass through extract_implications, this makes refactoring easier.

We implemented namespacing for implications early on to avoid collisions between different contributors. Didn't think to also do this to avoid collisions between us and Mathlib, but in retrospect that would have made a lot of sense. Maybe in our paper we can recommend using namespaces by default in downstream projects, even when there is no immediate need to do so because "everything is working fine without them"?

[Shreyas Srinivas]

I don't know. Personally I have considered the lack of at least package level namespacing by default in lean a mistake, and always used namespaces in my projects as they are.

[Shreyas Srinivas]

Secondly, upstream libraries have a moral (in the sense used in PL) responsibility to not flood the global namespace with names and symbols. Endpoint projects don't have a similar moral obligation.

[Mario Carneiro]

I think it is the role of the standard library to provide the centralized names

[Shreyas Srinivas]

yes, but it must allow end users to pick and choose

[Shreyas Srinivas]

We also had this issue with notation. I brought this up in the community meeting.

[Mario Carneiro]

no, the philosophy of mathlib is to centralize on having single definitions for things in order to maximize interoperability

[Shreyas Srinivas]

that's internal to mathlib. That can still be achieved within a "Mathlib" namespace

[Shreyas Srinivas]

External users should not be forced to jump through hoops to find names and symbols that mathlib hasn't already used

[Shreyas Srinivas]

Especially since mathlib is so large and users might only care about a fraction of it in practice and yet want to import Mathlib

[Mario Carneiro]

so it is very much by design that when we define the real numbers we stake a claim on the global name, because we want it to be a global convention to the extent we have influence over it

[Mario Carneiro]

there are other proof assistant libraries which take a different approach to things, but this is a core part of mathlib's value proposition

[Shreyas Srinivas]

One of the reasons we used \dimwwas David found it to be one of the symbols that didn't clash with anything else in mathlib (using priority for already used notation blew up CI time)

[Shreyas Srinivas]

Mario Carneiro said:

so it is very much by design that when we define the real numbers we stake a claim on the global name, because we want it to be a global convention to the extent we have influence over it

Yeah I think that's going to make it hard for downstream users to build on top of it

[Mario Carneiro]

In this case, the name collision was actually on the same object for the same purpose. It is going against the grain to define a second equivalent thing, because it's creating an island which will make interoperation harder

[Mario Carneiro]

Shreyas Srinivas said:

Mario Carneiro said:

so it is very much by design that when we define the real numbers we stake a claim on the global name, because we want it to be a global convention to the extent we have influence over it

Yeah I think that's going to make it hard for downstream users to build on top of it

No, it makes it hard for downstream users to ignore it and build their own isomorphic copy without reference to the original, which is by design

[Shreyas Srinivas]

Sometimes users want to write their own definitions by design. They are simply using mathlib but have no interest in upstreaming to Mathlib.

[Shreyas Srinivas]

I don't see why mathlib should stop anybody from doing that

[Eric Wieser]

It doesn't stop them:

import Mathlib

namespace IDontNeedYourReal
abbrev Real := Float
theorem oops : (0.1 + 0.2 : Real) = 0.3 := by sorry
end IDontNeedYourReal

[Shreyas Srinivas]

It stops them when notation is involved

[Shreyas Srinivas]

(And priority incurs build time costs)

[Shreyas Srinivas]

This conversation partially belongs elsewhere. Let's keep this thread for discussing what should be done in Equational theories.

[Shreyas Srinivas]

the task here is equational#751

[Shreyas Srinivas]

Eric Wieser said:

It doesn't stop them:

import Mathlib

namespace IDontNeedYourReal
abbrev Real := Float
theorem oops : (0.1 + 0.2 : Real) = 0.3 := by sorry
end IDontNeedYourReal

Further, while namespacing is fine, the onus should be on upstream libraries to do this and avoid forcing downstream users through hoops.

[Michael Bucko]

I think what could help future projects with interoperability and reusability (SW-wise) is an assistant that could help users make Lean software design decisions.

The good news is: v 0.1 can be done very quickly using GPTs. We can just feed a GPT with a pdf of the docs, and get it to respond, and evaluate. Eventually, the v1 could be a custom VSCode / Cursor plugin-assistant (that uses a combination of sparse and dense embeddings in the backend), or a (better) knowledge base search engine on the website.

Perhaps LeanDojo could eventually take over this responsibility? (an LLM-driven copilot for theorem proving)

Side-note: I asked ChatGPT to propose magmas and it gave me has_mul, has_add, semigroup, monoid, group. Then I checked in Cursor with Claude - it gave me Mul, Add, Semigroup, Monoid.

But I love the idea of being able to deeply integrate a valuable math project into one global math library. The deeper the integration will be, the easier it will be for future AI to create new knowledge.