feat: abbrev produces theorems where appropriate

[kim-em]

This PR modifies the abbrev keyword, ensuring that it produces a theorem when the declaration is a Prop. This is convenient for the frequent current use case of abbrev to set up deprecations.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0d7c3ac79bd9167ce7d295f51bf3779a04f7a07 --onto 9a8543347796e52070ff7936661ae48fcebfea60. (2024-11-14 23:35:49)
• ✅ Mathlib branch lean-pr-testing-6083 has successfully built against this PR. (2024-11-21 08:55:45) View Log
• ✅ Mathlib branch lean-pr-testing-6083 has successfully built against this PR. (2024-11-26 07:13:12) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 827062f807cd869709fb71d5d04a00ff10320be3 --onto 6d495586a1836da3e12efb4fbf9946bd9088ac5f. (2024-11-29 01:12:55)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 904404303b5b7f2f597498af14f793ab72d82c87 --onto 3c5e612dc54733cd707becb929457d2f9d8ca6fd. (2024-12-03 04:27:53)

[eric-wieser]

Is there any advantage of using abbrev over theorem in this case?

[kim-em]

Is there any advantage of using abbrev over theorem in this case?

Yes, we can use abbrev X := @Y, to avoid having the type out the signature, when deprecating. In Batteries and below, we have alias, but I don't think alias is ready to move upstream (precisely because it results in us having too many ways to do the same thing: eventually I would like a unification of abbrev and alias functionality into a single keyword).

[kim-em]

I'm adding the awaiting-review tag as I would like another set of eyes on this before merging. It feels a bit hacky to me still. :-(

This is an intermediate measure until we decide on a unification of alias / abbrev etc.

[nomeata]

For just offering something under a different name, I guess that can be done on the level of renaming variables.

theorem foo : True := .intro

open _root_ renaming foo → alias

(Likely this idiom doens't work completely the way it seems to work, e.g. across modules.)

Unfortunately deprecation attributes are attached to the underlying constant, not to the alias:

theorem foo : True := .intro

open _root_ renaming foo → alias

attribute [deprecated "test"] alias

/-- warning: `foo` has been deprecated: test -/
#guard_msgs in def ok := foo
/-- warning: `foo` has been deprecated: test -/
#guard_msgs in def not_ok := alias

If the latter could change then the whole use-case of providing alternative names could be moved from the level of definitions to the level of name resolution, which is likely more robust anyways?

[Kha]

@kim-em Could you explain what the limitations of the current behavior are, i.e. abbrev not creating a theorem?

Note that declarations changing their kind post-hoc can also be an issue for parallelism.

[kim-em]

@kim-em Could you explain what the limitations of the current behavior are, i.e. abbrev not creating a theorem?

Note that declarations changing their kind post-hoc can also be an issue for parallelism.

It's not super important, but I have been trying to get the Batteries environment linter suite running on Lean itself, and all the abbrevs currently make the defLemma linter very noisy, and hard to be sure we're otherwise satisfying.

[Kha]

Ok, given the additional complication with parallelism, I'd prefer adjusting the linter instead