making definitions

Stream: general

[Billy Price]

What's the functional difference between the following declarations, and how do you go about choosing which to use?

def foo := bar
abbreviation foo := bar
notation `foo` := bar

[Mario Carneiro]

Default to the def

[Mario Carneiro]

Use a notation when you need, well, notation

[Mario Carneiro]

never use a notation abbreviating something more complicated than the application of a constant to some variables, because it's not actually abbreviating anything internally

[Mario Carneiro]

abbreviation is something like a reducible definition that is eagerly unfolded. I believe it has special kernel support, but for the longest time there was only one example of an abbreviation being needed (and it was implemented in core using tactics to create the definition), so adding a keyword for it was probably overkill. I have never seen a genuine use for it

[Mario Carneiro]

You should also add @[reducible] def foo and @[irreducible] def foo to your list. A reducible def is unfolded more eagerly by tactics, in particular rw and simp will unfold reducible defs but not semireducible (regular) defs. This makes them somewhat "transparent". An example of a reducible def is gt, which is supposed to be treated "basically the same" as lt. However they aren't perfect, and mathlib bans the use of gt because the difference sometimes leaks and simp lemmas don't fire, etc. I would recommend avoiding them in favor of a notation, which is "unfolded" immediately at parse time.

Irreducible defs are used when you want the usual unification to not unfold the definition at all. It's not completely airtight because you can still dunfold and delta to unfold an irreducible def, and actually there is no way to get a completely airtight opaque definition in DTT (as implemented by lean). (I believe lean 4 is changing this with constant declarations.)

[Mario Carneiro]

Finally, there is theorem (or its synonym lemma), which acts like an irreducible def, but also elaborates the body asynchronously. This is primarily intended for proofs of propositions (and I believe the linter will yell at you if you mark a non-proposition as theorem). Again, you can still unfold the theorem proof using delta, but this requires some synchronization behind the scenes and it's not recommended.

[Billy Price]

Thanks, that's very helpful! I think I understand what you mean. I had something like @[simp] def subst_nth : nat -> ...and @[simp] def subst := subst_nth 0, and I noticed that I had to apply simp twice in my proofs. Then I noticed I could use abbreviation and just do one simp. So now, as I understand, I should do @[simp] def subst_nth : nat -> ... and @[reducible] def subst := subst_nth 0?

[Mario Carneiro]

You shouldn't have to call simp twice in a row, although it happens occasionally, usually due to a bug or edge case

[Billy Price]

I may be misremembering

[Mario Carneiro]

Having @[simp] on a definition that is not from the equation compiler is a bit odd, as it means that the term will always be eagerly expanded by simp

[Billy Price]

I just picked it up from somewhere - should I just be using reducible everywhere?

[Mario Carneiro]

@[reducible] is not a replacement for this, as it means that simp will see through the definition but will not actually rewrite it, and other tactics may get caught up on it

[Mario Carneiro]

I would say use @[reducible] sparingly

[Mario Carneiro]

Try to get lean to see what you see. That prevents miscommunication and generally speeds things up because things can get out of hand behind your back if you aren't careful

[Billy Price]

Oh okay I misunderstood the point of @[reducible]- how do I get lean to actually rewrite it for me automatically - or when I request it to?

[Mario Carneiro]

@[simp] does that mostly (either on the definition, as a local attribute, or in the simp bracket list)

[Mario Carneiro]

but it is generally best to mark "definitional equations" and simplification lemmas like 0 + x = x as simp lemmas

[Mario Carneiro]

especially for definitions by recursion

[Billy Price]

Why is it odd to use it outside an equational context?

[Mario Carneiro]

If simp is supposed to always rewrite the definition away, then maybe you didn't want the definition in the first place

[Mario Carneiro]

since it seems to be getting in your way enough that you thought to make a blanket rule "this definition is always unwanted"

[Mario Carneiro]

in which case you might consider going for a notation instead

[Mario Carneiro]

If you want it to be rewritten within a section, for example because you are proving basic properties about it by induction and everything requires unfolding the definition, then use a local attribute [simp]

[Mario Carneiro]

because it's not that the definition is unwanted, it's just that you are proving the basic API, and outside the section you will want the definition to be treated mostly atomically, modulo the theorems that have been proven about it

[Billy Price]

But say I'm making a free-variables function. I still want to "unfold" the definition and get the resulting set of free variables outside the "basic API" section. Why would I want to treat it atomically?

[Mario Carneiro]

why would you want to unfold the free variables function? You want equational lemmas saying "the free variables of forall x, phi are the free variables of phi minus {x}" and so on, but you wouldn't want to unfold x \in FV phi to x \in term.rec <unreadable mess>.

[Mario Carneiro]

simp on x \in FV phi should do nothing

[Mario Carneiro]

because that expression is already the most simple and compact way of saying what it says

[Mario Carneiro]

If you have a particular formula, like FV (forall x, x = y /\ y = 0), then equational lemmas will trigger on it and simp will be able to reduce it to {y}

[Billy Price]

equational lemmas which just unfold any given definition - regardless of tag?

[Mario Carneiro]

I mean theorems of the form FV (forall x, phi) = FV phi - {x}

[Mario Carneiro]

which should be marked @[simp]

[Mario Carneiro]

If you write a definition using the equation compiler, these may well be the branches in the definition, in which case you can just mark the definition itself as @[simp] and it will be passed along to these equations

[Mario Carneiro]

but you can also write the equations yourself, in particular if the equations you want to simp with are different from the equations you used in the definition

[Billy Price]

Semi-related, why does this notation compile but when I use it I get "invalid expression" on the right >.

notation '<' a ',' b '>' := pair a b

^^^ I've replaced the back ticks with single quotes so it renders properly

[Mario Carneiro]

unless those are fancy unicode symbols you are probably trampling on another notation

[Mario Carneiro]

btw you can quote backticks with more backticks ``like `this` ``

[Billy Price]

What's the difference between trampling on another notation and overriding?

[Kevin Buzzard]

Maybe you got overrode?