feat: add `@[backward_defeq]` attribute and local `useBackward` simp option by nomeata · Pull Request #13492 · leanprover/lean4

nomeata · 2026-04-21T11:07:03Z

This PR introduces stricter inference for the @[defeq] attribute and a
companion @[backward_defeq] attribute that preserves the pre-PR behavior
as an opt-in.

What changed

@[defeq] is now inferred only when the equation holds at
.instances transparency (the transparency dsimp operates at).
@[backward_defeq] is the old set: every theorem whose rfl proof
the legacy inference would have accepted is tagged @[backward_defeq],
so defeq ⊆ backward_defeq holds by construction.
The option backward.defeqAttrib.useBackward (default false) makes
dsimp also use @[backward_defeq] theorems, restoring the pre-PR
behavior for a specific proof or file.
The option is eqn-affecting: its value at the point of a function's
definition is recorded so that the equation lemmas later generated for
that function use the same value, regardless of the ambient option at
the use site.

Mathlib adaption

A companion adaption branch (lean-pr-testing-backward-defeq-attrib on
mathlib4) builds cleanly against this PR and passes lake test without
warnings. Most adaption changes are scoped
set_option backward.defeqAttrib.useBackward true in additions on the
failing declarations; a small number of files needed proof-level edits
where the stored form of a dsimp%/@[reassoc]/@[elementwise]
/@[simps]/@[to_app]-generated lemma had drifted under the stricter
regime.

…option This PR splits the implicit inference of the `@[defeq]` attribute on equation theorems (from `def`, `@[simps]`, structural/WF unfold lemmas, etc.) into two tiers: * A theorem is tagged `@[defeq]` when the equation holds at instance transparency (matching the transparency at which `dsimp` operates). * A theorem is additionally tagged with the new `@[backward_defeq]` attribute whenever the old permissive inference (at `.default`/`.all` transparency) would have accepted it — i.e. the `@[backward_defeq]` set is a superset of `@[defeq]`. The previous permissive behavior for `dsimp` is preserved behind a new option `backward.defeqAttrib.useBackward` (default `false`), which is consumed at `simp`/`dsimp` use sites: when `true`, `dsimp` treats `@[backward_defeq]` theorems like `@[defeq]` ones. Because the option is consumed locally at the use site, adaptation can be per-proof (`set_option backward.defeqAttrib.useBackward true in ...`) rather than requiring the option to be flipped at definition sites. Theorems with `:= rfl` as their proof (via `DefView.markDefEq`) continue to be tagged as `@[defeq]` (and also `@[backward_defeq]`, to maintain the superset invariant) regardless of the stricter inference. Core-library adaptations: * `Init/BinderNameHint`: marked `@[implicit_reducible]`. * `Std/Data/DHashMap/Internal/Model`: two `dsimp only` proofs rewritten to `simp only` with an extra `AssocList.contains_eq` argument. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

`@[defeq]` now additionally tags `@[backward_defeq]` (done inside the `defeq` attribute's validator), so that theorems auto-tagged `@[defeq]` via `DefView.markDefEq` (the `:= rfl` path) also end up in the `@[backward_defeq]` set. This keeps the superset invariant uniform: any theorem that would have been treated as rfl under the permissive pre-stricter-inference rules is in `@[backward_defeq]`, whether the tagging came from `inferDefEqAttr`, explicit `@[defeq]`, or the `:= rfl` auto-tagging. `mkSimpTheoremCore` similarly enforces `rfl → backwardRfl` on the `SimpTheorem` fields. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

leanprover-bot · 2026-04-21T12:10:52Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-21 12:10:51)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-24 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-24 15:10:09)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-27 06:42:07)

