squeeze_erw

Stream: general

[Scott Morrison]

The rw technology I'd most love would be squeeze_erw that gave some hint why an erw was necessary rather than a rw.

[Simon Hudon]

Yes, I'm with you on that. I have no idea where to begin there

[Scott Morrison]

I tried thinking about it at one point, and it seemed hard. :-)

[Simon Hudon]

Actually, for squeeze_erw, maybe we could start with erw h, rw <- h and then do a diff. We'd expect to land back on the initial state but the differences should be telling

[Scott Morrison]

Huh!

[Simon Hudon]

I'm not sure how to translate those differences into something the user can find helpful

[Scott Morrison]

Can we do a convert to compare the initial and final terms?

[Simon Hudon]

I like the idea but because the two terms should be definitionally equal, congr should close the proof with refl. We might need a customized version of convert / congr that refrains from using refl unless we have syntactic equality.

[Simon Hudon]

Maybe that could get us to a series of equalities of the form f x y z = _ where we need to unfold f

[Simon Hudon]

We might want to advise to user to do unfold f before the rewrite but it might also mess our opportunity to rewrite

[Simon Hudon]

Do we have in Lean the equivalent of rewrite _ at 3 in Coq? That would allow us to have very targeted pieces of advice

[Bryan Gin-ge Chen]

There's rw _ {occs := occurrences.pos [3]} as I recently learned.

[Simon Hudon]

Has this been there all along?

[Reid Barton]

Yes

[Simon Hudon]

Uh! I learn every day

[Johan Commelin]

Simon Hudon said:

Do we have in Lean the equivalent of rewrite _ at 3 in Coq? That would allow us to have very targeted pieces of advice

And there is nth_rewrite