Preferred tactic selection heuristics

Stream: new members

[Louis Cabarion]

Do the following tactic selection heuristics sound reasonable? Are there any similar rules of thumb that could be added?

1. When both exact … and simp can close a goal, it is generally preferable to use exact ….
2. When both simp and simp_all can close a goal, it is generally preferable to use simp.
3. When both simp_all and grind can close a goal, it is generally preferable to use simp_all.
4. When both grind and omega can close a goal, it is generally preferable to use grind.
5. When both omega and aesop can close a goal, it is generally preferable to use omega.

[Kenny Lau]

I don't actually know which one is preferred out of rw and simp only

[Louis Cabarion]

It would be nice to have tactic selection heuristics also for the pairs:

• simp vs. {abel, assumption, congr, contradiction, linarith, norm_num, positivity, ring, tauto, trivial}: do we always want to use simp in these cases?
• grind vs. {abel, assumption, congr, contradiction, linarith, norm_num, positivity, ring, tauto, trivial}: when is grind the proper choice?

Any ideas/opinions?

[Kyle Miller]

1: It depends on what exact is doing. Is it causing lots of definitions to unfold? Is it doing "defeq abuse"? Then no, simp would be preferred.

3: Both simp_all and grind can be better than the other, even if both close the goal. I'd time it. Even so, I might prefer grind.

4: Yes, prefer grind because it's meant to subsume omega, and omega I believe is planned to be deprecated, eventually.

[Kyle Miller]

My opinion: the rule of thumb is that you should use the tactic that logically makes sense to use, and if it's slow you may want to consider alternatives. The valuable thing here is knowing what alternatives are available; it's unclear to me what the purpose of further heuristics are. Maintainable proofs? Fast proofs? Easier-to-write proofs? Etc.