Zulip Chat Archive

Stream: general

Topic: Best practice for numeral lemmas

Yaël Dillies (Oct 10 2025 at 14:44):

It used to be the case that numerals in Lean went 0, 1, bigger. That meant that, whenever proving a lemma involving a natural number n : ℕ coerced to eg a ring, one would need to prove three additional lemmas: one for 0, one for 1, one for ofNat(n) where (n : ℕ) [n.AtLeastTwo]. But as of recently, it seems that all three cases can be dealt at once with the new docs#Semiring.toGrindSemiring_ofNat instance. Is this intended?

Kenny Lau (Oct 10 2025 at 14:49):

Yaël Dillies said:

all three cases can be dealt at once

but grind is not the universal tactic

Yaël Dillies (Oct 10 2025 at 14:54):

What? This has nothing to do with grind; I am talking about rewriting tactics. Consider:

import Mathlib.Algebra.Ring.Defs

variable (R : Type) [Semiring R]

def foo (n : ℕ) : R := 0

-- This lemma used not to be stateable because of the lack
-- of a "generic" `ofNat` instance.
@[simp] lemma foo_ofNat (n : ℕ) : foo R ofNat(n) = 0 := rfl

-- These used to be the three cases one would need to prove.
example : foo R 0 = 0 := by simp
example : foo R 1 = 0 := by simp
example (n : ℕ) [n.AtLeastTwo] : foo R ofNat(n) = 0 := by simp

Kenny Lau (Oct 10 2025 at 14:55):

interesting, I just thought this is grind because the name contains grind

Yaël Dillies (Oct 10 2025 at 14:56):

The instance was introduced to be used in grind internals, correct, but the connection stops there.

Yury G. Kudryashov (Oct 10 2025 at 15:13):

The instance was introduced by @Kim Morrison , see docs#Semiring.toGrindSemiring, to make grind work with Mathlib's (semi)rings.

Yury G. Kudryashov (Oct 10 2025 at 15:16):

I see 2 ways to go forward with it in a consistent way:

introduce an instance for OfNat assuming [NatCast R]; we have it for semirings anyway.
restrict the grind-related instances (incl. GrindSemiring -> OfNat) to some scope and make grind open this scope.

Aaron Liu (Oct 10 2025 at 16:57):

Maybe we should bundle an ofNat field into AddMonoidWithOne

Yury G. Kudryashov (Oct 10 2025 at 18:28):

I see no reason to have both NatCast R and \forall n, OfNat R n.

Aaron Liu (Oct 10 2025 at 18:49):

It's to fix definitional equalities

Aaron Liu (Oct 10 2025 at 18:51):

since we have a Zero R which gives OfNat R 0 and we have a One R which gives OfNat R 1 and of course we want the NatCast R to be something as well

Yury G. Kudryashov (Oct 10 2025 at 18:52):

I see not issues with OfNat being | 0 => 0 | 1 => 1 | n + 2 => Nat.cast (n + 2). It isn't defeq to Nat.cast n for a generic n, but it is defeq for any specific n.