## Stream: general

### Topic: Why is x + -x normalized to x - x?

#### Ruotong Cheng (Apr 05 2022 at 00:13):

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 (Apr 05 2022 at 00:46):

Ruotong Cheng said:

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

Puzzling indeed!

#### Alex J. Best (Apr 05 2022 at 07:33):

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

#### Alex J. Best (Apr 05 2022 at 07:35):

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 (Apr 05 2022 at 09:31):

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

Last updated: Dec 20 2023 at 11:08 UTC