hint

Stream: new members

[Julian Berman]

How should I think about what hint's "job" is?
I used to (in Mathlib3) use it as "I think one of the 'simple' tactics in the library will fully solve the goal but I forget which, so run all of them and tell me which ones do". Perhaps this was wrong even in Lean 3, but it worked some small amount of time, mostly to remind me about goals where trivial or something worked. Now however, in the small amount of time that I try hint, it often will recommend aesop and simp, tactics which then will potentially complain they didn't make any progress after trying them. I've assumed that's simply hint saying "I have no ideas but these tactics are pretty strong, try those" -- but is there now something that will do what my previous mental model had, i.e. "try a set of tactics and tell me if they solve the goal"?

[Johan Commelin]

I am quite sure that your mental model about the Lean 3 version is correct.

[Johan Commelin]

My impression is also that hint should only suggest tactics that actually make progress.

[Julian Berman]

Thanks! OK. I don't have an example in front of me, but I'm somewhat sure I had one recently where hint suggested aesop which didn't solve the goal or seemingly make any progress, even with unfolding. I'll have to follow up.

[David Renshaw]

yeah, I've noticed this too. hint suggests aesop but aesop does not actually do anything

[David Renshaw]

example that I have at hand:

import Mathlib.Tactic

lemma lemma1 (x : ZMod 13) : x^3 = 0 ∨ x^3 = 1 ∨ x^3 = -1 ∨ x^3 = 5 ∨ x^3 = -5 := by
  hint
-- Try these:
-- • aesop

-- ... but `aesop` fails with "failed to prove the goal after exhaustive search."