feat: simps support additional simp-attributes (#2398)

* Also fix the configuration option `Simps.Config.lemmasOnly` and use it in the library
* Also use `@[simps!]` in the test file
* Also remove the temporary configuration in `LocalHomeomorph`
* [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/print.20simp.20set)
* Fixes #2350

Mathlib/Algebra/Algebra/Equiv.lean

@@ -643,7 +643,7 @@ def ofRingEquiv {f : A₁ ≃+* A₂} (hf : ∀ x, f (algebraMap R A₁ x) = alg
 end OfRingEquiv
 
 -- Porting note: projections mul & one not found, removed [simps] and added theorems manually
--- @[simps (config := { attrs := [] }) one]
+-- @[simps (config := .lemmasOnly) one]
 instance aut : Group (A₁ ≃ₐ[R] A₁) where
   mul ϕ ψ := ψ.trans ϕ
   mul_assoc ϕ ψ χ := rfl

Mathlib/Algebra/Algebra/Hom.lean

@@ -430,7 +430,7 @@ theorem map_list_prod (s : List A) : φ s.prod = (s.map φ).prod :=
   φ.toRingHom.map_list_prod s
 #align alg_hom.map_list_prod AlgHom.map_list_prod
 
-@[simps (config := { attrs := [] }) toSemigroup_toMul_mul toOne_one]
+@[simps (config := .lemmasOnly) toSemigroup_toMul_mul toOne_one]
 instance End : Monoid (A →ₐ[R] A) where
   mul := comp
   mul_assoc ϕ ψ χ := rfl

Mathlib/Algebra/Invertible.lean

@@ -412,7 +412,7 @@ theorem map_invOf {R : Type _} {S : Type _} {F : Type _} [MulOneClass R] [Monoid
   then `r : R` is invertible if `f r` is.
 
 The inverse is computed as `g (⅟(f r))` -/
-@[simps! (config := { attrs := [] })]
+@[simps! (config := .lemmasOnly)]
 def Invertible.ofLeftInverse {R : Type _} {S : Type _} {G : Type _} [MulOneClass R] [MulOneClass S]
     [MonoidHomClass G S R] (f : R → S) (g : G) (r : R) (h : Function.LeftInverse g f)
     [Invertible (f r)] : Invertible r :=

Mathlib/CategoryTheory/FinCategory.lean

@@ -77,8 +77,7 @@ abbrev AsType : Type :=
   Fin (Fintype.card α)
 #align category_theory.fin_category.as_type CategoryTheory.FinCategory.AsType
 
--- Porting note: The `lemmasOnly` simps configuration changed to `{ attrs := [] }`.
-@[simps (config := { attrs := [] }) Hom id comp]
+@[simps (config := .lemmasOnly) Hom id comp]
 noncomputable instance categoryAsType : SmallCategory (AsType α)
     where
   Hom i j := Fin (Fintype.card (@Quiver.Hom (ObjAsType α) _ i j))

Mathlib/Logic/Equiv/LocalEquiv.lean

@@ -94,7 +94,7 @@ attribute [mfld_simps]
 
 /-- Common `@[simps]` configuration options used for manifold-related declarations. -/
 def mfld_cfg : Simps.Config where
-  attrs := [`simp, `mfld_simps]
+  attrs := [`mfld_simps]
   fullyApplied := false
 #align mfld_cfg mfld_cfg
 

Mathlib/Tactic/Simps/Basic.lean

@@ -55,7 +55,6 @@ There are some small changes in the attribute. None of them should have great ef
   a lemma with that name (in Lean 3 it would generate a different unique name)
 * `transparency.none` has been replaced by `TransparencyMode.reducible`
 * The `attr` configuration option has been split into `isSimp` and `attrs` (for extra attributes)
-  (todo)
 * Because Lean 4 uses bundled structures, this means that `simps` applied to anything that
   implements a notation class will almost certainly require a user-provided custom simps projection.
 
@@ -793,7 +792,8 @@ register_option linter.simpsNoConstructor : Bool := {
 structure Config where
   /-- Make generated lemmas simp lemmas -/
   isSimp := true
-  /-- [TODO] Other attributes to apply to generated lemmas -/
+  /-- Other simp-attributes to apply to generated lemmas.
+  Attributes that are currently not simp-attributes are not supported. -/
   attrs : List Name := []
   /-- simplify the right-hand side of generated simp-lemmas using `dsimp, simp`. -/
   simpRhs := false
@@ -817,13 +817,14 @@ structure Config where
 declare_config_elab elabSimpsConfig Config
 
 /-- A common configuration for `@[simps]`: generate equalities between functions instead equalities
-  between fully applied Expressions. -/
-def Config.asFn : Config where
+  between fully applied Expressions. Use this using `@[simps (config := .asFn)]`. -/
+def Config.asFn : Simps.Config where
   fullyApplied := false
 
-/-- A common configuration for `@[simps]`: don't tag the generated lemmas with `@[simp]`. -/
+/-- A common configuration for `@[simps]`: don't tag the generated lemmas with `@[simp]`.
+  Use this using `@[simps (config := .lemmasOnly)]`. -/
 def Config.lemmasOnly : Config where
-  attrs := []
+  isSimp := false
 
 /-- `instantiateLambdasOrApps es e` instantiates lambdas in `e` by expressions from `es`.
 If the length of `es` is larger than the number of lambdas in `e`,
@@ -922,7 +923,10 @@ def addProjection (declName : Name) (type lhs rhs : Expr) (args : Array Expr)
     ← mkConstWithLevelParams declName
   if cfg.isSimp then
     addSimpTheorem simpExtension declName true false .global <| eval_prio default
-  -- cfg.attrs.mapM fun nm ↦ setAttribute nm declName tt -- todo: deal with attributes
+  _ ← cfg.attrs.mapM fun simpAttr ↦ do
+    let .some simpDecl ← getSimpExtension? simpAttr |
+      throwError "{simpAttr} is not a simp-attribute."
+    addSimpTheorem simpDecl declName true false .global <| eval_prio default
 
 /--
 Perform head-structure-eta-reduction on expression `e`. That is, if `e` is of the form

Mathlib/Topology/LocalHomeomorph.lean

@@ -198,7 +198,7 @@ protected theorem surjOn : SurjOn e e.source e.target :=
 #align local_homeomorph.surj_on LocalHomeomorph.surjOn
 
 /-- A homeomorphism induces a local homeomorphism on the whole space -/
-@[simps! (config := { mfld_cfg with simpRhs := true })]
+@[simps! (config := mfld_cfg)]
 def _root_.Homeomorph.toLocalHomeomorph (e : α ≃ₜ β) : LocalHomeomorph α β where
   toLocalEquiv := e.toEquiv.toLocalEquiv
   open_source := isOpen_univ
@@ -207,10 +207,6 @@ def _root_.Homeomorph.toLocalHomeomorph (e : α ≃ₜ β) : LocalHomeomorph α
   continuous_invFun := e.symm.continuous.continuousOn
 #align homeomorph.to_local_homeomorph Homeomorph.toLocalHomeomorph
 
--- porting note: todo: see #2350
-attribute [mfld_simps] Homeomorph.toLocalHomeomorph_apply Homeomorph.toLocalHomeomorph_symm_apply
-  Homeomorph.toLocalHomeomorph_source Homeomorph.toLocalHomeomorph_target
-
 /-- Replace `toLocalEquiv` field to provide better definitional equalities. -/
 def replaceEquiv (e : LocalHomeomorph α β) (e' : LocalEquiv α β) (h : e.toLocalEquiv = e') :
     LocalHomeomorph α β where
@@ -701,14 +697,11 @@ theorem restrOpen_source (s : Set α) (hs : IsOpen s) : (e.restrOpen s hs).sourc
 sure that the restriction is well defined whatever the set s, since local homeomorphisms are by
 definition defined on open sets. In applications where `s` is open, this coincides with the
 restriction of local equivalences -/
-@[simps! (config := mfld_cfg) apply symm_apply, simps! (config := { attrs := [] }) source target]
+@[simps! (config := mfld_cfg) apply symm_apply, simps! (config := .lemmasOnly) source target]
 protected def restr (s : Set α) : LocalHomeomorph α β :=
   e.restrOpen (interior s) isOpen_interior
 #align local_homeomorph.restr LocalHomeomorph.restr
 
--- porting note: todo: see #2350
-attribute [mfld_simps] restr_apply restr_symm_apply
-
 @[simp, mfld_simps]
 theorem restr_toLocalEquiv (s : Set α) :
     (e.restr s).toLocalEquiv = e.toLocalEquiv.restr (interior s) :=
@@ -740,14 +733,11 @@ theorem restr_source_inter (s : Set α) : e.restr (e.source ∩ s) = e.restr s :
 #align local_homeomorph.restr_source_inter LocalHomeomorph.restr_source_inter
 
 /-- The identity on the whole space as a local homeomorphism. -/
-@[simps! (config := mfld_cfg) apply, simps! (config := { attrs := [] }) source target]
+@[simps! (config := mfld_cfg) apply, simps! (config := .lemmasOnly) source target]
 protected def refl (α : Type _) [TopologicalSpace α] : LocalHomeomorph α α :=
   (Homeomorph.refl α).toLocalHomeomorph
 #align local_homeomorph.refl LocalHomeomorph.refl
 
--- porting note: todo: see #2350
-attribute [mfld_simps] refl_apply
-
 @[simp, mfld_simps]
 theorem refl_localEquiv : (LocalHomeomorph.refl α).toLocalEquiv = LocalEquiv.refl α :=
   rfl
@@ -763,7 +753,7 @@ section
 variable {s : Set α} (hs : IsOpen s)
 
 /-- The identity local equiv on a set `s` -/
-@[simps! (config := mfld_cfg) apply, simps! (config := { attrs := [] }) source target]
+@[simps! (config := mfld_cfg) apply, simps! (config := .lemmasOnly) source target]
 def ofSet (s : Set α) (hs : IsOpen s) : LocalHomeomorph α α where
   toLocalEquiv := LocalEquiv.ofSet s
   open_source := hs
@@ -772,9 +762,6 @@ def ofSet (s : Set α) (hs : IsOpen s) : LocalHomeomorph α α where
   continuous_invFun := continuous_id.continuousOn
 #align local_homeomorph.of_set LocalHomeomorph.ofSet
 
--- porting note: todo: see #2350
-attribute [mfld_simps] ofSet_apply
-
 @[simp, mfld_simps]
 theorem ofSet_toLocalEquiv : (ofSet s hs).toLocalEquiv = LocalEquiv.ofSet s :=
   rfl
@@ -1023,7 +1010,7 @@ section Prod
 
 /-- The product of two local homeomorphisms, as a local homeomorphism on the product space. -/
 @[simps! (config := mfld_cfg) toLocalEquiv apply,
-  simps! (config := { attrs := [] }) source target symm_apply]
+  simps! (config := .lemmasOnly) source target symm_apply]
 def prod (e : LocalHomeomorph α β) (e' : LocalHomeomorph γ δ) :
     LocalHomeomorph (α × γ) (β × δ) where
   open_source := e.open_source.prod e'.open_source
@@ -1033,9 +1020,6 @@ def prod (e : LocalHomeomorph α β) (e' : LocalHomeomorph γ δ) :
   toLocalEquiv := e.toLocalEquiv.prod e'.toLocalEquiv
 #align local_homeomorph.prod LocalHomeomorph.prod
 
--- porting note: todo: see #2350
-attribute [mfld_simps] prod_toLocalEquiv prod_apply
-
 @[simp, mfld_simps]
 theorem prod_symm (e : LocalHomeomorph α β) (e' : LocalHomeomorph γ δ) :
     (e.prod e').symm = e.symm.prod e'.symm :=
@@ -1270,10 +1254,6 @@ def toHomeomorphOfSourceEqUnivTargetEqUniv (h : e.source = (univ : Set α)) (h'
     simpa only [continuous_iff_continuousOn_univ, h'] using e.continuousOn_symm
 #align local_homeomorph.to_homeomorph_of_source_eq_univ_target_eq_univ LocalHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv
 
--- porting note: todo: see #2350
-attribute [mfld_simps] toHomeomorphOfSourceEqUnivTargetEqUniv_apply
-  toHomeomorphOfSourceEqUnivTargetEqUniv_symm_apply
-
 /-- A local homeomorphism whose source is all of `α` defines an open embedding of `α` into `β`.  The
 converse is also true; see `OpenEmbedding.toLocalHomeomorph`. -/
 theorem to_openEmbedding (h : e.source = Set.univ) : OpenEmbedding e := by
@@ -1326,9 +1306,6 @@ noncomputable def toLocalHomeomorph [Nonempty α] : LocalHomeomorph α β :=
     h.continuous.continuousOn h.isOpenMap isOpen_univ
 #align open_embedding.to_local_homeomorph OpenEmbedding.toLocalHomeomorph
 
--- porting note: todo: see #2350
-attribute [mfld_simps] toLocalHomeomorph_apply toLocalHomeomorph_source toLocalHomeomorph_target
-
 theorem continuousAt_iff {f : α → β} {g : β → γ} (hf : OpenEmbedding f) {x : α} :
     ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x) :=
   hf.tendsto_nhds_iff'

test/Simps.lean

@@ -140,16 +140,16 @@ noncomputable def bar2 {α} : α ≃ α :=
 Classical.choice ⟨foo.rfl⟩
 
 run_cmd liftCoreM <| do
-  _ ← successIfFail <| simpsTac .missing `foo.bar1
+  _ ← successIfFail <| simpsTac .missing `foo.bar1 { rhsMd := .default, simpRhs := true }
   --   "Invalid `simps` attribute. Target Nat is not a structure"
-  _ ← successIfFail <| simpsTac .missing `foo.bar2
+  _ ← successIfFail <| simpsTac .missing `foo.bar2 { rhsMd := .default, simpRhs := true }
   --   "Invalid `simps` attribute. The body is not a constructor application:
   -- Classical.choice (_ : Nonempty (α ≃ α))"
   pure ()
 
 /- test that if a non-constructor is given as definition, then
   `{rhsMd := .default, simpRhs := true}` is applied automatically. -/
-@[simps] def rfl2 {α} : α ≃ α := foo.rfl
+@[simps!] def rfl2 {α} : α ≃ α := foo.rfl
 
 example {α} (x : α) : rfl2.toFun x = x ∧ rfl2.invFun x = x := by
   dsimp
@@ -177,11 +177,11 @@ def my_equiv := Equiv'
 /- check projections for nested structures -/
 
 namespace CountNested
-@[simps (config := {attrs := [`norm]})]
+@[simps]
 def nested1 : MyProd ℕ $ MyProd ℤ ℕ :=
 ⟨2, -1, 1⟩
 
