3.7 and maths

Stream: general

[Kevin Buzzard]

There has been talk of changing various bits of maths in core -- e.g. the definition of a group (to remove the superfluous axiom), and Mario in another thread talking about whether singleton a should change to {x | x = a} (it is currently {x | x = a \or false}). I'm not saying these are good or bad ideas, but I did just want to make the trivial observation that it's far easier to change mathlib than core Lean (unless we're planning on having daily Lean releases) so perhaps it would just be easier to rip all of the maths we can out of core Lean and put it into mathlib? Or are there arguments against this? I have no real idea about how much maths is still in mathlib, or how much it is needed. Did the max amount of maths it's reasonably possible to rip out already get ripped out?

[Gabriel Ebner]

I don't have a strong opinion on changes in the core Lean library. It is not much harder to change core than it is to change mathlib: but it is definitely less convenient. You manually have to coordinate the changes between Lean and mathlib, while for mathlib-only changes you only need to wait for the green checkmark from the CI. But I can tell you about my plans for future Lean releases. Although we probably won't have daily releases, I am aiming for at least a release a month (if we have PRs). There will be no library changes in 3.7 to keep the mathlib porting effort reasonable. (The faster we port mathlib to 3.7, the sooner we can release 3.8.) A hypothetical singleton PR could make it into 3.8 though, which will probably be released in April.

[Mario Carneiro]

ooh, a release schedule

[Sebastian Ullrich]

Kevin Buzzard said:

so perhaps it would just be easier to rip all of the maths we can out of core Lean and put it into mathlib?

Seems sensible to me given that it will be similar to that in Lean 4. Note however that the Lean 3 C++ code (e.g. norm_num) has some dependencies on typeclasses etc, which will not be there in Lean 4.

[Patrick Massot]

I don't understand: what will not be there in Lean 4?

[Simon Hudon]

The Lean core library won't include much in the way of mathematics.

[Kevin Buzzard]

I think Patrick was probably referring to the comment about typeclasses not being there?

[Simon Hudon]

Oh! The idea for Lean 4 is to hook the automation into more agnostic type classes / indexing systems. Whereas in Lean 3, mathlib uses the notion of group defined in core, we'd be left to define our own notion of group and the Lean automation would use typeclasses like associative_operator α (+). All we have to do is to derive an instance of associative_operator from our notion of group.

[Patrick Massot]

Does it mean the indexing issues related to that kind of type classes have been solved?

[Reid Barton]

I don't think this is about things like simp, but rather ring

[Sebastian Ullrich]

Yes, or norm_num as mentioned. There is no reason to write it in C++ anymore, so it doesn't need to be part of corelib, and neither do its dependencies.

[Mario Carneiro]

I think it is about time that norm_num moved to full lean code. It's already a bit awkward that half of norm_num is implemented in c++ (addition, subtraction, multiplication) and the other half is in lean (inequality, division, modulo, primality), and the implementation of real division relies on some typeclasses that are too strong (linear ordered field instead of characteristic zero) which limits applicability.

[Mario Carneiro]

I don't think it would be a big problem if we just deleted tactic.norm_num and moved what remains to the mathlib tactic

[Gabriel Ebner]

Mario Carneiro said:

I don't think it would be a big problem if we just deleted tactic.norm_num and moved what remains to the mathlib tactic

Maybe a performance problem? In any case, we (=Mario) could reimplement norm_num in mathlib first---this doesn't require any changes in core Lean.

[Yury G. Kudryashov]

I have a feature request for Lean (3.7 or later): when you're going to resolve a class instance, would it be hard to see if it can be found by unification first? Then we would be able to remove "use unification" workarounds in algebra/group/hom.

[Gabriel Ebner]

Is https://github.com/leanprover-community/lean/pull/135 what you're looking for?