Zulip Chat Archive

Stream: new members

Topic: Rewriting on objects that haven't been introduced


view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 19 2018 at 18:29):

I have the following term in my goal:

tendsto (λ (h : ), ((f + g) (x + h) - (f x + g x) - (f' x + g' x) * h) / h) (nhds 0) (nhds (0 + 0))

And want to rewrite pi.add_apply to the (f + g) (x + h) term. But I can't, since h is not really a variable. Is there any way to work with rewrites on h without introducing everything before it?

view this post on Zulip Patrick Massot (Nov 19 2018 at 18:34):

simp can do it

view this post on Zulip Patrick Massot (Nov 19 2018 at 18:34):

Try simp only [pi.add_apply]

view this post on Zulip Patrick Massot (Nov 19 2018 at 18:35):

In this case it's probably definitionaly true, so you could probably also use change

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 19 2018 at 18:36):

Ok, sure, that works here -- but in a situation where the rewrite can't be done with simp (e.g. if it involves \l), is there a more general solution? I mean, what is simp actually using behind the scenes?

view this post on Zulip Patrick Massot (Nov 19 2018 at 18:36):

something like tendsto (λ (h : ℝ), (f (x + h) + g (x + h) - (f x + g x) - (f' x + g' x) * h) / h) (nhds 0) (nhds (0 + 0))

view this post on Zulip Patrick Massot (Nov 19 2018 at 18:36):

conv can be the answer

view this post on Zulip Patrick Massot (Nov 19 2018 at 18:36):

but simp can also go under binders sometimes

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 19 2018 at 18:37):

Hm, hadn't heard of conv. Interesting.

view this post on Zulip Patrick Massot (Nov 19 2018 at 18:37):

https://github.com/leanprover/mathlib/blob/master/docs/extras/conv.md

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 19 2018 at 18:38):

One more question -- to get the goal in the form above with nhds(0 + 0) and stuff, I couldn't just use a simple rewrite rw ←zero_add, because rw becomes too overzealous and turns both 0s to 0+0 (instead I had to have a statement that the new goal implies the old goal and prove that by rw zero_add). Is there any way to gain some control over the rewrite and make it transform things one at a time?

view this post on Zulip Patrick Massot (Nov 19 2018 at 18:40):

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/rewrite_cfg and also the conv doc I mentioned in my previous answer

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 19 2018 at 18:41):

Thanks, I'll have a look at it.


Last updated: May 18 2021 at 17:44 UTC