ring_exp bug

Stream: general

[Patrick Massot]

@Anne Baanen ring_exp is not pleasing the kernel:

import tactic.ring_exp data.real.basic

example (l ε : ℝ) (ε_pos : ε ≥ 0) : |l - l| ≤ ε :=
begin
  ring_exp,
  rw abs_zero,
  exact ε_pos,
end

[Patrick Massot]

Sorry about the edits, I simplified the example

[Patrick Massot]

To be clear: the interactive Lean says "goals accomplished" but the proof is rejected by the kernel.

[Patrick Massot]

and replacing ring_exp by ring_nf works

[Anne Baanen]

Thanks for the bug report! From a quick check, it looks like the issue occurs when the goal can't be closed and ring_exp tries to normalize as much as possible.

[Anne Baanen]

Further simplified example:

import tactic.ring_exp

example (l : ℤ) : l - l = 0 :=
begin
  tactic.replace_at (tactic.ring_exp.normalize tactic.transparency.reducible) [] tt >> pure (),
  refl
end

[Anne Baanen]

#11394

[Patrick Massot]

Thanks a lot for this very quick fix!