[Merged by Bors] - chore(Analysis/CStarAlgebra): cleanup .ofCoreReplaceAll instances

[JovanGerb]

The uses of NormedAddCommGroup.ofCoreReplaceAll currently cause leaky instances, because the instance arguments get filled in by unification instead of by synthesis. To fix this, we can use ?_ for the proofs, and fill them in at the end using where finally. This way, the proofs do not influence the synthesized instances.

An added benefit is that we get to remove some privateInPublic flags.

---

[github-actions]

PR summary 50d5513e83

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

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

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (5.22, 0.02)

Current number	Change	Type
6752	-1	backward.isDefEq.respectTransparency
795	-10	backward.privateInPublic
412	-3	backward.privateInPublic.warn

Current commit d75c557fa9
Reference commit 50d5513e83

You can run this locally as

./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).

[sgouezel]

I'm not sure I get the point of this change. As far as I can tell, they are reducibly defeq, no? And wouldn't it be better just with fast_instance%?

[JovanGerb]

I tried to explain it in the PR description: "the instance arguments get filled in by unification instead of by synthesis". So basically the instance arguments in .ofCoreReplaceAll were wrong, and this change fixes that.

It doesn't work to fix this with fast_instance%, because the fields in question, PseudoMetricSpace.toUniformSpace and PseudoMetricSpace.toBornology are "normal" fields, rather than parent fields (i.e. not created by extends).

[sgouezel]

I checked that the old definition and your definition are reducibly defeq, so unless I messed up I still don't understand why it makes a difference.

[JovanGerb]

Ah, you are right, I hadn't realized they are defeq in reducible_and_instances. Here's the difference:

• Original

@NormedAddCommGroup.ofCoreReplaceAll ℂ C⋆ᵐᵒᵈ(A, (i : ι) → E i) Complex.instNormedField
  (instAddCommGroup A ((i : ι) → E i)) (instModule A ((i : ι) → E i)) instNormForall
  (UniformSpace.comap (⇑(equiv A ((i : ι) → E i))) inferInstance) (Bornology.induced ⇑(equiv A ((i : ι) → E i))) ⋯ ⋯ ⋯

• Modified

@NormedAddCommGroup.ofCoreReplaceAll ℂ C⋆ᵐᵒᵈ(A, (i : ι) → E i) Complex.instNormedField
  (instAddCommGroup A ((i : ι) → E i)) (instModule A ((i : ι) → E i)) instNormForall instUniformSpace instBornology ⋯ ⋯
  ⋯

The difference is that the new instance has instBornology and instUniformSpace as instance arguments, instead of this other longer expression that happens to be defeq. So, the instances in this file were not leaky to begin with. But I think my change is still an improvement.

The reason I made this change was that in the other file, the instance was genuinely leaky, and I then went to look for the same pattern in other places and found this file.

[sgouezel]

Yes, I agree that in the other file your fix is definitely needed.

I am a little bit worried here: using this kind of lemma to replace some instance by a propostionally equal one is something we do a lot in Mathlib. Here you noticed the flaw, but do you understand the underlying mechanism and why it works elsewhere but not here -- or is it also broken elsewhere but we've never noticed?

[sgouezel]

Also, shouldn't we use fast_instance% in addition to your fix, to get an even nicer instance?

[JovanGerb]

Sure, I've used fast_instance% now.

The underlying mechanism is that unification can fill in implicit arguments. So depending on the order in which elaboration does things, the instances are filled in from the type of the given proof, or from type class search

What are the other cases in Mathlib do you think this problem may be occurring?

[sgouezel]

Well, whenever we create an instance in which there are preexisting instances and then a proof field about them. Taking a random example,

instance instAddZeroClass : AddZeroClass (ι →₀ M) :=
  fast_instance% DFunLike.coe_injective.addZeroClass _ coe_zero coe_add

Here coe_zero and coe_add prove something about zero. If the proof were a little bit more involved, then maybe the zero that would come out of the proof would be subtly different from the zero in the instance, and it's the zero from the proof that would be picked by unification, right? To me, it looks exactly the same kind of thing as in the current PR, except that here the proof is trivial so it won't create an issue. And this kind of construction is pervasive throughout Mathlib. Do you think this never creates issues?

[sgouezel]

For a more serious example, we have

noncomputable scoped instance (priority := 80)
    {B : Type*} {E : B → Type*} [(b : B) → TopologicalSpace (E b)]
    [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)]
    [h : RiemannianBundle E] [∀ (b : B), IsTopologicalAddGroup (E b)]
    [∀ (b : B), ContinuousConstSMul ℝ (E b)] (b : B) :
    NormedAddCommGroup (E b) := fast_instance%
  (h.g.toCore b).toNormedAddCommGroupOfTopology (h.g.continuousAt b) (h.g.isVonNBounded b)

which I'm double-checking now.

(It looks fine)

[JovanGerb]

Yeah, that makes sense. I think in this case it goes right because the instance that is inferred by unification is identical to the instance that would have been synthesized. I presume this is the case most of the time.

[sgouezel]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Post-Build Step
• ci (staging) / Build
• ci (staging) / Lint style