alias

Stream: new members

[Alex Zhang]

What is the function of alias here? Where can I look up such commands? I didn't find it in the Lean Reference Manual.
image.png

[Kevin Buzzard]

Where are you seeing this? I don't think I've ever heard of alias. If you're learning about Lean 3 (the best place to start) you should be reading #tpil

[Kevin Buzzard]

The point of it seems to be that le_trans is used in lots of places but dot notation is cool so we also wanted a version where we could do hab.trans hbc but it looks like we didn't want to remove the gazillion uses of le_trans in mathlib.

[Kevin Buzzard]

alias A <- B seems to define B to be A.

[Eric Wieser]

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

[Bryan Gin-ge Chen]

(command#alias for short)

[Damiano Testa]

When applying alias to a lemma that is tagged with to_additive, Is there a way for alias to automatically generate the to_additive name-alias as well?

[Damiano Testa]

e.g. what is below does not work:

@[to_additive]
lemma mul_le_of_le_of_le_one [covariant_class α α (*) (≤)]
  {a b c : α} (hbc : b ≤ c) (ha : a ≤ 1) : b * a ≤ c :=
calc  b * a ≤ b * 1 : mul_le_mul_left' ha b
        ... = b     : mul_one b
        ... ≤ c     : hbc

@[to_additive]
alias mul_le_of_le_of_le_one ← mul_le_one'
#check add_nonpos'
-- unknown identifier 'add_nonpos''

[Eric Wieser]

Does attribute [to_additive] mul_le_one' work?

[Damiano Testa]

It does!!

alias mul_le_of_le_of_le_one ← mul_le_one'
attribute [to_additive] mul_le_one'
#check add_nonpos'
-- theorem add_nonpos' : ∀ {α : Type u_1} [_inst_1 : add_zero_class α] [_inst_2 : preorder α]
-- [_inst_3 : covariant_class α α has_add.add has_le.le] {a b c : α}, b ≤ c → a ≤ 0 → b + a ≤ c :=
-- add_le_of_le_of_nonpos

[Damiano Testa]

Thanks a lot!

[Eric Wieser]

The downside of that approach is that the additive version doesn't get the alias docstring

[Damiano Testa]

Ok, for the moment, none of these lemmas actually had a doc-string to begin with...

[Eric Wieser]

If you use alias they get a docstring that says "this is an alias of ..."

[Damiano Testa]

Ah, I see.