feat(to_additive): copy _refl_lemma attribute (#7011)

also warn user if if `simps` and `to_additive` are provided out of order.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

src/algebra/category/Mon/basic.lean

@@ -128,8 +128,8 @@ section
 variables [monoid X] [monoid Y]
 
 /-- Build an isomorphism in the category `Mon` from a `mul_equiv` between `monoid`s. -/
-@[simps, to_additive add_equiv.to_AddMon_iso "Build an isomorphism in the category `AddMon` from
-an `add_equiv` between `add_monoid`s."]
+@[to_additive add_equiv.to_AddMon_iso "Build an isomorphism in the category `AddMon` from
+an `add_equiv` between `add_monoid`s.", simps]
 def mul_equiv.to_Mon_iso (e : X ≃* Y) : Mon.of X ≅ Mon.of Y :=
 { hom := e.to_monoid_hom,
   inv := e.symm.to_monoid_hom }
@@ -140,8 +140,8 @@ section
 variables [comm_monoid X] [comm_monoid Y]
 
 /-- Build an isomorphism in the category `CommMon` from a `mul_equiv` between `comm_monoid`s. -/
-@[simps, to_additive add_equiv.to_AddCommMon_iso "Build an isomorphism in the category `AddCommMon`
-from an `add_equiv` between `add_comm_monoid`s."]
+@[to_additive add_equiv.to_AddCommMon_iso "Build an isomorphism in the category `AddCommMon`
+from an `add_equiv` between `add_comm_monoid`s.", simps]
 def mul_equiv.to_CommMon_iso (e : X ≃* Y) : CommMon.of X ≅ CommMon.of Y :=
 { hom := e.to_monoid_hom,
   inv := e.symm.to_monoid_hom }

src/algebra/category/Semigroup/basic.lean

@@ -101,8 +101,8 @@ section
 variables [has_mul X] [has_mul Y]
 
 /-- Build an isomorphism in the category `Magma` from a `mul_equiv` between `has_mul`s. -/
-@[simps, to_additive add_equiv.to_AddMagma_iso "Build an isomorphism in the category `AddMagma` from
-an `add_equiv` between `has_add`s."]
+@[to_additive add_equiv.to_AddMagma_iso "Build an isomorphism in the category `AddMagma` from
+an `add_equiv` between `has_add`s.", simps]
 def mul_equiv.to_Magma_iso (e : X ≃* Y) : Magma.of X ≅ Magma.of Y :=
 { hom := e.to_mul_hom,
   inv := e.symm.to_mul_hom }
@@ -113,8 +113,8 @@ section
 variables [semigroup X] [semigroup Y]
 
 /-- Build an isomorphism in the category `Semigroup` from a `mul_equiv` between `semigroup`s. -/
-@[simps, to_additive add_equiv.to_AddSemigroup_iso "Build an isomorphism in the category
-`AddSemigroup` from an `add_equiv` between `add_semigroup`s."]
+@[to_additive add_equiv.to_AddSemigroup_iso "Build an isomorphism in the category
+`AddSemigroup` from an `add_equiv` between `add_semigroup`s.", simps]
 def mul_equiv.to_Semigroup_iso (e : X ≃* Y) : Semigroup.of X ≅ Semigroup.of Y :=
 { hom := e.to_mul_hom,
   inv := e.symm.to_mul_hom }

src/algebra/group/pi.lean

@@ -136,9 +136,9 @@ lemma monoid_hom.apply_apply (i : I) (g : Π i, f i) :
 /-- Coercion of a `monoid_hom` into a function is itself a `monoid_hom`.
 
 See also `monoid_hom.eval`. -/
-@[simps, to_additive "Coercion of an `add_monoid_hom` into a function is itself a `add_monoid_hom`.
+@[to_additive "Coercion of an `add_monoid_hom` into a function is itself a `add_monoid_hom`.
 
-See also `add_monoid_hom.eval`. "]
+See also `add_monoid_hom.eval`. ", simps]
 def monoid_hom.coe_fn (α β : Type*) [mul_one_class α] [comm_monoid β] : (α →* β) →* (α → β) :=
 { to_fun := λ g, g,
   map_one' := rfl,

src/algebra/group/to_additive.lean

@@ -307,7 +307,10 @@ protected meta def attr : user_attribute unit value_type :=
     then proceed_fields env src tgt prio
     else do
       transform_decl_with_prefix_dict dict src tgt
-        [`reducible, `simp, `instance, `refl, `symm, `trans, `elab_as_eliminator, `no_rsimp],
+        [`reducible, `_refl_lemma, `simp, `instance, `refl, `symm, `trans, `elab_as_eliminator,
+         `no_rsimp],
+      mwhen (has_attribute' `simps src)
+        (trace "Apply the simps attribute after the to_additive attribute"),
       match val.doc with
       | some doc := add_doc_string tgt doc
       | none := skip

src/data/equiv/mul_add.lean

@@ -287,9 +287,8 @@ rfl
 A multiplicative analogue of `equiv.arrow_congr`,
 where the equivalence between the targets is multiplicative.
 -/
-@[simps apply,
-  to_additive "An additive analogue of `equiv.arrow_congr`,
-where the equivalence between the targets is additive."]
+@[to_additive "An additive analogue of `equiv.arrow_congr`,
+where the equivalence between the targets is additive.", simps apply]
 def arrow_congr {M N P Q : Type*} [mul_one_class P] [mul_one_class Q]
   (f : M ≃ N) (g : P ≃* Q) : (M → P) ≃* (N → Q) :=
 { to_fun := λ h n, g (h (f.symm n)),
@@ -302,9 +301,8 @@ def arrow_congr {M N P Q : Type*} [mul_one_class P] [mul_one_class Q]
 A multiplicative analogue of `equiv.arrow_congr`,
 for multiplicative maps from a monoid to a commutative monoid.
 -/
-@[simps apply,
-  to_additive "An additive analogue of `equiv.arrow_congr`,
-for additive maps from an additive monoid to a commutative additive monoid."]
+@[to_additive "An additive analogue of `equiv.arrow_congr`,
+for additive maps from an additive monoid to a commutative additive monoid.", simps apply]
 def monoid_hom_congr {M N P Q} [mul_one_class M] [mul_one_class N] [comm_monoid P] [comm_monoid Q]
   (f : M ≃* N) (g : P ≃* Q) : (M →* P) ≃* (N →* Q) :=
 { to_fun := λ h,

src/topology/continuous_function/algebra.lean

@@ -112,8 +112,8 @@ instance continuous_map_monoid {α : Type*} {β : Type*} [topological_space α]
   ..continuous_map.has_one }
 
 /-- Coercion to a function as an `monoid_hom`. Similar to `monoid_hom.coe_fn`. -/
-@[simps,
-  to_additive "Coercion to a function as an `add_monoid_hom`. Similar to `add_monoid_hom.coe_fn`."]
+@[to_additive "Coercion to a function as an `add_monoid_hom`. Similar to `add_monoid_hom.coe_fn`.",
+  simps]
 def coe_fn_monoid_hom {α : Type*} {β : Type*} [topological_space α] [topological_space β]
   [monoid β] [has_continuous_mul β] : C(α, β) →* (α → β) :=
 { to_fun := coe_fn, map_one' := continuous_map.one_coe, map_mul' := continuous_map.mul_coe }

test/simps.lean

@@ -1,5 +1,5 @@
 import tactic.simps
-import algebra.group.to_additive
+import algebra.group.hom
 
 universe variables v u w
 -- set_option trace.simps.verbose true
@@ -810,4 +810,20 @@ begin
   contradiction
 end
 
+/- Test that `to_additive` copies the `@[_refl_lemma]` attribute correctly -/
+@[to_additive, simps]
+def monoid_hom.my_comp {M N P : Type*} [mul_one_class M] [mul_one_class N] [mul_one_class P]
+  (hnp : N →* P) (hmn : M →* N) : M →* P :=
+{ to_fun := hnp ∘ hmn, map_one' := by simp, map_mul' := by simp, }
+
+-- `simps` adds the `_refl_lemma` attribute to `monoid_hom.my_comp_apply`
+example {M N P : Type*} [mul_one_class M] [mul_one_class N] [mul_one_class P]
+  (hnp : N →* P) (hmn : M →* N) (m : M) : hnp.my_comp hmn m = hnp (hmn m) :=
+by { dsimp, guard_target (hnp (hmn m) = hnp (hmn m)), refl }
+
+-- `to_additive` adds the `_refl_lemma` attribute to `add_monoid_hom.my_comp_apply`
+example {M N P : Type*} [add_zero_class M] [add_zero_class N] [add_zero_class P]
+  (hnp : N →+ P) (hmn : M →+ N) (m : M) : hnp.my_comp hmn m = hnp (hmn m) :=
+by { dsimp, guard_target (hnp (hmn m) = hnp (hmn m)), refl }
+
 end