feat(Tactic/Alias): let attributes know that the constant is an alias

[JovanGerb]

When tagging an alias with to_additive, we would like to have the translated declaration also be an alias, and have it get the docstring that normal aliases get. To do this, we need alias to first tag the declaration as an alias before elaborating the attributes.

I noticed that the aliasExt extension was not actually storing aliases how they appear, but some funny kind of transitive extension of this. This is annoying, because this is not what is used for the generated docstring. Hence, I've changed this so that the environment extension stores the aliases how they are written down. If desired, it is always possible to compute a transitive closure of this.

[fgdorais]

I wrote this three years ago, adapting Mario's code for the old alias command. Mario insisted that the aliasExt references the root alias instead of the (given) head alias. I thought it best for the docstring to be generated from the head alias. We were to revisit these choices when users found them inconvenient. This is finally the day! Three years seems long but I suspect chains of aliases are relatively rare.

Yes, the two decisions are incompatible with each other. Interestingly, nothing breaks after your change. However, this doesn't mean there aren't any downstream tools that rely on the current behavior. For prudence, let's have two versions of getAliasInfo: getRootAliasInfo for the old behavior, getHeadAliasInfo for the new behavior. Then let's deprecate getAliasInfo to getRootAliasInfo. That way any existing tools will be easy to fix (unless they rely directly on the aliasExt, which they shouldn't do anyway).

[JovanGerb]

All right, I have implemented it as you suggested. Though I would be surprised if anyone was relying on this behaviour.

At first I tried to use alias for the deprecation, but sadly that doesn't work in the same file where alias is defined 😆

[JovanGerb]

I think my implementation of getRootAlias doesn't quite do the same as the old behaviour in the case of a directional alias of an alias. But this is such an edge case that I don't think this is problematic.

[fgdorais]

The precise old behavior is important for some use cases. After digging in some dusty cabinets, I found some tools that use it. They rely on the fact that two aliases are definitionally the same exactly when their root aliases are equal, and two aliases are "iff-siblings" exactly when their root alias names are the same.

I think Mario also wanted all aliases to be defined in terms of the root alias. That makes sense for defeq checks, for example, but I think it's more brittle. Anyway, that's not how it's done now and there is no need for that change here.

Why don't we have aliasExt record both the head alias and the root alias so that the root calculation is amortized along each alias declaration. That way getHeadAlias and getRootAlias would both be O(1).

By the way, the names should be getHeadAlias? and getRootAlias? since they return an Option type.

[JovanGerb]

I don't think that there would be any performance bottleneck in getRootAlias. I understand that the new implementation is in principle not O(1), but I don't think there exist any long chains of aliases.

What kind of tools are these that rely on the AliasExt? I'm a bit surprised that any tool would rely on AliasExt for checking that constants are definitionally equal. You should be able to figure this out by looking at their definition.

[fgdorais]

These tools are for analyzing how aliases are used in practice. For example, I have a #print aliases command that uses the old behavior but it never made it to production. Admittedly, I haven't used it much and never in the past two years.

As far as cost, recording both is cheap. It will have no significant effect on the alias command since it already did this and each alias declaration is responsible for just one step of root calculation. This is way better than an "incorrect" root alias calculation that is usually O(1)-ish.

[JovanGerb]

I don't think the performance cost is really an issue either way, due to how little this extension is used, an how short the transitive chains are.

The cost is more for maintenance. A more complicated environment extensioin will more easily have bugs (especially if the feature is not used), and the to_additive code will have to be more complicated, as it will have to add the right aliasExt entries.

[fgdorais]

Please tell me more about the relation with to_additive and to_dual. I'm familiar with basics but it seems you are concerned about aspects I don't know about.

[JovanGerb]

I don't mean that it's really a problem. What to_additive/to_dual needs to do is given an alias entry, generate the new alias info for the generated declaration by translating the constants appearing in the old alias info.

[JovanGerb]

Note that also the original implementation of the transitive closure was not entirely "correct". Because if A is the forward alias of B, B is the forward alias of C, A' is the forward alias of B', and B' is the forward alias of C, then it would not have caught that A and A' were the same. So it feels a bit pointless to restore this behaviour that was already flawed.

[fgdorais]

I don't understand: a forward alias is always an implication, not an iff.

[JovanGerb]

An implication can have an iff as its conclusion.

[fgdorais]

Oh! I think you're right, the implementation of mkIffMpApp will eat the hypotheses. Good thing it's about never used that way!

[fgdorais]

This should fix it.

[fgdorais]

Suggested change

	/-- Get the transitive alias information for a name -/
	partial def getRootAliasInfo? [Monad m] [MonadEnv m] (name : Name) : m (Option AliasInfo) := do
	let info? ← getHeadAliasInfo? name
	if let some (.plain n) := info? then
	if let some info ← getRootAliasInfo? n then
	return info
	return info?
	/-- Get the old alias information for a name. -/
	partial def getOldAliasInfo? [Monad m] [MonadEnv m] (name : Name) : m (Option AliasInfo) := do
	match ← getAliasInfo? name with
	| some (.plain n) => getOldAliasInfo? n
	| some (.forward n) =>
	if let some (.plain n') ← getOldAliasInfo? n then
	return some (.forward n')
	else
	return some (.forward n)
	| some (.reverse n) =>
	if let some (.plain n') ← getOldAliasInfo? n then
	return some (.reverse n')
	else
	return some (.reverse n)
	| none => return none

[fgdorais]

Suggested change

	def getHeadAliasInfo? [Monad m] [MonadEnv m] (name : Name) : m (Option AliasInfo) := do
	def getAliasInfo? [Monad m] [MonadEnv m] (name : Name) : m (Option AliasInfo) := do

[fgdorais]

Suggested change

	@[deprecated getRootAliasInfo? (since := "2026-04-11")]
	@[deprecated "use `getAliasInfo?` or `getOldAliasInfo?` for the original behavior" (since := "2026-04-11")]

[fgdorais]

Suggested change

	/-- Returns the path of aliases starting at a given name.
	The return value is a pair `(mps, name)` where `name` is the final non-aliased name in the
	alias chain and `mps` is a list of `Bool` indicating the sequence of forward (`true`) and
	reverse (`false`) aliases along the chain.
	-/
	partial def getAliasPath [Monad m] [MonadEnv m] (name : Name) : m (List Bool × Name) := do
	match ← getAliasInfo? name with
	| some (.plain name) => getAliasPath name
	| some (.forward name) =>
	let (p, name) ← getAliasPath name
	return (true :: p, name)
	| some (.reverse name) =>
	let (p, name) ← getAliasPath name
	return (false :: p, name)
	| none => return ([], name)