Choosing closing tactic when having more than one option

Stream: new members

[Louis Cabarion]

Suppose you have a goal that several tactics below could close. What practical rules of thumb or heuristics help you decide which terminal tactic to apply?

For example:

• If both simp and aesop would close the goal, prefer simp (it’s usually faster).
• If both apply […] and exact […] would close the goal, prefer exact […].
• And so on.

Here is a preliminary list of tactics to consider:

abel
aesop
apply […]
congr
contradiction
convert […]
decide
exact […]
field_simp
grind
infer_instance
linarith
linear_combination
norm_num
norm_num1
omega
positivity
rfl
ring
ring_nf
ring1
rw […]
rwa […]
simp
simp_all
simp_rw […]
simpa
tauto
use […]

[Kenny Lau]

I never use apply, as a rule of thumb (refine/exact instead)

[Louis Cabarion]

@Kenny Lau Is that the recommendation for Mathlib as well?

[Louis Cabarion]

Would it be possible be to establish a simple, rule‐of‐thumb ranking of tactics so that whenever two or more will solve a goal, we generally pick the one that appears earlier on the list?

For example, one might imagine something like this (hypothetically):

1. exact […] (cheapest?, requires no extra tactic import)
2. simp (usually cheap, requires no extra tactic import)
3. grind (usually cheap, requires no extra tactic import)
…
10. aesop (somewhat costly, requires tactic import)
…

Of course, it won’t be perfectly accurate in every case, but it can serve as a useful first-order heuristic.

Would the list above serve as a reasonable initial ordering? What additional tactics might we include?

[Kenny Lau]

1. cheapest: exact, refine
2. very cheap: rintro, cases, induction, subst, rcases, by_cases, generalize
3. cheap: rw, conv
4. moderate: simp (beware of "non-terminal simp")
5. heavy: ring, omega, aesop, norm_num, grind, linarith

[Kenny Lau]

something like this @Isak Colboubrani

[Louis Cabarion]

@Kenny Lau That’s an excellent foundation. Thanks a lot! Which buckets would you assign tauto and abel to, respectively? I assume rfl also belongs to the most cost-effective bucket (though it does carry the caveat "beware of defeq abuse"), right?

[Kenny Lau]

@Isak Colboubrani I've made full statistics in #mathlib4 > Tactic uses in mathlib

[Damiano Testa]

Honestly, I don't think that such a linear ranking will always yield something desirable.

[Damiano Testa]

Kenny, apply improved a lot since the mathlib3 days. I still have a little bit of a prejudice against it, but I actually like it much more than I used to.

[Eric Wieser]

Kenny Lau said:

1. heavy: ring, omega, aesop, norm_num, grind, linarith

I'll note that tactics like ring and norm_num and linarith are more readable to a human than grind or aesop, so if performance is similar, should be chosen instead

[Louis Cabarion]

Kenny Lau said:

Isak Colboubrani I've made full statistics in #mathlib4 > Tactic uses in mathlib

Do you mean performance statistics? I'm afraid I couldn't find any performance statistics in that thread.

[Louis Cabarion]

Damiano Testa said:

Honestly, I don't think that such a linear ranking will always yield something desirable.

Great point! Since it’s meant just as a first-pass guideline, I know it won’t always pick the best tactic. Do you have any examples where a simple linear ranking leads to less-than-ideal results? I understand such examples do exist and I’d appreciate learning from them.

[Jason Reed]

Damiano Testa said:

Kenny, apply improved a lot since the mathlib3 days. I still have a little bit of a prejudice against it, but I actually like it much more than I used to.

Out of curiosity, what were the downsides of apply that have been since ameliorated? Performance? Maintainability in the face of library changes? Something else?

[Kenny Lau]

@Jason Reed the main reason why I avoided apply is because it wouldn't know actually how many holes to leave us with

[Kenny Lau]

theoretically if i have f : A -> B -> C -> D and goal is C -> D and i do apply f then I should end up with two goals, which are A and B

[Kenny Lau]

but sometimes it gets stuck trying to unify D (output of f) with C -> D (goal)

[Jason Reed]

Ah, I see, makes sense, thanks for explaining. I think in practice so far in my use of it it's been such that it usually leaves me with one hole. I can see how that would be undesirable to leave in the final proof. I do find myself using apply and then show_term to get out the refine that I actually leave as the final proof.

[Kenny Lau]

so instead of apply f i just manually specify the correct number of holes as refine f ?_ ?_

[metakuntyyy]

Yeah, once I understood how refine works I really can't not use it. Truly a hidden champion tactic