What is the difference between abbreviation and def

Stream: new members

[Lars Ericson]

What is the difference between abbreviation and def? Is abbreviation more like macro expansion with less type checking/type inference?

Is there a canonical example requiring use of abbreviation where def won't work?

I looked for abbreviation in TPIL and Logic&Proof and the Reference Manual and couldn't find it.

[Eric Wieser]

abbreviation is @[inline, reducible] def

[Eric Wieser]

I thinkalias is stronger than abbreviation

[Mario Carneiro]

alias is just a regular def/theorem

[Mario Carneiro]

I wouldn't recommend using it for defs actually

[Mario Carneiro]

I don't think there are any reasons to use abbreviation

[Eric Wieser]

alias shows up specially in doc-gen, somehow

[Calle Sönne]

(deleted)

[Lars Ericson]

The @[inline, reducible] has a pragmatic effect. I had a situation where abbreviation worked for something and def did not.

[Lars Ericson]

For example this works with abbreviation:

import measure_theory.lebesgue_measure
import measure_theory.borel_space
import data.set.intervals.basic
import measure_theory.measure_space

open measure_theory

noncomputable instance {α} {p : α → Prop} [m : measure_space α] : measure_space (subtype p) :=
{ volume := measure.comap (coe : _ → α) volume }

theorem subtype.volume_apply {α} {p : α → Prop} [measure_space α]
  (hp : is_measurable {x | p x}) {s : set (subtype p)} (hs : is_measurable s) :
  volume s = volume ((coe : _ → α) '' s) :=
measure.comap_apply _ subtype.coe_injective (λ _, is_measurable.subtype_image hp) _ hs

abbreviation I01 := (set.Icc (0 : ℝ) 1)

instance : probability_measure (volume : measure I01) :=
{ measure_univ := begin
    refine (subtype.volume_apply is_measurable_Icc is_measurable.univ).trans _,
    suffices : volume I01 = 1, {simpa},
    rw [real.volume_Icc], simp
  end }

and if I change the abbreviation to a def, I get this:

bar.lean:22:4
rewrite tactic failed, did not find instance of the pattern in the target expression
  ⇑volume (set.Icc ?m_1 ?m_2)
state:
⊢ ⇑volume I01 = 1

I'm guessing that's the inline or macro effect and in this case it is required to get the proof to go through.

[Reid Barton]

it's reducible

[Reid Barton]

I01 is still not a macro, it's just that more things are willing to unfold it automatically.

[Mario Carneiro]

Eric Wieser said:

alias shows up specially in doc-gen, somehow

alias is primarily intended for documentation purposes, or to make a theorem available under two names to make it easier to find (e.g. left_distrib vs mul_add)

[Eric Wieser]

Is aliasbuiltin syntax, or is it a mathlib command?

[Mario Carneiro]

https://leanprover-community.github.io/mathlib_docs/tactic/alias.html

[Eric Wieser]

What I thought was "special doc-gen treatment" was actually just this generated docstring:

https://github.com/leanprover-community/mathlib/blob/702b1e8c778d6b18444cc57858c636c8ae2ad700/src/tactic/alias.lean#L134