fix(Tactic/Simps): skip @[defeq] inference for non-exposed definitions by kim-em · Pull Request #32989 · leanprover-community/mathlib4

kim-em · 2025-12-17T03:33:55Z

This PR makes @[simps] check whether the source definition's body is exposed before calling inferDefEqAttr. When the body is not exposed, we skip the @[defeq] inference to avoid validation errors.

Without this fix, using @[simps] on a definition that is not @[expose]d produces an error like:

Theorem Foo_bar has a `rfl`-proof and was thus inferred to be `@[defeq]`, but validating that attribute failed:
 Not a definitional equality: the left-hand side ... is not definitionally equal to the right-hand side ...
 Note: This theorem is exported from the current module. This requires that all definitions that need to be unfolded to prove this theorem must be exposed.

The fix checks (← getEnv).setExporting true |>.find? cfg.srcDeclName |>.any (·.hasValue) to determine if the definition body is visible in the public scope, and only calls inferDefEqAttr if it is.

🤖 Prepared with Claude Code

github-actions · 2025-12-17T03:35:00Z

PR summary b2d2bc6029

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ MyStruct
+ helperVal
+ myDef

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

JovanGerb · 2025-12-19T09:52:04Z

Now you don't need the srcDeclName field anymore right?

JovanGerb · 2025-12-20T00:03:04Z

The test file is not currently a module. So I don't see how it is testing what it says it is testing.

kim-em · 2025-12-20T00:38:42Z

The test file is not currently a module. So I don't see how it is testing what it says it is testing.

Indeed, thanks. Fixed now.

JovanGerb · 2025-12-20T01:04:32Z

I copy-pasted the test file into the web editor, and it successfully build. Maybe you meant to add public section to the test file?

joneugster

Thank you, besides the adjustment to the test file mentioned this looks good!

joneugster

failing linter do due to some superfluous simp arguments.

Otherwise looks good. Suggesting delegate so that this doesn't lie around for another week

maintainer delegate

github-actions · 2026-02-13T11:21:09Z

🚀 Pull request has been placed on the maintainer queue by joneugster.

Vierkantor

The fix itself looks good, some quibbles about implementation.

Vierkantor · 2026-02-23T17:10:30Z

  let lhs : Expr := mkConst d.name <| d.levelParams.map Level.param
  let todo := todo.eraseDups |>.map fun (proj, stx) ↦ (proj ++ "_", stx)
-  let mut cfg := cfg
+  let bodyExposed := (← getEnv).setExporting true |>.find? d.name |>.any (·.hasValue)


I was surprised that there is no easier way. This is the same check as in the delta-derive handler, so I don't expect any bug here. But it should really be something implemented in core.

Agreed it would be nicer in core — left the check as-is for now since it mirrors Lean's delta-derive handler. Thanks.

Actually, I've decided to just do this now, after realizing how much duplication we'd already produced in lean4.

leanprover/lean4#13868

Thanks for the suggestion.

Vierkantor · 2026-02-23T17:22:13Z

(Also please note that the build is failing.)

mathlib-merge-conflicts · 2026-03-02T16:56:44Z

This pull request has conflicts, please merge master and resolve them.

joneugster · 2026-03-06T09:57:45Z

@kim-em 🏓 would you have time to address the review above and fix the pipeline?

When `@[simps]` is applied to a definition whose body is not exposed, the generated simp lemmas would trigger `@[defeq]` validation errors because `inferDefEqAttr` tries to validate the definitional equality in the exporting (public) scope where the definition body is not visible. This PR fixes the issue by checking whether the source definition's body is exposed before calling `inferDefEqAttr`. If not exposed, we skip the `@[defeq]` inference entirely, avoiding the validation error. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>

Co-authored-by: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com>

Store the bodyExposed check as a Boolean in Config so it's only computed once instead of every time addProjectionSimp is called. This addresses the review comment on the PR. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>

🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Move the test for @[simps] with non-exposed definition bodies to a separate file that uses `module`, so that definition bodies are properly non-exposed by default. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

The `@[simps]` change skips `@[defeq]` for non-exposed definitions, which means `cat_disch` can no longer discharge this goal automatically. Provide an explicit proof using `ext` and `simp`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…ig field Per Vierkantor's review: `bodyExposed` is internal state, not a user-facing option, so it does not belong in `Config` (a user setting it would be silently ignored). Remove the field and pass `bodyExposed` as an explicit parameter to `addProjection` and `addProjections`, computed once in `simpsTac`.

