[Merged by Bors] - feat: recover as a tactic combinator

[siddhartha-gadgil]

Following a suggestion of @digama0 recover is implemented as wrapping tactics so that if goals are closed incorrectly they are reopened. Below are examples (test suggested by @gebner). Some code is from Aesop.

/-- problematic tactic for testing recovery -/
elab "this" "is" "a" "problem" : tactic =>
  Lean.Elab.Tactic.setGoals []

/- The main test-/
example : 1 = 1 := by
  recover this is a problem
  rfl

/- Tests that recover does no harm -/
example : 3 < 4 := by
    recover decide

example : 1 = 1 := by
    recover skip ; rfl

example : 2 = 2 := by
    recover skip
    rfl

[gebner]

The actual tactic implementation looks good.

[JLimperg]

Now that I think about it: does recover actually want to recurse into the found metavariables? If we make the 'dropped' metavariables goals, any mvars occurring in them are not dropped any more, so they don't need to also become goals. cc @gebner

[siddhartha-gadgil]

A situation I can imagine: a new metavariable is created, a dropped mvar assigned to it and removed from goals but the new mvar is not added to goals.

[JLimperg]

If I understand correctly, your situation looks like this:

• initial goal: ?g[?m1] (this is my notation for '?g contains ?m')
• tactic introduces ?m2 and assigns ?m1 := ?m2
• tactics returns goals: []

Now if we just collect unassigned mvars in ?g, we correctly find ?m2 (and not ?m1 since it gets substituted away by instantiateMVars). So we set goals:

• goals after recover: [?m2]

If there's another mvar ?m3 with ?m2[?m3], this is fine because ?m3 is already reachable from the tactic state after recover. So we don't need to recursively get mvars from ?m2. However, maybe we want to do it anyway because it's nicer to have an mvar in the goal list than to not have it?

[siddhartha-gadgil]

I think I misunderstood your point. Is what you are saying that we should collect unassigned mvars in the original goals list, but no need to do this recursively. That sounds reasonable. I will make the change if you confirm that is what you mean and feel it will make things better.

[JLimperg]

Yes exactly, but I'm not sure about this. Let's wait and see what Gabriel thinks.

[siddhartha-gadgil]

Sure.

[digama0]

It's not actually necessary to recurse into the initial goals at all, that was just an optimization. It suffices to just hold on to the list of goals itself and do all recursing through assignments at the end of the block.

[gebner]

Thanks!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build