From e62206c3bb6b568709c414cc0bdcb7750aa05827 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 5 May 2026 13:43:49 +1000 Subject: [PATCH] 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