recursion limit in `exact?`

Stream: mathlib4

[Eric Wieser]

This causes a maximum recursion depth error:

import Mathlib

example (n : Nat) : n = 55 := by
  exact?

[Eric Wieser]

Is this expected? It doesn't do it with import Batteries, even for much larger constants

[llllvvuu]

minimized a bit:

import Mathlib.SetTheory.Ordinal.Basic

theorem natCast_inj {m n : ℕ} : (m : Ordinal) = n ↔ m = n := sorry

example (n : Nat) : n = 55 := by
  exact?

[Eric Wieser]

Thanks! That's not what I expected at all, I was sure the 55 would have to decrease with the number of imports!

[Eric Wieser]

Adding natCast := Nat.unaryCast to docs#Ordinal.addMonoidWithOne fixes it

[Eric Wieser]

#20784

[llllvvuu]

I guess I should have considered that multiple things can trigger this:

def factorial : Nat → Nat
  | 0 => 1
  | .succ n => .succ n * factorial n

theorem factorial_inj (hn : 1 < n) : factorial n = factorial m ↔ n = m := by sorry

example (n : Nat) : n = 125 := by
  exact?

Probably it is just hard to reduce the Nat.rec:

import Mathlib.SetTheory.Ordinal.Basic

#reduce inferInstanceAs (NatCast Ordinal)
#reduce (inferInstanceAs (NatCast Ordinal)).natCast 84

[Eric Wieser]

I guess this is an argument for with_reducible exact?

[Violeta Hernández]

Dammit! Is this my fault?