hint tactic

Stream: PR reviews

[Scott Morrison]

I think the hint tactic in #8363 is ready to go.

(History here: @Pol'tta / Miyahara Kō had already implemented this in #5363, and somehow I had missed it. They kindly merged their version into mine, producing something better than either of them.)

We will need to play around with the list of tactic we want to run register_hint on, to get the best user experience, but I think that can happen progressively.

[Scott Morrison]

I have a followup PR that runs all the hint tactics in parallel, and it is really speedy. It means that aesop and exact? start running, but if simp_all quickly comes back with a solution we report that immediately to the user. However it requires some import restructuring, so won't be part of the initial PR.

[Scott Morrison]

Anyone interested in reviewing / merging? It is meta code, but nothing particularly deep.

[Scott Morrison]

@Damiano Testa and @Jireh Loreaux made suggestions of tactics to register with hint (tauto, constructor, and split_ifs).

They are good suggestions, but I think the best strategy will be to ship hint initially with few tactics, and then let people try it out.

It is extremely easy to add more tactics locally: just register_hint constructor etc. I would like to see examples of the form:

example foo : X := by hint -- no suggestions

register_hint my_tactic

example foo : X := by hint -- Try these: my_tactic

to go along with additions.

If anything, perhaps we should remove register_hints from the initial PR.

[Scott Morrison]

(Note split_ifs is already covered by split, which also splits match statements.)

[Jireh Loreaux]

I'll give a more thorough look later tonight if no one merges first.

[Damiano Testa]

I am happy to see fewer tactics in hint and add them gradually, if/when needed!

[Scott Morrison]

Okay, it has been merged! Please try out hint and request further tactics to be added.

[Scott Morrison]

#8435 is the parallel version of hint.

[Scott Morrison]

I have just improved the parallel version of hint to include automatic cancellation of other tasks once one task succeeds!