fix: change show tactic to work as documented

[Rob23oba]

This PR changes the show t tactic to match its documentation. Previously it was a synonym for change t, but now it finds the first goal that unifies with the term t and moves it to the front of the goal list.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 141e519009fc74d444cb8a32b55daf3c2d192bbd --onto ca0d8226192e7c0cdcc71d6322c3226ad4f73f30. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-08 11:41:46)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b9f8a859e7f354f026de7c910e17ce29e23678f9 --onto ca0d8226192e7c0cdcc71d6322c3226ad4f73f30. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-08 13:41:28)
• 💥 Mathlib branch lean-pr-testing-7395 build failed against this PR. (2025-06-11 15:50:11) View Log
• 💥 Mathlib branch lean-pr-testing-7395 build failed against this PR. (2025-06-11 19:12:50) View Log
• 💥 Mathlib branch lean-pr-testing-7395 build failed against this PR. (2025-06-11 22:02:21) View Log
• 💥 Mathlib branch lean-pr-testing-7395 build failed against this PR. (2025-06-12 08:26:08) View Log
• 🟡 Mathlib branch lean-pr-testing-7395 build this PR didn't complete normally. (2025-06-12 08:39:12) View Log
• 🟡 Mathlib branch lean-pr-testing-7395 build against this PR was cancelled. (2025-06-12 09:07:18) View Log
• 🟡 Mathlib branch lean-pr-testing-7395 build this PR didn't complete normally. (2025-06-12 09:08:11) View Log
• 💥 Mathlib branch lean-pr-testing-7395 build failed against this PR. (2025-06-12 09:57:23) View Log
• 💥 Mathlib branch lean-pr-testing-7395 build failed against this PR. (2025-06-12 11:29:24) View Log
• 💥 Mathlib branch lean-pr-testing-7395 build failed against this PR. (2025-06-12 15:06:07) View Log
• ❌ Mathlib branch lean-pr-testing-7395 built against this PR, but testing failed. (2025-06-12 15:28:12) View Log
• ✅ Mathlib branch lean-pr-testing-7395 has successfully built against this PR. (2025-06-12 15:55:39) View Log
• ✅ Mathlib branch lean-pr-testing-7395 has successfully built against this PR. (2025-06-12 16:15:18) View Log

[nomeata]

Thanks! Just wants to let you know that this is a change we want. Didn't look at the changes yet, since it's still a draft. And maybe I'll leave it to @kmill to review when he gets to it.

[kmill]

Thanks for your contribution. It generally looks good.

Some Lean design comments (don't act on this in this PR, but if you are interested, you should feel free to make a followup PR): When I made change, I made sure to replicate how the refine_lift implementation could create new goals, but I now think I was wrong to continue to use withCollectingNewGoalsFrom. There do not seem to be any realistic circumstances where you want to make a goal contain new assigned metavariables.

I think we should have a withCheckingNewMVarsAssigned combinator like the following:

def getNewMVars (e : Expr) (mvarCounterSaved : Nat)  : TermElabM (Array MVarId) := do
  let mut newMVarIds ← getMVarsNoDelayed e
  newMVarIds ← filterOldMVars newMVarIds mvarCounterSaved
  /- ignore let-rec auxiliary variables, they are synthesized automatically later -/
  newMVarIds ← newMVarIds.filterM fun mvarId => return !(← Term.isLetRecAuxMVar mvarId)
  return newMVarIds

def checkAssignedNewMVars (e : Expr) (mvarCounterSaved : Nat) : TacticM Unit := do
  let newMVarIds ← getNewMVars e mvarCounterSaved
  logUnassignedAndAbort newMVarIds

def withCheckingNewMVarsAssigned (x : TacticM Expr) (mvarCounterSaved? : Option Nat := none) :
    TacticM Expr := do
  let mvarCounterSaved ← (mvarCounterSaved?.getDM do pure (← getMCtx).mvarCounter : MetaM Nat)
  let e ← x
  checkAssignedNewMVars e mvarCounterSaved
  return e

Then the entire body of elabChange could be wrapped in withCheckingNewMVarsAssigned.

The getNewMVars function could also be used to refactor tactic functions that do this filterOldMVars calculation, like withCollectingNewGoalsFrom.

[Rob23oba]

One other thing: Because of the replaceTargetDefEq behavior, trivial shows (in the sense of repeating the goal state) get flagged by the unused tactic linter. Should we keep this or add show as an exception to the linter for proof readability concerns?

[Rob23oba]

Oh and I forgot about the throwAbortTactic. Why would that be needed? I mean change _ doesn't use it either.

[kmill]

I think it could make sense to allow "unused" shows in mathlib — it's better than change for inserting checkpoints since change sounds like it changes the goal. Feel free to create a zulip thread to discuss it with mathlib.

[kmill]

throwAbortTactic

I'm assuming that elabTerm in elabChange is going to log messages to indicate error, but this assumes bug-free elaboration, and that withoutRecover doesn't make terms that successfully elaborate become unsuccessful terms.

throwAbortTactic creates a "silent" exception to abort tactic evaluation, and hopefully there are errors in the message log from the failed elaboration. We don't want double errors: the elaboration error should take precedence.

A way to be robust here is to do something like if message log has errors then throwAbortTactic else throwError "internal error, failed elaboration produced no errors (please report)".

[kmill]

You know what, maybe you don't need this throwAbortTactic logic. I was assuming that you got some doubled errors, but change doesn't seem to have this problem. I guess there's something else that checks whether there are errors in the message log already.

Edit: Right, that's the purpose of the es argument in lazy messages. Ok, ignore this suggestion to use throwAbortTactic.

[Rob23oba]

Oh uh I haven't merged the adapation yet; might that be a problem?