Zulip Chat Archive

Stream: general

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


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

@[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...

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

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

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

view this post on Zulip Patrick Massot (Aug 05 2018 at 22:12):

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

view this post on Zulip Kevin Buzzard (Aug 05 2018 at 22:13):

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

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

view this post on Zulip Kevin Buzzard (Aug 05 2018 at 22:14):

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

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

view this post on Zulip Patrick Massot (Aug 05 2018 at 22:14):

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

view this post on Zulip Mario Carneiro (Aug 05 2018 at 22:14):

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

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

view this post on Zulip Mario Carneiro (Aug 05 2018 at 22:15):

this is an active area of research

view this post on Zulip Kevin Buzzard (Aug 05 2018 at 22:15):

Oh wow

view this post on Zulip Kevin Buzzard (Aug 05 2018 at 22:15):

How come humans are so good at it?

view this post on Zulip Mario Carneiro (Aug 05 2018 at 22:15):

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

view this post on Zulip Mario Carneiro (Aug 05 2018 at 22:16):

and that's really hard and complicated

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

view this post on Zulip Mario Carneiro (Aug 05 2018 at 22:17):

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

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