feat: solve equalities of instances in convert

[Vierkantor]

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

---

Ideally we'd run a benchmark on this PR, or even better one that compares preTransparency and postTransparency. But we don't have a lot of calls to plain convert yet, since I'd want to wait for the migration until #38071 is merged.

[github-actions]

PR summary 652cd22844

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 652cd22).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 652cd22844
Reference commit 9fbe5e0065

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[JovanGerb]

I discovered this issue yesterday independently, but it seem you beat me to it!

I think it would be best to ensure convert, convert! and congr! all do the same strength of pre-processing, rather than have convert be stronger. I'm also not so sure about running the assumptionCore discharger at instances transparency.

Maybe an alternative solution would be to simply wrap the particular mvarId.refl call in a withAtLeastTransparency .instances.

[Vierkantor]

rather than have convert be stronger

Just to be clear, because we have the setup of Convert.ExpensiveConfig extending Convert.CheapConfig, the default pre-transparency for convert! is now also .instances. It is indeed the case that the pre-transparency for (both forms of) convert is stronger than for congr!, that is true.

[Vierkantor]

Thinking about it a bit more: maybe the right way to go is to have congr! set the transparency in implicit arguments differently from explicit arguments, similar to how it works now for the usual kinds of unification?

[Vierkantor]

!bench

[leanprover-radar]

Benchmark results for 652cd22 against 9fbe5e0 are in. No significant results found. @Vierkantor

• 🟥 build//instructions: +56.9G (+0.04%)

No significant changes detected.

[Vierkantor]

I've seen noise of size ±0.07% before, so I don't feel like investigating the benchmark results is worth the effort. I am happy to have this be reviewed.

[joneugster]

Thank you for the PR. I believe we talked about this or other similar changes at the mathlib retreat. Seems very reasonable

[joneugster]

I think you should useguard_target (and maybe guard_hyp) instead of catching an error message which contains the goal the test tries to test for.

[joneugster]

Suggested change

	convert! (preTransparency := reducible) one_mul _
	convert! one_mul _

I think all of these three are accidental left-overs, aren't they?