## Stream: general

### Topic: simp lemma a + (b + -a) = b?

#### Kevin Buzzard (Aug 05 2018 at 21:55):

@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

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 (Aug 05 2018 at 22:07):

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 (Aug 05 2018 at 22:11):

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 (Aug 05 2018 at 22:12):

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 (Aug 05 2018 at 22:12):

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

#### Kevin Buzzard (Aug 05 2018 at 22:13):

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

#### Mario Carneiro (Aug 05 2018 at 22:13):

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 (Aug 05 2018 at 22:14):

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

#### Mario Carneiro (Aug 05 2018 at 22:14):

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 (Aug 05 2018 at 22:14):

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

#### Mario Carneiro (Aug 05 2018 at 22:14):

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

#### Kevin Buzzard (Aug 05 2018 at 22:14):

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

Might I suggest a different secret ordering?

#### Mario Carneiro (Aug 05 2018 at 22:15):

this is an active area of research

Oh wow

#### Kevin Buzzard (Aug 05 2018 at 22:15):

How come humans are so good at it?

#### Mario Carneiro (Aug 05 2018 at 22:15):

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

#### Mario Carneiro (Aug 05 2018 at 22:16):

and that's really hard and complicated

#### Mario Carneiro (Aug 05 2018 at 22:16):

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

#### Mario Carneiro (Aug 05 2018 at 22:17):

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

#### Mario Carneiro (Aug 05 2018 at 22:18):

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

Last updated: May 16 2021 at 21:11 UTC