Zulip Chat Archive

Stream: general

Topic: squeeze_dsimp?


view this post on Zulip Scott Morrison (May 03 2019 at 18:15):

Is there any prospect, @Simon Hudon, of writing a squeeze_dsimp? I would find this very useful when debugging dsimp, simp, dsimp, simp fiascos.

view this post on Zulip Scott Morrison (May 03 2019 at 18:20):

A related thing that would be really useful would be a method for diagnosing the need for erw instead of rw.

view this post on Zulip Scott Morrison (May 03 2019 at 18:21):

Very often, erw can be replaced with a change ..., rw (i.e. change by hand the defeq thing that erw is finding, that rw can't). It would be lovely to be told what the required change ... actually is.

view this post on Zulip Scott Morrison (May 03 2019 at 18:21):

Because often this is actually a missing refl-lemma..

view this post on Zulip Simon Hudon (May 03 2019 at 18:27):

Two interesting projects. I can look into them.

view this post on Zulip Simon Hudon (May 03 2019 at 18:28):

For the erw one, maybe I can do it by applying erw, then rw <- with the same lemma. I'll see.

view this post on Zulip Simon Hudon (May 03 2019 at 18:28):

What do you want it to be called?

view this post on Zulip Johan Commelin (May 03 2019 at 18:28):

I like the convention of tagging a ? onto the name

view this post on Zulip Johan Commelin (May 03 2019 at 18:29):

But for things in core that is hard...

view this post on Zulip Simon Hudon (May 03 2019 at 18:29):

We'd need to change core for that. I'm trying to make 3.5.0c backward compatible so for now, I'm not moving tactics from mathlib to core or even adding tactics that are needed in mathlib.

view this post on Zulip Johan Commelin (May 03 2019 at 18:30):

I understand

view this post on Zulip Johan Commelin (May 03 2019 at 18:31):

Even though foo? should of course never appear in mathlib. These tactics are for debugging/optimizing proofs only.

view this post on Zulip Johan Commelin (May 03 2019 at 18:31):

Anyway... in that case I would suggest squeeze_erw etc

view this post on Zulip Simon Hudon (May 03 2019 at 18:43):

:+1:


Last updated: May 15 2021 at 00:39 UTC