a fast but unreliable `refl`

Stream: general

[Scott Morrison]

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]

what if you write something like:

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

[Scott Morrison]

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

[Scott Morrison]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Mario Carneiro]

most tactics like rw close with a refl reducible

[Scott Morrison]

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]

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]

#3380