## Stream: general

### Topic: a fast but unreliable refl

#### 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 }...

#### 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


#### Scott Morrison (Jul 13 2020 at 01:13):

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

#### Scott Morrison (Jul 13 2020 at 01:13):

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

#### Simon Hudon (Jul 13 2020 at 01:14):

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

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

#### Mario Carneiro (Jul 13 2020 at 01:36):

most tactics like rw close with a refl reducible

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

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

#### Scott Morrison (Jul 13 2020 at 02:31):

#3380

Last updated: May 13 2021 at 16:25 UTC