feat: restrict simpa using h close to reducible transparency

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")

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₂ ≠ []) :

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

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