Instance-implicit vs implicit

Stream: mathlib4

[Yury G. Kudryashov]

I remember that in Lean 3 times, we've got some compilation speed improvements when we changed a bunch of lemmas about (f : M →* N) from [Monoid M] to {_ : Monoid M} (we didn't have MulOneClass back then). Does it make sense to do the same in Mathlib 4 for lemmas like docs#isClosed_compl_iff ?

[Yury G. Kudryashov]

Of course, we can't do this for lemmas that assume a typeclass, then use projections of this typeclass.

[Yury G. Kudryashov]

As a side effect, isClosed_compl_iff will work with simp for non-canonical topologies.

[Yaël Dillies]

That would definitely be a performance improvement (and we previously mentioned it), but I think this is something that we should not have to do by hand. Instead it should be automatic.

[Yury G. Kudryashov]

When exactly should it be done automatically?

[Yury G. Kudryashov]

When the definition/lemma is declared or when it is used?

[Yaël Dillies]

When it is declared (at least that's what I had in mind)

[Yury G. Kudryashov]

How should Lean decide that it should replace [MyClass a] with {_ : MyClass a}?

[Yaël Dillies]

For rewriting lemmas (_ = _ or _ ↔ _), there are at least three criteria that come to mind:

• An instance argument can be inferred from the LHS
• An instance argument can be inferred from the RHS
• Both of the above

[Joachim Breitner]

Is there an issue for this already?

[Yury G. Kudryashov]

I'd prefer "both of the above" to be on the safe side.

[Joachim Breitner]

(I'd - naively - expect that the unification that happens when rw or simp tries to apply the lemma would already instantiate these arguments, if present, at least if they aren't in Prop, without changes to the types, so I'd be curious to read more about the issue and why this doesn't happen already.)

[Yury G. Kudryashov]

As far as I understand, Lean 4 tries to be strict about "instance implicit args must match whatever is generated by instance search".

[Yury G. Kudryashov]

Also, there is more than "Prop/non-Prop" that can happen. E.g., if your lemma has [UniformSpace X] assumption, then uses projections to TopologicalSpace X and uniformity on LHS and RHS, then Lean can't recover UniformSpace.

[Joachim Breitner]

Ah, so it actively avoids instantiating them by unification. Thanks!

[Eric Rodriguez]

Joachim Breitner said:

Ah, so it actively avoids instantiating them by unification. Thanks!

As far as I understand, it actually runs both processes, so that it can complain if the one inferred is not the one gotten by unification. This makes working with non-canonical instances near-impossible, which is good and bad. (Also, I think this resynth every time must be costly - but Kyle told me that it's so core to how Lean4 is designed that it's unlikely to be removed no matter what, so it's likely not even worth testing)

[Yury G. Kudryashov]

But we can change some assumptions from [SomeClass _] to {_ : SomeClass _} in Mathlib, either manually or by overriding theorem in some clever way.

[Yury G. Kudryashov]

Is it worth testing?

[Eric Wieser]

Only on some theorems though, and those theorems will become much more fragile to further generalization

[Yury G. Kudryashov]

You can't further generalize isClosed_compl_iff...

[Michael Stoll]

(deleted)

[Yury G. Kudryashov]

Were you going to post this in some other thread?

[Michael Stoll]

Yes, sorry.