inline definitions into instances

Stream: general

[Violeta Hernández]

Asking here to see what the general consensus is. Do we have any sort of preference for

def foo : bar := sorry -- [long definition]

instance : has_foo := ⟨foo⟩

over

instance : has_foo := ⟨sorry⟩ -- [long definition]

Here foo can be add or insert or empty or something like that.

[Violeta Hernández]

I had been going around changing the former into the latter in a few parts of the code, until I was stopped by @Mario Carneiro who showed me that we don't really have any explicit preference.

[Violeta Hernández]

I prefer the latter for two reasons, which I outlined during that conversation:

• the extra definition means one extra layer of unfolding: e.g. first has_add.add, then add.
• if someone tries using the direct definition rather than the instance, all the usual simp lemmas and rws won't work (this is particularly bad with insert, where the goals look the same).

[Violeta Hernández]

Also worth pointing out, the latter pattern can't be used when the equation compiler is involved.

[Violeta Hernández]

So ehm yeah, would be nice to hear what others think or do in their own code.

[Mario Carneiro]

One reason to prefer the definition is that instances are unfolded at instance reducibility but definitions are not, which means that if you have two instance paths to a definition then you don't have to compare the definition bodies and can stop at the constant application

[Violeta Hernández]

I wonder what happens with the converse - are there any real-world scenarios where we might have two definitions that actually coincide?

[Violeta Hernández]

I think I have one: the definition of ≤ on set α and the one defined for the set_like instance are separate (neither depends on the other), but turn out to be definitionally equal

[Violeta Hernández]

So using the definition pattern would create a diamond

[Eric Wieser]

I was under the impression that typeclass inference could unfold semireducible definitions when unifying diamonds

[Mario Carneiro]

There was some example where I think we needed int.sub to match algebra.sub and it wasn't working out because they are separate definitions, defeq at semireducible level but not instance level

[Mario Carneiro]

the only reference I can find is https://leanprover.zulipchat.com/#narrow/stream/180721-mathlib-maintainers/topic/.235303/near/219994192 though, I think we are doing something else now since sub is a field

[Junyan Xu]

Wow, a secret stream.

[Mario Carneiro]

whoops

[Mario Carneiro]

reproducing, Mario Carneiro said:

There is a definition in core that looks very similar to algebra.sub but it isn't, and this causes problems with definitional unfolding in norm_num proofs like 5 - 2 = 3 on int

[Eric Wieser]

That's sounds like an annoying detail to think about when writing tactics rather a typeclass inference issue