refactor(algebra/ordered_group): multiplicative versions of ordered m…

…onoids/groups (#2844)

This PR defines multiplicative versions of ordered monoids and groups. It also lints the file.

src/algebra/group/defs.lean

@@ -207,13 +207,19 @@ class comm_monoid (M : Type u) extends monoid M, comm_semigroup M
 class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M
 attribute [to_additive add_comm_monoid] comm_monoid
 
+/-- A monoid in which multiplication is left-cancellative. -/
+@[protect_proj, ancestor left_cancel_semigroup monoid]
+class left_cancel_monoid (M : Type u) extends left_cancel_semigroup M, monoid M
+
 /-- An additive monoid in which addition is left-cancellative.
 Main examples are `ℕ` and groups. This is the right typeclass for many sum lemmas, as having a zero
 is useful to define the sum over the empty set, so `add_left_cancel_semigroup` is not enough. -/
-@[protect_proj]
+@[protect_proj, ancestor add_left_cancel_semigroup add_monoid]
 class add_left_cancel_monoid (M : Type u) extends add_left_cancel_semigroup M, add_monoid M
 -- TODO: I found 1 (one) lemma assuming `[add_left_cancel_monoid]`.
--- Should we port more lemmas to this typeclass? Should we add a multiplicative version?
+-- Should we port more lemmas to this typeclass?
+
+attribute [to_additive add_left_cancel_monoid] left_cancel_monoid
 
 /-- A `group` is a `monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`. -/
 @[protect_proj, ancestor monoid has_inv]

src/algebra/group/to_additive.lean

@@ -107,17 +107,25 @@ do let n := src.mk_string "_to_additive",
 @[derive has_reflect, derive inhabited]
 structure value_type := (tgt : name) (doc : option string)
 
-/-- Dictionary of words used by `to_additive.guess_name` to autogenerate
-names. -/
-meta def tokens_dict : native.rb_map string string :=
-native.rb_map.of_list $
-[("mul", "add"), ("one", "zero"), ("inv", "neg"), ("prod", "sum")]
+/-- Dictionary used by `to_additive.guess_name` to autogenerate names. -/
+meta def tr : list string → list string
+| ("one" :: "le" :: s) := "nonneg" :: tr s
+| ("one" :: "lt" :: s) := "pos"    :: tr s
+| ("le" :: "one" :: s) := "nonpos" :: tr s
+| ("lt" :: "one" :: s) := "neg"    :: tr s
+| ("mul" :: s)         := "add"    :: tr s
+| ("inv" :: s)         := "neg"    :: tr s
+| ("div" :: s)         := "sub"    :: tr s
+| ("one" :: s)         := "zero"   :: tr s
+| ("prod" :: s)        := "sum"    :: tr s
+| (x :: s)             := (x :: tr s)
+| []                   := []
 
 /-- Autogenerate target name for `to_additive`. -/
 meta def guess_name : string → string :=
-string.map_tokens '_' $
 string.map_tokens ''' $
-λ s, (tokens_dict.find s).get_or_else s
+λ s, string.intercalate (string.singleton '_') $
+tr (s.split_on '_')
 
 meta def target_name (src tgt : name) (dict : name_map name) : tactic name :=
 (if tgt.get_prefix ≠ name.anonymous -- `tgt` is a full name