Re: backporting ofNat from Lean 4

Stream: general

[Gabriel Ebner]

As many of you will have heard by now, numerals in Lean 4 look quite a bit different than in Lean 3. In Lean 3, numerals were constructed from 0, 1, and addition. In Lean 4 there is now a function ofNat : Nat → α which embeds the natural numbers into the desired type. (Actually it's a tad more complicated than that: the type class is OfNat α n, which means that a type may only have some but not all numerals...)

Effectively this means that in mathlib4 we now have these type classes:

class Zero (α : Type u) where zero : α
class One (α : Type u) where one : α
class Numeric (α : Type u) where ofNat : Nat → α

class Monoid (α : Type u) extends One α, ...
class Semiring (α : Type u) extends Numeric α, ... -- but not `One α` or `Zero α`

This works mostly well and doesn't result in any weird diamonds. The only downside is that Semiring no longer extends Monoid, so you have to type all properties by hand (i.e. Semiring only extends Semigroup and AddSemigroup directly, because they don't reference 0/1). In mathlib4 that's perfectly workable because the algebraic hierarchy is still very coarse, and we have few theorems.

After some prodding by @Alex J. Best I've tried to backport this change (i.e. the numeric type class) to mathlib. Mathlib has a dozen ring-link structures each inheriting from various different subsets of additive/multiplicative structures. Then there's a corresponding cornucopia of function.injective and function.surjective functions. Typing the properties by hand is not really scalable. Some potential solutions I have thought of:

1) Make a separate hierarchy for the numeric-based classes. This is what I've tried so far. It is ugly but potentially automatable in Lean 4. Doing this by hand in Lean 4 is annoying though (because you have to define monoid, add_monoid, monoid', and add_monoid'). Concretely, create classes like this (where has_zero and has_one are replaced by numeric):

@[ancestor numeric has_mul, protect_proj]
class mul_one_class' (M : Type u) extends numeric M, has_mul M :=
(one_mul : ∀ (a : M), 1 * a = a)
(mul_one : ∀ (a : M), a * 1 = a)

Then semiring & co. can extend monoid_with_zero' instead of monoid_with_zero.

2) Patch Lean 3 and Lean 4 so that class Foo (α) extends Numeric α, Zero α works magically, i.e., Foo only contains ofNat, but not zero. Bikesheddable syntax (the semantics is similar to default fields, but of course completely different):

class Numeric (α : Type u) where
  ofNat : Nat → α
  let zero := ofNat 0
  let one := ofNat 1

3) Define the algebraic hierarchy in terms of unbundled is_group classes. Something like this:

class is_add_comm_monoid (α : Type u) [has_zero α] [has_add α] [has_nsmul α] : Prop extends is_add_monoid α, is_add_zero_class α :=  ...
class add_comm_monoid (α : Type u) extends has_zero α, has_add α, has_nsmul α, is_add_comm_monoid α
class semiring (α : Type u) extends numeric α, ..., is_add_comm_monoid α, ...

This allows some degree of reuse because is_add_comm_monoid R is defeq no matter whether you're talking about the underlying additive monoid, or the semiring itself.

I'm happy for any comments or ideas. There's probably unclear parts here, I'll gladly elaborate.

Frequently asked questions:

• Why don't we just make semiring extend both numeric and has_zero and a proof that 0 = 0? Because that's a type class diamond which we want to avoid.
• Why don't we just leave numeric out of semiring? Because then you can't state docs#char_two.two_eq_zero

[Reid Barton]

If we have OfNat α 1 then why do we also need a separate One α?

[Gabriel Ebner]

That's just a technical subtlety. class MonoidWithZero (α) extends OfNat α 0, OfNat α 1 doesn't work by itself (you get two ofNat fields with different types), so we need to add aliases. Lean 4 can infer OfNat α 0 from Zero α and vice versa though.

[Johan Commelin]

Does (3) lead to the exponential blowup in term sizes that is explained in a famous blogpost that I cannot find right now?

[Johan Commelin]

Oh, here it is: https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html

[Johan Commelin]

To my naive eye, (2) seems the most promising.

[Yury G. Kudryashov]

We can also move only numeric/has_one/has_zero from fields to args

[Reid Barton]

I don't really understand what is going on here but my gut reaction is that it is all very confusing.

[Reid Barton]

Gabriel Ebner said:

That's just a technical subtlety. class MonoidWithZero (α) extends OfNat α 0, OfNat α 1 doesn't work by itself (you get two ofNat fields with different types), so we need to add aliases. Lean 4 can infer OfNat α 0 from Zero α and vice versa though.

It seems like this is the natural place to fix things

[Yury G. Kudryashov]

Even if you fix this, extending Monoid, AddMonoid, and Numeric without some very special support from the language (see solution 2) will create conflicting projections

[Yury G. Kudryashov]

One will say "we have any numeral", another will say that we have numeral zero

[Reid Barton]

Maybe we should also include option 0: Semiring does not extend Numeric

[Yury G. Kudryashov]

How numerals in semirings should work then?

[Johan Commelin]

