feat: validate reducibility attribute setting

[leodemoura]

and new option set_option allowUnsafeReductibility true to override validation.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 092ca8530a6f272b7cb19235750479cdffab11de --onto 806e41151b6eb645e4ed5a40915b94b99f933564. (2024-05-02 18:25:05)

[tydeu]

Could ReducibilityHints.abbrev be used to distinguish between these cases?

[leodemoura]

Unfortunately, it does not help. The key issue here is that the current attribute management system does not tell us whether an attribute is being set at a declaration time or not.

[tydeu]

True, having the attribute know whether it is applied at declaration time would be the best solution. However, I was proposing a potential partial solution assuming that was too complicated for now.

If I understand correctly, abbrev is just a @[reducible, inline] def with ReducibilityHints.abbrev. Thus, the primary use case for a declaring @[reducible] def over an abbrev is when the definition is meant to be reducible but not inlined. In such a case, @[noinline] abbrev could serve the same purpose. Thus, to avoid the potential for applying @[reducible] after a declaration, we could forbid @[reducible] from being applied to anything except abbrev at declaration-time (i.e., when it is semireducible). This would avoid the need to make the declaration time distinction.

[leodemoura]

@tydeu This is a good suggestion. Then, we would not even have the attribute [reducible]. It seems there are very few instances of @[reducible] def in Mathlib. So, the impact would be minimal. @semorrison What do you think? We can use a different PR for this change.

[Kha]

Fwiw, adding a flag to AttributeImpl.add that tells us whether this is a post-hoc application seems like a simple (apart from downstream breakage) and generally very useful change to me