Zulip Chat Archive

Stream: general

Topic: making definitions


Billy Price (May 28 2020 at 04:24):

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 (May 28 2020 at 04:24):

Default to the def

Mario Carneiro (May 28 2020 at 04:25):

Use a notation when you need, well, notation

Mario Carneiro (May 28 2020 at 04:26):

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 (May 28 2020 at 04:27):

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 (May 28 2020 at 04:34):

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 (May 28 2020 at 04:37):

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 (May 28 2020 at 04:54):

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 (May 28 2020 at 04:57):

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 (May 28 2020 at 04:57):

I may be misremembering

Mario Carneiro (May 28 2020 at 04:58):

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 (May 28 2020 at 04:59):

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

Mario Carneiro (May 28 2020 at 04:59):

@[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 (May 28 2020 at 04:59):

I would say use @[reducible] sparingly

Mario Carneiro (May 28 2020 at 05:00):

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 (May 28 2020 at 05:01):

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 (May 28 2020 at 05:01):

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

Mario Carneiro (May 28 2020 at 05:02):

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

Mario Carneiro (May 28 2020 at 05:03):

especially for definitions by recursion

Billy Price (May 28 2020 at 05:03):

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

Mario Carneiro (May 28 2020 at 05:04):

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

Mario Carneiro (May 28 2020 at 05:04):

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 (May 28 2020 at 05:05):

in which case you might consider going for a notation instead

Mario Carneiro (May 28 2020 at 05:06):

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 (May 28 2020 at 05:07):

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 (May 28 2020 at 05:09):

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 (May 28 2020 at 05:11):

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 (May 28 2020 at 05:12):

simp on x \in FV phi should do nothing

Mario Carneiro (May 28 2020 at 05:12):

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

Mario Carneiro (May 28 2020 at 05:14):

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 (May 28 2020 at 05:20):

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

Mario Carneiro (May 28 2020 at 05:21):

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

Mario Carneiro (May 28 2020 at 05:21):

which should be marked @[simp]

Mario Carneiro (May 28 2020 at 05:22):

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 (May 28 2020 at 05:22):

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 (May 28 2020 at 08:16):

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 (May 28 2020 at 08:22):

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

Mario Carneiro (May 28 2020 at 08:23):

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

Billy Price (May 28 2020 at 08:42):

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

Kevin Buzzard (May 28 2020 at 08:55):

Maybe you got overrode?


Last updated: Dec 20 2023 at 11:08 UTC