use cases of abbrev

Stream: lean4

[Isaac Marlon da Silva Lourenço]

Hey, there! I'm curious to know what more interesting cases of abbrev command. On tutorial, the best advantage of using abbrev instead def is that the first overload automatically numerical values and second not. Is there better examples of when use abbrev? Thanks.

[Marcus Rossel]

Using abbrev marks the definition as @[reducible], which allows typeclass inference "see through"/unfold the definition (I don't understand typeclass inference well enough to explain what this means under the hood).

[Kyle Miller]

There are roughly three ways you can define a type in terms of another type, each with different properties:

inductive foo1
| mk (val : Nat → Nat)

def foo2 := Nat → Nat

abbrev foo3 := Nat → Nat

The first, foo1, is to create a completely new inductive type (note that you can also use structure for this, which has the same relevant properties). This example creates a type that's isomorphic to Nat -> Nat, but Lean considers it to be completely different from Nat -> Nat itself. Nothing about Nat -> Nat carries over, and you can't use it interchangably with Nat -> Nat in any way.

The second, foo2, is to create a plain definition that is a synonym for the type. A big difference between foo2 and foo1 is that Lean can see that foo2 is definitionally equal to Nat -> Nat, so you can use terms of foo2 or Nat -> Nat mostly interchangably. A big difference is that you do not get any typeclass instances of Nat -> Nat for foo2 terms. You can manually carry ones you are interested in over though. The reason for this is that, like Marcus says, typeclass inference doesn't expand definitions when they have the default reducibility setting.

The third, foo3, is to create an abbrev definition that is a synonym for the type. This is just a def, but it has the added feature that typeclass inference will expand it while doing typeclass search. Abbreviations are meant to stand for exactly what they are a synonym for.

[Kyle Miller]

If you're familiar with Haskell, this is similar to defining type synonyms using data vs newtype vs type, but there's the difference that a newtype in Haskell is not definitionally equal to the type it's wrapping.