feat: explicit defeq attribute

[nomeata]

This PR introduces an explicit defeq attribute to mark theorems that can be used by dsimp. The benefit of an explicit attribute over the prior logic of looking at the proof body is that we can reliably omit theorem bodies across module boundaries. It also helps with intra-file parallelism.

If a theorem is syntactically defined by := rfl, then the attribute is assumed and need not given explicitly. This is a purely syntactic check and can be fooled, e.g. if in the current namespace, rfl is not actually “the” rfl of Eq. In that case, some other syntax has be used, such as := (rfl). This is also the way to go if a theorem can be proved by defeq, but one does not actually want dsimp to use this fact.

The defeq attribute will look at the type of the declaration, not the body, to check if it really holds definitionally. Because of different reduction settings, this can sometimes go wrong. Then one should also write := (rfl), if one does not want this to be a defeq theorem. (If one does then this is currently not possible, but it’s probably a bad idea anyways).

The set_option debug.tactic.simp.checkDefEqAttr true, dsimp will warn if could not apply a lemma due to a missing defeq attribute.

With set_option backward.dsimp.useDefEqAttr.get false one can revert to the old behavior of inferring rfl-ness based on the theorem body.

Both options will go away eventually (too bad we can’t mark them as deprecated right away, see #7969)

Meta programs that generate theorems (e.g. equational theorems) can use inferDefEqAttr to set the attribute based on the theorem body of the just created declaration.

This builds on #8501 to update Init to @[expose] a fair amount of definitions that, if not exposed, would prevent some existing := rfl theorems from being defeq theorems. In the interest of starting backwards compatible, I exposed these function. Hopefully many can be un-exposed later again.

A mathlib adaption branch exists that includes both the meta programming fixes and changes to the theorems (e.g. changing := by rfl to := rfl).

With the module system there is now no special handling for defeq theorem bodies, because we don’t look at the body anymore. The previous hack is removed. The defeq-ness of the theorem needs to be checked in the context of the theorem’s type; the error message contains a hint if the defeq check fails because of the exported context.

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-8419 build failed against this PR. (2025-05-20 15:26:26) View Log
• 💥 Mathlib branch lean-pr-testing-8419 build failed against this PR. (2025-05-20 17:22:21) View Log
• 💥 Mathlib branch lean-pr-testing-8419 build failed against this PR. (2025-05-21 08:40:44) View Log
• ✅ Mathlib branch lean-pr-testing-8419 has successfully built against this PR. (2025-05-21 09:44:21) View Log
• ✅ Mathlib branch lean-pr-testing-8419 has successfully built against this PR. (2025-05-21 10:35:45) View Log
• ✅ Mathlib branch lean-pr-testing-8419 has successfully built against this PR. (2025-05-21 13:17:24) View Log
• ✅ Mathlib branch lean-pr-testing-8419 has successfully built against this PR. (2025-05-21 15:21:49) View Log
• ✅ Mathlib branch lean-pr-testing-8419 has successfully built against this PR. (2025-05-21 20:05:51) View Log
• 💥 Mathlib branch lean-pr-testing-8419 build failed against this PR. (2025-05-27 16:18:55) View Log
• ✅ Mathlib branch lean-pr-testing-8419 has successfully built against this PR. (2025-05-27 22:39:18) View Log
• 💥 Mathlib branch lean-pr-testing-8419 build failed against this PR. (2025-05-28 08:47:27) View Log
• ✅ Mathlib branch lean-pr-testing-8419 has successfully built against this PR. (2025-05-28 15:54:19) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b9243e19bea83bfa12620e30bc79ef85d78a5c0a --onto c12159b51982221bdd66f0c5997f85e1f9d91772. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-04 13:36:39)
• 💥 Mathlib branch lean-pr-testing-8419 build failed against this PR. (2025-06-05 10:08:11) View Log
• 💥 Mathlib branch lean-pr-testing-8419 build failed against this PR. (2025-06-05 10:30:40) View Log
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-06-05 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-05 11:22:51)
• 💥 Mathlib branch lean-pr-testing-8419 build failed against this PR. (2025-06-05 11:44:19) View Log
• 💥 Mathlib branch lean-pr-testing-8419 build failed against this PR. (2025-06-05 12:03:59) View Log
• 🟡 Mathlib branch lean-pr-testing-8419 build against this PR was cancelled. (2025-06-05 14:51:26) View Log
• ✅ Mathlib branch lean-pr-testing-8419 has successfully built against this PR. (2025-06-05 15:33:30) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eddbe0811842cd38186876ce637274f7edbb4d50 --onto 9b9dd8546a123d746580649b239f26c26d370d20. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-06 18:52:51)

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit af15d77.
There were significant changes against commit 9b9dd85:

  Benchmark                              Metric                  Change
  =================================================================================
- Init.Data.BitVec.Lemmas                maxrss                   16.1%    (20.9 σ)
+ Init.Data.BitVec.Lemmas                wall-clock              -38.8%  (-119.9 σ)
+ Init.Data.BitVec.Lemmas re-elab        branches                 -2.4%   (-89.4 σ)
+ Init.Data.BitVec.Lemmas re-elab        instructions             -2.3%   (-95.2 σ)
+ Std.Data.DHashMap.Internal.RawLemmas   wall-clock              -13.4%   (-32.3 σ)
- riscv-ast.lean                         branches                  2.6%    (58.8 σ)
- riscv-ast.lean                         instructions              2.3%    (44.3 σ)
- stdlib                                 attribute application    16.0%    (56.6 σ)
+ stdlib                                 blocked                 -93.4% (-1430.0 σ)
- stdlib                                 tactic execution          8.7%    (31.3 σ)
+ stdlib                                 wall-clock               -4.1%  (-145.6 σ)