Rearranging minus signs

Stream: new members

[Jake Levinson]

Is there a good way to rearrange minus signs? For example, is this already in mathlib:

example (n k : ℕ) : (-1 : ℤ)^n = (-1 : ℤ)^k ↔ (-1 : ℤ)^(n+k) = 1 := sorry

Or equivalent over an arbitrary comm_ring, or similar things like

Here's a hacky proof over the integers:

example (n k : ℕ) : (-1 : ℤ)^n = (-1 : ℤ)^k ↔ (-1 : ℤ)^(n+k) = 1 :=
begin
  split; intro h,
  rw [pow_add, h, ← pow_add],
  exact even.neg_one_pow ⟨_, rfl⟩,
  rw [pow_add, int.mul_eq_one_iff_eq_one_or_neg_one] at h,
  cases h; rw [h.1, h.2],
end

[Jake Levinson]

Here's a hacky proof over an arbitrary comm_ring:

example (n k : ℕ) (R : Type) [comm_ring R] :
  (-1 : R)^n = (-1 : R)^k ↔ (-1 : R)^(n+k) = 1 :=
begin
  split; intro h,
  rw [pow_add, h, ← pow_add],
  exact even.neg_one_pow ⟨_, rfl⟩,
  rw pow_add at h,
  rw ← mul_one ((-1 : R)^n),
  nth_rewrite 1 ← even.neg_one_pow ⟨k, rfl⟩,
  rw [pow_add, ← mul_assoc],
  convert one_mul _,
  convert h,
  refl,
end

There's a strange goal at the end: ⊢ sub_neg_monoid.to_has_neg R = has_involutive_neg.to_has_neg R. Really the last three lines should just be rw h.

[Jake Levinson]

Anyway, it would be nice to add some of this functionality to mathlib.

[Eric Wieser]

This was perhaps a bit easier:

import algebra.ring.units
import algebra.group_power.ring
import algebra.field.power
import data.int.basic

example (n k : ℕ) (R : Type) [comm_ring R] :
  (-1 : R)^n = (-1 : R)^k ↔ (-1 : R)^(n+k) = 1 :=
