drawbacks of abbrev

Stream: lean4

[Andrés Goens]

I've seen that sometimes people prefer not to use abbrev (e.g. here) and instead prefer copy-pasting definitions, e.g. when specializing a definition for a concrete type (monomorphizing). I thought abbrev had extra hints to the kernel and such. Is there some cases where abbrev not reduce things enough, or is this primarily for performance? (and how much of a difference does it have on performance)?

[Mac Malone]

Note that, instead of copy-pasting definitions, you can use metaprogramming. See, for example, the elab_inline tool I used in this thread.

[Andrés Goens]

I guess my main question is why someone would not want to use abbrev; If there's concrete examples where one would expect abbrev to be reduced/unfolded and it doesn't, or where using abbrev makes things noticeably slower?

[Yaël Dillies]

Maybe the reason is that abbreviation in Lean 3 meant the same as @[reducible, inline] def + "Whoops, I forgot to generate the equation lemmas", which made it very irritating to use.

[Andrés Goens]

so it might be more of a remnant of Lean 3 that is less the case with Lean 4's abbrev?

[Shreyas Srinivas]

Andrés Goens said:

I guess my main question is why someone would not want to use abbrev; If there's concrete examples where one would expect abbrev to be reduced/unfolded and it doesn't, or where using abbrev makes things noticeably slower?

I use abbrev because defining a proxy (or a more descriptive name) for a type using def means I get none of the typeclass instances of the actual type.

[Shreyas Srinivas]

If I define def distance := \Q I don't get all the ring, field, and arithmetic related instances. For something as simple as adding two objects of the distance type, the compiler complains about HAdd instances for distance. If I instead use abbrev distance := \Q, I get all the instances of \Q automatically for distance

[Andrés Goens]

@Shreyas Srinivas but then you are arguing in favor of using abbrev, right? I was trying to understand the reasons not to use it. Or do you mean you don't want those instances because you want to define your own?

[Andrés Goens]

(but then you wouldn't copy-paste the definitions)

[Shreyas Srinivas]

Yes indeed I am arguing in favour of your point

[Andrés Goens]

I guess this is a good example by @Siddharth Bhat https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Ergonomics.3A.20linarith.20does.20not.20work.20on.20Nat.20alias

[Shreyas Srinivas]

Andrés Goens said:

I guess this is a good example by Siddharth Bhat https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Ergonomics.3A.20linarith.20does.20not.20work.20on.20Nat.20alias

That looks like a bug. Besides, the use of abbrev is still important there, because if you replace it with def then H : a < b is an error since the relevant typeclasses are not defined for the type Index.

[Shreyas Srinivas]

If you look closely at the example : The step simp [Index] at * is transforming @LT.lt Index instLTNat a b : Prop to @LT.lt ℕ instLTNat a b : Prop, implying that an instance of LT was inferred for Index. Why linarith failed to use it without this step is beyond me. But this instance only exists when one uses abbrev

[Eric Wieser]

linarith presumably fails there because at some point it asks "is this type syntactically Nat"

[Shreyas Srinivas]

Can that be replaced by a check for "is it definitionally equal to Nat"?

[Scott Morrison]

Yes, presumably a slight tweak to src4#Linarith.isNatProp

[Eric Wieser]

Arguably that check is wrong anyway; it shouldn't be checking that the type is nat, but that the instance unifies with the nat one

[Eric Wieser]

Otherwise it will create an invalid proof if we put the dual order on nat, rather than crashing