feat(tactic/hint): if hint can solve the goal, say so (#2474)

It used to be that `hint` would print:

```
the following tactics make progress:
----
tac1
tac2
tac3
```

with the tactics listed in order of number of resulting goals. In particular, if `tac1` and `tac2` actually solve the goal, while `tac3` only makes progress, this isn't explained.

With this PR, if any of those tactics actually close the goal, we only print those tactics, with text:
```
the following tactics solve the goal:
----
tac1
tac2
```

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/tactic/core.lean

@@ -893,14 +893,14 @@ the value produced by a subsequent execution of the `sort_by` tactic,
 and reverting to the original `tactic_state`.
 -/
 meta def try_all_sorted {α : Type} (tactics : list (tactic α)) (sort_by : tactic ℕ := num_goals) :
-  tactic (list α) :=
+  tactic (list (α × ℕ)) :=
 λ s, result.success
-(((tactics.map $
+((tactics.map $
 λ t : tactic α,
   match (do a ← t, n ← sort_by, return (a, n)) s with
   | result.success a s' := [a]
   | _ := []
-  end).join.qsort (λ p q : α × ℕ, p.2 < q.2)).map (prod.fst)) s
+  end).join.qsort (λ p q : α × ℕ, p.2 < q.2)) s
 
 /-- Return target after instantiating metavars and whnf. -/
 private meta def target' : tactic expr :=

src/tactic/hint.lean

@@ -66,23 +66,33 @@ add_hint_tactic "unfold_aux"
 
 end hint
 
-/-- report a list of tactics that can make progress against the current goal -/
-meta def hint : tactic (list string) :=
-do names ← attribute.get_instances `hint_tactic,
-   try_all_sorted (names.reverse.map name_to_tactic)
+/--
+Report a list of tactics that can make progress against the current goal,
+and for each such tactic, the number of remaining goals afterwards.
+-/
+meta def hint : tactic (list (string × ℕ)) :=
+do
+  names ← attribute.get_instances `hint_tactic,
+  focus1 $ try_all_sorted (names.reverse.map name_to_tactic)
 
 namespace interactive
 
 /--
-report a list of tactics that can make progress against the current goal
+Report a list of tactics that can make progress against the current goal.
 -/
 meta def hint : tactic unit :=
-do hints ← tactic.hint,
-   if hints.length = 0 then
-     fail "no hints available"
-   else
-     do trace "the following tactics make progress:\n----",
-        hints.mmap' (λ s, tactic.trace format!"Try this: {s}")
+do
+  hints ← tactic.hint,
+  if hints.length = 0 then
+    fail "no hints available"
+  else do
+    t ← hints.nth 0,
+    if t.2 = 0 then do
+      trace "the following tactics solve the goal:\n----",
+      (hints.filter (λ p : string × ℕ, p.2 = 0)).mmap' (λ p, tactic.trace format!"Try this: {p.1}")
+    else do
+      trace "the following tactics make progress:\n----",
+      hints.mmap' (λ p, tactic.trace format!"Try this: {p.1}")
 
 /--
 `hint` lists possible tactics which will make progress (that is, not fail) against the current goal.

test/hint.lean

@@ -4,14 +4,14 @@ import tactic.finish
 
 example : 1 = 1 :=
 begin
-  (do hints ← tactic.hint, guard $ "refl" ∈ hints),
+  (do hints ← tactic.hint, guard $ ("refl", 0) ∈ hints),
   refl
 end
 
 -- `split_ifs` is designated as a `hint_tactic` in its own file
 example : if 1 = 1 then true else false :=
 begin
-  (do hints ← tactic.hint, guard $ "split_ifs" ∈ hints),
+  (do hints ← tactic.hint, guard $ ("split_ifs", 2) ∈ hints),
   split_ifs; trivial
 end
 
@@ -25,18 +25,28 @@ end
 -- Check that tactics are sorted by the number of goals they leave.
 example : 1 = 1 ∧ 2 = 2 :=
 begin
-  (do hints ← tactic.hint, guard $ hints.indexes_of "finish" < hints.indexes_of "fconstructor"),
+  (do hints ← tactic.hint, guard $ hints.indexes_of ("finish", 0) < hints.indexes_of ("fconstructor", 2)),
   finish
 end
 
 example (h : false) : false :=
 begin
-  (do hints ← tactic.hint, guard $ "assumption" ∈ hints),
+  (do hints ← tactic.hint, guard $ ("assumption", 0) ∈ hints),
   assumption
 end
 
 example {P Q : Prop} (p : P) (h : P → Q) : Q :=
 begin
-  (do hints ← tactic.hint, guard $ "solve_by_elim" ∈ hints),
+  (do hints ← tactic.hint, guard $ ("solve_by_elim", 0) ∈ hints),
   solve_by_elim,
 end
+
+-- Check that `num_goals` is counted correctly, when `hint` is called with multiple goals.
+example : 1 = 1 ∧ 2 = 2 :=
+begin
+  split,
+  (do hints ← tactic.hint, guard $ ("solve_by_elim", 0) ∈ hints),
+  solve_by_elim,
+  (do hints ← tactic.hint, guard $ ("refl", 0) ∈ hints),
+  refl,
+end