OfNat/Numeric

Stream: mathlib4

[Chris B]

With the understanding that everything is still in the feeling out phase and that core != mathlib, etc., is there a possible future in which the indexed OfNat in core has a more pleasant relationship with mathlib's Nat situation? The motivation for an OfNat that only needs to be defined on zero and/or one makes perfect sense, but after working through the new normNum my impression was that OfNat in the presence of Numeric, Zero, and One seems to cause quite a bit of paper-shuffling.

[Mario Carneiro]

I started rewriting normNum a little while ago, and I decided to not use canonical lean numerals in the inner functions anymore, because the dependent arguments lead to a lot of needless extra fluff in a performance critical area (and normNum doesn't work on fancy instances that only support some numbers and not others anyway)

[Mario Carneiro]

instead the basic proof object is a proof about

def isNat [Semiring α] (a : α) (n : ℕ) := a = OfNat.ofNat n

[Mario Carneiro]

note that n here is a raw literal

[Mario Carneiro]

so for instance it would prove that isNat (2 + 2) (nat_lit 4)

[Mario Carneiro]

and then the front end puts that back in terms of ofNat on the appropriate instance

[Chris B]

Thanks. Two follow-up questions related to the normNum discussion:

1. Do you know why, when the only variables are (A : Type) [Semiring A], typeclass inference uses @OfNat.ofNat α n (@Numeric.OfNat α n (@Semiring.toNumeric α inst)) for (n : A) when n > 1 but uses @OfNat.ofNat α 0 (@instOfNat α (@MonoidWithZero.toZero α (@instMonoidWithZero_1 α inst))) for 0 and 1? Neither instance seems to be declared with higher/lower priority.

2. What's the policy for naming/not naming certain instance declarations?

[Mario Carneiro]

Chris B said:

1. Do you know why, when the only variables are (A : Type) [Semiring A], typeclass inference uses @OfNat.ofNat α n (@Numeric.OfNat α n (@Semiring.toNumeric α inst)) for (n : A) when n > 1 but uses @OfNat.ofNat α 0 (@instOfNat α (@MonoidWithZero.toZero α (@instMonoidWithZero_1 α inst))) for 0 and 1? Neither instance seems to be declared with higher/lower priority.

That behavior makes sense if the MonoidWithZero instance is added later, since later definitions take priority over earlier ones as a tie breaker. In that case, the zero proof takes priority over the general proof, but of course the zero proof only works on zero so if the number is 2 then it will use the general proof.

[Mario Carneiro]

Chris B said:

2. What's the policy for naming/not naming certain instance declarations?

Presumably the same as lean 3: use an explicit name when the autogenerated name is not good. That instMonoidWithZero_1 instance sounds like a bad name since it's clashing with something else, so I would probably want to give it an explicit name

[Chris B]

Mario Carneiro said:

Chris B said:

1. Do you know why, when the only variables are (A : Type) [Semiring A], typeclass inference uses @OfNat.ofNat α n (@Numeric.OfNat α n (@Semiring.toNumeric α inst)) for (n : A) when n > 1 but uses @OfNat.ofNat α 0 (@instOfNat α (@MonoidWithZero.toZero α (@instMonoidWithZero_1 α inst))) for 0 and 1? Neither instance seems to be declared with higher/lower priority.

That behavior makes sense if the MonoidWithZero instance is added later, since later definitions take priority over earlier ones as a tie breaker. In that case, the zero proof takes priority over the general proof, but of course the zero proof only works on zero so if the number is 2 then it will use the general proof.

MonoidWithZero is declared before Semiring (Ring/Basic.lean imports Mathlib.Algebra.GroupWithZero.Defs), and normNum only imports the Ring module, but MonoidWithZero wins for 0 and 1.
I understand conceptually why 0 and 1 would in some cases be different, but it seems unintuitive that when you set up a context saying "I want to work with [Semiring A]" which comes with its own instance of Numeric -> OfNat that 0 and 1 suddenly find this alternate instance.

[Mario Carneiro]

I've put the revised normNum in a PR, mathlib4#49

[Mario Carneiro]

I'm still not sure about what causes these particular paths to appear, but I added yet another typeclass LawfulOfNat to prove that the OfNat instance is equal to the "canonical" semiring OfNat instance. (Fight dependent types with even dependent-er types...)

[Chris B]

That's an interesting way of resolving it. I can't seem to get priorities to work, but my first thought would have been to just force the resolution system to always use the Semiring path if the type in question has an instance of Semiring. Is the approach of showing that the instances are equal more robust in the context of more complex hierarchies? I guess doing these proofs as they're needed is a better way of handling diamonds than trying to sort out priorities.

[Mario Carneiro]

I don't think we can really ensure that we always get the same instance, since there are at least some instances that won't go through the semiring instance, like the one on Nat which is defined prior.

Also, it occurs to me that this LawfulOfNat approach can also potentially handle cases where the OfNat is partially defined but is lawful where it is defined. So for instance you could prove (2 + 2 : fin 5) = 4

[Chris B]

Ok. I'll defer to your judgment here.