Why is `x + -x` normalized to `x - x`?

Stream: general

[Ruotong Cheng]

Hi, everyone!

I am trying to use the tactics ring_nf and norm_num to prove x + -x ≠ 1 for any real number x.

import data.real.basic
example (x : ℝ) : x + -x ≠ 1 :=
begin
  ring_nf,
  norm_num
end

It worked, but in a way different from my expectation. I expected ring_nf to change the goal to 0 ≠ 1, but it actually changed the goal to x - x ≠ 1. I also noticed that ring_nf raw would give 0 ≠ 1. I thought norm_num could only normalize numerical expressions, but it did work with x - x ≠ 1; it even worked with x + -x ≠ 1 directly.

My questions are:

• Why is x + -x not normalized to 0 by default?
• What does the raw option of ring_nf do?
• Why can norm_num normalize expressions not purely numerical?

Thank you.

[Heather Macbeth]

Ruotong Cheng said:

• Why is x + -x not normalized to 0 by default?

Puzzling indeed!

[Alex J. Best]

This might be #12430 again @Anne Baanen @Mario Carneiro .
What does repeat { ring_nf } do?

[Alex J. Best]

norm_num calls simp often as part of it's execution so I'd guess it's just one of the simp calls that makes norm num close this goal

[Mario Carneiro]

yes, the issue is fixed on that PR. I will try to get it merged