-@[simps (config := {isSimp := false})]
+@[simps (config := .lemmasOnly)]
 def nested2 : ℕ × MyProd ℕ ℕ :=
 ⟨2, MyProd.map Nat.succ Nat.pred ⟨1, 2⟩⟩
 
@@ -353,7 +353,8 @@ run_cmd liftTermElabM <| do
 -- You can also see this information by running
 --   `initialize_simps_projections? prod`.
 -- Note: these projection names might not correspond to the projection names of the structure."
-  _ ← successIfFail <| simpsTac .missing `specify.specify5 {} [("snd_snd", .missing)]
+  _ ← successIfFail <| simpsTac .missing `specify.specify5 { rhsMd := .default, simpRhs := true }
+    [("snd_snd", .missing)]
 --     "Invalid simp lemma specify.specify5_snd_snd.
 -- The given definition is not a constructor application:
 --   Classical.choice specify.specify5._proof_1"
@@ -409,7 +410,7 @@ run_cmd liftTermElabM <| do
   guard <| env.find? `pprodEquivProd2_invFun_snd |>.isSome
 
 -- we can disable this behavior with the option `notRecursive`.
-@[simps (config := {notRecursive := []})] def pprodEquivProd22 : PProd ℕ ℕ ≃ ℕ × ℕ :=
+@[simps! (config := {notRecursive := []})] def pprodEquivProd22 : PProd ℕ ℕ ≃ ℕ × ℕ :=
 pprodEquivProd2
 
 run_cmd liftTermElabM <| do
@@ -491,7 +492,7 @@ example {α} (x x' : α) (h : x = x') : coercing.rfl2.invFun x = x' := by simp;
 @[simps] protected def Equiv2.symm2 {α β} (f : Equiv2 α β) : Equiv2 β α :=
 ⟨f.invFun, f.toFun, f.right_inv, f.left_inv⟩
 
-@[simps (config := {fullyApplied := false})] protected def Equiv2.symm3 {α β} (f : Equiv2 α β) : Equiv2 β α :=
+@[simps (config := .asFn)] protected def Equiv2.symm3 {α β} (f : Equiv2 α β) : Equiv2 β α :=
 ⟨f.invFun, f, f.right_inv, f.left_inv⟩
 
 example {α β} (f : Equiv2 α β) (y : β) {x} (h : f.invFun y = x) : f.symm y = x := by simp; rw [h]
@@ -774,7 +775,7 @@ example (e₁ : α ≃ β) (e₂ : β ≃ γ) (x : α) {z} (h : e₂ (e₁ x) =
 ⟨e₂ ∘ (e₁ : α → β), e₁.symm ∘ (e₂.symm : γ → β)⟩
 
 -- it interacts somewhat well with multiple projections (though the generated name is not great)
-@[simps snd_coe_fst] def foo {α β γ δ : Type _} (x : α) (e₁ : α ≃ β) (e₂ : γ ≃ δ) :
+@[simps! snd_coe_fst] def foo {α β γ δ : Type _} (x : α) (e₁ : α ≃ β) (e₂ : γ ≃ δ) :
   α × (α × γ ≃ β × δ) :=
 ⟨x, Prod.map e₁ e₂, Prod.map e₁.symm e₂.symm⟩
 
@@ -1022,7 +1023,7 @@ example {α : Type} (x z : α) (h : x = z) : (foo α).symm x = z := by
   guard_target = x = z
   rw [h]
 
-@[simps toEquiv' apply symm_apply] def foo2 (α : Type) : DecoratedEquiv α α :=
+@[simps! toEquiv' apply symm_apply] def foo2 (α : Type) : DecoratedEquiv α α :=
 { foo.rfl with
   P_toFun  := λ _ _ h => h
   P_invFun := λ _ _ h => h }
@@ -1078,10 +1079,10 @@ example {α : Type} (x z : α) (h : x = z) : (ffoo α).symm x = z := by
   guard_target = x = z
   rw [h]
 
-@[simps] def ffoo3 (α : Type) : FurtherDecoratedEquiv α α :=
+@[simps!] def ffoo3 (α : Type) : FurtherDecoratedEquiv α α :=
 { foo α with Q_toFun  := λ y => ⟨y, rfl⟩, Q_invFun  := λ y => ⟨y, rfl⟩ }
 
-@[simps apply toEquiv' toEquiv'_toFun toDecoratedEquiv_apply]
+@[simps! apply toEquiv' toEquiv'_toFun toDecoratedEquiv_apply]
 def ffoo4 (α : Type) : FurtherDecoratedEquiv α α :=
 { Q_toFun := λ y => ⟨y, rfl⟩, Q_invFun := λ y => ⟨y, rfl⟩, toDecoratedEquiv := foo α }
 
@@ -1112,7 +1113,7 @@ initialize_simps_projections OneMore (toFun → apply, invFun → symm_apply,
 
 example {α : Type} (x : α) : (fffoo α).symm x = x := by dsimp
 
-@[simps apply to_dequiv_apply toFurtherDecoratedEquiv_apply to_dequiv]
+@[simps! apply to_dequiv_apply toFurtherDecoratedEquiv_apply to_dequiv]
 def fffoo2 (α : Type) : OneMore α α := fffoo α
 
 /- test the case where a projection takes additional arguments. -/