Upstream to Mathlib

Stream: Equational

[Pietro Monticone]

I am golfing and upstreaming some of our code to Mathlib.

I'm prefixing all the Mathlib branches with EquationalTheories/ and adding the sentence "Upstreamed from the EquationalTheories project." to make sure they're findable when we need to mention them in the paper.

[Pietro Monticone]

Opened #17971

[Pietro Monticone]

Opened #17973

[Pietro Monticone]

Opened #17976

[Pietro Monticone]

Opened #17977

[Shreyas Srinivas]

Sounds like this should be brought up on the mathlib channel

[Shreyas Srinivas]

(deleted)

[Pietro Monticone]

Here it is #mathlib4 > Upstream from the EquationalTheories Project .

For archival purposes I'll keep posting here too.

[Pietro Monticone]

If you want to keep track of the ET-related Mathlib PRs, see here.

We have also added it to the Wiki homepage and in the plan of the paper together with the LeanBlueprint ones.

[Michael Bucko]

Pietro Monticone schrieb:

Opened #17971.

Can this be somehow seen as Set:Action:Modify:Preserve-Bijection? (or JS-wise OnSetModify (Preserve Bijection)?)

[Pietro Monticone]

All of the above Mathlib PRs have been merged.

[Alex Meiburg]

Opened #19618

[Alex Meiburg]

And opened #19695

[Bernhard Reinke]

Opened #22507

[Bernhard Reinke]

Opened #22510

[Bernhard Reinke]

Opened #22511

[Bernhard Reinke]

Opened #22513

[Bernhard Reinke]

Opened #22639

[Bernhard Reinke]

This one was a bit too big so I decided to split it into some smaller PRs, see #PR reviews > #22639 (cyclically) reduced words @ 💬 here.

[Bernhard Reinke]

@Joachim Breitner, could you maybe have a look at them? I get you as a suggested reviewer on GitHub

[Joachim Breitner]

It’s been a long time that I touched that code; I’d rather not get involved in mathlib pr reviewing at the moment, sorry.

[Bernhard Reinke]

No worries!

[Pietro Monticone]

(deleted)

[Pietro Monticone]

(deleted)

[Pietro Monticone]

(deleted)

[Pietro Monticone]

I’ve just realised that some declarations had already been upstreamed. Please either add a comment with the [UPSTREAMED]: PR LINK tag or remove the declaration from the related Mathlib or ForMathlib subfolders. Thanks!

[Bernhard Reinke]

Oh, when I asked about this I was told it wasn't necessary #Equational > Finishing the formalization of anti-implications @ 💬

Where do you want it to be added? As a PR to the bump PR?

[Pietro Monticone]

Yes, as a PR to the bump PR would be totally fine. Thanks!

[Shreyas Srinivas]

Bernhard Reinke said:

Oh, when I asked about this I was told it wasn't necessary #Equational > Finishing the formalization of anti-implications @ 💬

Where do you want it to be added? As a PR to the bump PR?

Back then we were still finishing the anti implications. Now it makes sense to keep the project toolchain up to date.

[Bernhard Reinke]

Ok, here is equational#1226. There is one PR that is in up-to-date mathlib, but not in the one where we are bumping to. I marked the corresponding lemmas accordingly. In principle I could also try to make the version of ReducedWords.lean correspond more to the PR #23368 that is still under review

[Pietro Monticone]

Thanks! Merged.

[Alex Meiburg]

(deleted)

[Pietro Monticone]

Opened bump PR (equational#1229) to remove the declarations and files upstreamed by @Bernhard Reinke (#23367).

[Bernhard Reinke]

The upstreaming of our lemmas for free groups is almost done, see #27679. Once this is merged to mathlib, does it make sense to bump Mathlib again or should we keep it at v4.20?

[Pietro Monticone]

I’d personally avoid bumping Mathlib at this stage. It would probably be quite painful and bring very little, if any, concrete benefit.

[Bernhard Reinke]

Yeah, makes sense

[Kevin Buzzard]

In my experience, projects which depend on mathlib, once they are finished, sometimes go through a "let's keep everything up to date" phase where people try and keep up with mathlib, especially if there are things in the repo which people actively want to get into mathlib, but after a while people just lose interest if the project has achieved its main objective and the paper is written, and then the code rots (in the weak sense that bumping mathlib gets harder -- the code still compiles!). So perhaps the real question here is "what (if any) code in this project should be in mathlib but isn't, and is there a plan to get it there"? Once all the code which should be upstreamed is upstreamed, it's not clear (at least to me) what the motivation is to keep the code up to date with mathlib; the project will always compile (at least in theory) because the whole point of the system files like lakefile.toml and in paticular lake-manifest.json is to tell the system which versions of lean/mathlib to use if you want to compile locally.

[Shreyas Srinivas]

I am going to create an artefact out of whatever state the repository is in when we upload the preprint. If there are any updates that we want in the review artefact, it should ideally be done now (next 2 days)

[Terence Tao]

In the long term we do need to figure out a way to create cryptographic hashes or other condensed versions of formalized theorems that can actually be imported into other repositories that use a different version of Mathlib than the one used to prove the theorem, as per #general > Minimally exporting a theorem from a repository . But for this particular repository the upside of further Mathlib maintainance is indeed low, though I could see the ETP being forked at some point for some further mathematical exploration, at which point it makes sense to bump the fork.

[Shreyas Srinivas]

Basically you would have to create a merkle tree for the theorem. The problem is, anything inferred (such as implicit args or typeclasses) would be hard to detect.

[Cody Roux]

This is, I suspect, a stupendously hard problem.

[Alex Meiburg]

I don't think it should be a "stupendously hard problem". In principle all you need is to add a hash to every constant added to the environment, that checks hashes of constants it depends on. This is actually quite similar to how #print axioms is propagated internally. Then you could #print hash mainTheorem. That would be pretty easy, and a way to check that the hashes of two constants match (they're the same mathematical content).

Then you could make a very minified version of your result with only the necessary declarations to state it, and this would be a vastly more portable version. Automatically generating such a statement would be trickier but should be perfectly doable I think.

What would be extremely hard would be adapting to any changes in the definitions. For instance, I recently split out docs#AddZeroClass into docs#AddZero, in Mathlib. This means that (for instance) any mathematical statement about any additive monoid would now have a different signature after a Mathlib upgrade, so hashes would change. I don't see any feasible way to adapt to this.