Repeat tactic does not terminate instead of giving an error or functioning as it should.

[Karthik-Dulam]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Repeat tactic does not terminate instead of giving an error or functioning as it should.

Steps to Reproduce

theorem add_left_cancel (t a b : nat) : t + a = t + b → a = b :=
begin
  intro h,
  repeat {rw nat.add_comm at h},
end

Expected behavior:

Either give out an error or change the goals to

1 goal
tab: ℕ
h: a + t = b + t
⊢ a = b

Actual behavior: Does not terminate and the Infoview shows

Loading...

Reproduces how often: All the time.

Versions

Lean (version 3.30.0, commit a5822ea47ebc, Release) Windows 10 Home Edition

Additional Information

None.

[fpvandoorn]

Why do you expect this to terminate exactly? You're asking to run rw nat.add_comm at h as often as it doesn't fail, and this tactic will happily rewrite t + a to a + t and then back to t + aover and over.

To get the behavior you want, use any of

• simp [nat.add_comm t] at h
• simp_rw [nat.add_comm t] at h
• have h : a + t = b + t, by simpa [nat.add_comm] using h (requires import tactic.basic from mathlib)
• I don't think you should use repeat for something like this, but if you really want to: repeat {rw nat.add_comm t at h},