Zulip Chat Archive

Stream: Is there code for X?

Topic: Simple ring lemma


view this post on Zulip 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

view this post on Zulip Oliver Nash (Jul 08 2020 at 18:38):

Are you aware of the noncomm_ring tactic?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 08 2020 at 18:40):

Also rw [sub_eq_add_neg] probably helps.

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jul 08 2020 at 18:45):

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

view this post on Zulip Yakov Pechersky (Jul 08 2020 at 18:45):

Why is noncomm_ring needed instead of ring?

view this post on Zulip Kevin Buzzard (Jul 08 2020 at 18:45):

Because ring only works with commutatve rings :-)

view this post on Zulip Kevin Buzzard (Jul 08 2020 at 18:47):

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

view this post on Zulip Mario Carneiro (Jul 08 2020 at 18:49):

shouldn't simp be able to do this one?

view this post on Zulip Johan Commelin (Jul 08 2020 at 18:50):

What is the SNF?

view this post on Zulip 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]

view this post on Zulip Johan Commelin (Jul 08 2020 at 18:50):

Aah, with some help :thumbs_up:

view this post on Zulip Mario Carneiro (Jul 08 2020 at 18:50):

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

view this post on Zulip Johan Commelin (Jul 08 2020 at 18:51):

This happened several months ago, I think.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 08 2020 at 18:53):

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

view this post on Zulip 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.

view this post on Zulip 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:)

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 08 2020 at 19:11):

#mwe

view this post on Zulip Mario Carneiro (Jul 08 2020 at 19:11):

what is B, what are the imports

view this post on Zulip Mario Carneiro (Jul 08 2020 at 19:12):

oh wait B is local

view this post on Zulip Mario Carneiro (Jul 08 2020 at 19:12):

I don't see sub_neg_mul though

view this post on Zulip Mario Carneiro (Jul 08 2020 at 19:13):

oh ignore me I'm being silly

view this post on Zulip Mario Carneiro (Jul 08 2020 at 19:13):

import tactic
universe u

view this post on Zulip Yakov Pechersky (Jul 08 2020 at 19:14):

Yes, edited above

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jul 08 2020 at 19:19):

That's amazing.

view this post on Zulip 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,

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Jul 08 2020 at 19:23):

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

view this post on Zulip 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'''',

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 08 2020 at 19:31):

= 1 not = 0


Last updated: May 07 2021 at 22:14 UTC