Confusion about add_eq_zero_iff

Stream: new members

[Patrick Lutz]

When I try the following:

import data.real.basic

example (x y : ℝ) : x*x + y*y = 0 → x = 0 ∧ y = 0 :=
begin
    intro h,
    rw add_eq_zero_iff at h,
end

Lean tells me rewrite tactic failed, did not find instance of the pattern in the target expression _ = 0
Why is that? To me h obviously looks like an instance of add_eq_zero_iff. Is it because $\mathbb{R}$ is not a canonically_ordered_add_monoid which add_eq_zero_iff requires?

[Kyle Miller]

It doesn't seem like $\mathbb{R}$ should satisfy that. The monoid of non-negative reals under addition would, though, I think.

[Patrick Lutz]

Lol, oh yeah I somehow just realized I'm being stupid

[Patrick Lutz]

I didn't really think about what that theorem means

[Patrick Lutz]

It looks like what I really want is add_eq_zero_iff'

[Alex J. Best]

Or add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg

[Alex J. Best]

Which looks to be exactly the same lemma as add_eq_zero_iff_eq_zero_of_nonneg just with a longer name :rolling_on_the_floor_laughing:

[Alex J. Best]

So we should remove the two I just mentioned perhaps as they assume ordered_cancel_add_comm_monoid rather than ordered_add_comm_monoid

[Kyle Miller]

If you do library_search, it suggests exact mul_self_add_mul_self_eq_zero.mp which is exactly the theorem.

[Kevin Buzzard]

Oh yeah, I still remember the day that I understood that "canonically ordered" means "a<=b iff there exists c such that b=a+c". So basically if you're canonical then everything is >=0. So basically it's just nat

[Kevin Buzzard]

Computer scientists are so fixated with nat, it's crazy

[Johan Commelin]

What about nnreal?

[Mario Carneiro]

I think the general practice comes from monoid orders

[Mario Carneiro]

Any (add_)monoid can be canonically ordered

[Kenny Lau]

how do you canonically order $\Bbb Z$?

[Mario Carneiro]

I suppose the order is usually not a partial order though

[Mario Carneiro]

nat can be canonically ordered as a multiplicative monoid by divisibility

[Mario Carneiro]

int can be canonically ordered but the order is trivial

[Kevin Buzzard]

Kenny you can canonically order any group, because any set is a category

[Jalex Stark]

do the nonnegative elements of an arbitrary ordered ring form a canonically ordered monoid?
(my motivating example is the cone of psd matrices, where you put an order on matrices $A \le B$ if $A - B$ is positive semi-definite)

[Kevin Buzzard]

Wouldn't surprise me at all