issue !4#31745: Missing definitional theorems

Stream: triage

[Random Issue Bot]

Today I chose issue #31745 for discussion!

Missing definitional theorems
Created by @Kenny Lau (@kckennylau) on 2025-11-17
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Violeta Hernández]

Why would we ever want to unfold this definition? And assuming we did, why is unfold not sufficient?

[Snir Broshi]

IIUC definitional lemmas prevent defeq abuse since the definition is treated as opaque, which makes changing it in the future easier (though I'm not sure IIUC)
Maybe the module system will surface these problems, since it let's us have opaque definitions?

[Ruben Van de Velde]

The (or one) benefit of having a foo_def is that you can change the actual definition but keep the lemma

[Violeta Hernández]

Surjective basically works as an abbrev already. The vast majority of ⊢ Surjective f goals are solved via intro x; use ....

[Johan Commelin]

Both can be true at the same time, right?
For some definitions we can decide that we want a firm boundary, for others absolutely not, and for others it's maybe more of a grey area. Tradeoffs and all that.

[Anne Baanen]

Whether we want downstream users to unfold a definition is now expressible with the module system, right? Namely, whether we have @[expose] on it or not.

[Ruben Van de Velde]

Do we now have documentation for how to use modules?

[Anne Baanen]

The Lean reference manual section on modules is quite thorough.

[Ruben Van de Velde]

I was hoping for short more than thorough, but I'll put it on my reading list