feat: restrict simpa using h close to reducible transparency#13636
Open
kim-em wants to merge 5 commits into
Open
feat: restrict simpa using h close to reducible transparency#13636kim-em wants to merge 5 commits into
simpa using h close to reducible transparency#13636kim-em wants to merge 5 commits into
Conversation
kim-em
force-pushed
the
simpa-reducible-impl
branch
from
d8a5f33 to
ef196db
Compare
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
This PR makes `simpa using h` require the simplified `h` and the simplified goal to match at reducible transparency, rather than at the ambient (default/semireducible) transparency used previously. This makes `simpa using h` more predictable: it no longer succeeds via incidental β/δ-reduction at the closing step, so adding new `simp` lemmas is less likely to silently break unrelated `simpa` calls. The new behaviour is gated by a backward-compat option `backward.simpa.using.reducibleClose` (defaulting to `true`); set it to `false` per-call, per-section, or globally to restore the previous behaviour. Two existing in-tree tests (`getElemV.lean`, `scopeCacheProofs.lean`) relied on the old behaviour; they are annotated with the option and an explanatory comment so the breakage is visible. The change wraps only the precondition `isDefEq` check inside `Lean.Elab.Tactic.Simpa.evalSimpa`. The downstream metavariable-assignment check (`MVarId.checkedAssign` → `checkTypesAndAssign`) still escalates transparency internally, but the reducible-transparency precondition strictly dominates it, so the escalation is benign. Motivated by Floris's Zulip thread on `simpa` code quality: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20code.20quality.3A.20simpa Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
kim-em
force-pushed
the
simpa-reducible-impl
branch
from
ef196db to
e62206c
Compare
github-actions
Bot
added
the
mathlib4-nightly-available
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
Collaborator
Author
|
I've asked for help fixing Mathlib in #mathlib4 > Mathlib code quality: simpa @ 💬. |
…ackward option This switches the opt-out for the new reducible-transparency close from a `backward.simpa.using.reducibleClose` option to the existing `simpa!` form. Users who need the previous default-transparency close write `simpa! using h`; the `backward` option is removed. Updates the two in-tree tests that previously used the option, and the `simpa_reducible.lean` test to exercise the new `simpa!` form. Per Johan's request in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20code.20quality.3A.20simpa. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 12, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
May 12, 2026
…lose Replaces the prefix-`!` conflation (where `simpa!` would both auto-unfold the simp set *and* close at default transparency) with a dedicated `using!` clause that affects only the close step. `simpa! using h` retains its existing meaning (auto-unfold during simp). `simpa using! h` opts into the permissive default-transparency close. The two can be combined as `simpa! ... using! h`. The new tactic is introduced as a parallel syntax declaration `simpaUsingBang` (`simpa ... using! e`) with its own elaborator that delegates to a shared core. This keeps the existing `simpa` syntax tree unchanged so stage0 keeps building. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…uniqueness `tacticDocUserName.lean` checks that user-facing tactics have unambiguous first tokens. Registering the new `simpaUsingBang` syntax as a `@[tactic_alt simpa]` groups it with the canonical `simpa` for documentation purposes and silences the ambiguity check. The own docstring is removed (the `simpa` docstring already covers `using!`) to satisfy the `linter.tactic.docsOnAlt` linter, which warns when an alternative has its own documentation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 12, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
May 12, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 12, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
May 12, 2026
…ause Adds parallel macro variants that accept a `simpaUsingBangArgsRest`, so `simpa? using! h`, `simpa! ... using! h`, and `simpa?! ... using! h` all parse correctly. Each variant is tagged `@[tactic_alt simpa]` to keep the first-token uniqueness check happy. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
May 12, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
May 12, 2026
mathlib-lean-pr-testing
Bot
added
builds-mathlib
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR makes
simpa using hclose at reducible transparency rather than the ambient (default/semireducible) transparency used previously, makingsimpa using hmore predictable under changes to the simp set. The previous behaviour is available assimpa using! h.The new
using!clause is introduced as a parallelsimpaUsingBangsyntax (registered as@[tactic_alt simpa]), so the existingsimpaAST is unchanged and stage0 keeps building.!here only affects the close-step match; it does not interact with the existingsimpa!prefix (auto-unfolding in the simp set, analogous tosimp!). The two modifiers can be combined:simpa! ... using! h.Motivated by Jovan's point (1) in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20code.20quality.3A.20simpa.
🤖 Prepared with Claude Code