Zulip Chat Archive

Stream: general

Topic: a fast but unreliable `refl`


view this post on Zulip Scott Morrison (Jul 13 2020 at 01:10):

Does anyone have any suggestions for a tactic that will perform a "cheap rfl", but not an expensive one?

I'm realising that often the reason the tidy is slow is that refl is at the top of its list of tactics. This is potentially very expensive.

Removing this from tidy entirely, mathlib still compiles (one irrelevant exception), but is actually slower. However I have some non-in-mathlib examples where removing refl speeds up tidy a lot.

So far my best idea is to replace it with try_for 100 { refl }...

view this post on Zulip Simon Hudon (Jul 13 2020 at 01:13):

what if you write something like:

do (l,r) <- target >>= match_eq,
   guard (l = r), -- or alpha equal
   refl

view this post on Zulip Scott Morrison (Jul 13 2020 at 01:13):

Oh ... I obviously should be trying refl transparency.reducible.

view this post on Zulip Scott Morrison (Jul 13 2020 at 01:13):

I'll also try that, @Simon Hudon, thanks.

view this post on Zulip Simon Hudon (Jul 13 2020 at 01:14):

That will be a very pessimistic refl but it should be faster than checking def equality

view this post on Zulip Simon Hudon (Jul 13 2020 at 01:15):

(also, you may want to use instantiate_mvars on the goal but if you can avoid it, it will be faster)

view this post on Zulip Mario Carneiro (Jul 13 2020 at 01:36):

most tactics like rw close with a refl reducible

view this post on Zulip Scott Morrison (Jul 13 2020 at 01:49):

Unfortunately refl reducible didn't give me the speed-up I wanted. (Or rather, it gives me the speed-up on not-in-mathlib examples, but slows down tidy in mathlib by almost 60s.)

view this post on Zulip Scott Morrison (Jul 13 2020 at 01:49):

It seems try_for 50 { refl } is actually pretty good. I get all the speed in mathlib, and it's a pretty tight bound.

view this post on Zulip Scott Morrison (Jul 13 2020 at 02:31):

#3380


Last updated: May 13 2021 at 16:25 UTC