Vierkantor flagged that the `setExporting true |>.find? n |>.any (·.hasValue)` idiom should really live in core. leanprover/lean4#13868 adds `Environment.hasExposedBody` for exactly this. Leave the inline check in place for now (so the PR remains buildable on the current toolchain), and add a note next to it pointing at the follow-up refactor. Also note the other in-tree caller of the same idiom in `Mathlib/Tactic/Translate/Core.lean` even though it is strictly off-topic for this PR — it'll save a future grep.

mathlib-merge-conflicts · 2026-05-29T23:42:54Z

This pull request has conflicts, please merge master and resolve them.

github-actions Bot added the t-meta Tactics, attributes or user commands label Dec 17, 2025

JovanGerb reviewed Dec 17, 2025

View reviewed changes

Comment thread Mathlib/Tactic/Simps/Basic.lean Outdated

JovanGerb reviewed Dec 18, 2025

View reviewed changes

Comment thread Mathlib/Tactic/Simps/Basic.lean Outdated

leanprover-community-bot-assistant assigned eric-wieser Dec 21, 2025

joneugster approved these changes Jan 23, 2026

View reviewed changes

Comment thread MathlibTest/SimpsModule.lean

joneugster assigned joneugster and unassigned eric-wieser Jan 23, 2026

joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 23, 2026

kim-em removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 29, 2026

joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 30, 2026

kim-em removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 12, 2026

kim-em force-pushed the simps-respects-non-exposed-body branch 2 times, most recently from 6613418 to 141689c Compare February 12, 2026 06:57

joneugster approved these changes Feb 13, 2026

View reviewed changes

mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 13, 2026

robin-carlier mentioned this pull request Feb 17, 2026

[Merged by Bors] - feat(CategoryTheory/Monoidal/Closed): Prove the isomorphism of internal hom objects C(x \otimes y, z) and C(y, C(x, z)) #35436

Closed

Vierkantor reviewed Feb 23, 2026

View reviewed changes

Vierkantor added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 23, 2026

ocfnash removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 26, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 2, 2026

grunweg added the LLM-generated PRs with substantial input from LLMs - review accordingly label Mar 16, 2026

Jun2M mentioned this pull request Apr 8, 2026

[Merged by Bors] - feat(Combinatorics/Graph): graph deletion operations #35879

Closed

1 task

joneugster added the please-adopt Inactive PR (would be valuable to adopt) label Apr 17, 2026

kim-em and others added 8 commits April 18, 2026 08:49

Update Mathlib/Tactic/Simps/Basic.lean

1974659

Co-authored-by: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com>

chore: restart CI

aba2a78

refactor: remove unused srcDeclName field from Config

3f46657

🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

Update MathlibTest/SimpsModule.lean

c092468

Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

kim-em force-pushed the simps-respects-non-exposed-body branch from 338e61b to 177a992 Compare April 17, 2026 22:51

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 17, 2026

joneugster removed their assignment May 8, 2026

kim-em removed awaiting-author A reviewer has asked the author a question or requested changes. please-adopt Inactive PR (would be valuable to adopt) labels May 27, 2026

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 29, 2026

Conversation

kim-em commented Dec 17, 2025

Uh oh!

github-actions Bot commented Dec 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary b2d2bc6029

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

JovanGerb commented Dec 19, 2025

Uh oh!

JovanGerb commented Dec 20, 2025

Uh oh!

kim-em commented Dec 20, 2025

Uh oh!

JovanGerb commented Dec 20, 2025

Uh oh!

joneugster left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

joneugster left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented Feb 13, 2026

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

Vierkantor Feb 23, 2026

Choose a reason for hiding this comment

Uh oh!

kim-em May 27, 2026

Choose a reason for hiding this comment

Uh oh!

kim-em May 28, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Vierkantor commented Feb 23, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Mar 2, 2026

Uh oh!

joneugster commented Mar 6, 2026

Uh oh!

mathlib-merge-conflicts Bot commented May 29, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

github-actions Bot commented Dec 17, 2025 •

edited

Loading

joneugster left a comment •

edited

Loading