squeeze_dsimp?

Stream: general

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Simon Hudon]

Two interesting projects. I can look into them.

[Simon Hudon]

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

[Simon Hudon]

What do you want it to be called?

[Johan Commelin]

I like the convention of tagging a ? onto the name

[Johan Commelin]

But for things in core that is hard...

[Simon Hudon]

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.

[Johan Commelin]

I understand

[Johan Commelin]

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

[Johan Commelin]

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

[Simon Hudon]

:+1: