Zulip Chat Archive

Stream: general

Topic: 3.7 and maths


Kevin Buzzard (Mar 07 2020 at 12:25):

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 (Mar 07 2020 at 12:43):

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 (Mar 07 2020 at 12:44):

ooh, a release schedule

Sebastian Ullrich (Mar 07 2020 at 12:55):

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 (Mar 07 2020 at 12:59):

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

Simon Hudon (Mar 07 2020 at 20:30):

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

Kevin Buzzard (Mar 07 2020 at 20:59):

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

Simon Hudon (Mar 07 2020 at 21:23):

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 (Mar 07 2020 at 21:24):

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

Reid Barton (Mar 07 2020 at 23:40):

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

Sebastian Ullrich (Mar 08 2020 at 10:44):

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 (Mar 08 2020 at 11:12):

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 (Mar 08 2020 at 11:13):

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 (Mar 08 2020 at 12:07):

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 (Mar 13 2020 at 01:13):

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 (Mar 13 2020 at 07:48):

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


Last updated: Dec 20 2023 at 11:08 UTC