feat(Translate): better relevant_arg heuristic

[JovanGerb]

This PR improves the heuristic around relevant_arg that to_dual and to_additive use. Currently, the we eagerly set (relevant_arg := 1) whenever we cannot find any relevant argument. This is problematic in a setting where there really should be no relevant argument, such as for ComplexShape.

After this PR, we only default to (relevant_arg := 1) for types (i.e. anything whose type is Sort _). For terms that aren't types, we instead purely rely on the algorithm that determines the relevant argument (which was added in #35318). In order for this algorithm to work in all cases, relevant_arg needs to be set on all relevant types. This includes some types that are dual to themselves, like LE and LinearOrder, and hence do not have a to_dual attribute (and hence also don't have a relevant_arg). To fix this, I added the following trick: when we add a translation for a class projection or class constructor, and if that class has no translation, then we first add a translation from that class to itself.

As a result, classes like LE and LinearOrder are now part of the translation dictionary, and are being translated into themselves.

---

[github-actions]

PR summary 8077d16145

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ SomeClass
+ SomeStructure
+ ensureClassTranslated

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 -- stale, waiting for the new build)

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

• +1 new declarations
• −0 removed declarations

+Mathlib.Tactic.Translate.ensureClassTranslated

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 8077d16145
Reference commit 3a33b9d429

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.py 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]

!radar

[leanprover-radar]

Benchmark results for df1ccc6 against 3a33b9d are in. No significant results found. @JovanGerb

• ✅ build//instructions: -50.3M (-0.00%)

No significant changes detected.

[Vierkantor]

I'm not completely sure about the default behaviour. But the heuristic seems to be a strict improvement at least, so I can easily be convinced that we are in a local maximum :)

[Vierkantor]

I can imagine that the first argument is often the right one, but it seems like it might misbehave on something unbundled like IsOrderedSMul? (Or maybe even IsOrderConnected?)

[JovanGerb]

Thanks, this could indeed go wrong (although I don't think there are examples in practice). I've fixed it by running the translation from the type of cls to itself, and using the relevant_arg inferred from that.