apply_rules getting stuck

Stream: general

[Heather Macbeth]

Why does apply_rules get stuck in the following example?

import tactic

example {m n : ℤ} (hn : 2 < n) : m + 0 < m + 6000 :=
begin
  apply_rules [add_lt_add_left],
  -- deep recursion was detected at 'replace' (potential solution: increase stack space in your system)
end

It doesn't get stuck without the useless hypothesis h, and it doesn't get stuck for a slightly smaller number (5000 rather than 6000).

[Heather Macbeth]

Just bumping this question :up: about apply_rules, in case there's someone around who can answer.

[Johan Commelin]

Not sure, but maybe this is the problem?

import tactic

example {m n : ℤ} (hn : 2 < n) : m + 0 < m + 5 :=
begin
  refine add_lt_add_left _ _,
  refine add_lt_add_left (_ : 0 < 5) 0,
  refine add_lt_add_left (_ : 0 < 5) 0,
  refine add_lt_add_left (_ : 0 < 5) 0,
  refine add_lt_add_left (_ : 0 < 5) 0,
  refine add_lt_add_left (_ : 0 < 5) 0,
  refine add_lt_add_left (_ : 0 < 5) 0,
  refine add_lt_add_left (_ : 0 < 5) 0,
  refine add_lt_add_left (_ : 0 < 5) 0,
  refine add_lt_add_left (_ : 0 < 5) 0,
  refine add_lt_add_left (_ : 0 < 5) 0,
  refine add_lt_add_left (_ : 0 < 5) 0,
  refine add_lt_add_left (_ : 0 < 5) 0,
end

[Johan Commelin]

I don't know why apply_rules does work for small numbers. But I can imagine random defeqs play a role in the failure.