mathlib-lean-pr-testing · 2026-04-21T12:16:21Z

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-13492 build failed against this PR. (2026-04-21 12:16:19) View Log
🟡 Mathlib branch lean-pr-testing-13492 build against this PR was cancelled. (2026-04-21 13:25:30) View Log
❌ Mathlib branch lean-pr-testing-13492 built against this PR, but linting failed. (2026-04-21 14:19:45) View Log
💥 Mathlib branch lean-pr-testing-13492 build failed against this PR. (2026-04-21 17:29:29) View Log
💥 Mathlib branch lean-pr-testing-13492 build failed against this PR. (2026-04-21 20:22:52) View Log
💥 Mathlib branch lean-pr-testing-13492 build failed against this PR. (2026-04-21 21:47:38) View Log
💥 Mathlib branch lean-pr-testing-13492 build failed against this PR. (2026-04-21 21:55:40) View Log
💥 Mathlib branch lean-pr-testing-13492 build failed against this PR. (2026-04-21 23:53:14) View Log
💥 Mathlib branch lean-pr-testing-13492 build failed against this PR. (2026-04-22 13:54:09) View Log
🟡 Mathlib branch lean-pr-testing-13492 build against this PR was cancelled. (2026-04-22 14:03:14) View Log
🟡 Mathlib branch lean-pr-testing-13492 build this PR didn't complete normally. (2026-04-22 14:04:17) View Log
💥 Mathlib branch lean-pr-testing-13492 build failed against this PR. (2026-04-22 14:54:18) View Log
💥 Mathlib branch lean-pr-testing-13492 build failed against this PR. (2026-04-22 15:15:48) View Log
✅ Mathlib branch lean-pr-testing-13492 has successfully built against this PR. (2026-04-22 16:09:57) View Log
✅ Mathlib branch lean-pr-testing-13492 has successfully built against this PR. (2026-04-22 17:38:18) View Log
✅ Mathlib branch lean-pr-testing-13492 has successfully built against this PR. (2026-04-22 22:53:22) View Log
✅ Mathlib branch lean-pr-testing-13492 has successfully built against this PR. (2026-04-24 03:00:02) View Log
✅ Mathlib branch lean-pr-testing-13492 has successfully built against this PR. (2026-04-24 04:16:38) View Log
✅ Mathlib branch lean-pr-testing-13492 has successfully built against this PR. (2026-04-24 04:55:43) View Log
✅ Mathlib branch lean-pr-testing-13492 has successfully built against this PR. (2026-04-24 05:09:01) View Log
✅ Mathlib branch lean-pr-testing-13492 has successfully built against this PR. (2026-04-24 05:19:02) View Log
✅ Mathlib branch lean-pr-testing-13492 has successfully built against this PR. (2026-04-24 06:59:17) View Log
✅ Mathlib branch lean-pr-testing-13492 has successfully built against this PR. (2026-04-24 10:20:45) View Log
💥 Mathlib branch lean-pr-testing-13492 build failed against this PR. (2026-04-24 15:46:49) View Log
✅ Mathlib branch lean-pr-testing-13492 has successfully built against this PR. (2026-04-26 21:53:47) View Log
💥 Mathlib branch lean-pr-testing-13492 build failed against this PR. (2026-04-27 07:31:35) View Log
✅ Mathlib branch lean-pr-testing-13492 has successfully built against this PR. (2026-04-27 09:09:01) View Log
🟡 Mathlib branch lean-pr-testing-13492 build against this PR was cancelled. (2026-04-27 09:34:57) View Log
✅ Mathlib branch lean-pr-testing-13492 has successfully built against this PR. (2026-04-27 09:43:32) View Log

Without this, even with `backward.defeqAttrib.useBackward true` globally, `dsimp` could pick up a `@[backward_defeq]` theorem (via the gate in `rewriteUsingIndex?`/`rewriteNoIndex?`), but the `tryTheoremCore` path would still fall through to emitting an explicit rewrite proof rather than using the implicit-defeq-proof shortcut. The resulting generated proof term differed from the one produced when the theorem was `@[defeq]`, which broke downstream metaprograms that translate proof terms (e.g. `@[to_dual]`): the reordered translation ended up ill-typed at the kernel level. Making `useImplicitDefEqProof` treat a `@[backward_defeq]` theorem as rfl-like when the option is on restores proof-term equivalence with the pre-stricter-inference behavior, and removes the need for mathlib-side metaprogramming patches (e.g. the `@[simps]`/`@[to_dual]` "set `[defeq]` directly for rfl proofs" workaround). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

This extends `backward.defeqAttrib.useBackward` to be stored at definition time and replayed at equation realization time, alongside `backward.eqns.nonrecursive` and `backward.eqns.deepRecursiveSplit`. Previously the option was consumed only at simp use sites. But certain downstream metaprograms (observed in `@[simps!]`-generated projections and their interaction with `Equiv.trans_def`-style rfl lemmas) trigger equation realization whose proof terms depend on the option; if it's only set at the use site, the realized const differs from what the use-site expects. Making the option eqn-affecting means the defining module's value of the option is replayed during realization, restoring the expected behavior. To share the option declaration between `Lean.Meta.Eqns` and `Lean.Meta.Tactic.Simp.SimpTheorems`, it is moved to `Lean.DefEqAttrib` (imported by both). Consequence for downstream adaptation: the option now acts non-locally — to restore the legacy behavior of a proof, the option may need to be set at the file level of both the defining module and the using module, not just at the using proof. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

