Rogue `Int.ofNat` maxing out recursion depth for decimals

Stream: mathlib4

[Thomas Murrills]

Int.ofNat is notoriously badly behaved and discouraged in favor of coercions. One of the reasons might be the following: simp expands natural numbers into 1 + 1 + 1 + ... + 1 when they appear as arguments to the argument of Int.ofNat (sometimes). For example,

example (x : ℤ) : x = Int.ofNat (12 * 2) := by simp

leaves us with the goal

x = (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) * (1 + 1)

But this thread isn't actually about Int.ofNat being badly behaved—it's about how it appears without warning in Rat.ofScientific.

The written definition of Rat.ofScientific in std is

/-- Implements "scientific notation" `123.4e-5` for rational numbers. -/
protected def ofScientific (m : Nat) (s : Bool) (e : Nat) : Rat :=
  if s then
    Rat.normalize m (10 ^ e) <| Nat.ne_of_gt <| Nat.pos_pow_of_pos _ (by decide)
  else
    (m * (10 ^ e) : Nat)

When we #print Rat.ofScientific, we see an Int.ofNat has slipped in:

protected def Rat.ofScientific : Nat → Bool → Nat → Rat :=
fun m s e => if s = true then normalize (↑m) (10 ^ e) else ↑(Int.ofNat (m * 10 ^ e))

This causes problems when writing something like 3.1—even though the false branch isn't explored, simp still expands it.

It might be worth looking at the trace of the simp call above. We see it constantly trying to discharge and failing each time it peels off another + 1:

@Nat.cast_ofNat, failed to assign instance
      NatCast ℤ
    sythesized value
      Int.instNatCastInt
    is not definitionally equal to
      NonAssocSemiring.toNatCast

I'm not sure what the best way to fix this is, but here are some possible approaches.

1. Change the cast that gets used in ofScientific. There are a few ways to do this, too:

• Simply use something like Int.mul or (m * (Nat.pow 10 e)) : Int. A band-aid; not sure if it would actually work.
• Add an instance of NatCast Rat. We only have IntCast Rat defined directly; NatCast Rat relies on algebraic structure inclusions (namely #synth NatCast Rat yields NonAssocRing.toNatCast).
• Remove the instance of IntCast Rat and rely on algebraic inclusions for the cast in general. (For ofScientific, we'd define the rational number directly via e.g. mkRat instead of relying on a cast to the rationals.)

2. Fix the behavior that causes Int.ofNat to expand into 1 + 1 + 1 + ... + 1. I don't know why this happens, but it's not just with *; it also happens with the first argument of ^, and possibly other operations. I'm guessing this would resolve other problems as well, but I don't know if it's feasible to fix it. I think zify ran into a similar problem, and I wonder if the reason is the same.
3. Stop Int.ofNat from being inserted automatically like this. Where did this Int.ofNat even come from? Why doesn't it appear as an up-arrow? It just seems a bit fishy, so I wonder if there's something to address in this direction—but if there is, I don't have the background necessary to do so.

If we could resolve this quickly somehow it would be great! @Heather Macbeth is looking to use decimals for teaching in less than a week, and I found out that even trying to use norm_num with e.g. 3.141 hangs, and 3.14159 causes a stack overflow. I suspect this behavior is the culprit; when we try to simplify 3.141 with simp we hit the max recursion depth:

example (x : ℚ) : 3.141 = x := by
  simp [OfScientific.ofScientific]; rw [Rat.ofScientific]; simp
-- maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

(I could technically be wrong about this being the source of the issues for the new norm_num extension, as I'm still looking into it—but still, this seems like it should be fixed one way or another!)

[Mario Carneiro]

Thomas Murrills said:

Int.ofNat is notoriously badly behaved and discouraged in favor of coercions.

This seems like a strange mischaracterization. Int.ofNat is the constructor, it's not badly behaved performance-wise but it is not the coercion and hence not the simp-normal form.

[Mario Carneiro]

You will certainly find calls to Int.ofNat and other non-simp-normal functions if you unfold enough definitions. This is not a problem that needs to be solved

[Mario Carneiro]

Thomas Murrills said:

One of the reasons might be the following: simp expands natural numbers into 1 + 1 + 1 + ... + 1 when they appear as arguments to the argument of Int.ofNat (sometimes). For example,

example (x : ℤ) : x = Int.ofNat (12 * 2) := by simp

leaves us with the goal

x = (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) * (1 + 1)

This is certainly a problem (which has been mentioned elsewhere although I don't think it has a dedicated issue for it), although I don't think it is specific to Int.ofNat. I think you can cause the same behavior using Nat.cast, it's a problem in simp and/or our simp set.

[Mario Carneiro]

This causes problems when writing something like 3.1—even though the false branch isn't explored, simp still expands it.

simp should not do anything to 3.1 as written. If you give it to norm_num it should hopefully rewrite it to 31 / 10 and leave it at that. simp [Rat.ofScientific] is not something you should be doing unless you are proving theorems about Rat.ofScientific, and in those cases the workaround would most likely be to disable simp lemmas like \u (n+1) = \u n + 1 that are causing this bad unfolding.

[Mario Carneiro]

@Thomas Murrills

[Thomas Murrills]

Mario Carneiro said:

Thomas Murrills said:

Int.ofNat is notoriously badly behaved and discouraged in favor of coercions.

This seems like a strange mischaracterization. Int.ofNat is the constructor, it's not badly behaved performance-wise but it is not the coercion and hence not the simp-normal form.

Ok, makes sense! That last bit clarifies the motivation behind the sentiment I’ve seen about it, I’m guessing.

[Thomas Murrills]

Cool, I’ll see if disabling those lemmas in the proofs about Rat.ofScientific fixes the problems next time that I have some downtime! :)