Surprising behavior of `withTacticInfoContext`

Stream: lean4

[Sebastian Zimmer]

I just spent a few hours debugging a tactic and it turns out the cause is that withTacticInfoContext implicitly prunes the solved goals after it has completed. It does this because getUnsolvedGoals calls pruneSolvedGoals as a side effect.

I found this extremely surprising. Now that I know why it happens it is easy to work around, but I doubt I'm the last guy who will run into this issue. If it is intended that getUnsolvedGoals should have this side effect, then I would strongly suggest that it should be renamed.

[Jannis Limperg]

The fact that there can be assigned mvars in the goal list is just a performance optimisation -- ideally any assignment would immediately remove the assigned mvar (since it's not a goal anymore). So you should never rely on assigned mvars staying in the goal list, and you should always prune the goal list before reading it, which is why getUnsolvedGoals does just that. I'm curious why your use case would require assigned mvars to be preserved as 'goals'.

[Sebastian Zimmer]

I was solving the goal and then doing replaceMainGoal afterwards, but because withTacticInfoContext was being used the goal was being removed from the list too early and the wrong goal was replaced.

[Jannis Limperg]

I see how that might be confusing. I wouldn't object to renaming getUnsolvedGoals to pruneAndGetUnsolvedGoal or something, but I doubt you're going to get this past Leo.

[Sebastian Zimmer]

If the tactic author is supposed to handle solved goals nondeterministically going away then I don't see how you could ever safely use replaceMainGoal

Maybe instead of replaceMainGoal there should be a function which prepends to the list of goals and then prunes them.

[Kyle Miller]

I find replaceMainGoal to be sketchy, and you should only use it if you're sure of the current state of the goal list.

There are functions like docs#Lean.Elab.Tactic.liftMetaTactic for running a MetaM tactic on the main goal and prepending the list.

[Kyle Miller]

It seems like it'd make sense to have a popMainGoal function and a prependGoals function (like appendGoals)

def prependGoals (mvarIds : List MVarId) : TacticM Unit :=
  modify fun s => { s with goals := mvarIds ++ s.goals }

/-- Returns `getMainGoal` and removes it from the goal list. -/
def popMainGoal : TacticM MVarId := do
  let (mvarId :: mvarIds') ← getUnsolvedGoals | throwNoGoalsToBeSolved
  modify fun _ => { goals := mvarIds' }
  return mvarId

[Sebastian Zimmer]

There are functions like docs#Lean.Elab.Tactic.liftMetaTactic for running a MetaM tactic on the main goal and prepending the list.

Glancing at the code I don't think that avoids the issue I was having. If you do

liftMetaTactic do
  withTacticInfoContext [...] do
    -- assign the goal to something

I'm pretty sure this fails since the assigned goal gets pruned before liftMetaTacticAux calls replaceMainGoal

It seems like it'd make sense to have a popMainGoal function and a prependGoals function (like appendGoals)

This makes sense to me and avoids these issues

[Kyle Miller]

The trick is that liftMetaTactic only takes a MetaM, so it can't modify the goals list. (In particular you can't use withTacticInfoContext in MetaM)

[Sebastian Zimmer]

Ah I see

[Scott Morrison]

Doing as much as possible down in MetaM is usually a good idea. I try and escape TacticM at the first available opportunity. :-)