Check goal solved

Stream: lean4

[Marcus Rossel]

How does one check whether a given goal is solved after running a tactic?
It seems that getMainGoal isn't the correct API for this. And also the goal's MVarId changes after running a tactic:

import Lean
open Lean Meta Elab Tactic

elab "simp'" : tactic => do
  logInfo m!"before: {(← getMainGoal).name}"
  evalSimp <| ← `(simp)
  logInfo m!"after: {(← getMainGoal).name}"

example : True = True := by
  simp'
  -- before: _unique.1990
  -- no goals to be solved

example (a b : Nat): a + 0 = b := by
  simp'
  -- before: _unique.2015
  -- after: _unique.2062

[Notification Bot]

Marcus Rossel has marked this topic as resolved.

[Notification Bot]

Marcus Rossel has marked this topic as unresolved.

[Jannis Limperg]

getGoals to get the list of remaining goals, then check whether this is empty.

[Jannis Limperg]

When a tactic is run on a goal (represented by an MVarId), it does not modify the goal. Rather, it 'solves' the goal (assigns the MVarId) and returns zero or more remaining goals (with different MVarIds).

[Marcus Rossel]

Thanks! From what I can tell that still means I need to do some additional checks when the tactic is run without focussing on a single goal:

import Lean
open Lean Meta Elab Tactic

elab "simp'" : tactic => do
  logInfo m!"before: {(← getGoals).map MVarId.name}"
  evalSimp <| ← `(simp)
  logInfo m!"after: {(← getGoals).map MVarId.name}"

example : True = True := by
  by_cases 0 = 0
  · simp'
  -- before: [_uniq.2065]
  -- after: []

example : True = True := by
  by_cases 0 = 0
  simp'
  -- before: [_uniq.2065, _uniq.2080]
  -- after: [_uniq.2080]

example (a b : Nat): a + 0 = b := by
  by_cases 0 = 0
  simp'
  -- before: [_uniq.2405, _uniq.2420]
  -- after: [_uniq.2466, _uniq.2420]

[Damiano Testa]

One thing that confused me, is that changing the goal from a + 0 = ... to a = ... counts as having solved a goal and replaced it with a new one. In fact, it is not so easy to persistently maintain a notion of which new MVar is "the old one", unless you are careful about each step and you manage them yourself.

[Damiano Testa]

So, the outcome that you see now is what I've come to expect, but not what my initial intuition was.

[Damiano Testa]

E.g. 2466 is morally a witness that the goal has not been solved, but in reality the goal 2405 was solved and "out of nowhere" 2466 appeared.

[Jannis Limperg]

When you have multiple goals, you should indeed check whether all remaining goals were already present before you ran the tactic. Or you focus on the main goal only, i.e. setGoals [mainGoal] before executing your tactic. Or you drop down to the MetaM level, where each tactic has the form MVarId /- old goal -/ -> MetaM (List MVarId) /- new goals -/.

[Damiano Testa]

Or if you are using MVarId.apply, then you know that the list of goals that it returs is the list of "children" of your initial goal. This is a very robust way of proceeding, while calling evalSimp (or something analogous) may mean that you lose control of what is going on.

[Damiano Testa]

I have the impression that the tag system is intended as a quick-and-dirty way of doing some of the bookkeeping, but it can get cumbersome quickly.

[Jannis Limperg]

Afaik the tags are only visual aids for users. I wouldn't count on them being handled appropriately by all tactics (and it's not even clear what 'appropriately' means).

[Damiano Testa]

I agree: propagating tactics is much more consistent in Lean 4 than it was in Lean 3, but still not very robust.

However, for simple-minded implementations, I have manually set them to sort and retrieve side-goals: it was ok, but as soon as you have to do something a little involved, you are better off maintaining your own lists of MVars.

[Kyle Miller]

A goal is "solved" if when you instantiate its metavariables, then it contains no more metavariables. You can approximate this by keeping track of the goal state, but you can also calculate this yourself.

import Lean
open Lean Meta Elab Tactic

elab "simp'" : tactic => do
  let g := Expr.mvar (← getMainGoal)
  logInfo m!"before: {g}"
  evalTactic <| ← `(tactic| focus simp)
  let g ← instantiateMVars g
  logInfo m!"after: {g}"
  if g.hasExprMVar then
    logInfo m!"not solved"
  else
    logInfo m!"solved"

example : True = True := by
  simp'
  -- before: ?m.2205
  -- after: of_eq_true (eq_self True)
  -- solved

example (a b : Nat): a + 0 = b := by
  simp'
  -- before: ?m.2287
  -- after: id ?m.2334
  -- not solved

(I switched your code to use evalTactic and focus just to be sure the tactic is only applying to the top goal. That wasn't necessary for the experiment.)

[Kyle Miller]

Well, that's one notion of "solved". Maybe it's better to keep track of the goal states after all, since there might be some metavariables in your goal that are from the other not-yet-solved-for goals, and you might consider that to be "solved".

[Marcus Rossel]

Thanks for the help! I ended up going for the simple approach of using focus, because that makes it simple to understand the output of getGoals:

import Lean
open Lean Meta Elab Tactic

elab "simp'" : tactic => do
  focus do
    logInfo m!"before: {(← getGoals).map MVarId.name}"
    evalSimp <| ← `(simp)
    logInfo m!"after: {(← getGoals).map MVarId.name}"

example : True = True := by
  by_cases 0 = 0
  · simp'
  -- before: [_uniq.2065]
  -- after: []

example : True = True := by
  by_cases 0 = 0
  simp'
  -- before: [_uniq.2230]
  -- after: []

example (a b : Nat): a + 0 = b := by
  by_cases 0 = 0
  simp'
  -- before: [_uniq.2405]
  -- after: [_uniq.2466]

[Damiano Testa]

It may be that the first do is superfluous (untested).