tidy hole command

Stream: general

[Johan Commelin]

@Scott Morrison The tidy hole command is really marvellous. Here are some trivialities that might give epsilon improvement:
(1) If tidy generates the proof begin refl end, generate rfl instead.
(2) If tidy generates the proof begin exact foo end, generate foo instead.

[Scott Morrison]

@Johan Commelin, the first is impossible, or rather useless: Lean actually decides _in the parser_ whether you not you proved by rfl, rather than inspecting the proof term!

[Scott Morrison]

But (2) will go on my todo list. (i.e. I'll leave your message starred :-)

[Johan Commelin]

No, I mean that you inspect the string you are about to return.

[Johan Commelin]

The hole command returns some string, and VScode substitutes that for the hole. Is that right?

[Scott Morrison]

Ah, okay. Absolutely, I can do that.

[Johan Commelin]

If that string is exactly begin refl end, then you might as well output rfl instead.

[Kenny Lau]

by induction convert tactic proofs to term proofs

[Scott Morrison]

I can also have "begin just_one_tactic end" into "by just_one_tactic".

[Patrick Massot]

I think refl tries slightly harder than rfl

[Johan Commelin]

That's somewhere on the VScode extension wishlist

[Johan Commelin]

I think refl tries slightly harder than rfl

Hmmm... that might be true. So maybe we need to slightly patch tidy, to first try exact rfl. Then (1) will be a special case of (2).

[Johan Commelin]

Anyway, this is not high priority stuff.

[Chris Hughes]

refl works for any reflexive relation I think. rfl is just equality.

[Patrick Massot]

I think it also does more definitional reduction

[Chris Hughes]

Can you give an example? If I prove something with by refl, the proof term is just eq.refl _ which is rfl