Definitions of "defeq", "diamond" and "β/δ/η/ζ reductions"

Stream: new members

[Isak Colboubrani]

To be able to accurately explain it to others I’m looking for precise definitions/explanations of some technical terms that often appear in discussions about Lean/Mathlib internals:

• “defeq”: I’ve seen references to "defeq abuse", “defeq check”, “defeq problem”, “non-defeq instance”, “not defeq”, “non-defeq diamonds”, “leak defeq”, etc. What does “defeq” mean in these contexts?

• “diamond”: I've seen phrases like “diamond problem”, “typeclass diamonds”, “recipe for diamonds”, “instance diamonds”, “good diamond”, “non-defeq diamonds”, etc. What does “diamond” mean in these contexts?

• “β/δ/η/ζ reductions”: I’d like to understand the notions of beta, delta, eta, and zeta reduction. I also see references to kernel, native, and elaborator reduction. What are these, and how do they differ from each other?

[suhr]

Defeq means definitional equality. The Lean Language reference says a few words on it as well as on reduction rules.

[Dan Abramov]

If I'm not mistaken, "defeq" means "definitional equality". So defeq abuse means relying on the current exact definition of something without considering that that definition might change in the future (and break your proof). The "fix" for defeq abuse is to use theorems (i.e. "public API") that were specifically intended to be used to unwrap that definition — and which don't expose implementation details that might change over time.

[suhr]

It says a few words on diamonds as well: https://lean-lang.org/doc/reference/latest//Type-Classes/Instance-Synthesis/#--tech-term-Diamonds

[Dan Abramov]

While this isn't quite the same thing in Lean, for intuition, I think it might be helpful to look at the "diamond problem" in traditional OOP inheritance (https://en.wikipedia.org/wiki/Multiple_inheritance#The_diamond_problem). It's a much older term and doesn't originate in Lean.

[Weiyi Wang]

a follow up question on defeq abuse: how do I know when not to unfold the definition of something defined in mathlib? or never do it?

[Kevin Buzzard]

As a rule of thumb, you should never do it, you should find the definition in mathlib and read the ten lemmas directly after the definition and use them instead.

Note that this doesn't always work: nowadays you might be in the unlucky situation that the definition you want is in a file called Foo/Defs.lean with no API at all. In this case you want to look at the first 10 lemmas that mention the foo in the file Foo/Basic.lean.

[Jireh Loreaux]

Dan Abramov said:

So defeq abuse means relying on the current exact definition of something without considering that that definition might change in the future (and break your proof).

@Dan Abramov I think that's not quite the definition of defeq abuse that I would give. Depending on the circumstance, I would call that either convenient defeq use or sloppy defeq use depending on how prone to breakage / change it is.

I would contend that defeq abuse refers more specifically to the situation where we have an equality of types like X : Type and def Y := X, and then things are proven involving Y by using a theorem about X, especially if this causes Lean to infer the wrong type for other parts of the proof (and therefore breaks simp or rw calls). Note that this kind of abuse can still have negative effects even if the definition of Y is never altered.

Of course, at the very beginning when constructing the API for Y, it is necessary to do this kind of thing, but after these abstraction layers are erected, there should be no further reason to "look through" this definitional equality, and doing so is what constitutes abuse.

[Johan Commelin]

@Isak Colboubrani Some of these concepts are also explained in https://leanprover-community.github.io/glossary.html
This page was written in the Lean 3 era. Unfortunately it hasn't been updated yet. But most of the info is still relevant.

[Julian Berman]

Yes it's a shame that I let that stagnate :/ it was a good way for me myself to learn the answers to some of these questions, so getting it back up to date is definitely something I'd like to do as well. We also have (had? let's see if it still works): term#diamond

[Julian Berman]

Apparently not anymore. OK well if we get that page back in shape we can re-ask for it.

[Chris Bailey]

Definitional equality and reduction are broken down in this book: https://ammkrn.github.io/type_checking_in_lean4/

And their theory is discussed in this thesis: https://github.com/digama0/lean-type-theory/releases/tag/v1.0

[Chris Bailey]

The diamond and instance stuff, or at least the theory, is covered in the tabled typeclass resolution paper: https://arxiv.org/pdf/2001.04301.pdf

[Luigi Massacci]

#mil also has a paragraph about diamonds if I remember correctly