From e62206c3bb6b568709c414cc0bdcb7750aa05827 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 5 May 2026 13:43:49 +1000 Subject: [PATCH 1/5] feat: restrict `simpa using h` close to reducible transparency MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- src/Lean/Elab/Tactic/Simpa.lean | 26 +++++++++++++- tests/elab/getElemV.lean | 7 +++- tests/elab/scopeCacheProofs.lean | 7 ++++ tests/elab/simpa_reducible.lean | 58 ++++++++++++++++++++++++++++++++ 4 files changed, 96 insertions(+), 2 deletions(-) create mode 100644 tests/elab/simpa_reducible.lean diff --git a/src/Lean/Elab/Tactic/Simpa.lean b/src/Lean/Elab/Tactic/Simpa.lean index 81d08abf39eb..906d79b213db 100644 --- a/src/Lean/Elab/Tactic/Simpa.lean +++ b/src/Lean/Elab/Tactic/Simpa.lean @@ -21,6 +21,27 @@ register_option linter.unnecessarySimpa : Bool := { descr := "enable the 'unnecessary simpa' linter" } +/-- +Controls the transparency used for the final unification in `simpa using h`. + +When `true` (the default), the simplified `h` must match the simplified goal at +**reducible** transparency. This makes `simpa using h` more predictable: it no +longer succeeds via incidental β/δ-reduction, so adding new `simp` lemmas is +less likely to silently break unrelated `simpa` calls. + +Set to `false` to restore the previous behaviour, where the match was checked +at the ambient (default/semireducible) transparency. + +This option only affects the final `isDefEq` check of `simpa using h`. The +`simp` calls themselves, elaboration of the `using` term, and the +metavariable-assignment's internal type check are unaffected. +-/ +register_builtin_option backward.simpa.using.reducibleClose : Bool := { + defValue := true + descr := "if true (the default), `simpa using h` requires the simplified \ + `h` and goal to match at reducible transparency" +} + namespace Lean.Elab.Tactic.Simpa open Lean Parser.Tactic Elab Meta Term Tactic Simp Linter @@ -79,7 +100,10 @@ def getLinterUnnecessarySimpa (o : LinterOptions) : Bool := let h ← Term.elabTerm (mkIdent name) gType Term.synthesizeSyntheticMVarsNoPostponing let hType ← inferType h - unless (← withAssignableSyntheticOpaque <| isDefEq gType hType) do + let isCompatible : MetaM Bool := + withAssignableSyntheticOpaque <| isDefEq gType hType + let useReducible := backward.simpa.using.reducibleClose.get (← getOptions) + unless (← if useReducible then withReducible isCompatible else isCompatible) do -- `e` still is valid in this new local context Term.throwTypeMismatchError gType hType h (header? := some m!"Type mismatch: After simplification, term{indentExpr e}\n") diff --git a/tests/elab/getElemV.lean b/tests/elab/getElemV.lean index 0b67cb678808..ea75f1079bdc 100644 --- a/tests/elab/getElemV.lean +++ b/tests/elab/getElemV.lean @@ -559,7 +559,12 @@ theorem prefix_iff_getElemV [Nonempty α] {l₁ l₂ : List α} : theorem isEqv_eq_decide_getElemV {_ : Nonempty α} {as bs : List α} {r : α → α → Bool} : isEqv as bs r = if as.length = bs.length then decide (∀ (i : Nat), i < as.length → r as｢i｣ bs｢i｣) else false := by - -- Have to disable `Bool.if_false_right` because of spurious dependency + -- Have to disable `Bool.if_false_right` because of spurious dependency. + -- The `dite` in `isEqv_eq_decide`'s conclusion does not reduce to `ite` at + -- reducible transparency (`dite_eq_ite` requires the `fun _ => …` form + -- which simp cannot always normalize the hypothesis into), so we opt out + -- of the reducible-close behaviour here. + set_option backward.simpa.using.reducibleClose false in simpa [- Bool.if_false_right] using isEqv_eq_decide (as := as) (bs := bs) (r := r) theorem head_append_copy {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) : diff --git a/tests/elab/scopeCacheProofs.lean b/tests/elab/scopeCacheProofs.lean index 9390dd52131b..af5978861511 100644 --- a/tests/elab/scopeCacheProofs.lean +++ b/tests/elab/scopeCacheProofs.lean @@ -301,6 +301,13 @@ Key rewind properties are stated as separate lemmas. -/ namespace Proofs +-- Several `simpa using h` calls below close their goal by unfolding the +-- semireducible definitions `Imp.EntryOrdered` and `GensConsistent` (both +-- abbreviations for `List.Pairwise …`). The new default of +-- `backward.simpa.using.reducibleClose` would reject this; opt out for the +-- whole namespace. +set_option backward.simpa.using.reducibleClose false + /-! ### Rewind helper lemmas These lemmas capture the essential properties of the `rewind` function needed diff --git a/tests/elab/simpa_reducible.lean b/tests/elab/simpa_reducible.lean new file mode 100644 index 000000000000..72d6a00e60bb --- /dev/null +++ b/tests/elab/simpa_reducible.lean @@ -0,0 +1,58 @@ +/-! +# `simpa using h` final unification at reducible transparency + +`simpa using h` checks that the simplified `h` matches the simplified goal at +**reducible** transparency. Semireducible definitions do not unfold during +this check. + +The previous behaviour can be restored with +`set_option backward.simpa.using.reducibleClose false`. +-/ + +def foo : Nat := 37 + +/-! +With the new default, `foo` is not unfolded during the close, so this fails. +-/ +/-- +error: Type mismatch: After simplification, term + h + has type + @Eq Nat foo n +but is expected to have type + @Eq Nat 37 n +-/ +#guard_msgs in +example (n : Nat) (h : foo = n) : 37 = n := by + simpa using h + +/-! +With the option turned off, the previous semireducible behaviour is restored +and `foo` reduces to `37` during the close. +-/ +set_option backward.simpa.using.reducibleClose false in +example (n : Nat) (h : foo = n) : 37 = n := by + simpa using h + +/-! +Reducible definitions still unfold during the close under the new default. +-/ +@[reducible] def fooR : Nat := 37 + +example (n : Nat) (h : fooR = n) : 37 = n := by + simpa using h + +/-! +`simpa` without `using` is unaffected — the option only gates the final +unification of the `using`-clause term against the simplified goal. +-/ +example (n : Nat) (h : n = n) : n = n := by + simpa + +/-! +Simplification itself is unaffected: `simp` may freely rewrite the goal and +the `using` term; the reducible check applies only to the post-simplification +match. +-/ +example (n m : Nat) (h : n + 0 = m) : n = m := by + simpa using h From 11336d3c6203c02efca80fea9bf76271682f300f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 12 May 2026 12:04:51 +1000 Subject: [PATCH 2/5] refactor: gate `simpa using h` permissive close on `!` instead of a backward 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) --- src/Init/Tactics.lean | 8 ++++++++ src/Lean/Elab/Tactic/Simpa.lean | 27 +++++---------------------- tests/elab/getElemV.lean | 7 +++---- tests/elab/scopeCacheProofs.lean | 21 ++++++++++----------- tests/elab/simpa_reducible.lean | 19 +++++++++---------- 5 files changed, 35 insertions(+), 47 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index bc6a40bde0aa..79aedb1c88a3 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -761,9 +761,17 @@ This is a "finishing" tactic modification of `simp`. It has two forms. (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set. + The final match between the simplified `e` and the simplified goal uses + **reducible** transparency, so it does not unfold semireducible definitions. + Use `simpa! ... using e` to perform the match at the ambient + (default/semireducible) transparency. + * `simpa [rules, ⋯]` will simplify the goal and the type of a hypothesis `this` if present in the context, then try to close the goal using the `assumption` tactic. + +As with `simp`, the `!` modifier also enables auto-unfolding of definitions +in the simp set. -/ syntax (name := simpa) "simpa" "?"? "!"? simpaArgsRest : tactic diff --git a/src/Lean/Elab/Tactic/Simpa.lean b/src/Lean/Elab/Tactic/Simpa.lean index 906d79b213db..cdad8674b8ae 100644 --- a/src/Lean/Elab/Tactic/Simpa.lean +++ b/src/Lean/Elab/Tactic/Simpa.lean @@ -21,27 +21,6 @@ register_option linter.unnecessarySimpa : Bool := { descr := "enable the 'unnecessary simpa' linter" } -/-- -Controls the transparency used for the final unification in `simpa using h`. - -When `true` (the default), the simplified `h` must match the simplified goal at -**reducible** transparency. This makes `simpa using h` more predictable: it no -longer succeeds via incidental β/δ-reduction, so adding new `simp` lemmas is -less likely to silently break unrelated `simpa` calls. - -Set to `false` to restore the previous behaviour, where the match was checked -at the ambient (default/semireducible) transparency. - -This option only affects the final `isDefEq` check of `simpa using h`. The -`simp` calls themselves, elaboration of the `using` term, and the -metavariable-assignment's internal type check are unaffected. --/ -register_builtin_option backward.simpa.using.reducibleClose : Bool := { - defValue := true - descr := "if true (the default), `simpa using h` requires the simplified \ - `h` and goal to match at reducible transparency" -} - namespace Lean.Elab.Tactic.Simpa open Lean Parser.Tactic Elab Meta Term Tactic Simp Linter @@ -102,7 +81,11 @@ def getLinterUnnecessarySimpa (o : LinterOptions) : Bool := let hType ← inferType h let isCompatible : MetaM Bool := withAssignableSyntheticOpaque <| isDefEq gType hType - let useReducible := backward.simpa.using.reducibleClose.get (← getOptions) + -- `simpa` (default) requires the simplified `h` and goal to match at + -- reducible transparency, making `simpa using h` more predictable. + -- `simpa!` opts into the previous behaviour, matching at the ambient + -- (default/semireducible) transparency. + let useReducible := unfold.isNone unless (← if useReducible then withReducible isCompatible else isCompatible) do -- `e` still is valid in this new local context Term.throwTypeMismatchError gType hType h diff --git a/tests/elab/getElemV.lean b/tests/elab/getElemV.lean index ea75f1079bdc..fcb8d3952db7 100644 --- a/tests/elab/getElemV.lean +++ b/tests/elab/getElemV.lean @@ -562,10 +562,9 @@ theorem isEqv_eq_decide_getElemV {_ : Nonempty α} {as bs : List α} {r : α → -- Have to disable `Bool.if_false_right` because of spurious dependency. -- The `dite` in `isEqv_eq_decide`'s conclusion does not reduce to `ite` at -- reducible transparency (`dite_eq_ite` requires the `fun _ => …` form - -- which simp cannot always normalize the hypothesis into), so we opt out - -- of the reducible-close behaviour here. - set_option backward.simpa.using.reducibleClose false in - simpa [- Bool.if_false_right] using isEqv_eq_decide (as := as) (bs := bs) (r := r) + -- which simp cannot always normalize the hypothesis into), so we use + -- `simpa!` to close at default transparency here. + simpa! [- Bool.if_false_right] using isEqv_eq_decide (as := as) (bs := bs) (r := r) theorem head_append_copy {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) : head (l₁ ++ l₂) w = diff --git a/tests/elab/scopeCacheProofs.lean b/tests/elab/scopeCacheProofs.lean index af5978861511..cd13efde98c3 100644 --- a/tests/elab/scopeCacheProofs.lean +++ b/tests/elab/scopeCacheProofs.lean @@ -303,10 +303,9 @@ namespace Proofs -- Several `simpa using h` calls below close their goal by unfolding the -- semireducible definitions `Imp.EntryOrdered` and `GensConsistent` (both --- abbreviations for `List.Pairwise …`). The new default of --- `backward.simpa.using.reducibleClose` would reject this; opt out for the --- whole namespace. -set_option backward.simpa.using.reducibleClose false +-- abbreviations for `List.Pairwise …`). The default `simpa` close at reducible +-- transparency would reject this, so these sites use `simpa!` to opt into the +-- permissive default-transparency close. /-! ### Rewind helper lemmas @@ -351,7 +350,7 @@ theorem findValidLevel_skip_fresh (eGens cGens : Imp.GenList) (n g resultScope : simp [Imp.findValidLevel] | cons v vs => -- eGens = v :: vs, head? = some v, tail = vs - have hvg : v < g := by have := hFreshHead 0 (by simp); simpa using this + have hvg : v < g := by have := hFreshHead 0 (by simp); simpa! using this rw [Imp.findValidLevel] simp [show (v == g) = false from by simp [Nat.ne_of_lt hvg], show ¬(n + 1 ≤ resultScope) from Nat.not_le.mpr (Nat.lt_succ_of_le hRS)] @@ -711,7 +710,7 @@ theorem rewind_entryOrdered {entries : List Imp.Entry} {n : Nat} {gens : Imp.Gen (Imp.rewind.go n gens revEntries acc).Pairwise (fun a b => a.scopeLevel < b.resultScope) by exact this entries.reverse [] - (by simpa using hOrd) List.Pairwise.nil + (by simpa! using hOrd) List.Pairwise.nil intro revEntries acc hAll hAcc induction revEntries generalizing acc with | nil => simpa [Imp.rewind.go] @@ -986,7 +985,7 @@ theorem fvl_pop_entry (e : Imp.Entry) (n : Nat) (gens : Imp.GenList) simp only [show ¬(n ≤ n - 1) from by omega, ↓reduceIte, show min n (n - 1) = n - 1 from Nat.min_eq_right (Nat.pred_le n)] -- By gensSuffix: e.scopeGens.drop(sl-n) = gens, so v :: vs = w :: ws - have hveq : v = w := by simpa using heq + have hveq : v = w := by simpa! using heq have hi : e.scopeLevel - n < e.scopeGens.length := by have : (e.scopeGens.drop (e.scopeLevel - n)).length > 0 := by rw [hvvs]; simp simp [List.length_drop] at this; omega @@ -1141,9 +1140,9 @@ theorem rewind_pop_equiv (entries : List Imp.Entry) (n : Nat) (gens : Imp.GenLis exact this entries.reverse [] [] (fun e he => List.mem_reverse.mp he) (fun e he => hRSSL e (List.mem_reverse.mp he)) - (by simpa using hOrd) + (by simpa! using hOrd) (fun e he => hGensSuffix e (List.mem_reverse.mp he)) - (by simpa using hGC) + (by simpa! using hGC) (by simp) intro revEntries acc1 acc2 hMem hRSSLrev hOrdRev hGSrev hGCrev hAccEq induction revEntries generalizing acc1 acc2 with @@ -1568,8 +1567,8 @@ private theorem rewind_gens_aligned e.scopeGens = gens.drop (n - e.scopeLevel) by exact this entries.reverse [] (fun e he => List.mem_reverse.mp he) - (by simpa using hGC) - (by simpa using hOrd) + (by simpa! using hGC) + (by simpa! using hOrd) (by simp) intro revEntries acc hMem hGCrev hOrdRev hAccAligned induction revEntries generalizing acc with diff --git a/tests/elab/simpa_reducible.lean b/tests/elab/simpa_reducible.lean index 72d6a00e60bb..e809318476c0 100644 --- a/tests/elab/simpa_reducible.lean +++ b/tests/elab/simpa_reducible.lean @@ -5,14 +5,14 @@ **reducible** transparency. Semireducible definitions do not unfold during this check. -The previous behaviour can be restored with -`set_option backward.simpa.using.reducibleClose false`. +`simpa! using h` performs the match at the ambient (default/semireducible) +transparency, recovering the previous behaviour. -/ def foo : Nat := 37 /-! -With the new default, `foo` is not unfolded during the close, so this fails. +With the default, `foo` is not unfolded during the close, so this fails. -/ /-- error: Type mismatch: After simplification, term @@ -27,15 +27,14 @@ example (n : Nat) (h : foo = n) : 37 = n := by simpa using h /-! -With the option turned off, the previous semireducible behaviour is restored -and `foo` reduces to `37` during the close. +With `simpa!`, the previous semireducible behaviour is used and +`foo` reduces to `37` during the close. -/ -set_option backward.simpa.using.reducibleClose false in example (n : Nat) (h : foo = n) : 37 = n := by - simpa using h + simpa! using h /-! -Reducible definitions still unfold during the close under the new default. +Reducible definitions still unfold during the close under the default. -/ @[reducible] def fooR : Nat := 37 @@ -43,8 +42,8 @@ example (n : Nat) (h : fooR = n) : 37 = n := by simpa using h /-! -`simpa` without `using` is unaffected — the option only gates the final -unification of the `using`-clause term against the simplified goal. +`simpa` without `using` is unaffected — the transparency choice only gates +the final unification of the `using`-clause term against the simplified goal. -/ example (n : Nat) (h : n = n) : n = n := by simpa From 8105849eea397b3de254c33b514e14d0629a288f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 12 May 2026 13:51:22 +1000 Subject: [PATCH 3/5] refactor: switch from `simpa!` to `simpa ... using!` for permissive close 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) --- src/Init/Tactics.lean | 14 ++++++++---- src/Lean/Elab/Tactic/Simpa.lean | 37 +++++++++++++++++++++++--------- tests/elab/getElemV.lean | 4 ++-- tests/elab/scopeCacheProofs.lean | 18 ++++++++-------- tests/elab/simpa_reducible.lean | 6 +++--- 5 files changed, 51 insertions(+), 28 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 79aedb1c88a3..e1d08653531a 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -763,18 +763,24 @@ This is a "finishing" tactic modification of `simp`. It has two forms. The final match between the simplified `e` and the simplified goal uses **reducible** transparency, so it does not unfold semireducible definitions. - Use `simpa! ... using e` to perform the match at the ambient - (default/semireducible) transparency. + Write `simpa [rules, ⋯] using! e` to perform the match at the ambient + (default/semireducible) transparency instead. * `simpa [rules, ⋯]` will simplify the goal and the type of a hypothesis `this` if present in the context, then try to close the goal using the `assumption` tactic. -As with `simp`, the `!` modifier also enables auto-unfolding of definitions -in the simp set. +As with `simp`, the `!` modifier before `simpa` enables auto-unfolding of +definitions in the simp set. -/ syntax (name := simpa) "simpa" "?"? "!"? simpaArgsRest : tactic +/-- Variant of `simpa` whose `using!` clause performs the final match at the +ambient (default/semireducible) transparency, instead of the default reducible +transparency used by `simpa ... using`. -/ +syntax (name := simpaUsingBang) + "simpa" "?"? "!"? optConfig (discharger)? &" only "? (simpArgs)? " using! " term : tactic + @[inherit_doc simpa] macro "simpa!" rest:simpaArgsRest : tactic => `(tactic| simpa ! $rest:simpaArgsRest) diff --git a/src/Lean/Elab/Tactic/Simpa.lean b/src/Lean/Elab/Tactic/Simpa.lean index cdad8674b8ae..dabd682b579b 100644 --- a/src/Lean/Elab/Tactic/Simpa.lean +++ b/src/Lean/Elab/Tactic/Simpa.lean @@ -29,7 +29,13 @@ open Lean Parser.Tactic Elab Meta Term Tactic Simp Linter def getLinterUnnecessarySimpa (o : LinterOptions) : Bool := getLinterValue linter.unnecessarySimpa o -@[builtin_tactic Lean.Parser.Tactic.simpa] def evalSimpa : Tactic := fun stx => do +/-- +Core implementation of the `simpa` tactic, parameterized by whether the final +unification of the simplified `using` term against the simplified goal should +be performed at reducible transparency (`useReducible := true`) or at the +ambient (default/semireducible) transparency (`useReducible := false`). +-/ +private def evalSimpaCore (useReducible : Bool) : Tactic := fun stx => do match stx with | `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using%$usingTk? $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do @@ -81,11 +87,6 @@ def getLinterUnnecessarySimpa (o : LinterOptions) : Bool := let hType ← inferType h let isCompatible : MetaM Bool := withAssignableSyntheticOpaque <| isDefEq gType hType - -- `simpa` (default) requires the simplified `h` and goal to match at - -- reducible transparency, making `simpa using h` more predictable. - -- `simpa!` opts into the previous behaviour, matching at the ambient - -- (default/semireducible) transparency. - let useReducible := unfold.isNone unless (← if useReducible then withReducible isCompatible else isCompatible) do -- `e` still is valid in this new local context Term.throwTypeMismatchError gType hType h @@ -116,13 +117,29 @@ def getLinterUnnecessarySimpa (o : LinterOptions) : Bool := let usingArg : Option Term := usingArg.map (⟨·.raw.unsetTrailing⟩) let stx ← match ← mkSimpOnly stx.raw.unsetTrailing stats.usedTheorems with | `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?) => - if unfold.isSome then - `(tactic| simpa! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?) - else - `(tactic| simpa $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?) + match unfold.isSome, useReducible, usingArg with + | true, true, _ => `(tactic| simpa! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?) + | false, true, _ => `(tactic| simpa $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?) + | true, false, some ua => `(tactic| simpa ! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? using! $ua) + | false, false, some ua => `(tactic| simpa $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? using! $ua) + | _, false, none => unreachable! -- `using!` requires a term | _ => unreachable! TryThis.addSuggestion tk stx (origSpan? := ← getRef) return stats.diag | _ => throwUnsupportedSyntax +@[builtin_tactic Lean.Parser.Tactic.simpa] def evalSimpa : Tactic := + evalSimpaCore (useReducible := true) + +@[builtin_tactic Lean.Parser.Tactic.simpaUsingBang] def evalSimpaUsingBang : Tactic := fun stx => do + -- The `simpa ... using! e` syntax is identical to `simpa ... using e` except for + -- the trailing `using!` vs `using`. Rewrite to the `simpa` shape and dispatch. + match stx with + | `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $cfg:optConfig $(disch)? $[only%$only]? + $[[$args,*]]? using! $usingArg) => do + let stx' ← `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $cfg:optConfig $(disch)? $[only%$only]? + $[[$args,*]]? using $usingArg) + evalSimpaCore (useReducible := false) stx' + | _ => throwUnsupportedSyntax + end Lean.Elab.Tactic.Simpa diff --git a/tests/elab/getElemV.lean b/tests/elab/getElemV.lean index fcb8d3952db7..9dd04c2486e2 100644 --- a/tests/elab/getElemV.lean +++ b/tests/elab/getElemV.lean @@ -563,8 +563,8 @@ theorem isEqv_eq_decide_getElemV {_ : Nonempty α} {as bs : List α} {r : α → -- The `dite` in `isEqv_eq_decide`'s conclusion does not reduce to `ite` at -- reducible transparency (`dite_eq_ite` requires the `fun _ => …` form -- which simp cannot always normalize the hypothesis into), so we use - -- `simpa!` to close at default transparency here. - simpa! [- Bool.if_false_right] using isEqv_eq_decide (as := as) (bs := bs) (r := r) + -- `simpa ... using!` to close at default transparency here. + simpa [- Bool.if_false_right] using! isEqv_eq_decide (as := as) (bs := bs) (r := r) theorem head_append_copy {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) : head (l₁ ++ l₂) w = diff --git a/tests/elab/scopeCacheProofs.lean b/tests/elab/scopeCacheProofs.lean index cd13efde98c3..9ff0956bda9e 100644 --- a/tests/elab/scopeCacheProofs.lean +++ b/tests/elab/scopeCacheProofs.lean @@ -304,8 +304,8 @@ namespace Proofs -- Several `simpa using h` calls below close their goal by unfolding the -- semireducible definitions `Imp.EntryOrdered` and `GensConsistent` (both -- abbreviations for `List.Pairwise …`). The default `simpa` close at reducible --- transparency would reject this, so these sites use `simpa!` to opt into the --- permissive default-transparency close. +-- transparency would reject this, so these sites use `simpa using!` to opt +-- into the permissive default-transparency close. /-! ### Rewind helper lemmas @@ -350,7 +350,7 @@ theorem findValidLevel_skip_fresh (eGens cGens : Imp.GenList) (n g resultScope : simp [Imp.findValidLevel] | cons v vs => -- eGens = v :: vs, head? = some v, tail = vs - have hvg : v < g := by have := hFreshHead 0 (by simp); simpa! using this + have hvg : v < g := by have := hFreshHead 0 (by simp); simpa using! this rw [Imp.findValidLevel] simp [show (v == g) = false from by simp [Nat.ne_of_lt hvg], show ¬(n + 1 ≤ resultScope) from Nat.not_le.mpr (Nat.lt_succ_of_le hRS)] @@ -710,7 +710,7 @@ theorem rewind_entryOrdered {entries : List Imp.Entry} {n : Nat} {gens : Imp.Gen (Imp.rewind.go n gens revEntries acc).Pairwise (fun a b => a.scopeLevel < b.resultScope) by exact this entries.reverse [] - (by simpa! using hOrd) List.Pairwise.nil + (by simpa using! hOrd) List.Pairwise.nil intro revEntries acc hAll hAcc induction revEntries generalizing acc with | nil => simpa [Imp.rewind.go] @@ -985,7 +985,7 @@ theorem fvl_pop_entry (e : Imp.Entry) (n : Nat) (gens : Imp.GenList) simp only [show ¬(n ≤ n - 1) from by omega, ↓reduceIte, show min n (n - 1) = n - 1 from Nat.min_eq_right (Nat.pred_le n)] -- By gensSuffix: e.scopeGens.drop(sl-n) = gens, so v :: vs = w :: ws - have hveq : v = w := by simpa! using heq + have hveq : v = w := by simpa using! heq have hi : e.scopeLevel - n < e.scopeGens.length := by have : (e.scopeGens.drop (e.scopeLevel - n)).length > 0 := by rw [hvvs]; simp simp [List.length_drop] at this; omega @@ -1140,9 +1140,9 @@ theorem rewind_pop_equiv (entries : List Imp.Entry) (n : Nat) (gens : Imp.GenLis exact this entries.reverse [] [] (fun e he => List.mem_reverse.mp he) (fun e he => hRSSL e (List.mem_reverse.mp he)) - (by simpa! using hOrd) + (by simpa using! hOrd) (fun e he => hGensSuffix e (List.mem_reverse.mp he)) - (by simpa! using hGC) + (by simpa using! hGC) (by simp) intro revEntries acc1 acc2 hMem hRSSLrev hOrdRev hGSrev hGCrev hAccEq induction revEntries generalizing acc1 acc2 with @@ -1567,8 +1567,8 @@ private theorem rewind_gens_aligned e.scopeGens = gens.drop (n - e.scopeLevel) by exact this entries.reverse [] (fun e he => List.mem_reverse.mp he) - (by simpa! using hGC) - (by simpa! using hOrd) + (by simpa using! hGC) + (by simpa using! hOrd) (by simp) intro revEntries acc hMem hGCrev hOrdRev hAccAligned induction revEntries generalizing acc with diff --git a/tests/elab/simpa_reducible.lean b/tests/elab/simpa_reducible.lean index e809318476c0..27e6b9a0b08b 100644 --- a/tests/elab/simpa_reducible.lean +++ b/tests/elab/simpa_reducible.lean @@ -5,7 +5,7 @@ **reducible** transparency. Semireducible definitions do not unfold during this check. -`simpa! using h` performs the match at the ambient (default/semireducible) +`simpa using! h` performs the match at the ambient (default/semireducible) transparency, recovering the previous behaviour. -/ @@ -27,11 +27,11 @@ example (n : Nat) (h : foo = n) : 37 = n := by simpa using h /-! -With `simpa!`, the previous semireducible behaviour is used and +With `simpa using!`, the previous semireducible behaviour is used and `foo` reduces to `37` during the close. -/ example (n : Nat) (h : foo = n) : 37 = n := by - simpa! using h + simpa using! h /-! Reducible definitions still unfold during the close under the default. From 2bcfa08d6a9674500b219446b3531121c678946d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 12 May 2026 14:35:34 +1000 Subject: [PATCH 4/5] fix: mark `simpaUsingBang` as alternative of `simpa` for first-token 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) --- src/Init/Tactics.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index e1d08653531a..4e225647f1a8 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -775,9 +775,7 @@ definitions in the simp set. -/ syntax (name := simpa) "simpa" "?"? "!"? simpaArgsRest : tactic -/-- Variant of `simpa` whose `using!` clause performs the final match at the -ambient (default/semireducible) transparency, instead of the default reducible -transparency used by `simpa ... using`. -/ +@[tactic_alt simpa] syntax (name := simpaUsingBang) "simpa" "?"? "!"? optConfig (discharger)? &" only "? (simpArgs)? " using! " term : tactic From 6b86220b075db4cfeb17b9a1ce476e3653385c25 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 12 May 2026 17:01:13 +1000 Subject: [PATCH 5/5] feat: extend `simpa?`/`simpa!`/`simpa?!` macros to accept `using!` clause 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) --- src/Init/Tactics.lean | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 4e225647f1a8..9bab76c85b92 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -775,9 +775,13 @@ definitions in the simp set. -/ syntax (name := simpa) "simpa" "?"? "!"? simpaArgsRest : tactic +/-- The arguments to `simpa ... using! e` — like `simpaArgsRest`, but with a +mandatory `using!` clause selecting the permissive default-transparency close. -/ +syntax simpaUsingBangArgsRest := + optConfig (discharger)? &" only "? (simpArgs)? " using! " term + @[tactic_alt simpa] -syntax (name := simpaUsingBang) - "simpa" "?"? "!"? optConfig (discharger)? &" only "? (simpArgs)? " using! " term : tactic +syntax (name := simpaUsingBang) "simpa" "?"? "!"? simpaUsingBangArgsRest : tactic @[inherit_doc simpa] macro "simpa!" rest:simpaArgsRest : tactic => `(tactic| simpa ! $rest:simpaArgsRest) @@ -788,6 +792,18 @@ syntax (name := simpaUsingBang) @[inherit_doc simpa] macro "simpa?!" rest:simpaArgsRest : tactic => `(tactic| simpa ?! $rest:simpaArgsRest) +@[inherit_doc simpa, tactic_alt simpa] +macro "simpa!" rest:simpaUsingBangArgsRest : tactic => + `(tactic| simpa ! $rest:simpaUsingBangArgsRest) + +@[inherit_doc simpa, tactic_alt simpa] +macro "simpa?" rest:simpaUsingBangArgsRest : tactic => + `(tactic| simpa ? $rest:simpaUsingBangArgsRest) + +@[inherit_doc simpa, tactic_alt simpa] +macro "simpa?!" rest:simpaUsingBangArgsRest : tactic => + `(tactic| simpa ?! $rest:simpaUsingBangArgsRest) + /-- `delta id1 id2 ...` delta-expands the definitions `id1`, `id2`, .... This is a low-level tactic, it will expose how recursive definitions have been