… generation (#13475) This PR replaces the eager equation realization that was triggered by non-default values of equation-affecting options (like `backward.eqns.nonrecursive`) with a `MapDeclarationExtension` that stores non-default option values at definition time. These values are then restored when equations are lazily realized, so the same equations are produced regardless of when generation occurs. Restoring the options is done via a new `withEqnOptions` helper in `Lean.Meta.Eqns`. Because `realizeConst` overrides the caller's options with the options saved in its `RealizationContext` — which are empty for imported constants — the helper must also be applied inside the `realizeConst` callbacks in `mkSimpleEqThm`, `mkEqns` (in `Elab/PreDefinition/Eqns.lean`), `getConstUnfoldEqnFor?`, and `Structural.mkUnfoldEq`. Without that, equation generation code that reads eqn-affecting options inside the realize callback would see the caller-independent defaults rather than the values stored in `eqnOptionsExt` — so the store-at-definition-time behavior would not carry across module boundaries. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

This PR fixes a benchmark regression introduced in #13475: `eqnOptionsExt` was using `.async .asyncEnv` asyncMode, which accumulates state in the `checked` environment and can block. Switching to `.local` — consistent with the neighbouring `eqnsExt` and the other declaration caches in `src/Lean/Meta` — restores performance (the `build/profile/blocked (unaccounted) wall-clock` bench moves from +33% back to baseline). `.local` is safe here because `saveEqnAffectingOptions` is only called during top-level `def` elaboration and downstream readers see the imported state; modifications on non-main branches are merged into the main branch on completion. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Use \`getAsyncConstInfo\` + \`toConstantInfo\` instead of plain \`getConstInfo\`, otherwise \`info.value?\` may return \`none\` for theorems whose body is still being filled in by async elaboration. The caller (e.g. mathlib's \`@[simps!]\`) then sees an axiom-shaped proxy and silently skips tagging the theorem. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

This reverts commit 390403b.

… rfl proofs The legacy \`inferDefEqAttr\` (pre-\`[defeq]\`/\`[backward_defeq]\` split) tagged \`@[defeq]\` unconditionally whenever \`isRflProofCore\` returned true — only logging an error if \`validateDefEqAttr\` also failed. The new split variant instead gated \`@[backward_defeq]\` tagging on the validation succeeding, meaning some theorems that the old inference covered get NEITHER tag now. That breaks the superset guarantee between old \`[defeq]\` and new \`[backward_defeq]\`, so \`set_option backward.defeqAttrib.useBackward true\` does not reliably restore pre-PR behavior. Tag \`@[backward_defeq]\` unconditionally on \`isRfl\` theorems, matching the old inference's unconditional tag. Still log when strict fails and permissive validation also fails, as before.

…achable This PR adds a test case exploring whether the `unless strict do logError` branch in `inferDefEqAttr` (which swallows `validateDefEqAttr` errors when the strict `.instances`-transparency check succeeded) can actually be reached. Attempting to construct such a case with `@[reducible]` and/or smart-unfolding shows that every public theorem where strict could succeed also has permissive succeed — the `withoutExporting` in `inferDefEqAttr` does not give strict a bigger view than the permissive validator has. The defensive guard therefore appears to be unreachable in practice; the test documents the phenomenon for future reference.

…lean4 into joachim/backward-defeq-attrib

@nomeata

…ng-line fixers (#38602) This PR cherry-picks a set of adaptation-helper scripts that @nomeata developed on the `lean-pr-testing-13492` branch during the adaptation for leanprover/lean4#13492 (now merged). He flagged on Zulip ([thread](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/lean.2313492.2C.20stricter.20.40.5Bdefeq.5D.20inference/near/591078800)) that he plans to delete them from the adaptation branch and offered them up for adoption. Changes: - `scripts/add_set_option.py`, `scripts/rm_set_option.py`: new `--value` flag, so the scripts work for options whose default is `false` (where you want to insert `set_option X true in`) as well as the existing `false` case. - `scripts/add_module_set_option.py` (new): file-level variant of `add_set_option.py` — inserts a module-scoped `set_option` after the imports (and module docstring, if present) rather than scoped to a declaration. Needed for eqn-affecting options. - `scripts/rm_module_set_option.py` (new): file-level variant of `rm_set_option.py`. Traverses the import DAG backward, with resume support keyed on toolchain. - `scripts/fix_nonlocal_set_option.py` (new): given failing modules, adds the option to all transitive deps then binary-search minimizes back to the smallest set whose modules need it. - `scripts/fix_unused_simp_args.py` (new): parses `This simp argument is unused: X` warnings from `lake build` and removes `X` from the corresponding `simp` / `simp only` call. For `← X` it rewrites to `- X` because the `←` has simp-set side effects. - `scripts/fix_long_lines.py` (new): breaks too-long lines at the last comma before column 100 and indents the continuation. Useful as a follow-up to scripts that rewrite simp lists. - `scripts/README.md`: documents all of the above. The defaults for `--option` in the new module-level scripts point at `backward.defeq.atInstanceTransparency` (the option from leanprover/lean4#13492); for current options pass `--option <name>` explicitly. Original commits from `lean-pr-testing-13492`: - `6f1a3512906` chore(scripts): add `--value` flag to add/rm_set_option.py (had a small conflict with #38532's `lakefile.lean` existence check; resolved by combining) - `36625b2a675` chore(scripts): bring back module-level / nonlocal scripts - `de2a59b5839` chore(scripts): thread `--value` through `fix_nonlocal_set_option.py` - `45f3ee41b94` (extracted) `fix_unused_simp_args.py` - `4278b885305` (extracted) `fix_long_lines.py` - `80852596213` doc(scripts): document new helpers I sanity-checked each script: all parse, all `--help`s render, and `fix_long_lines.py` / `fix_unused_simp_args.py` produce the expected output on synthetic inputs. 🤖 Prepared with Claude Code Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

nomeata added changelog-language Language features and metaprograms changelog-tactics User facing tactics labels Apr 21, 2026

nomeata requested review from TwoFX and leodemoura as code owners April 21, 2026 11:07

nomeata changed the base branch from nightly-with-mathlib to master April 21, 2026 11:07

nomeata marked this pull request as draft April 21, 2026 11:07

github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 21, 2026

github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Apr 21, 2026

mathlib-lean-pr-testing Bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 21, 2026

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 21, 2026

Update lean-toolchain for leanprover/lean4#13492

39a9fb8

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 21, 2026

Update lean-toolchain for leanprover/lean4#13492

25496f7

chore: request stage0 update

04c73ba

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 21, 2026

Update lean-toolchain for leanprover/lean4#13492

150df03

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 21, 2026

Update lean-toolchain for leanprover/lean4#13492

c1a493b

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 21, 2026

Update lean-toolchain for leanprover/lean4#13492

c369611

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 21, 2026

Update lean-toolchain for leanprover/lean4#13492

9cf3fce

nomeata and others added 2 commits April 21, 2026 21:09

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 21, 2026

Update lean-toolchain for leanprover/lean4#13492

bd1c78c

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 21, 2026

Update lean-toolchain for leanprover/lean4#13492

29bec3c

nomeata and others added 4 commits April 22, 2026 06:59

Revert "fix: await async theorem body in \inferDefEqAttr\"

c1e2e25

This reverts commit 390403b.

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 22, 2026

Update lean-toolchain for leanprover/lean4#13492

16eda9d

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 22, 2026

Update lean-toolchain for leanprover/lean4#13492

a6acd94

Kick CI

544ab66

mathlib-lean-pr-testing Bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Apr 22, 2026

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 22, 2026

Update lean-toolchain for leanprover/lean4#13492

3bec183

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 22, 2026

Update lean-toolchain for leanprover/lean4#13492

f3bf1a6

nomeata mentioned this pull request Apr 24, 2026

feat: equational lemmas are only [defeq] when so at .instance transparency #13330

Closed

Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/…

78abb2f

…lean4 into joachim/backward-defeq-attrib

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 24, 2026

Update lean-toolchain for leanprover/lean4#13492

db95397

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 24, 2026

Update lean-toolchain for leanprover/lean4#13492

8f54182

Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/…

d049638

…lean4 into joachim/backward-defeq-attrib

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 27, 2026

Update lean-toolchain for leanprover/lean4#13492

202f6a6

mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 27, 2026

Update lean-toolchain for leanprover/lean4#13492

23aa2cf

mathlib-lean-pr-testing Bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Apr 27, 2026

nomeata marked this pull request as ready for review April 27, 2026 07:41

mathlib-lean-pr-testing Bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Apr 27, 2026

nomeata added this pull request to the merge queue Apr 27, 2026

Merged via the queue into master with commit ac9a1cb Apr 27, 2026
41 checks passed

kim-em mentioned this pull request Apr 28, 2026

[Merged by Bors] - chore(scripts): add module-level set_option helpers and simp-arg / long-line fixers leanprover-community/mathlib4#38602

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add `@[backward_defeq]` attribute and local `useBackward` simp option#13492

feat: add `@[backward_defeq]` attribute and local `useBackward` simp option#13492
nomeata merged 14 commits intomasterfrom
joachim/backward-defeq-attrib

nomeata commented Apr 21, 2026 •

edited

Loading

Uh oh!

leanprover-bot commented Apr 21, 2026 •

edited

Loading

Uh oh!

mathlib-lean-pr-testing Bot commented Apr 21, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

nomeata commented Apr 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What changed

Mathlib adaption

Uh oh!

leanprover-bot commented Apr 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing Bot commented Apr 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

nomeata commented Apr 21, 2026 •

edited

Loading

leanprover-bot commented Apr 21, 2026 •

edited

Loading

mathlib-lean-pr-testing Bot commented Apr 21, 2026 •

edited

Loading