Zulip Chat Archive

Stream: new members

Topic: What is the difference between abbreviation and def


view this post on Zulip Lars Ericson (Dec 10 2020 at 15:49):

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.

view this post on Zulip Eric Wieser (Dec 10 2020 at 15:59):

abbreviation is @[inline, reducible] def

view this post on Zulip Eric Wieser (Dec 10 2020 at 16:00):

I thinkalias is stronger than abbreviation

view this post on Zulip Mario Carneiro (Dec 10 2020 at 16:04):

alias is just a regular def/theorem

view this post on Zulip Mario Carneiro (Dec 10 2020 at 16:04):

I wouldn't recommend using it for defs actually

view this post on Zulip Mario Carneiro (Dec 10 2020 at 16:05):

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

view this post on Zulip Eric Wieser (Dec 10 2020 at 16:14):

alias shows up specially in doc-gen, somehow

view this post on Zulip Calle Sönne (Dec 10 2020 at 16:43):

(deleted)

view this post on Zulip Lars Ericson (Dec 10 2020 at 17:41):

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

view this post on Zulip Lars Ericson (Dec 10 2020 at 17:52):

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.

view this post on Zulip Reid Barton (Dec 10 2020 at 17:53):

it's reducible

view this post on Zulip Reid Barton (Dec 10 2020 at 17:53):

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

view this post on Zulip Mario Carneiro (Dec 10 2020 at 18:05):

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)

view this post on Zulip Eric Wieser (Dec 10 2020 at 18:07):

Is aliasbuiltin syntax, or is it a mathlib command?

view this post on Zulip Mario Carneiro (Dec 10 2020 at 18:08):

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

view this post on Zulip Eric Wieser (Dec 10 2020 at 18:13):

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


Last updated: May 09 2021 at 20:11 UTC