feat: to_additive can reorder arguments of generated declaration (#818)

* This allows `@[to_additive]` on lemmas about `Pow` without having to write the corresponding lemmas about SMul explicitly.
* Add syntax `to_additive (reorder := ...)` that will automatically reorder the arguments in the additive declaration and will reorder the arguments in all future uses of `to_additive`
* Deprecate `@[to_additive_reorder]` attribute.
  * We keep it for now, so that it can display a warning message when porting a file with the attribute
  * We allow `@[to_additive (reorder := ...)]` on declarations that are already additivized, so that we can give the `reorder` information to projections of structures.
* Maybe at some point we can add a syntax to "doubly additivize" a declaration about `Pow`, so that it generates both the `SMul` and `VAdd` declarations.

Author: fpvandoorn

Mathlib/Algebra/Group/Defs.lean

@@ -81,26 +81,12 @@ infixl:65 " +ᵥ " => HVAdd.hVAdd
 infixl:65 " -ᵥ " => HasVsub.vsub
 infixr:73 " • " => HSMul.hSMul
 
-attribute [to_additive] Mul
-attribute [to_additive] Div
-attribute [to_additive] HMul
-attribute [to_additive] instHMul
-attribute [to_additive] HDiv
-attribute [to_additive] instHDiv
-
+attribute [to_additive] Mul Div HMul instHMul HDiv instHDiv instHSMul HSMul
 attribute [to_additive_relevant_arg 3] HMul HAdd HPow HSMul
 attribute [to_additive_relevant_arg 3] HAdd.hAdd HMul.hMul HPow.hPow HSMul.hSMul
-attribute [to_additive_reorder 1] HPow
-attribute [to_additive_reorder 1 5] HPow.hPow
-attribute [to_additive_reorder 1] Pow
-attribute [to_additive_reorder 1 4] Pow.pow
-attribute [to_additive] Pow
-attribute [to_additive_reorder 1] instHPow
-attribute [to_additive] instHPow
-attribute [to_additive] HPow
-
-attribute [to_additive] instHSMul
-attribute [to_additive] HSMul
+attribute [to_additive (reorder := 1)] Pow instHPow HPow
+attribute [to_additive (reorder := 1 5)] HPow.hPow
+attribute [to_additive (reorder := 1 4)] Pow.pow
 
 universe u
 

Mathlib/Algebra/Group/OrderSynonym.lean

@@ -32,20 +32,15 @@ instance [h : Inv α] : Inv αᵒᵈ := h
 @[to_additive]
 instance [h : Div α] : Div αᵒᵈ := h
 
-@[to_additive]
-instance [h : SMul α β] : SMul α βᵒᵈ := h
-
-@[to_additive]
-instance instSMulOrderDual' [h : SMul α β] : SMul αᵒᵈ β := h
-#align order_dual.has_smul' instSMulOrderDual'
-
-@[to_additive]
+@[to_additive (reorder := 1)]
 instance [h : Pow α β] : Pow αᵒᵈ β := h
 #align order_dual.has_pow instPowOrderDual
+#align order_dual.has_smul instSMulOrderDual
 
-@[to_additive]
+@[to_additive (reorder := 1)]
 instance instPowOrderDual' [h : Pow α β] : Pow α βᵒᵈ := h
 #align order_dual.has_pow' instPowOrderDual'
+#align order_dual.has_smul' instSMulOrderDual'
 
 @[to_additive]
 instance [h : Semigroup α] : Semigroup αᵒᵈ := h
@@ -130,35 +125,19 @@ theorem toDual_div [Div α] (a b : α) : toDual (a / b) = toDual a / toDual b :=
 theorem ofDual_div [Div α] (a b : αᵒᵈ) : ofDual (a / b) = ofDual a / ofDual b := rfl
 #align of_dual_div ofDual_div
 
-@[simp, to_additive]
-theorem toDual_smul [SMul α β] (a : α) (b : β) : toDual (a • b) = a • toDual b := rfl
-#align to_dual_smul toDual_smul
-
-@[simp, to_additive]
-theorem ofDual_smul [SMul α β] (a : α) (b : βᵒᵈ) : ofDual (a • b) = a • ofDual b := rfl
-#align of_dual_smul ofDual_smul
-
-@[simp, to_additive]
-theorem toDual_smul' [SMul α β] (a : α) (b : β) : toDual a • b = a • b := rfl
-#align to_dual_smul' toDual_smul'
-
-@[simp, to_additive]
-theorem ofDual_smul' [SMul α β] (a : αᵒᵈ) (b : β) : ofDual a • b = a • b := rfl
-#align of_dual_smul' ofDual_smul'
-
-@[simp, to_additive, to_additive_reorder 1 4]
+@[simp, to_additive (reorder := 1 4)]
 theorem toDual_pow [Pow α β] (a : α) (b : β) : toDual (a ^ b) = toDual a ^ b := rfl
 #align to_dual_pow toDual_pow
 
-@[simp, to_additive, to_additive_reorder 1 4]
+@[simp, to_additive (reorder := 1 4)]
 theorem ofDual_pow [Pow α β] (a : αᵒᵈ) (b : β) : ofDual (a ^ b) = ofDual a ^ b := rfl
 #align of_dual_pow ofDual_pow
 
-@[simp, to_additive toDual_smul', to_additive_reorder 1 4]
+@[simp, to_additive toDual_smul' (reorder := 1 4)]
 theorem pow_toDual [Pow α β] (a : α) (b : β) : a ^ toDual b = a ^ b := rfl
 #align pow_to_dual pow_toDual
 
-@[simp, to_additive ofDual_smul', to_additive_reorder 1 4]
+@[simp, to_additive ofDual_smul' (reorder := 1 4)]
 theorem pow_ofDual [Pow α β] (a : α) (b : βᵒᵈ) : a ^ ofDual b = a ^ b := rfl
 #align pow_of_dual pow_ofDual
 
@@ -177,20 +156,15 @@ instance [h : Inv α] : Inv (Lex α) := h
 @[to_additive]
 instance [h : Div α] : Div (Lex α) := h
 
-@[to_additive]
-instance [h : SMul α β] : SMul α (Lex β) := h
-
-@[to_additive]
-instance instSMulLex' [h : SMul α β] : SMul (Lex α) β := h
-#align lex.has_smul' instSMulLex'
-
-@[to_additive]
+@[to_additive (reorder := 1)]
 instance [h : Pow α β] : Pow (Lex α) β := h
 #align lex.has_pow instPowLex
+#align lex.has_smul instSMulLex
 
-@[to_additive]
+@[to_additive (reorder := 1)]
 instance instPowLex' [h : Pow α β] : Pow α (Lex β) := h
 #align lex.has_pow' instPowLex'
+#align lex.has_smul' instSMulLex'
 
 @[to_additive]
 instance [h : Semigroup α] : Semigroup (Lex α) := h
@@ -275,34 +249,23 @@ theorem toLex_div [Div α] (a b : α) : toLex (a / b) = toLex a / toLex b := rfl
 theorem ofLex_div [Div α] (a b : Lex α) : ofLex (a / b) = ofLex a / ofLex b := rfl
 #align of_lex_div ofLex_div
 
-@[simp, to_additive]
-theorem toLex_smul [SMul α β] (a : α) (b : β) : toLex (a • b) = a • toLex b := rfl
-#align to_lex_smul toLex_smul
-
-@[simp, to_additive]
-theorem ofLex_smul [SMul α β] (a : α) (b : Lex β) : ofLex (a • b) = a • ofLex b := rfl
-#align of_lex_smul ofLex_smul
-
-@[simp, to_additive]
-theorem toLex_smul' [SMul α β] (a : α) (b : β) : toLex a • b = a • b := rfl
-#align to_lex_smul' toLex_smul'
-
-@[simp, to_additive]
-theorem ofLex_smul' [SMul α β] (a : Lex α) (b : β) : ofLex a • b = a • b := rfl
-#align of_lex_smul' ofLex_smul'
-
-@[simp, to_additive, to_additive_reorder 1 4]
+@[simp, to_additive (reorder := 1 4)]
 theorem toLex_pow [Pow α β] (a : α) (b : β) : toLex (a ^ b) = toLex a ^ b := rfl
 #align to_lex_pow toLex_pow
 
-@[simp, to_additive, to_additive_reorder 1 4]
+@[simp, to_additive (reorder := 1 4)]
 theorem ofLex_pow [Pow α β] (a : Lex α) (b : β) : ofLex (a ^ b) = ofLex a ^ b := rfl
 #align of_lex_pow ofLex_pow
 
-@[simp, to_additive toLex_smul, to_additive_reorder 1 4]
+@[simp, to_additive toLex_smul' (reorder := 1 4)]
 theorem pow_toLex [Pow α β] (a : α) (b : β) : a ^ toLex b = a ^ b := rfl
 #align pow_to_lex pow_toLex
 
-@[simp, to_additive ofLex_smul, to_additive_reorder 1 4]
+@[simp, to_additive ofLex_smul' (reorder := 1 4)]
 theorem pow_ofLex [Pow α β] (a : α) (b : Lex β) : a ^ ofLex b = a ^ b := rfl
 #align pow_of_lex pow_ofLex
+
+attribute [to_additive] instSMulOrderDual instSMulOrderDual'
+  toDual_smul ofDual_smul toDual_smul' ofDual_smul'
+  instSMulLex instSMulLex'
+  toLex_smul ofLex_smul toLex_smul' ofLex_smul'

Mathlib/Data/Pi/Algebra.lean

@@ -93,43 +93,29 @@ instance instSMul [∀ i, SMul α <| f i] : SMul α (∀ i : I, f i) :=
 #align pi.has_smul Pi.instSMul
 #align pi.has_vadd Pi.instVAdd
 
-@[simp, to_additive]
-theorem smul_apply [∀ i, SMul α <| f i] (s : α) (x : ∀ i, f i) (i : I) : (s • x) i = s • x i :=
-  rfl
-
-@[to_additive]
-theorem smul_def [∀ i, SMul α <| f i] (s : α) (x : ∀ i, f i) : s • x = fun i => s • x i :=
-  rfl
-
-@[simp, to_additive]
-theorem smul_const [SMul α β] (a : α) (b : β) : a • const I b = const I (a • b) :=
-  rfl
-
-@[to_additive]
-theorem smul_comp [SMul α γ] (a : α) (x : β → γ) (y : I → β) : (a • x) ∘ y = a • x ∘ y :=
-  rfl
-
 @[to_additive]
 instance instPow [∀ i, Pow (f i) β] : Pow (∀ i, f i) β :=
   ⟨fun x b i => x i ^ b⟩
 
-@[simp, to_additive, to_additive_reorder 5]
+@[simp, to_additive (reorder := 5)]
 theorem pow_apply [∀ i, Pow (f i) β] (x : ∀ i, f i) (b : β) (i : I) : (x ^ b) i = x i ^ b :=
   rfl
 
-@[to_additive, to_additive_reorder 5]
+@[to_additive (reorder := 5)]
 theorem pow_def [∀ i, Pow (f i) β] (x : ∀ i, f i) (b : β) : x ^ b = fun i => x i ^ b :=
   rfl
 
 -- `to_additive` generates bad output if we take `Pow α β`.
-@[simp, to_additive smul_const, to_additive_reorder 5]
+@[simp, to_additive smul_const (reorder := 5)]
 theorem const_pow [Pow β α] (b : β) (a : α) : const I b ^ a = const I (b ^ a) :=
   rfl
 
-@[to_additive, to_additive_reorder 6]
+@[to_additive (reorder := 6)]
 theorem pow_comp [Pow γ α] (x : β → γ) (a : α) (y : I → β) : (x ^ a) ∘ y = x ∘ y ^ a :=
   rfl
 
+attribute [to_additive] smul_apply smul_def smul_const smul_comp
+
 /-!
 Porting note: `bit0` and `bit1` are deprecated. This section can be removed entirely
 (without replacement?).

Mathlib/Lean/Expr/Basic.lean

@@ -77,40 +77,49 @@ end Name
 
 namespace ConstantInfo
 
+/-- Checks whether this `ConstantInfo` is a definition, -/
 def isDef : ConstantInfo → Bool
   | defnInfo _ => true
   | _          => false
 
+/-- Checks whether this `ConstantInfo` is a theorem, -/
 def isThm : ConstantInfo → Bool
   | thmInfo _ => true
   | _          => false
 
-def updateName : ConstantInfo → Name → ConstantInfo
-  | defnInfo   info, n => defnInfo   {info with name := n}
-  | axiomInfo  info, n => axiomInfo  {info with name := n}
-  | thmInfo    info, n => thmInfo    {info with name := n}
-  | opaqueInfo info, n => opaqueInfo {info with name := n}
-  | quotInfo   info, n => quotInfo   {info with name := n}
-  | inductInfo info, n => inductInfo {info with name := n}
-  | ctorInfo   info, n => ctorInfo   {info with name := n}
-  | recInfo    info, n => recInfo    {info with name := n}
-
-def updateType : ConstantInfo → Expr → ConstantInfo
-  | defnInfo   info, y => defnInfo   {info with type := y}
-  | axiomInfo  info, y => axiomInfo  {info with type := y}
-  | thmInfo    info, y => thmInfo    {info with type := y}
-  | opaqueInfo info, y => opaqueInfo {info with type := y}
-  | quotInfo   info, y => quotInfo   {info with type := y}
-  | inductInfo info, y => inductInfo {info with type := y}
-  | ctorInfo   info, y => ctorInfo   {info with type := y}
-  | recInfo    info, y => recInfo    {info with type := y}
-
+/-- Update `ConstantVal` (the data common to all constructors of `ConstantInfo`)
+in a `ConstantInfo`. -/
+def updateConstantVal : ConstantInfo → ConstantVal → ConstantInfo
+  | defnInfo   info, v => defnInfo   {info with toConstantVal := v}
+  | axiomInfo  info, v => axiomInfo  {info with toConstantVal := v}
+  | thmInfo    info, v => thmInfo    {info with toConstantVal := v}
+  | opaqueInfo info, v => opaqueInfo {info with toConstantVal := v}
+  | quotInfo   info, v => quotInfo   {info with toConstantVal := v}
+  | inductInfo info, v => inductInfo {info with toConstantVal := v}
+  | ctorInfo   info, v => ctorInfo   {info with toConstantVal := v}
+  | recInfo    info, v => recInfo    {info with toConstantVal := v}
+
+/-- Update the name of a `ConstantInfo`. -/
+def updateName (c : ConstantInfo) (name : Name) : ConstantInfo :=
+  c.updateConstantVal {c.toConstantVal with name}
+
+/-- Update the type of a `ConstantInfo`. -/
+def updateType (c : ConstantInfo) (type : Expr) : ConstantInfo :=
+  c.updateConstantVal {c.toConstantVal with type}
+
+/-- Update the level parameters of a `ConstantInfo`. -/
+def updateLevelParams (c : ConstantInfo) (levelParams : List Name) :
+  ConstantInfo :=
+  c.updateConstantVal {c.toConstantVal with levelParams}
+
+/-- Update the value of a `ConstantInfo`, if it has one. -/
 def updateValue : ConstantInfo → Expr → ConstantInfo
   | defnInfo   info, v => defnInfo   {info with value := v}
   | thmInfo    info, v => thmInfo    {info with value := v}
   | opaqueInfo info, v => opaqueInfo {info with value := v}
   | d, _ => d
 
+/-- Turn a `ConstantInfo` into a declaration. -/
 def toDeclaration! : ConstantInfo → Declaration
   | defnInfo   info => Declaration.defnDecl info
   | thmInfo    info => Declaration.thmDecl     info

Mathlib/Tactic/Simps/Basic.lean

@@ -837,7 +837,10 @@ def simpsAddProjection (declName : Name) (type lhs rhs : Expr) (args : Array Exp
   if let some tgt := cfg.addAdditive then
     ToAdditive.addToAdditiveAttr declName
       -- tracing seems to fail
-      ⟨false, (← getOptions) |>.getBool `trace.to_additive, tgt, none, true, ref⟩
+      { trace := (← getOptions) |>.getBool `trace.to_additive,
+        allowAutoName := true
+        tgt
+        ref }
 
 /--
 Perform head-structure-eta-reduction on expression `e`. That is, if `e` is of the form