Related to Reid's option 0: Is there an OfInt α (-2)? And will Ring need to extend some int-version of Numeric?
If Ring doesn't extend IntNumeric, why should Semiring extend Numeric?

[Reid Barton]

Yury G. Kudryashov said:

How numerals in semirings should work then?

A general instance recreating the old behavior? It's not great, but sounds better than SemiRing not extending Monoid at least

[Anne Baanen]

The reason that Semiring has to extend Numeric is that we want ofNat : ℕ → ℕ to be defeq to the identity function, right?

[Johan Commelin]

@Reid Barton Why is it a problem if Semiring doesn't extend Monoid? There will always be an instance, right?

[Yury G. Kudryashov]

I guess, -2 works as -(ofNat 2). Am I right?

[Gabriel Ebner]

That's just a technical subtlety. class MonoidWithZero (α) extends OfNat α 0, OfNat α 1 doesn't work by itself (you get two ofNat fields with different types), so we need to add aliases. Lean 4 can infer OfNat α 0 from Zero α and vice versa though.

It seems like this is the natural place to fix things

Please ignore this part of the issue. This is just a distraction. There's absolutely no problem here.

[Eric Rodriguez]

why can't we just have OfNat α 0 instead of Zero α?

[Gabriel Ebner]

Does (3) lead to the exponential blowup in term sizes that is explained in a famous blogpost that I cannot find right now?

Jung describes a different encoding, namely one where we'd have group [div_inv_monoid α] : Prop. Option 3 should not lead to exponential blowup.

[Gabriel Ebner]

why can't we just have OfNat α 0 instead of Zero α?

Again, this is absolutely not the issue here. Please replace Zero α by OfNat α 0 in the examples if it helps you.

[Johan Commelin]

Ok, cool. But we would still need to write

variables {A : Type*} [has_zero A] [has_add A] [scalar ℕ A] [add_group A]

just to say "A is an additive group".
If some syntax can make that easier/shorter, than (3) seems like a good option to me.

[Gabriel Ebner]

Option 3 (in my original post) would have two hierarchies, the is_add_group hierarchy and the add_group hierarchy. And we'd have:

class add_group (A) extends has_zero A, has_add A, ..., is_add_group A

[Johan Commelin]

Ah, and because Lean 4 doesn't care about cycles in the TC graph, this just works like a charm?

[Gabriel Ebner]

(deleted)

[Eric Rodriguez]

Johan Commelin said:

Ok, cool. But we would still need to write

variables {A : Type*} [has_zero A] [has_add A] [scalar ℕ A] [add_group A]

just to say "A is an additive group".
If some syntax can make that easier/shorter, than (3) seems like a good option to me.

I mean, I think something to help alleviate this would still be nice; I remember Anne proposed a [[my_class A B C]]that expands this out into all the required TC arguments

[Gabriel Ebner]

(deleted)

[Gabriel Ebner]

Ah, and because Lean 4 doesn't care about cycles in the TC graph, this just works like a charm?

The only instance this declares is add_group A → is_add_group A so there's no cycle.

[Reid Barton]

I think why your comments are confusing me is that I would just put OfNat 0 in AddGroup, OfNat 1 in Monoid and extend both in Ring and call it a day.

[Gabriel Ebner]

Then you don't have numeric instances for rings, i.e. (42 : R) doesn't work.

[Reid Barton]

I wonder if that is a real problem?

[Gabriel Ebner]

We have enough lemmas that contain numerals > 1.

[Floris van Doorn]

So is it possible to only have OfNat 0 and OfNat 1 inside Ring and then manually define the instance OfNat n?

One problem is that ofNat : ℕ → ℕ using this instance is not defeq to the identity function (mentioned by @Anne Baanen). Is that a big issue? A simple simp lemma will mostly fix this.

Are there other problems?

[Eric Rodriguez]

maybe the correct way to do this is to make them arguments, e.g. class Monoid (α) [ofNat α 1] extends ..., class Ring (α) [∀ n, ofNat α n] extends Monoid α, ..., or does this not work for subtle reasons?

[Eric Rodriguez]

currently, I guess this means you'd need to type [ofNat α 1] [Monoid α], but with Anne's proposal that should be pretty painless

[Anne Baanen]

