Zulip Chat Archive

Stream: general

Topic: tidy hole command


view this post on Zulip Johan Commelin (Sep 03 2018 at 17:50):

@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.

view this post on Zulip Scott Morrison (Sep 03 2018 at 20:04):

@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!

view this post on Zulip Scott Morrison (Sep 03 2018 at 20:05):

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

view this post on Zulip Johan Commelin (Sep 03 2018 at 20:05):

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

view this post on Zulip Johan Commelin (Sep 03 2018 at 20:06):

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

view this post on Zulip Scott Morrison (Sep 03 2018 at 20:06):

Ah, okay. Absolutely, I can do that.

view this post on Zulip Johan Commelin (Sep 03 2018 at 20:06):

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

view this post on Zulip Kenny Lau (Sep 03 2018 at 20:07):

by induction convert tactic proofs to term proofs

view this post on Zulip Scott Morrison (Sep 03 2018 at 20:07):

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

view this post on Zulip Patrick Massot (Sep 03 2018 at 20:07):

I think refl tries slightly harder than rfl

view this post on Zulip Johan Commelin (Sep 03 2018 at 20:07):

That's somewhere on the VScode extension wishlist

view this post on Zulip Johan Commelin (Sep 03 2018 at 20:08):

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).

view this post on Zulip Johan Commelin (Sep 03 2018 at 20:09):

Anyway, this is not high priority stuff.

view this post on Zulip Chris Hughes (Sep 03 2018 at 20:14):

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

view this post on Zulip Patrick Massot (Sep 03 2018 at 20:15):

I think it also does more definitional reduction

view this post on Zulip Chris Hughes (Sep 03 2018 at 20:29):

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


Last updated: May 14 2021 at 23:14 UTC