Zulip Chat Archive

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