5
$\begingroup$

In Lean 4, I've seen the terms "reducible", "semi-reducible" and "irreducible" mentioned a lot. What is the precise meaning and how are these concepts used in code? When should they be used?

For example, I've read that abbrev makes definitions reducible and def makes them semi-reducible. But what does that mean, both exactly and in practice?

Is this related to noncomputable definitions? Are there other related "kinds of definitions"?

$\endgroup$
3
  • $\begingroup$ I was going to point you to the lean glossary, but these don’t seem to be there. $\endgroup$
    – Jason Rute
    Sep 23, 2023 at 3:03
  • $\begingroup$ Have they finished writing the Lean 4 manual yet? $\endgroup$ Sep 23, 2023 at 6:29
  • $\begingroup$ @AndrejBauer Well, there is some text that hasn't changed in a while... I guess that means it's done? (Okay, looking around I see there are still some empty sections, so I guess not.) There hasn't really been a push to work on the manual, but David Christiansen recently joined the Lean FRO and I think he is focused on documentation work so maybe things will start moving soon. $\endgroup$ Sep 23, 2023 at 7:18

1 Answer 1

5
$\begingroup$

The short version is that these are just settings you can apply to definitions. When you define a definition you say whether it is reducible (abbrev or @[reducible] def), semi-reducible or "regular" (def), or irreducible (@[irreducible] def), and this is an extra flag stored along with the definition.

But what does that mean? This flag is generally interacted with by tactics and elaboration, which choose at various points what kind of reducibility they are interested in working with. This affects whether marked definitions will be unfolded when weak head normalizing things, and when checking if two things are definitionally equal and/or unifying metavariables in an expression as a result. You can, when writing a tactic, say "I want to check if these two terms are reducibly def-eq", meaning that reducible defs will be unfolded but not normal defs, or you can say "I want to unfold semi-reducible defs too if necessary" or "unfold everything".

Customarily, everything unfolds reducible definitions (in fact, lean 4 has no setting in isDefEq and friends which does not unfold reducibles), but semi-reducibles are also unfolded when you give a term and it needs to match the type (e.g. exact) or when using the rfl tactic. You can explicitly request reducible-only unfolding using the with_reducible tactic combinator, as in with_reducible rfl, and the rw tactic uses with_reducible rfl as a way to close the goal if it is reduced to a trivial reflexive equality but without trying too hard because it might just be a random non-refl equation and unfolding regular definitions could get expensive.

@[irreducible] def is not unfolded by either of these mechanisms. So if you have @[irreducible] def Foo := Nat then example : Foo := (1 : Nat) will be a type error, because standard unification will only unfold up to semi-reducible transparency. You can still make this definition typecheck though, if you crank up the transparency setting using with_unfolding_all.

There is another, even more irreducible level than irreducible: opaque. Unlike regular defs, the kernel itself will not accept an equality of an opaque with its definition, so no amount of tinkering with reducibility settings will help. If you have opaque foo : Nat := 1 then foo is an arbitrary Nat; the RHS is only relevant to prove that Nat is inhabited. (It is also used by the compiler to interpret the constant, which means you can prove that foo = 1 using native_decide, but this uses ofReduceBool which is a special axiom that is considered a bit borderline because of how much it adds to the TCB.)

$\endgroup$
3
  • $\begingroup$ Thanks a lot for the nice answer! Could you maybe add a comment of how noncomputable relates to this? Is it entirely unrelated? Also, is it true that theorem makes definitions opaque? $\endgroup$ Sep 23, 2023 at 11:20
  • $\begingroup$ @AdomasBaliuka I believe noncomputable is an orthogonal concept to reducibility, so not directly related. $\endgroup$
    – Jason Rute
    Sep 23, 2023 at 20:14
  • $\begingroup$ @AdomasBaliuka Theorems are their own category, but as far as reducibility is concerned they are equivalent to irreducible defs. (The way to observe this is that after theorem foo : Nat := 1, example : foo = 1 := by with_unfolding_all rfl works, which is not the case for opaque.) As Jason says, noncomputable is basically unrelated to reducibility and if you would like to ask more about that it would be best to use a separate question. $\endgroup$ Sep 25, 2023 at 6:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.