Simple ring lemma

Stream: Is there code for X?

[Yakov Pechersky]

Is there no such lemma? Seems helpful on the way to cancel subtraction of negative things, particularly if c is negative:

example {R : Type*} [ring R] {a b c : R} : a - (b * c) = a + (-b * c) :=
begin
  refine (add_right_inj a).mpr _,
  simp only [neg_mul_eq_neg_mul_symm],
end

[Oliver Nash]

Are you aware of the noncomm_ring tactic?

[Oliver Nash]

E.g.,

import tactic.noncomm_ring

example {R : Type*} [ring R] {a b c : R} : a - (b * c) = a + (-b * c) := by noncomm_ring

[Johan Commelin]

Also rw [sub_eq_add_neg] probably helps.

[Yakov Pechersky]

Great:

lemma sub_neg_mul {R : Type*} [ring R] {a b c : R} : a - (b * c) = a + (-b * c) :=
begin
  rw [sub_eq_add_neg, add_right_inj _, neg_mul_eq_neg_mul_symm]
end

[Yakov Pechersky]

Really, I have a larger term, but noncomm_ring is putting (-1) •ℤ in the term.

[Yakov Pechersky]

Why is noncomm_ring needed instead of ring?

[Kevin Buzzard]

Because ring only works with commutatve rings :-)

[Kevin Buzzard]

I propose fixing this by renaming the comm_ring class to ring but not everyone agrees...

[Mario Carneiro]

shouldn't simp be able to do this one?

[Johan Commelin]

What is the SNF?

[Mario Carneiro]

example {R : Type*} [ring R] {a b c : R} : a - (b * c) = a + (-b * c) :=
by simp [sub_eq_add_neg]

[Johan Commelin]

Aah, with some help :thumbs_up:

[Mario Carneiro]

I guess we finally took sub_eq_add_neg out of the default simp set

[Johan Commelin]

This happened several months ago, I think.

[Mario Carneiro]

We could have a simp lemma going the other way now, which would solve this one but might make other AC addition proofs harder

[Johan Commelin]

I think that "move --signs outwards, and merge with +, are reasonable simp-moves.

[Johan Commelin]

I think we have all the simp-lemmas for has_sub.sub already, so the simp-set should stay confluent if we add sub_eq_add_neg.symm.

[Johan Commelin]

(Did I just use the word "confluent"? Did I use it correctly? :open_mouth: :see_no_evil:)

[Mario Carneiro]

theorem add_neg {α} [add_group α] (a b : α) : a + -b = a - b := rfl
example {R : Type*} [ring R] {a b c : R} : a - (b * c) = a + (-b * c) :=
by simp [add_neg]

[Yakov Pechersky]

Here's my actual proof:

import tactic

universe u

lemma sub_neg_mul {R : Type*} [ring R] {a b c : R} : a - (b * c) = a + (-b * c) :=
begin
  simp [sub_eq_add_neg],
end

example {R : Type u} [field R] {a b c d : R} {B : fin 2 -> fin 2 -> R} (hb : b ≠ 0)
  (hAB'''' :  b * c / d * B 0 (0 : fin 2).succ + b * B (0 : fin 2).succ (0 : fin 2).succ = 0)
  : B 1 1 = - c / d * B 0 1 :=
begin
  rw <-sub_eq_zero,
  rw <-mul_right_inj' hb,
  rw [mul_sub, mul_zero],
  rw sub_neg_mul,
  rw [<-mul_assoc, <-mul_div_assoc],
  rw neg_mul_neg,
  rw add_comm,
  rw [mul_div_assoc, mul_assoc],
  rw <-hAB'''',
  ring
end

[Yakov Pechersky]

Sorry for the complicated statement. I'm still not great at knowing how to supply *_assoc, *_comm to simp when necessary

[Yakov Pechersky]

The 0.succ is annoying. It's in a hypothesis that I have, after a simp and no simp_rw (0.succ = 1) at hAB'''' removes the .succ.

[Mario Carneiro]

#mwe

[Mario Carneiro]

what is B, what are the imports

[Mario Carneiro]

oh wait B is local

[Mario Carneiro]

I don't see sub_neg_mul though

[Mario Carneiro]

oh ignore me I'm being silly

[Mario Carneiro]

import tactic
universe u

[Yakov Pechersky]

Yes, edited above

[Mario Carneiro]

example {R : Type u} [field R] {a b c d : R} {B : fin 2 -> fin 2 -> R} (hb : b ≠ 0)
  (h :  b * c / d * B 0 (0 : fin 2).succ + b * B (0 : fin 2).succ (0 : fin 2).succ = 0)
  : B 1 1 = - c / d * B 0 1 :=
begin
  change ((0 : fin 2).succ : fin 2) with 1 at h,
  rw [← mul_right_inj' hb, ← add_right_inj, h],
  ring,
end

[Yakov Pechersky]

That's amazing.

[Yakov Pechersky]

Somehow change ((0 : fin 2).succ : fin 2) with 1 at * doesn't make the change in hypotheses I have that are of the form hBA'''' : b * B 0 0 + d * B 0 0.succ = 0,

[Mario Carneiro]

example {R : Type u} [field R] {a b c d : R} {B : fin 2 -> fin 2 -> R} (hb : b ≠ 0)
  (h :  b * c / d * B 0 (0 : fin 2).succ + b * B (0 : fin 2).succ (0 : fin 2).succ = 0)
  : B 1 1 = - c / d * B 0 1 :=
begin
  change ((0 : fin 2).succ : fin 2) with 1 at h,
  rw [← mul_right_inj' hb],
  simpa [neg_div, eq_neg_iff_add_eq_zero, mul_div_assoc, mul_assoc, add_comm] using h,
end

[Mario Carneiro]

I don't know what 0.succ is in that expression, but basically you have to match that expression syntactically on the lhs of the change with

[Yakov Pechersky]

It should be of type fin 2. Okay, I'll try to match it more precisely

[Mario Carneiro]

alternatively, you can ignore what it says and just say what you want using plain change as in

  change b * B 0 0 + d * B 0 1 = 0 at hBA'''',

[Yakov Pechersky]

On a similar hypothesis, trying your suggestion:

change (c * B 0 1 + d * B 1 1 = 0) at hAB'',

tactic.change failed, given type
  c * B 0 1 + d * B 1 1 = 0 → false
is not definitionally equal to
  c * B 0 0.succ + d * B 0.succ 0.succ = 1 → false

[Mario Carneiro]

= 1 not = 0

[Mark Andrew Gerads]

I need this lemma, and if I can help make the ring command gain the capability to solve this, that would be great. I tried library_search.

lemma inv_mul_other_mul_self_cancel (z1 z2:ℂ) (h:z1≠0): z1⁻¹ * z2 * z1 = z2:=

[Johan Commelin]

My guess

  field_simp,
  ring

[Eric Wieser]

Should be possible in two rewrites as well