feat: restrict simpa using h close to reducible transparency

src/Init/Tactics.lean

@@ -761,12 +761,28 @@ 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.
+  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 before `simpa` enables auto-unfolding of
+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" "?"? "!"? simpaUsingBangArgsRest : tactic
+
 @[inherit_doc simpa] macro "simpa!" rest:simpaArgsRest : tactic =>
   `(tactic| simpa ! $rest:simpaArgsRest)
 
@@ -776,6 +792,18 @@ syntax (name := simpa) "simpa" "?"? "!"? simpaArgsRest : tactic
 @[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

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
@@ -79,7 +85,9 @@ 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
+                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")
@@ -109,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

tests/elab/getElemV.lean

@@ -559,8 +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
-  simpa [- Bool.if_false_right] using isEqv_eq_decide (as := as) (bs := bs) (r := 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 use
+  -- `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 =

tests/elab/scopeCacheProofs.lean

@@ -301,6 +301,12 @@ 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 default `simpa` close at reducible
+-- transparency would reject this, so these sites use `simpa using!` to opt
+-- into the permissive default-transparency close.
+
 /-! ### Rewind helper lemmas
 
 These lemmas capture the essential properties of the `rewind` function needed
@@ -344,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)]
@@ -704,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]
@@ -979,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
@@ -1134,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
@@ -1561,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

tests/elab/simpa_reducible.lean

@@ -0,0 +1,57 @@
+/-!
+# `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.
+
+`simpa using! h` performs the match at the ambient (default/semireducible)
+transparency, recovering the previous behaviour.
+-/
+
+def foo : Nat := 37
+
+/-!
+With the 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 `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
+
+/-!
+Reducible definitions still unfold during the close under the default.
+-/
+@[reducible] def fooR : Nat := 37
+
+example (n : Nat) (h : fooR = n) : 37 = n := by
+  simpa using h
+
+/-!
+`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
+
+/-!
+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