How to debug recursive simp?

Stream: new members

[Dan Abramov]

So apparently I have simp recursion somewhere.

Screenshot 2025-08-06 at 15.40.35.png

Lean suggests two things:

• use set_option maxRecDepth <num> to increase limit
• use set_option diagnostics true to get diagnostic information

Both of these suggestions appear to be completely useless.

The first one is useless because I actually have an infinite recursion (and so increasing the limit actually crashes the server).

The second one seems to be useless because the information it output doesn't seem to shed light on the recursion cause:

Screenshot 2025-08-06 at 15.43.01.png

Of course I have no idea what _uniq.121567 ↦ 54 means.

As a result, I have two questions:

• How to debug this properly?
• Why isn't the debug pragma suggested by Lean actually useful in this case?

What I would have expected to see if some kind of runaway recursive stack which would tell me which @[simp] lemmas are going in circles.

[Kenny Lau]

@Dan Abramov in the second screenshot, hover over _uniq.121567 and take another screenshot

[Dan Abramov]

Alas, nothing happens on hover..

[Kenny Lau]

can you move the set_option before the theorem

[Kenny Lau]

also, click instead of hover

[Dan Abramov]

Same, neither clicking nor hover works.

Screenshot 2025-08-06 at 15.47.29.png

[Kenny Lau]

what does it say when you hover on ht

[Dan Abramov]

Definition:

Screenshot 2025-08-06 at 15.51.12.png

Usage:

Screenshot 2025-08-06 at 15.51.04.png

[Dan Abramov]

FWIW I did end up solving the actual exercise, seems like plain rw [ht] started working after I got rid of dsimps

  left_inv := by
    intro t
    have h := (mem_iProd _).mp t.property
    have ht := h.choose_spec
    ext
    rw [ht]

Still not sure why simp_rw [ht] recurses though.

[Dan Abramov]

Ohhh is 54 here the recursion limit?

[Dan Abramov]

Like, "how many times it got unfolded?"?

[Kenny Lau]

@Dan Abramov simp_rw does not call other lemmas, so simp_rw [ht] just means rw [ht] for as many times as possible, so try rw [ht, ht] and see what happens

[Aaron Liu]

it's actually simp only; simp only [ht]

[Dan Abramov]

Hmm, if I repeat the rewrite, it fails pretty early:

Screenshot 2025-08-06 at 16.16.53.png

However, simp_rw [ht] in the same spot recurses.

[Kenny Lau]

@Dan Abramov right, it fails because of "motive is not type correct", which means that theoretically it can still rewrite

[Kenny Lau]

note that as usual rw fails under the binder, and simp_rw can rewrite under the binder

[Kenny Lau]

so simp_rw is slightly stronger than rw

[Lawrence Wu (llllvvuu)]

my guess is that it’s because t appears in h

[Lawrence Wu (llllvvuu)]

#mwe:

set_option trace.Meta.Tactic.simp.rewrite true in
example (t : Nat) (h : ∃ x, t = x) (ht : t = h.choose) : h.choose = t := by
  simp [ht]

[Lawrence Wu (llllvvuu)]

My guess is that to improve this error message would involve catching it in simp and re-throwing a simp-specific error message. The current error is probably a generic stack overflow error that bubbles up.

[Robin Arnez]

You can debug using +singlePass which should prevent repeated application. You'll see:

example (t : Nat) (h : ∃ x, t = x) (ht : t = h.choose) : h.choose = t := by
  simp +singlePass [ht]
  -- ⊢ (⋯ : ∃ a, h.choose = a).choose = h.choose

so yeah it rewrites t in h.

[Lawrence Wu (llllvvuu)]

I also found lean4#8865 but it doesn't seem to work here

[Robin Arnez]

Yeah it should activate automatically but maybe it doesn't detect rewrites using local hypotheses?

[Kenny Lau]

@Robin Arnez I think in the ideal case I would be able to pass in the number 10 to simp and it will simplify ht exactly 10 times, and then it will be clear to anyone what is going on

[Robin Arnez]

import Batteries

example (t : Nat) (h : ∃ x, t = x) (ht : t = h.choose) : h.choose = t := by
  iterate 10 simp +singlePass [ht]

I guess

[Robin Arnez]

Although that won't say "simplify using ht exactly 10 times" but rather "simplify using ht only 10 times recursively"

[Kenny Lau]

@Robin Arnez but do you think that would be a useful feature to add?

[Robin Arnez]

I'm not sure; I'd think singlePass already covers most of the cases