ch4.2 - mysterious error when building inst `CommRing Rat`

Stream: Analysis I

[Rado Kirov]

Had a long flight back to San Francisco from London, so managed to wrap up ch4.2 too. I am down to one final error, but it is very mysterious to a beginner like me.

I have added proofs for the 5 axioms needed to turn our homemade Rats into a Commutative Ring - https://github.com/rkirov/analysis/blob/main/analysis/Analysis/Section_4_2.lean#L354-L442. The proofs type-check without error. However, I get an error over the where clause about failure to synthesize a default field natCast_succ.

Screenshot 2025-08-23 at 4.47.39 AM.png

How can I resolve this?

• should I try to manually define natCast_succ?
• given I have only provided proofs in the instance, I assume there is nothing I can do to the proofs themselves to fix this? Is there anything I can redefine to make this go away? What would that be?

[Rado Kirov]

Various casts are here - https://github.com/rkirov/analysis/blob/main/analysis/Analysis/Section_4_2.lean#L162-L193 , can they be fixed for this to work?

[Ruben Van de Velde]

Yeah, you can manually define the field

[Rado Kirov]

ok, will try that next, also rebasing to upstream head, to see if it will magically go away

[Rado Kirov]

rebasing didn't help, but manually providing a proof fixed it - https://github.com/rkirov/analysis/blob/main/analysis/Analysis/Section_4_2.lean#L441-L448.

Surprised, this error didn't show up earlier, and only happened after I provided the proofs of the other 5 properties. Feels independent of those.

[Terence Tao]

Oh, this is because the lean file had already introduced a NatCast Rat at an earlier stage, which Lean doesn't "know" is equivalent to the autogenerated NatCast Rat that a CommRing Rat structure would provide. One could delete that previous NatCast to allow the autogenerated NatCast to go through, and then provide a followup lemma to ensure that the autogenerated NatCast agrees with the book NatCast, but this would deviate from the spirit of the source text, so I guess one should just add natCast_succ as one of the fields the student has to fill in for this exercise (maybe with some comment to explain why it is needed).

[Rado Kirov]

Ah, that makes sense. Indeed removing the custom NatCast makes the error go away.

But it feels slightly different from mixing the custom NatCast from the autogenerated one, because hovering over the casts in natCast_succ it seems like there is a single instance - the custom one. The theorem Lean is asking for is not about equivalence between the custom and autogenerated one.

Turns out even before defining CommRing Rat, our custom natCast doesn't have a simple rfl proof of natCast_succ, and it seems to me that when defining CommRing Lean tries to reuse the default rfl proof and fails.

What do you think about making the following change (will send a PR shortly):

• add theorem Rat.coe_Nat_succ (n: ℕ) : ((n + 1: ℕ): Rat) = (n: Rat) + 1 := by sorry right after custom natCast is defined
• add natCast_succ := Rat.coe_Nat_succ with a comment to CommRing definition.

[Terence Tao]

Sounds good to me!

I believe CommRing will not attempt to introduce an autogenerated NatCast if it detects that one already exists, since this would create a dreaded "instance diamond" which is almost never a good idea to introduce. As a consequence, it will also fail to auto-generate natCast_succ.

But I was mentioning an alternate way to resolve the issue by instantiating CommRing first - with the autogenerated NatCast - and only afterwards adding a lemma that ∀ n: ℕ, (n:Rat) = (n:ℤ) // 1 instead of introducing the custom NatCast. But I prefer the current arrangement over this, as it aligns with the source text from the book.

[Rado Kirov]

Makes sense - https://github.com/teorth/analysis/pull/314. I just realized that the scaffold always had natCast_succ := by sorry and I must have accidentally have deleted it at some point which add more confusion here, but I think the PR makes it a bit more explicit (in case some is comparing to the CommRing Int definition in ch4.1)

[Li Xuanji]

I believe you'll run into the same issue for Real.instCommRing!

Here was my old solution (transport everything to our custom NatCast instance) - but @Rado Kirov 's looks cleaner. It was helpful for me to rename the custom instance to Rat.instOurCustomNatCast to see what's going on.

If I understood correctly, the possible conflict was that our custom natcast sent n to (n:ℤ) // 1, but the CommRing instance presumably sent it to 1:Rat + 1:Rat + ... , and we do not know a priori that these are equivalent?

lemma Rat.natCast_add (a b:ℕ) : (a:Rat) + (b:Rat) = (a+b:ℕ) := by
  rw [show (a:Rat) = ((a:ℤ):Rat) by rfl, show (b:Rat) = ((b:ℤ):Rat) by rfl, Rat.intCast_add]
  norm_cast

/-- Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3 -/
instance Rat.instCommRing : CommRing Rat where
  left_distrib := by sorry
  right_distrib := by sorry
  zero_mul := by sorry
  mul_zero := by sorry
  mul_assoc := by sorry
  natCast_succ a := by
    rw [show (1 : Rat) = ((1 : ℕ) : Rat) by norm_cast]
    rw [show @NatCast.natCast Rat instNatCast a = (a:Rat) by rfl]
    rw [Rat.natCast_add]

[Rado Kirov]

our custom natcast sent n to (n:ℤ) // 1, but the CommRing instance presumably sent it to 1:Rat + 1:Rat + ...

If I understand @Terence Tao comment correctly, in the presence of custom natcast, lean "backs off" from using 1:Rat + 1:Rat + ... at together, but now we have the problem that the autogenerated proof for natCast_succ which uses rfl no longer works, so we just need to provide our own non-rfl proof.

It would be interesting to me to understand how exactly the "backing off" works in terms of type class instances.

[Terence Tao]

I think it is here in the AddMonoidWithOne class (which CommRing ultimately extends) that the default natCast and natCast_succ are set. We override natCast with a new function (which is propositionally, but not definitionally, equal to the previous one), and the sequence of tactics provided as a default for natCast_succ no longer works and has to be replaced.

[Rado Kirov]

yep, this confirms it

#synth NatCast Rat
set_option trace.Meta.synthInstance true

--- in info view
  [] new goal NatCast Rat ▼
    [instances] #[@AddMonoidWithOne.toNatCast, Rat.instNatCast]
  [] ✅️ apply Rat.instNatCast to NatCast Rat ▼
    [tryResolve] ✅️ NatCast Rat ≟ NatCast Rat
    [answer] ✅️ NatCast Rat

I think Rat.instNatCast wins because it is provided directly to Rat while AddMonoidWithOne is provided through CommRing.