feat: improve toAdditive.guessName (#715)

* The heuristic to split names did it wrong on a long sequence of capital letters. The new heuristic is to have a sequence of "white-listed" names that only consist of capital letters (currently `["LE", "LT", "WF"]`). This new heuristic correctly splits `ZeroLEHAdd` and `HSMul`
* translate `[h]pow` to `[h]smul` (see #706). I believe Mathlib4 never used the previous automatic translation `pow -> nsmul` (I used regex `@\[to_additive\]\n?.*(_p|P| p)ow` to search). Since capitalization goes wrong in this case, add some cases in `fixAbbreviation` to fix it.
* Fix all places where the capitalization `Smul` was used instead of `SMul`.

Author: fpvandoorn

Mathlib/Algebra/Group/Defs.lean

@@ -97,13 +97,13 @@ 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 SMul] Pow
+attribute [to_additive] Pow
 attribute [to_additive_reorder 1] instHPow
-attribute [to_additive instHSMul] instHPow
-attribute [to_additive HSMul] HPow
+attribute [to_additive] instHPow
+attribute [to_additive] HPow
 
-attribute [to_additive instHVAdd] instHSMul
-attribute [to_additive HVAdd] HSMul
+attribute [to_additive] instHSMul
+attribute [to_additive] HSMul
 
 universe u
 
@@ -531,7 +531,7 @@ section
 
 variable {M : Type _} [Monoid M]
 
-@[simp, to_additive nsmul_eq_smul]
+@[simp, to_additive]
 theorem npow_eq_pow (n : ℕ) (x : M) : Monoid.npow n x = x ^ n :=
   rfl
 
@@ -770,7 +770,7 @@ section DivInvMonoid
 
 variable [DivInvMonoid G] {a b : G}
 
-@[simp, to_additive zsmul_eq_smul] theorem zpow_eq_pow (n : ℤ) (x : G) :
+@[simp, to_additive] theorem zpow_eq_pow (n : ℤ) (x : G) :
     DivInvMonoid.zpow n x = x ^ n :=
   rfl
 

Mathlib/Algebra/Group/OrderSynonym.lean

@@ -36,14 +36,14 @@ instance [h : Div α] : Div αᵒᵈ := h
 instance [h : SMul α β] : SMul α βᵒᵈ := h
 
 @[to_additive]
-instance OrderDual.hasSmul' [h : SMul α β] : SMul αᵒᵈ β := h
-#align order_dual.has_smul' OrderDual.hasSmul'
+instance OrderDual.SMul' [h : SMul α β] : SMul αᵒᵈ β := h
+#align order_dual.has_smul' OrderDual.SMul'
 
-@[to_additive OrderDual.hasSmul]
+@[to_additive OrderDual.SMul]
 instance OrderDual.hasPow [h : Pow α β] : Pow αᵒᵈ β := h
 #align order_dual.has_pow OrderDual.hasPow
 
-@[to_additive OrderDual.hasSmul']
+@[to_additive OrderDual.SMul']
 instance OrderDual.hasPow' [h : Pow α β] : Pow α βᵒᵈ := h
 #align order_dual.has_pow' OrderDual.hasPow'
 
@@ -146,11 +146,11 @@ theorem toDual_smul' [SMul α β] (a : α) (b : β) : toDual a • b = a • b :
 theorem ofDual_smul' [SMul α β] (a : αᵒᵈ) (b : β) : ofDual a • b = a • b := rfl
 #align of_dual_smul' ofDual_smul'
 
-@[simp, to_additive toDual_smul, to_additive_reorder 1 4]
+@[simp, to_additive, 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 ofDual_smul, to_additive_reorder 1 4]
+@[simp, to_additive, to_additive_reorder 1 4]
 theorem ofDual_pow [Pow α β] (a : αᵒᵈ) (b : β) : ofDual (a ^ b) = ofDual a ^ b := rfl
 #align of_dual_pow ofDual_pow
 
@@ -181,14 +181,14 @@ instance [h : Div α] : Div (Lex α) := h
 instance [h : SMul α β] : SMul α (Lex β) := h
 
 @[to_additive]
-instance Lex.hasSmul' [h : SMul α β] : SMul (Lex α) β := h
-#align lex.has_smul' Lex.hasSmul'
+instance Lex.SMul' [h : SMul α β] : SMul (Lex α) β := h
+#align lex.has_smul' Lex.SMul'
 
-@[to_additive Lex.hasSmul]
+@[to_additive Lex.SMul]
 instance Lex.hasPow [h : Pow α β] : Pow (Lex α) β := h
 #align lex.has_pow Lex.hasPow
 
-@[to_additive Lex.hasSmul']
+@[to_additive Lex.SMul']
 instance Lex.hasPow' [h : Pow α β] : Pow α (Lex β) := h
 #align lex.has_pow' Lex.hasPow'
 
@@ -291,11 +291,11 @@ theorem toLex_smul' [SMul α β] (a : α) (b : β) : toLex a • b = a • b :=
 theorem ofLex_smul' [SMul α β] (a : Lex α) (b : β) : ofLex a • b = a • b := rfl
 #align of_lex_smul' ofLex_smul'
 
-@[simp, to_additive toLex_smul, to_additive_reorder 1 4]
+@[simp, to_additive, 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 ofLex_smul, to_additive_reorder 1 4]
+@[simp, to_additive, 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
 

Mathlib/Data/Bracket.lean

@@ -25,7 +25,7 @@ these are the Unicode "square with quill" brackets rather than the usual square
   1. for certain binary operations on structures, like the product `⁅x, y⁆` of two elements
     `x`, `y` in a Lie algebra or the commutator of two elements `x` and `y` in a group.
   2. for certain actions of one structure on another, like the action `⁅x, m⁆` of an element `x`
-    of a Lie algebra on an element `m` in one of its modules (analogous to `Smul` in the
+    of a Lie algebra on an element `m` in one of its modules (analogous to `SMul` in the
     associative setting).
   3. for binary operations on substructures, like the commutator `⁅H, K⁆` of two subgroups `H` and
      `K` of a group. -/

Mathlib/Tactic/ToAdditive.lean

@@ -49,6 +49,10 @@ macro "to_additive!?" rest:to_additiveRest : attr => `(attr| to_additive ! ? $re
 /-- The `to_additive` attribute. -/
 macro "to_additive?!" rest:to_additiveRest : attr => `(attr| to_additive ! ? $rest)
 
+/-- A set of strings of names that are written in all-caps. -/
+def allCapitalNames : RBTree String compare :=
+.ofList ["LE", "LT", "WF"]
+
 /--
 This function takes a String and splits it into separate parts based on the following
 (naming conventions)[https://github.com/leanprover-community/mathlib4/wiki#naming-convention].
@@ -59,31 +63,17 @@ E.g. `#eval  "InvHMulLEConjugate₂Smul_ne_top".splitCase` yields
 partial def String.splitCase (s : String) (i₀ : Pos := 0) (r : List String := []) : List String :=
   -- We test if we need to split between `i₀` and `i₁`.
   let i₁ := s.next i₀
-  let i₂ := s.next i₁
   if s.atEnd i₁ then
     -- If `i₀` is the last position, return the list.
     let r := s::r
     r.reverse
-  -- First, we split on both sides of `_` to keep them there when rejoining the string.
-  else if (s.get i₀ = '_') || (s.get i₁ = '_') then
-    let r := (s.extract 0 i₁)::r
-    splitCase (s.extract i₁ s.endPos) 0 r
-  -- Otherwise, we only ever split when there is an upper case at `i₁`.
-  else if (s.get i₁).isUpper then
-    -- There are two cases we need to split:
-    if (s.get i₀).isUpper then
-      -- 1) If `i₀` and `i₁` are upper, `i₂` is not upper, and `i₀ > 0`.
-      -- This prevents single capital letters being split.
-      -- Example: Splits `LEOne`to `LE`, `One` but leaves `HMul` together.
-      if (i₀ ≠ 0) && ¬((s.get i₂).isUpper) then
-        let r := (s.extract 0 i₁)::r
-        splitCase (s.extract i₁ s.endPos) 0 r
-      else
-        splitCase s i₁ r
-    -- 2) Upper `i₁` is preceeded by non-upper `i₀`.
-    else
-      let r := (s.extract 0 i₁)::r
-      splitCase (s.extract i₁ s.endPos) 0 r
+  /- We split the string in three cases
+  * We split on both sides of `_` to keep them there when rejoining the string;
+  * We split after a sequence of capital letters in `allCapitalNames`;
+  * We split after a lower-case letter that is followed by an upper-case letter. -/
+  else if s.get i₀ == '_' || s.get i₁ == '_' ||
+    ((s.get i₁).isUpper && (!(s.get i₀).isUpper || allCapitalNames.contains (s.extract 0 i₁))) then
+    splitCase (s.extract i₁ s.endPos) 0 <| (s.extract 0 i₁)::r
   else
     splitCase s i₁ r
 
@@ -107,8 +97,7 @@ initialize ignoreArgsAttr : NameMapExtension (List Nat) ←
         let ids ← match stx with
           | `(attr| to_additive_ignore_args $[$ids:num]*) => pure <| ids.map (·.1.isNatLit?.get!)
           | _ => throwUnsupportedSyntax
-        return ids.toList
-  }
+        return ids.toList }
 
 /-- Gets the set of arguments that should be ignored for the given name
 (according to `@[to_additive_ignore_args ...]`).
@@ -407,7 +396,7 @@ partial def transformDeclAux
     return
   let srcDecl ← getConstInfo src
   let prefixes : NameSet := .ofList [pre, env.mainModule ++ `_auxLemma]
-  -- we first transform all auxilliary declarations generated when elaborating `pre`
+  -- we first transform all auxiliary declarations generated when elaborating `pre`
   for n in srcDecl.type.listNamesWithPrefixes prefixes do
     transformDeclAux none pre tgt_pre n
   if let some value := srcDecl.value? then
@@ -541,8 +530,7 @@ structure ValueType : Type where
   deriving Repr
 
 /-- Helper for `capitalizeLike`. -/
-partial def capitalizeLikeAux (s : String) (i : String.Pos := 0) : String →  String :=
-  fun p =>
+partial def capitalizeLikeAux (s : String) (i : String.Pos := 0) (p : String) : String :=
   if p.atEnd i || s.atEnd i then
     p
   else
@@ -558,7 +546,9 @@ partial def capitalizeLikeAux (s : String) (i : String.Pos := 0) : String →  S
 def capitalizeLike (r : String) (s : String) :=
   capitalizeLikeAux r 0 s
 
-/-- Capitalize First element of a list like `s`. -/
+/-- Capitalize First element of a list like `s`.
+Note that we need to capitalize multiple characters in some cases,
+in examples like `HMul` or `hAdd`. -/
 def capitalizeFirstLike (s : String) : List String → List String
   | x :: r => capitalizeLike s x :: r
   | [] => []
@@ -578,10 +568,11 @@ private def nameDict : String → List String
 | "div"         => ["sub"]
 | "prod"        => ["sum"]
 | "hmul"        => ["hadd"]
+| "hsmul"       => ["hvadd"]
 | "hdiv"        => ["hsub"]
-| "hpow"        => ["hmul"]
+| "hpow"        => ["hsmul"]
 | "finprod"     => ["finsum"]
-| "pow"         => ["nsmul"]
+| "pow"         => ["smul"]
 | "npow"        => ["nsmul"]
 | "zpow"        => ["zsmul"]
 | "monoid"      => ["add", "Monoid"]
@@ -634,19 +625,16 @@ def fixAbbreviation : List String → List String
 | "Add" :: "Support" :: s           => "Support" :: fixAbbreviation s
 | "add" :: "Support" :: s           => "support" :: fixAbbreviation s
 | "add" :: "_" :: "support" :: s    => "support" :: fixAbbreviation s
- -- TODO: Is it `TSupport` or `Tsupport`?
 | "Add" :: "TSupport" :: s          => "TSupport" :: fixAbbreviation s
 | "add" :: "TSupport" :: s          => "tsupport" :: fixAbbreviation s
 | "add" :: "_" :: "tsupport" :: s   => "tsupport" :: fixAbbreviation s
 | "Add" :: "Indicator" :: s         => "Indicator" :: fixAbbreviation s
 | "add" :: "Indicator" :: s         => "indicator" :: fixAbbreviation s
 | "add" :: "_" :: "indicator" :: s  => "indicator" :: fixAbbreviation s
--- TODO: Bug in `splitCase` splits like ["LEH", "Pow"] instead of ["LE", "HPow"].
--- Currently we just fix these cases manually.
-| "HNsmul" :: s                     => "HMul" :: fixAbbreviation s
-| "hnsmul" :: s                     => "hmul" :: fixAbbreviation s
-| "Zero" :: "LEH" :: s              => "NonnegH" :: fixAbbreviation s
-| "Zero" :: "LTH" :: s              => "PosH" :: fixAbbreviation s
+-- the capitalization heuristic of `applyNameDict` doesn't work in the following cases
+| "Smul"  :: s                      => "SMul" :: fixAbbreviation s
+| "HSmul" :: s                      => "HSMul" :: fixAbbreviation s
+| "hSmul" :: s                      => "hSMul" :: fixAbbreviation s
 | x :: s                            => x :: fixAbbreviation s
 | []                                => []
 

test/toAdditive.lean

@@ -222,7 +222,7 @@ def checkGuessName (s t : String) : Elab.Command.CommandElabM Unit :=
 
 run_cmd
   checkGuessName "HMul_Eq_LEOne_Conj₂MulLT'" "HAdd_Eq_Nonpos_Conj₂AddLT'"
-  checkGuessName "OneMulSmulInvDivPow"       "ZeroAddVaddNegSubNsmul"
+  checkGuessName "OneMulSMulInvDivPow"       "ZeroAddVAddNegSubSMul"
   checkGuessName "ProdFinprodNpowZpow"       "SumFinsumNsmulZsmul"
 
   -- The current design swaps all instances of `Comm`+`Add` in order to have
@@ -247,14 +247,9 @@ run_cmd
   checkGuessName "leftCancelMonoid" "addLeftCancelMonoid"
 
   checkGuessName "LTOne_LEOne_OneLE_OneLT" "Neg_Nonpos_Nonneg_Pos"
-
-  -- The current design splits this as `LTH, Mul, HPow, LEH, Div` before it translates.
-  -- This is kinda a bug.
-  checkGuessName "LTHMulHPowLEHDiv" "LTHAddHMulLEHSub"
+  checkGuessName "LTHMulHPowLEHDiv" "LTHAddHSMulLEHSub"
   checkGuessName "OneLEHMul" "NonnegHAdd"
-
-  -- -- TODO: This fails at the moment:
-  -- checkGuessName "OneLTHPow" "PosHMul"
+  checkGuessName "OneLTHPow" "PosHSMul"
 
 end guessName