Zulip Chat Archive

Stream: general

Topic: Why can't `rw` look inside lambda expressions?


view this post on Zulip Johan Commelin (Jul 24 2018 at 13:46):

I often find myself trying to do a rewrite, and then it fails miserably while it shouldn't. Suppose I have a finset.sum univ (\lam x, f(x + x)) in my goal, and I know that f is a group hom. Then I want to rewrite that f(x + x) to f(x) + f(x). But Lean always complains. So I have to do a little dance with rw show [relevant part goes here], which feels clumsy. What am I doing wrong?

view this post on Zulip Simon Hudon (Jul 24 2018 at 13:47):

rw can't rewrite bound variables. simp is more useful there.

view this post on Zulip Simon Hudon (Jul 24 2018 at 13:49):

If you're worried about simp trying too many rules, you can restrict it with simp only [my interesting rule] or disable individual simp rules with simp [my_rule, - no_no_rule]

view this post on Zulip Johan Commelin (Jul 24 2018 at 13:49):

It works!

view this post on Zulip Simon Hudon (Jul 24 2018 at 13:50):

:party_popper:

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 16:08):

You can also use conv in (f(x+x)) begin rw ... end. See Patrick's conv notes in the mathlib docs.

view this post on Zulip Johan Commelin (Jul 24 2018 at 16:26):

Thanks, I'll take a look.

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 16:29):

https://github.com/leanprover/mathlib/tree/master/docs/extras

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 16:29):

conv.md

view this post on Zulip Johan Commelin (Jul 24 2018 at 16:40):

Ok, it was a long time ago that I read that doc. It's really cool! I will be able to use that quite a lot I guess.


Last updated: May 14 2021 at 03:27 UTC