feedback on `hint`

Stream: mathlib4

[Julian Berman]

Scott Morrison said:

(Public service announcement for those who haven't been using it: please do report your experiences with hint!)

Where is a good place to put these? In particular I think one previous topic was to mention that hint often suggests aesop which then makes no progress

[Notification Bot]

A message was moved here from #mathlib4 > porting fprop tactic by Scott Morrison.

[Kim Morrison]

How about here.

A repro showing aesop doing nothing would be great. I do remember that, but I think it may have been fixed, too.

[Jannis Limperg]

Aesop should fail when it doesn't make progress. Anything else is a bug.

[Julian Berman]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/hint was one where David shared an example.

[Jannis Limperg]

Example from that thread:

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."

Aesop is working as intended here, but the result is quite confusing. Namely, Aesop makes progress using unsafe rules, but it doesn't manage to solve the goal. Hence, it reports the goals that remain after the safe rules were exhaustively applied, but the safe rules make no progress. So the reported goal is identical to the initial goal.

I see two possible solutions:

1. hint uses aesop (config := { terminal := true }) to suggest only Aesop calls that entirely solve the goal.
2. Aesop reports "no progress" if the safe rules haven't made any progress.

[Julian Berman]

(Separately, but just because I recall it now) -- another recent example where I wished hint had given me some recommendation was:

example {x : ℕ} (h : x ≤ 2) (h' : x ≠ 0) (h'' : x ≠ 2) : x = 1 := sorry

where I would have loved if hint told me interval_cases existed.

[Kim Morrison]

@Jannis Limperg, isn't there a 3rd option, which is that Aesop could report what it achieved with the unsafe rules?

[Kim Morrison]

I guess that too often will produce garbage? In that case, my preference is for option 2.

[Kim Morrison]

Julian Berman said:

(Separately, but just because I recall it now) -- another recent example where I wished hint had given me some recommendation was:

example {x : ℕ} (h : x ≤ 2) (h' : x ≠ 0) (h'' : x ≠ 2) : x = 1 := sorry

where I would have loved if hint told me interval_cases existed.

I would be much happier about register_hint omega, which also solves this goal.

[Kim Morrison]

But register_hint interval_cases is not terrible either.

[Kim Morrison]

register_hint omega is #10259.

[Julian Berman]

Fantastic! Thanks Scott. I guess this is offtopic for hint, but how about having omega run on trivial as well, do you have an opinion and/or advice on whether that's a good idea as well? The original context for that was https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/List.20access.20error/near/409839424 which IIRC was about list indexing, which uses trivial.

[Kim Morrison]

Yes, it's definitely on the agenda to run omega more automatically in array indexing and termination.

omega is intended to fail pretty fast if it has nothing useful to do, although I worry that as people keep asking for more features it is getting slower. :-( I will re-run some benchmarks soon.

[Joachim Breitner]

Issue for omega as default termination checking: https://github.com/leanprover/lean4/issues/3185

[Jannis Limperg]

Scott Morrison said:

Jannis Limperg, isn't there a 3rd option, which is that Aesop could report what it achieved with the unsafe rules?

The main issue with this is that unsafe rules produce multiple sets of leftover goals. Showing all of them would not make for great UI. I could show a heuristically chosen subset, but this would be quite unpredictable. So I think I'll just adjust the progress check.

[Jannis Limperg]

Jannis Limperg said:

Aesop reports "no progress" if the safe rules haven't made any progress.

This is now implemented on Aesop master.

[Julian Berman]

Thank you both! Looking forward to trying it out.