suggest

Stream: general

[Johan Commelin]

These lemmas seem to always drift to the top of suggest:

Try this: refine eq.symm _
Try this: refine eq_comm.mp _
Try this: refine eq_of_heq _
Try this: refine heq_iff_eq.mp _
Try this: refine plift.up.inj _
Try this: refine ulift.up.inj _

That's probably because the don't need anything (hypothesis-wise), but they also accomplish "nothing" (goal-wise).
Could suggest have a "blacklist" of lemmas that it will only suggest if they actually close the goal?

[Kevin Buzzard]

good luck closing a goal with eq.symm :-) Actually, I guess eq.symm zero_add might solve something, but would suggest spot this?

[Johan Commelin]

If you have assumption h : x = y, and goal y = x, then suggest should reply exact eq.symm h.

[Johan Commelin]

But if you don't have such a hypothesis, it should not reply refine eq.symm _

[Lucas Allen]

If @Scott Morrison doesn't want to do this right now, I can have a bit of a think about it.

I'd probably only take Scott about half an hour to do it though. It'll take me a little longer.

[Scott Morrison]

I'd prefer not to blacklist, but instead tweak the sorting algorithm, which is still quite dumb.

[Scott Morrison]

Currently we sort by (lexicographic ordering on) the pair: "number of resulting goals", "(negative) number of local hypotheses appearing in the partial proof term".

[Scott Morrison]

A known problem is that "appearing in the partial proof term" is not really what we want to count; at the moment we really just count appearances as subexpressions. Instead it would be better to count "voluntary" uses, i.e. actual occasions when solve_by_elim choose to use a hypothesis to fill a blank, and ignore the "involuntary" ones through dependencies.

[Scott Morrison]

I'm not sure either how to make to that precise, or do the counting without creating spaghetti.

[Scott Morrison]

By this counting, eq.symm will always create exactly one goal, and count as "hypotheses used" exactly those that implicitly appeared in the goal to begin with.

[Scott Morrison]

But in any case --- what I'm really saying is let's not say "please make suggest never report these", but instead say "please make suggest report these alternatives with higher priority"

[Scott Morrison]

and then we can think about how to tweak the sorting algorithm to achieve this.