repeat rw [add_comm] no longer harmful

Stream: general

[Kevin Buzzard]

Ha! I just wrote a short paragraph in NNG4 warning users about the dangers of repeat rw [add_comm] because it can lead to loops (and this was a common question in NNG3 -- "why did lean hang after I put it into an infinite loop?"). I then tested it on an example and it didn't hang! And indeed this is also true in core Lean:

example (a b c : Nat) : a + b + c = a + c + b := by
  rw [Nat.add_comm]
  rw [Nat.add_comm]
  rw [Nat.add_comm]
  rw [Nat.add_comm]
  -- you can do it as long as you like. But
  repeat rw [Nat.add_comm]
  -- doesn't hang Lean
  sorry

Is this a bug? ;-) The tactic is not doing what its docstring says it will do, as far as I can see.

[Mario Carneiro]

probably because it does it 100000 times and then stops

[Mario Carneiro]

does it actually typecheck if you fill in the sorry?

[Mario Carneiro]

actually it seems to stop far short of that, you can see by putting your cursor in the repeat that it runs around 124 times

[Mario Carneiro]

It appears to be limited by maxRecDepth, it produces n goals if the rec depth is set to 4*n+16

[Damiano Testa]

Also, closing the goal does not seem a problem:

example (a b c : Nat) : a + b + c = a + c + b := by
  rw [Nat.add_comm]
  rw [Nat.add_comm]
  rw [Nat.add_comm]
  rw [Nat.add_comm]
  -- you can do it as long as you like. But
  repeat rw [Nat.add_comm]
  rw [← Nat.add_assoc, Nat.add_comm _ a]

-- appears to work

[Mario Carneiro]

and the reason is because the implementation of repeat is non-tail-recursive so it fails with a recursion overflow fairly quickly

[Mario Carneiro]

syntax "repeat " tacticSeq : tactic
macro_rules
  | `(tactic| repeat $seq) => `(tactic| first | ($seq); repeat $seq | skip)

[Mario Carneiro]

repeat' is an elab and able to handle much larger recursions

[Kevin Buzzard]

Oh I see, so it really does fail and then stop!