simp lemma `a + (b + -a) = b`?

Stream: general

[Kevin Buzzard]

@Guillermo Barajas Ayuso wanted

import data.real.basic

theorem auxiliary_basic (a b : ℝ) (f : ℝ → ℝ → ℝ) :
f a b = f (a + (1 - 1) * (b - a) / (2 ^ 0)) (a + 1 * (b - a) / (2 ^ 0)) := by simp -- fails

and simp didn't quite do it; it reduces the problem to a + (b + -a) = b. There's a non-simp lemma add_sub_cancel'_right : a + (b - a) = b but by simp [add_sub_cancel'_right] doesn't work either, presumably because simp decides that replacing all subs with negs is a good idea before it can spot how to apply add_sub_cancel'_right. On the other hand actually adding what simp gets stuck on works fine:

import data.real.basic

@[simp] theorem add_bracket_add_neg_self_bracket_cancel {α : Type} [add_comm_group α] {a b : α} :
a + (b + -a) = b := by rw [add_comm,add_assoc,neg_add_self,add_zero]

theorem auxiliary_basic (a b : ℝ) (f : ℝ → ℝ → ℝ) :
f a b = f (a + (1 - 1) * (b - a) / (2 ^ 0)) (a + 1 * (b - a) / (2 ^ 0)) := by simp

Should a + (b + -a) = b be a simp lemma? It's about time I got the hang of this stuff. It's passing all the rules of thumb I've picked up, but my rules of thumb are not yet watertight...

[Patrick Massot]

It's funny, I came across the exact same problem yesterday. Don't forget you can also use simp [-sub_eq_add_neg, ...] to get rid of the annoying "simplification"

[Mario Carneiro]

I'm okay with adding this as a simp lemma, but it doesn't really fix the problem - you will also need lemmas for a + (b + (c + -a)) and a + (b + (-a + c)) and so on. The problem is that simp doesn't make any attempt to bring negatives together, so at best you can get lucky if they don't have so far to migrate

[Mario Carneiro]

This is in part what ring is for, and Jeremy suggested also focusing an abel type tactic focusing only on the additive stuff

[Patrick Massot]

I also wanted to ask for a version of ring working in an abelian group

[Kevin Buzzard]

removing sub_eq_add_neg stops Lean from simplifying (1 - 1) :-)

[Mario Carneiro]

I think sub_eq_add_neg is a bad choice of simp lemma, but I know why it's there - it limits the expressivity of input statements so you need fewer simp lemmas overall

[Kevin Buzzard]

I thought that simp internally put things into some secret ordering using associativity and commutativity?

[Mario Carneiro]

of course if sub_eq_add_neg was not a simp lemma we would need a - a = 0 to be a simp lemma

[Patrick Massot]

Is this also part of what Johannes simplifier work is meant to address?

[Mario Carneiro]

it does, but that ordering does not put a and -a close together

[Kevin Buzzard]

it does, but that ordering does not put a and -a close together

Might I suggest a different secret ordering?

[Mario Carneiro]

this is an active area of research

[Kevin Buzzard]

Oh wow

[Kevin Buzzard]

How come humans are so good at it?

[Mario Carneiro]

because they use adaptive algorithms that pay attention to the right things

[Mario Carneiro]

and that's really hard and complicated

[Mario Carneiro]

keep in mind that simp is used in way more circumstances than doing algebra on commutative groups

[Mario Carneiro]

and you need to keep up performance in the other areas too

[Mario Carneiro]

I think Johannes was working on adding "simpprocs" to the simplifier, which would enable this kind of adaptivity. It would notice we are doing algebra and fire up the algebra module that knows to do cancellation and stuff