squares equal iff args are

Stream: Is there code for X?

[Alex Kontorovich]

Does this exist already? (librarysearch doesn't find it, and I didn't find it immediately in mathlib.) Thanks in advance!

import algebra.ring.basic
import algebra.order.ring

lemma squares_eq_iff {R : Type*} [comm_ring R] [no_zero_divisors R] [ordered_ring R] (r s : R)
  (hr : 0 ≤ r) (hs : 0 ≤ s) : r = s ↔ r^2 = s^2 :=
begin
  refine ⟨congr_arg (λ (r : R), r ^ 2), _⟩,
  -- λ hh, by nlinarith -- works over ℝ
  intros hh,
  sorry, -- come on, this is annoying
end

[Ruben Van de Velde]

\le should be enough in the hypotheses, right? Have you tried looking for the variant that uses r*r instead of r^2?

[Alex Kontorovich]

Yes sorry, \le. I tried replacing squares with r*r, but nlinarith still doesn't work automatically as the last step... (It does work if R is replaced by ℝ)

[Moritz Doll]

There is docs#pow_left_inj with slightly more restrictive typeclasses

[Yakov Pechersky]

One issue here is that you have two ring structures

[Yakov Pechersky]

There is [ordered_comm_ring R]

[Moritz Doll]

and docs#sq_eq_sq is even closer to what you want

[Alex Kontorovich]

Perfect! That's exactly what I was looking for but for some reason librarysearch didn't find it... Thanks! (I was sure it was there already...)

[Moritz Doll]

library_search can be really annoying because it might not find lemmas if your formulation is very slightly different than what is in mathlib

[Moritz Doll]

Sometimes it's easier to guess the name (in this case it is an injectivity statement about the power), so searching for 'pow inj' in the docs gives the answer

[Yakov Pechersky]

import algebra.ring.basic
import algebra.order.ring
import tactic

lemma squares_eq_iff {R : Type*} [ordered_comm_ring R] [no_zero_divisors R] (r s : R)
  (hr : 0 ≤ r) (hs : 0 ≤ s) : r = s ↔ r^2 = s^2 :=
begin
  refine ⟨congr_arg (λ (r : R), r ^ 2), λ hh, _⟩,
  by_cases H : s + r = 0,
  { rcases hr.eq_or_lt with rfl|hr',
    { simpa using H.symm },
    rcases hs.eq_or_lt with rfl|hs',
    { simpa using H },
    { exact absurd H.symm (add_pos hs' hr').ne } },
  have : (r - s) ^ 2 = 2 * r * (r - s),
  { rw [sub_sq, ←hh],
    ring },
  rw ←sub_eq_zero at this ⊢,
  have key : (r - s) * ((r - s) - 2 * r) = 0,
  { rw ←this,
    ring },
  simp only [mul_eq_zero] at key,
  refine or.resolve_right key _,
  rwa [two_mul, sub_add_eq_sub_sub, sub_sub_cancel_left,
       ←neg_add', neg_eq_zero],
end

[Yakov Pechersky]

The linear_ordered... constrains the order that this one might not?

[Matt Diamond]

I'm surprised simp at hh doesn't work considering sq_eq_sq is tagged as a simp lemma (Edit: nvm, it looks like it's a typeclass issue)

[Junyan Xu]

Notice that the original spelling [comm_ring R] [ordered_ring R] endows R with two independent ring structures...

[Sebastien Gouezel]

What about docs#sq_eq_sq ?

[Sebastien Gouezel]

Oops, already mentioned, sorry.

[Junyan Xu]

shorter proof:

import algebra.order.ring
import tactic.ring

lemma squares_eq_iff {R : Type*} [ordered_comm_ring R] [no_zero_divisors R] (r s : R)
  (hr : 0 ≤ r) (hs : 0 ≤ s) : r = s ↔ r ^ 2 = s ^ 2 :=
⟨congr_arg (^ 2), λ h, begin
  rw [← sub_eq_zero, sq_sub_sq] at h,
  obtain h | h := mul_eq_zero.1 h,
  { obtain rfl|hr := hr.eq_or_lt,
    { convert h.symm, rw zero_add },
    { exact ((add_pos_of_pos_of_nonneg hr hs).ne h.symm).elim } },
  exact sub_eq_zero.1 h,
end⟩

This theorem replaces the "linear order" assumption in docs#sq_eq_sq by commutativity + no_zero_divisors; probably worth being in mathlib?

[Eric Rodriguez]

also needs a ring instead of a semiring, right?

[Yakov Pechersky]

Oops, I forgot the difference of squares identity :face_palm: