Commit 2026-09-09 20:00 ac7917d6

feat: solve equalities of instances in convert (#40663) This PR sets the preTransparency of convert to .instances, which means it will not run congruence on goals that already are equal at .instances transparency. In other words, convert (without exclamation) should leave no goals of the form instA.toC = instB.toC. There are 387 (~ 8.5%) additional convert! calls in Mathlib that could become convert after this change, in addition to 2626 (~ 57,8%) where convert already succeeds at reducible transparency. I found no cases where postTransparency := .instances would be needed instead. Full breakdown of stats, according to the test script below and passing the captured log messages to sort | uniq -c:

• 2626 convert would work
• 1513 convert! (i.e. convert (postTransparency := .default)) is required
• 387 convert (preTransparency := .instances) is required
• 16 cause an error in the test script The test script consists of replacing the elaborator for convert with:

def sameGoals (gs₁ gs₂ : List MVarId) : MetaM Bool := do
  if gs₁.length == gs₂.length then
    try
      (gs₁.zip gs₂).allM fun (g₁, g₂) => do
        -- Check that they agree on the set of free variables, otherwise we get errors.
        -- We assume the context in the `convert` case is a subset of the `convert!` case
        -- since `convert!` can more agressively unfold and introduce more variables.
        if !(← g₁.getDecl).lctx.isSubPrefixOf (← g₂.getDecl).lctx then return false
        g₂.withContext <| withReducible <| isDefEq (← g₁.getType) (← g₂.getType)
    catch _ => return false
  else
    return false
elab_rules : tactic
| `(tactic| convert $[!%$expensive]? $cfg $[←%$sym]? $term $[using $n]? $[with $ps?*]?) =>
  withMainContext do
    let actualConfig ← Convert.elabConfig expensive.isSome cfg
    let cheapConfig ← Convert.elabConfig false cfg
    let redConfig := { cheapConfig with
      preTransparency := .reducible, postTransparency := .reducible }
    let preInstConfig := { cheapConfig with
      preTransparency := .instances, postTransparency := .reducible }
    let postInstConfig := { cheapConfig with
      postTransparency := .instances, preTransparency := .reducible }
    let patterns := (ps?.getD #[]).toList
    let expectedType ← mkFreshExprMVar (mkSort (← getLevel (← getMainTarget)))
    let (e, gs) ← elabTermForConvert term expectedType
    liftMetaTactic fun g ↦ do
      -- Don't retain metavar assignments but do retain messages.
      let msgs ← withoutModifyingState do
        try
          let actualGoals ← g.convert e sym.isSome (n.map (·.getNat)) actualConfig patterns
          let redGoals ← g.convert e sym.isSome (n.map (·.getNat)) redConfig patterns
          if ← sameGoals actualGoals redGoals then
            logInfo m!"convert(reducible)"
          else
            let preInstGoals ← g.convert e sym.isSome (n.map (·.getNat)) preInstConfig patterns
            if ← sameGoals actualGoals preInstGoals then
              logInfo m!"convert(preInst)"
            else
              let postInstGoals ← g.convert e sym.isSome (n.map (·.getNat)) postInstConfig patterns
              if ← sameGoals actualGoals postInstGoals then
                logInfo m!"convert(postInst)"
              else if expensive.isSome then
                logInfo m!"convert(expensive)"
              else
                logInfo m!"convert(error)"
        catch e =>
          logInfo m!"convert(error {e.toMessageData})"
          pure ()
        Core.getMessageLog
      Core.setMessageLog msgs
      return (← g.convert e sym.isSome (n.map (·.getNat)) actualConfig patterns) ++ gs