Relationship between literals and OfNat instances

Stream: Analysis I

[Rado Kirov]

I am doing Ch3.4 and again somewhat surprisingly the parts that have to do with concrete numbers feel harder to me than the proofs for unspecified f and x.

I think a lot has to do with literals adding an extra wrinkle into the Object, Nat, \N` picture. I think the mental model is something like this
IMG_5249.jpg

Though I am not sure whether I should keep back arrows into lit or not? On one hand, not every natural number is written as a literal, on another
Screenshot 2025-07-07 at 9.48.57 AM.png
OfNat does take a \N somewhat magically, I kinda expected it to take some opaque literal representation like a string.

So basically all the problems boil down to, I have some term = some literal in one of Nat or Object (or for extra difficulty in Subset of either), I have to use injective theorems to move this into \N where I can do actual computations. However, I struggle to find the right theorem to apply from the 5-6 ones provided in ch3.1.

Specifically for literals, I am not even sure how to match the onNat(n) syntax in the theorem statement to the problem I have at hand.

Is there a missing theorem or simp-annotation, that prevents simp from achieving the above.

[Aaron Liu]

"raw natural number literals" are built into lean, they are always typed as the "mathlib nat"

[Rado Kirov]

If there is a hardcoded connection with mathlib Nat (which I write as \N to avoid confusion with custom Nat), why do we need to complicate everything with extra OfNat instances for Object and Nat, given there are \N -> Object and \N -> Nat mappings.

[Kevin Buzzard]

I thought that the point of OfNat was to get numerals working?

[Aaron Liu]

It's so you can also write numerals for Int, and for Real, and all the other types it would be useful to write a numeral for

[Rado Kirov]

I guess what I am wondering (sorry, I don't have the right language yet to make a lof ot his precise) is that it seems to me that literal have a direct mapping to some type X (in this case Object and Nat) though OfNat, but \N also has an injective map into those, and literals obviously can be turned into \N (and Lean does this someone preferentially? according to above?). So now we have two paths from lit to custom object that we 1) have to prove they commute 2) rewrite when necessary.

[Aaron Liu]

yes this is a hassle

[Aaron Liu]

but for stuff like docs#Group you only want the numeral 1 and you don't have a map from Nat

[Aaron Liu]

and OfNat can do this too

[Aaron Liu]

but NatCast cannot

[Terence Tao]

Wait, so OfNat(17) works (but presumably gives junk) in a group?

[Aaron Liu]

no it doesn't

[Aaron Liu]

typeclass synthesis will find ∀ α [Group α], OfNat α 1

[Aaron Liu]

it will not find ∀ α [Group α], OfNat α 17

[Terence Tao]

Ah, so OfNat is not a function but rather some sort of metasyntactic object?

[Aaron Liu]

it is a function

[Aaron Liu]

docs#OfNat

[Aaron Liu]

it return a type

[Aaron Liu]

and docs#OfNat.ofNat gets the value out

[Aaron Liu]

just like how docs#Group is a function that returns a type

[Aaron Liu]

and docs#Group.inv_mul_cancel is a gets you the cancellation

[Aaron Liu]

Group α is "the type of all the ways you can make α into a group"

[Terence Tao]

so what type would OfNat α 17 return for (α: Type u) [Group α]?

[Aaron Liu]

OfNat α 17 doesn't reduce

[Aaron Liu]

but it's equivalent to α

[Aaron Liu]

typeclass synthesis is a way to find a "canonical" inhabitant of a type

[Aaron Liu]

so for example it can find a "canonical" group structure on α, which is the "canonical" inhabitant of Group α

[Aaron Liu]

there is no "canonical" inhabitant of ∀ α [Group α], OfNat α 17, according to typeclass

[Aaron Liu]

so it fails

[Terence Tao]

Oh ok I think I see.

[Terence Tao]

A related question: Int, for instance, has the Zero and One classes which presumably give instances of OfNat Int 0 and OfNat Int 1, but there is also the more general OfNat Int n coming from Nat.cast for arbitrary literals n. What prevents instance diamonds from occurring here?

[Aaron Liu]

they turn out defeq

[Aaron Liu]

but this doesn't work for general rings semirings add monoids with one, so we have docs#Nat.AtLeastTwo

[Kevin Buzzard]

It is indeed a pain point making these defeq, and this is the reason we have that weird "at least two" typeclass (which did not exist in Lean 3, which had another numeral system)

[Aaron Liu]

and the instance is docs#instOfNatAtLeastTwo

[Terence Tao]

got it

[Terence Tao]

When I wrote the Lean companion I basically copied off of what Mathlib classes like Int were doing to implement natural number coercions, literals, etc.. It worked so I didn't question it, but now I understand things a bit better.

[Rado Kirov]

Ah, so OfNat is not a function but rather some sort of metasyntactic object?

That's what I thought too, purely based on seeing the parens ofNat(n) instead of ofNat n. But now I see when I hover on those, that they are macros on top of the it's just a typeclass function OfNat.ofNat - https://florisvandoorn.com/carleson/docs/Mathlib/Tactic/OfNat.html . So based on this and reading the docs more carefully, the metamagic happens when (3 : T) gets turned OfNat.ofNat T 3 [instance of OfNat T 3] (where 3 is now actual \N) but the rest is normal type-class resolution.

[Rado Kirov]

Back to something more concrete. I have h: ↑x = 1 where x: nat.toSubtype and the up arrow (coersion?) is from nat to Object. I want to have x = 1 in nat. Which _inj lemma to use?

By trial and error I found out that

have : x = 1 := by
  rw [← coe_inj]
  exact h

works but notice coe_inj doesn't mention the literal at all its injective property of the nat -> object. Is there a better way? and if not how would I have known to use coe_inj despite all the literal machinery I see when I hover over 1 (in a sense I have transformed what 1 means when I went from the first statement to the second).

[Rado Kirov]

Also why is the above not the same as just rw [coe_inj] at h (which lean doesn't accept)?

[Mario Carneiro]

norm_cast does this kind of simplification

[Mario Carneiro]

rewriting with coe_inj doesn't work because it requires the hypothesis to have type ↑x = ↑1 instead of ↑x = 1

[Rado Kirov]

How did exact exact succeed then?

[Mario Carneiro]

exact matches up to defeq, rw matches up to syntactic eq

[Rado Kirov]

I see. Is there a version of rw that matches fuzzily up to defeq objects?

[Rado Kirov]

I figured I can rewrite the above to:

      change ((x:Object) = ↑(1: nat)) at h
      rw [coe_inj] at h

but it still feels like a mouthful.

[Ruben Van de Velde]

There's erw, though that fuzzy matching tends to be seen as an antipattern