begin
  suffices : (-1 : Rˣ)^(n : ℤ) = (-1 : Rˣ)^(k : ℤ) ↔ (-1 : Rˣ)^(n+k : ℤ) = 1,
  { simp_rw [units.ext_iff, ←nat.cast_add, zpow_coe_nat] at this,
    push_cast at this,
    exact this },
  rw [←mul_inv_eq_one, ←inv_zpow, zpow_add, inv_neg', inv_one],
end

[Eric Wieser]

The trick is to move to the docs#units of R, and integer powers, where you can just move everything around

[Damiano Testa]

There is also the good old case-bash:

import algebra.group_power.ring

example (n k : ℕ) (R : Type) [comm_ring R] :
  (-1 : R)^n = (-1 : R)^k ↔ (-1 : R)^(n+k) = 1 :=
begin
  cases neg_one_pow_eq_or R n;
  cases neg_one_pow_eq_or R k;
  simp [*, pow_add, eq_comm],
end

[Jake Levinson]

Nice proofs, @Eric Wieser and @Damiano Testa . Either version seems worth adding to mathlib. (I came upon this while doing a different computation, so it would be nice not to be reproving a fact like this, even if the optimized proof is only 3-5 lines).

[Eric Wieser]

Can you share the statement of the larger computation?

[Eric Wieser]

Sometimes changing the formulation is a better option than adding slightly contrived algebraic lemmas

[Jake Levinson]

I see, let's see. It wasn't just one, though, it was a few different equations. For instance:
(n k : ℕ) : even (n + k) → (-1 : ℤ)^n = (-1)^k
(or with R in place of ℤ).

[Jake Levinson]

Or the same statement with odd and an extra sign. This was for the discussion in #18837 about even and odd polynomials, which actually leads to a goal of the form

example (n k : ℕ) (a : ℤ) : odd (n + k) → (-1 : ℤ)^n * a = (-1)^k * a → a = 0 := sorry

[Eric Wieser]

I would suggest writing (-1 : ℤ)^n * a = (-1)^k * a as (-1 : ℤˣ)^n • a = (-1 : ℤˣ)^k • a, and then you can prove it for any ring where 2 is invertible

[Eric Wieser]

Using (-1 : ℤˣ)^n • x as the canonical spelling for "attach an alternating sign to x" means you need fewer lemmas to work with

[Jake Levinson]

Oh interesting, OK

[Jake Levinson]

Hmm. But odd.neg_one_pow and even.neg_one_pow don't use this spelling, I don't think.

[Eric Wieser]

There was a PR at one point that added a dedicated neg_one_pow function to make this type of thing easier, but I argued we already had that function as (-1 : ℤˣ)^n

[Eric Wieser]

Jake Levinson said:

Hmm. But odd.neg_one_pow and even.neg_one_pow don't use this spelling, I don't think.

They should work fine, this is exactly why I created docs#has_distrib_neg

[Damiano Testa]

Eric Wieser said:

I would suggest writing (-1 : ℤ)^n * a = (-1)^k * a as (-1 : ℤˣ)^n • a = (-1 : ℤˣ)^k • a, and then you can prove it for any ring where 2 is invertible

It is in fact enough that 2 is not a zero-divisor, which holds for ℤ. :smile:

[Eric Wieser]

I'm slightly worried I have been using invertible 2 when I meant ne_zero 2

[Eric Wieser]

2 can only be a zero-divisor if it's zero, right?

[Damiano Testa]

ne_zero is not enough: 2 is a zero divisor in zmod 4.

[Damiano Testa]

Ultimately, you cook up 2 * x = 0 and you want to deduce that 2x is zero. You get this, but assuming that multiplication by 2 is injective.

[Eric Wieser]

And to think I only thought I had to worry about characteristic two...

[Damiano Testa]

You should not worry about characteristic 2, you should embrace it.

[Eric Wieser]

In the case I have in mind that's actually what I did; but now I can replace my "the usual approach fails in char 2" claim with a stronger "the usual approach fails in even characteristic" :smile:

[Damiano Testa]

Nevertheless,

import data.zmod.basic

example : (2 : zmod 4) = - 2 := rfl

[Jake Levinson]

Hmm. How would you prove the second lemma below?

import data.polynomial.algebra_map
open polynomial

lemma polynomial.coeff_comp_neg_X {R : Type} [comm_ring R] {p : polynomial R} (k : ℕ) :
  (p.comp (-X)).coeff k = (-1 : ℤˣ)^k * (p.coeff k) := sorry

lemma coeff_zero_of_odd_add {p : polynomial ℤ} {n k : ℕ}
  (hp : p.comp (-X) = (-1 : ℤˣ)^n * p) (hnk : odd (n + k)) :  p.coeff k = 0 :=
begin
  rw polynomial.ext_iff at hp,
  specialize hp k,
  rw polynomial.coeff_comp_neg_X at hp,
  -- hp : ↑-1 ^ k * p.coeff k = (↑-1 ^ n * p).coeff k
  sorry
end

[Damiano Testa]

Eric, when you say "even characteristic" I imagine that you are excluding characteristic 0... :upside_down:

[Damiano Testa]

Anyway, for these kinds of arguments, I find that "characteristic" does not isolate the right property.

[Damiano Testa]

More generally, while "characteristic" is defined for very general (semi)rings, it is only actually useful in situations where you are already quite close to a field.

[Eric Wieser]

@Jake Levinson: I guess there's tension here between my claim that (-1 : ℤˣ)^n • is the best spelling for multiplying by -1, and your use case being working with ℤ itself

[Eric Wieser]

I would suggest stating (hp : p.comp (-X) = (-1)^n * p) as (hp : p.comp (-X) = (-1 : ℤˣ)^n • p) though

[Jake Levinson]

Oops, I meant to include that change. The goal I showed (where the coercion from constants to polynomials and the coercion to a unit are both getting in the way) is with the hypotheses adjusted in that way.

[Heather Macbeth]

Here's another version!

example (n k : ℕ) (R : Type) [comm_ring R] :
  (-1 : R)^n = (-1 : R)^k ↔ (-1 : R)^(n+k) = 1 :=
begin
  split ; intro h,
  { linear_combination (-1:R) ^ k * h + pow_mul (-1:R) 2 k,
    ring_exp, },
  { linear_combination -(-1:R) ^ n * h + (-1:R) ^ k * pow_mul (-1:R) 2 n,
    ring_exp }
end

[Jake Levinson]

Relatedly, (C (-1 : ℤˣ)^k) doesn't work (failed to synthesize type class instance for semiring ℤˣ). But it's preferable to express this as a constant to say that it affects each coefficient individually (polynomial.coeff_C_mul rather than polynomial.coeff_mul).

[Jake Levinson]

@Heather Macbeth Cool! ring_exp and linear_combination seem like good tactics to learn.

[Eric Wieser]

does docs#polynomial.coeff_smul exist? (edit: yes)

[Jake Levinson]

It exists, but it doesn't work on that hypothesis (not sure why)

[Eric Wieser]

Can you make a mwe? I don't see where C appears above

[Jake Levinson]

I'll show you the approach I had before making this thread - I rewrote -1 to C (-1).

import data.polynomial.algebra_map

open polynomial

lemma polynomial.coeff_comp_neg_X {R : Type} [comm_ring R] {p : polynomial R} (k : ℕ) :
  (p.comp (-X)).coeff k = (-1)^k * (p.coeff k) := sorry

lemma coeff_zero_of_odd_add' {p : polynomial ℤ} {n k : ℕ}
  (hp : p.comp (-X) = (-1)^n * p) (hnk : odd (n + k)) :
  p.coeff k = 0 :=
begin
  rw polynomial.ext_iff at hp,
  specialize hp k,
  rw [polynomial.coeff_comp_neg_X, (by simp : (-1 : polynomial ℤ) = C (-1)),
      ← C_pow, coeff_C_mul, mul_eq_mul_right_iff,
      (_ : (-1 : ℤ)^k = (-1)^n ↔ (-1 : ℤ)^(n+k) = 1), hnk.neg_one_pow] at hp,
  norm_num at hp,
  exact hp,
  sorry -- ⊢ (-1) ^ k = (-1) ^ n ↔ (-1) ^ (n + k) = 1
  -- use one of the supplied proofs :)
