hint tactic

Stream: metaprogramming / tactics

[Tristan Figueroa-Reid]

I wanted to improve the hint tactic with some suggestions from a potential finish tactic:

I want hint to take in three different categories of tactics:

• Finishing tactics (rfl, assumption, contradiction, exist?, trivial, tauto, bv_normalize, bv_decide, decide, norm_num, field_simp, dsimp, simp, dsimp_all, simp_all): These are tactics that close a goal.
• Suggesting tactics (apply?, aesop): Tactics that offer suggestions and/or? close a goal.
• 'Breaker' tactics (constructor, split, intro, ext, congr, congr!): Tactics that further reduce a goal.
  Each tactic in every category should also have an associated weight: some PRs (e.g. https://github.com/leanprover-community/mathlib4/pull/20483) are dedicated to "this aesop could be a simp" or "this simp could be a rw:" if hint suggests the least computationally expensive tactic, that could avoid these PRs.

I did have two questions about this:

1. Does it make sense to modify hint to do this? I was initially thinking of just having a finish tactic that would have the finish and suggest tactic categories. However, if there isn't a tactic that combines finish and hint, people would run both anyway.
2. Does this configuration make sense?

[Kim Morrison]

My suggestion would be to have modifiers on the hint tactic.

[Kim Morrison]

But I think the current behaviour, where hint suggests a finishing tactic if it can, and otherwise suggests something that makes progress, is actually what you want?

[Tristan Figueroa-Reid]

Kim Morrison said:

But I think the current behaviour, where hint suggests a finishing tactic if it can, and otherwise suggests something that makes progress, is actually what you want?

It would be close, but I think having a system where less intensive tactics are tried first would be better for dealing with the time spent on golfing.

[Tristan Figueroa-Reid]

*Not necessarily ran first (as it would be best to run tactics in parallel if possible), but suggested in order of compute time.