## Stream: Is there code for X?

### Topic: Simple ring lemma

#### Yakov Pechersky (Jul 08 2020 at 18:24):

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 (Jul 08 2020 at 18:38):

Are you aware of the noncomm_ring tactic?

#### Oliver Nash (Jul 08 2020 at 18:39):

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 (Jul 08 2020 at 18:40):

Also rw [sub_eq_add_neg] probably helps.

#### Yakov Pechersky (Jul 08 2020 at 18:44):

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 (Jul 08 2020 at 18:45):

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

#### Yakov Pechersky (Jul 08 2020 at 18:45):

Why is noncomm_ring needed instead of ring?

#### Kevin Buzzard (Jul 08 2020 at 18:45):

Because ring only works with commutatve rings :-)

#### Kevin Buzzard (Jul 08 2020 at 18:47):

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

#### Mario Carneiro (Jul 08 2020 at 18:49):

shouldn't simp be able to do this one?

What is the SNF?

#### Mario Carneiro (Jul 08 2020 at 18:50):

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

#### Johan Commelin (Jul 08 2020 at 18:50):

Aah, with some help :thumbs_up:

#### Mario Carneiro (Jul 08 2020 at 18:50):

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

#### Johan Commelin (Jul 08 2020 at 18:51):

This happened several months ago, I think.

#### Mario Carneiro (Jul 08 2020 at 18:52):

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 (Jul 08 2020 at 18:53):

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

#### Johan Commelin (Jul 08 2020 at 18:54):

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 (Jul 08 2020 at 18:54):

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

#### Mario Carneiro (Jul 08 2020 at 18:55):

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 (Jul 08 2020 at 19:07):

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 (Jul 08 2020 at 19:08):

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

#### Yakov Pechersky (Jul 08 2020 at 19:09):

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.

#mwe

#### Mario Carneiro (Jul 08 2020 at 19:11):

what is B, what are the imports

#### Mario Carneiro (Jul 08 2020 at 19:12):

oh wait B is local

#### Mario Carneiro (Jul 08 2020 at 19:12):

I don't see sub_neg_mul though

#### Mario Carneiro (Jul 08 2020 at 19:13):

oh ignore me I'm being silly

import tactic
universe u

#### Yakov Pechersky (Jul 08 2020 at 19:14):

Yes, edited above

#### Mario Carneiro (Jul 08 2020 at 19:17):

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

That's amazing.

#### Yakov Pechersky (Jul 08 2020 at 19:20):

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 (Jul 08 2020 at 19:20):

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 (Jul 08 2020 at 19:22):

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 (Jul 08 2020 at 19:23):

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

#### Mario Carneiro (Jul 08 2020 at 19:28):

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 (Jul 08 2020 at 19:31):

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 (Jul 08 2020 at 19:31):

= 1 not = 0

Last updated: May 07 2021 at 22:14 UTC