From 659db85510b89fef59785e50ea1870e5683974f8 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 8 Apr 2026 10:21:23 +0200 Subject: [PATCH] fix: suggest `(rfl)` not `id rfl` in linter (#13319) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR amends #13317 to suggest `:= (rfl)` as the recommended way to avoid a theorem to be automatically marked `[defeq]`, for consistency with existing documentation. Rationale: the special treatment of `:= rfl` is based on syntax, not the proof term, so it’s appropriate to use different syntax. And also I like the way it reads like a “muted whisper of `rfl`”. --- src/Init/Data/Nat/Gcd.lean | 2 +- src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 4 ++-- tests/elab/simp_rfl_check_transparency.lean | 12 ++++++------ 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean index 487470c2fc..6b3ac409cc 100644 --- a/src/Init/Data/Nat/Gcd.lean +++ b/src/Init/Data/Nat/Gcd.lean @@ -60,7 +60,7 @@ theorem gcd_def (x y : Nat) : gcd x y = if x = 0 then y else gcd (y % x) x := by cases n with | zero => simp | succ n => - -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `id rfl` instead + -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `(rfl)` instead rw [gcd_succ] exact gcd_zero_left _ instance : Std.LawfulIdentity gcd 0 where diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index 301c6e263f..5b61095fc4 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean @@ -382,10 +382,10 @@ private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array forallTelescopeReducing type fun _ type => do let checkDefEq (lhs rhs : Expr) := do unless (← withTransparency .instances <| isDefEq lhs rhs) do - logWarning m!"`{origin.key}` is a `rfl` simp theorem, but its left-hand side{indentExpr lhs}\n\ + logWarning m!"`{origin.key}` is a `[defeq]` simp theorem, but its left-hand side{indentExpr lhs}\n\ is not definitionally equal to the right-hand side{indentExpr rhs}\n\ at `.instances` transparency. Possible solutions:\n\ - 1- use `id rfl` as the proof\n\ + 1- use `(rfl)` as the proof\n\ 2- mark constants occurring in the lhs and rhs as `[implicit_reducible]`" match_expr type with | Eq _ lhs rhs => checkDefEq lhs rhs diff --git a/tests/elab/simp_rfl_check_transparency.lean b/tests/elab/simp_rfl_check_transparency.lean index 1f3ba9013a..e92cbed3b9 100644 --- a/tests/elab/simp_rfl_check_transparency.lean +++ b/tests/elab/simp_rfl_check_transparency.lean @@ -5,19 +5,19 @@ def myId (n : Nat) : Nat := n -- LHS `myId n` and RHS `n` are only defeq if `myId` is unfolded (requires default transparency) /-- -warning: `myId_eq` is a `rfl` simp theorem, but its left-hand side +warning: `myId_eq` is a `[defeq]` simp theorem, but its left-hand side myId n is not definitionally equal to the right-hand side n at `.instances` transparency. Possible solutions: -1- use `id rfl` as the proof +1- use `(rfl)` as the proof 2- mark constants occurring in the lhs and rhs as `[implicit_reducible]` -/ #guard_msgs in @[simp] theorem myId_eq (n : Nat) : myId n = n := rfl #guard_msgs in -@[simp] theorem myId_eq' (n : Nat) : myId n = n := id rfl +@[simp] theorem myId_eq' (n : Nat) : myId n = n := (rfl) attribute [implicit_reducible] myId @@ -32,16 +32,16 @@ attribute [implicit_reducible] myId @[simp] theorem myId2_eq (n : Nat) : myId2 n = n := rfl /-- -warning: `add_zero` is a `rfl` simp theorem, but its left-hand side +warning: `add_zero` is a `[defeq]` simp theorem, but its left-hand side n + 0 is not definitionally equal to the right-hand side n at `.instances` transparency. Possible solutions: -1- use `id rfl` as the proof +1- use `(rfl)` as the proof 2- mark constants occurring in the lhs and rhs as `[implicit_reducible]` -/ #guard_msgs in @[simp] theorem add_zero (n : Nat) : n + 0 = n := rfl #guard_msgs in -@[simp] theorem add_zero' (n : Nat) : n + 0 = n := id rfl +@[simp] theorem add_zero' (n : Nat) : n + 0 = n := (rfl)