(I don't want to take too much credit for that, it's just Coq's `{}.)

[Eric Rodriguez]

(I'm just excited for it instead of the pages-long variables we have to write sometimes now!)

[Anne Baanen]

Could you remind me why we didn't go for accepting a Zero α → OfNat α 0 and Semiring α → OfNat α 0 diamond?

[Mario Carneiro]

If Semiring implies AddMonoid which implies Zero, then there are two definitely not defeq ways to write 0 in a generic semiring

[Mario Carneiro]

we would at least need an equality theorem

[Anne Baanen]

Wouldn't that go away if we replace extends with a custom instance Semiring.ToAddMonoid which sets zero := ofNat 0?

[Anne Baanen]

Or would disinheriting Semiring → Monoid mess up diamond inheritance so we can't say Ring extends Semiring, Group?

[Mario Carneiro]

It would, but I'm not sure how important that is

[Sebastian Ullrich]

Floris van Doorn said:

One problem is that ofNat : ℕ → ℕ using this instance is not defeq to the identity function (mentioned by Anne Baanen). Is that a big issue? A simple simp lemma will mostly fix this.

And applied to any specific Nat they should hopefully be defeq after all. Is that not the (only) important use case?

[Mario Carneiro]

I think that will not be good, we don't want 27 : Nat to have to build it up in binary if we can just inject the literal 27. This could potentially affect LLVM optimizations if it can't work out the value of the constant

[Sebastian Ullrich]

The generic instance should probably have lower priority than the specific one. I would be surprised if you instantiated generic literals to Nat often enough to create noticeable overhead in compile or run time.

[Yury G. Kudryashov]

What are we going to use for coercion from nat?

[Sebastian Ullrich]

What do you use in Lean 3? If it is not the identity function for Nat there either, I don't see a reason to change it, so it should be distinct from OfNat.

[Yury G. Kudryashov]

I can imagine that some algorithm is written for any semiring (possibly, with extra requirements) and involves coercion from nat. When it is applied to nat, we probably want this coercion to go away

[Yaël Dillies]

It's docs#nat.cast and docs#nat.bin_cast

[Yaël Dillies]

nat.cast is pretty dumb indeed

[Sebastian Ullrich]

For the run time use case, this should eventually be covered by compiler rewrite rules. Which are not implemented yet, but their lack should probably not influence how you want to model your algebraic hierarchies too much.

[Sebastian Ullrich]

Regarding the subtopic of the additive/multiplicative split, I opened a new thread in #lean4 with a perhaps naive alternative approach making use of new Lean 4 features https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Additive.2Fmultiplicative.20split.20in.20Lean.204/near/269595572

[Gabriel Ebner]

The generic instance should probably have lower priority than the specific one. I would be surprised if you instantiated generic literals to Nat often enough to create noticeable overhead in compile or run time.

From what I remember, Joe Hendrix stopped using mathlib because of this computationally problematic nat.cast instance. So I'd really like to avoid it.

[Gabriel Ebner]

A simple simp lemma will mostly fix this.

Then some simp lemmas will no longer apply to natural numbers. For example, 2 | a ↔ even a will work for every type, except the natural numbers (and other types that have a custom ofNat function).

[Gabriel Ebner]

And applied to any specific Nat they should hopefully be defeq after all. Is that not the (only) important use case?

I had hoped we could eventually use the same function for coercions as well to get rid of nat.cast. For actual numerals alone, a low-priority OfNat instance doing nat.cast could work.

[Gabriel Ebner]

If it is not the identity function for Nat there either, I don't see a reason to change it, so it should be distinct from OfNat.

The coercion Nat → α is an ongoing minor issue (with associated VM performance issues and diamonds), so there's certainly a good reason to change it.

[Gabriel Ebner]

so it should be distinct from OfNat.

Okay let's call this option 4). We have all three of 0, 1, and ofNat. Numerals are built from 0, 1, +. And ofNat is only used for coercions.

class Semiring (α) extends AddCommMonoid α, Monoid α, Numeric α, ...
instance (priority := low) [Semiring α] : OfNat α n := -- constructed from 0, 1, +
instance [Numeric α] : CoeTail Nat α := ⟨ofNat⟩

It's somewhat disappointing that Numeric.ofNat n and OfNat.ofNat n are not defeq, but it's a much smaller issue than 1 or 3.

[Sebastian Ullrich]

It's not perfect, but a separate class also feels more appropriate because there is no need for the n type parameter for this use case

[Gabriel Ebner]

Okay, I've implemented option 4) in mathlib4. https://github.com/leanprover-community/mathlib4/pull/177 The performance issues are real, avoid (123456 : R) for now.

[Gabriel Ebner]

I've also removed the coercion ℕ → R for semirings R for performance reasons. How about adding the following type class to mathlib3, and replacing nat.cast?

class cast_nat (α : Type u) extends has_zero α, has_one α, has_add α :=
(cast_nat : ℕ → α)
(cast_nat_zero : cast_nat 0 = 0)
(cast_nat_succ : ∀ n, cast_nat (n + 1) = cast_nat n + 1)

I'm also happy about other values of cast_nat 1.

[Yakov Pechersky]

And a low prio default instance that uses nat.bin_cast?

[Gabriel Ebner]

No, we'd bundle it in semiring and co. so cast_nat would be available anywhere we'd need it. Having a second non-defeq instance only introduces a diamond.

[Eric Rodriguez]

if we're allowing other values of cast_nat 1, should we have cast_nat (n + 1) = cast_nat n + cast_nat 1?

[Gabriel Ebner]

I meant that there are two reasonable values we could specify for cast_nat 1, either 0 + 1 or 1. These are of course not equal in general.

[Gabriel Ebner]

And yes, cast_nat (n + 1) = cast n + 1 would not be true with cast_nat 1 = 1. (But it would be true for semirings, and in general we'd have cast_nat (n+2) = cast_nat (n+1) 1.)