end

[Eric Wieser]

This gets pretty close: works:

import data.polynomial.algebra_map

open polynomial

lemma polynomial.coeff_comp_neg_X {R : Type} [comm_ring R] {p : polynomial R} (k : ℕ) :
  (p.comp (-X)).coeff k = (-1 : ℤˣ)^k • (p.coeff k) := sorry

lemma coeff_zero_of_odd_add' {p : polynomial ℤ} {n k : ℕ}
  (hp : p.comp (-X) = (-1 : ℤˣ)^n • p) (hnk : odd (n + k)) :
  p.coeff k = 0 :=
begin
  rw polynomial.ext_iff at hp,
  specialize hp k,
  rwa [polynomial.coeff_comp_neg_X, coeff_smul, smul_eq_iff_eq_inv_smul,smul_smul,
    ←inv_pow, inv_neg', inv_one, ←pow_add, add_comm, hnk.neg_pow, one_pow, units.neg_smul,
    one_smul, eq_neg_self_iff] at hp,
end

[Jake Levinson]

Hmm. Changing the muls to smuls throughout makes it better. But, I'm still ending up with needing to move / deal with minus signs:

import data.polynomial.algebra_map
open polynomial

lemma polynomial.coeff_comp_neg_X {R : Type} [comm_ring R] {p : polynomial R} (k : ℕ) :
  (p.comp (-X)).coeff k = (-1 : ℤˣ)^k • (p.coeff k) := sorry

lemma coeff_zero_of_odd_add' {p : polynomial ℤ} {n k : ℕ}
  (hp : p.comp (-X) = (-1 : ℤˣ)^n • p) (hnk : odd (n + k)) :
  p.coeff k = 0 :=
begin
  rw polynomial.ext_iff at hp,
  specialize hp k,
  rw [polynomial.coeff_comp_neg_X, coeff_smul] at hp,
  -- hp: (-1) ^ k • p.coeff k = (-1) ^ n • p.coeff k
  sorry
end

[Eric Wieser]

Annoyingly docs#neg_one_smul doesn't work for the ℤˣ action

[Eric Wieser]

Edited above, now sorry-free

[Yaël Dillies]

wink wink has_smul_distrib_neg

[Eric Wieser]

docs#units.neg_smul is good enough for now

[Jake Levinson]

hooray!

[Eric Wieser]

I suspect my "(-1 : ℤˣ)^n • sign-application is best sign-application" stance is not one that is universally held, so you might want to see if anyone has a short proof leveraging a different spelling

[Jake Levinson]

Yes, that looks like exactly the way the proof should go. So a lesson here for me is to use smul and, for minus signs, the units.

[Jake Levinson]

Hm, fair. Still, smul_eq_iff_eq_inv_smul is literally the rearrangement lemma I was asking for. :)

[Eric Wieser]

eq_inv_smul_iff₀ would have worked without units, but you'd have to keep reminding lean that 0 \ne -1

[Jake Levinson]

To be fair, who among us doesn't forget 0 \ne -1 from time to time?

[Kevin Buzzard]

It's false in characteristic 1 (which is odd and still satisfies 2=0, although 2 is a unit anyway)