Cancel out common terms

Stream: new members

[Jakub Nowak]

It there really no non-terminal tactic that can cancel out common terms on both sides of equality?

import Mathlib

example [AddCommGroup α] (a b c d x y z : α) : a + b + c + d = a + x + y + z := by
  rw [add_assoc (a + b) c d, add_assoc a b (c + d), add_assoc (a + x) y z, add_assoc a x (y + z), add_right_inj a]

-- This happens to work too, because abel_nf decided to reorder the terms.
example [AddCommGroup α] (a b c d x y z : α) : a + b + c + d = a + x + y + z := by
  abel_nf
  rw [add_right_inj a]

example [AddCommGroup α] (a b c d x y z : α) : a + b + c + d = a + x + y + z := by
  hint

[Yan Yablonovskiy 🇺🇦]

Not sure if this fits your criteria since its not a tactic per say but you can do

simp [add_assoc]

[Jakub Nowak]

Tbh, I just want a one-shot tactic that can simplify arithmetic/group/ring expressions like this one. I would expect abel_nf to be able to do this, is there some technical reason why abel_nf can't cancel terms? Maybe that's something that could be improved? Or should we wait for non-terminal grind?

[Yan Yablonovskiy 🇺🇦]

Jakub Nowak said:

Tbh, I just want a one-shot tactic that can simplify arithmetic/group/ring expressions like this one. I would expect abel_nf to be able to do this, is there some technical reason why abel_nf can't cancel terms?

I think the main issue is associativity by default from the right here, so your a is buried by invisible parenthesis'.
For example if you put your a at the end:

example [AddCommGroup α] (a b c d x y z : α) : b + c + d + a = x + y + z + a := by
 simp -- ⊢ b + c + d = x + y + z

Though that doesn't help abel seemingly. And typically associativity doesn't play well with simp for technical reasons so they aren't tagged by default usually afaik.

[Jakub Nowak]

Yes, simp machinery can't deal with things like that. That's why there's e.g. abel_nf. I'm not sure how it works, but I'm assuming it stores addition as a set of terms, instead of list, to deal with them regardless of order?

[Yan Yablonovskiy 🇺🇦]

Looking at the docs it seems to try reduce expressions, but doesn't seem to cancel out equations ( from what i can see). So i think it might only reduce with its rules on both sides.

[Yan Yablonovskiy 🇺🇦]

(deleted)

[Ruben Van de Velde]

A more robust approach is

import Mathlib

example [AddCommGroup α] (a b c d x y z : α) : a + b + c + d = a + x + y + z := by
  move_add [a]; simp only [add_left_inj]
  sorry

but it does make you repeat the term you want to cancel

[Ruben Van de Velde]

@Damiano Testa do you think something for this would be easy to add? I've often wanted it as well

[Jakub Nowak]

Oh, I didn't know about move_*, that's nice. Thanks!

[Damiano Testa]

Actually, move_add was supposed to be the first step towards this further simplification.

[Damiano Testa]

Adding the cancellation would be straightforward.

[Kevin Buzzard]

example [AddCommGroup α] (a b c d x y z : α) : a + b + c + d = a + x + y + z := by
  abel_nf
  congr 1

is a lemma-free way.

[Ruben Van de Velde]

Does abel guarantee that the common terms end up on the correct side to cancel?

[Yan Yablonovskiy 🇺🇦]

Ruben Van de Velde said:

Does abel guarantee that the common terms end up on the correct side to cancel?

Doesn't seem like it

example [AddCommGroup α] (a b c d x y z : α) : b + a + c + d = x + a + y + z := by
  abel_nf
  congr 1

[Jakub Nowak]

It looks like abel_nf simplifies lhs and rhs separately.
What do you think of a tactic abel_simp, that collects both sides of equation into one polynomial, and then outputs monomials on either lhs or rhs, to make coefficients positive? We could also have abel_simp +collect that outputs all monomials on lhs, and 0 on rhs.
Or we could just make this a default behaviour for abel_nf, is there any reason, to have handling of equations as separate tactic? And if someone wanted to disable this behaviour, they can do

conv => lhs; abel_nf
conv => rhs; abel_nf

[Kevin Buzzard]

example [AddCommGroup α] (a b c d x y z : α) : b + a + c + d = x + a + y + z := by
  move_add [a]
  congr 1
  -- ⊢ b + c + d = x + y + z
  sorry