adding fact to type class inference system

Stream: general

[Kevin Buzzard]

Occasionally I run into a situation where Lean's type class inference system fails in the middle of a tactic mode proof -- say, for concreteness, that I attempted to infer that R was a ring, but type class inference didn't do it. Usually what happened was that I applied lemma X, perhaps to some elements of R, and this lemma needed R to be a ring but expected this proof to be supplied by type class inference but I have managed to construct R so that Lean didn't notice it was a ring. I can supply my own proof H that R is a ring though, and my fix is usually to replace X with @X _ _ H _ _ .... Are there other ways of doing this though? I don't like that big pile of _s and I think that in the particular case I'm working on now I'd rather just inject H directly into the type class inference system somehow rather than using the @ notation and then adding a whole bunch of _s. Is there a trick for doing this? In term mode I would create an instance but I'm in tactic mode.

[Kenny Lau]

letI := H

[Kevin Buzzard]

Oh, that's what it does ;-)

[Kevin Buzzard]

Oh -- does this mean that my code is now likely to break in Lean 4? :-/

[Chris Hughes]

Yes, but I don't see why it would be more likely than it was otherwise. There'll be a way to do that in lean4 I imagine, even if Mario has to write it.

[Kevin Buzzard]

The reason I mentioned this specifically was that I believe this might have been something which Leo (probably for an important reason) actively tried to stop people from doing.

[Chris Hughes]

I think it was just that have could previously be used for introducing instances, which wasn't the intended behaviour, since most of the time, you don't want a have to be an instance, and it might confuse the type class system when every single have is marked instance.