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
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 hrequire the simplifiedhand the simplified goal to match at reducible transparency, rather than at the ambient (default/semireducible) transparency used previously. This makessimpa using hmore predictable: it no longer succeeds via incidental β/δ-reduction at the closing step, so adding newsimplemmas is less likely to silently break unrelatedsimpacalls.The previous behaviour remains available via
simpa using! h— the!is attached to theusingclause, indicating that the close-step match should use the ambient transparency.!here is purely about close transparency; it does not interact with the existingsimpa!prefix (which enables auto-unfolding in the simp set, analogous tosimp!). Both modifiers can be combined:simpa! ... using! h.simpa ... using! eis introduced as a parallel syntax declaration (simpaUsingBang) so the existingsimpaAST is unchanged. This keeps the stage0 bootstrap intact — no files inInit/Stdneedusing!.The change wraps only the precondition
isDefEqcheck insideLean.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.This addresses Jovan's point (1) of the proposal in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20code.20quality.3A.20simpa, narrowing what
simpacan do without the broader behaviour change of also usinghas a simp lemma. The PR is branched fromnightly-with-mathlibso Mathlib breakage data can be gathered via the existing nightly-testing infrastructure.🤖 Prepared with Claude Code