feat(algebra/to_additive): map pow to smul (#7888)

* Allows `@[to_additive]` to reorder consecutive arguments of specified identifiers.
* This can be specified with the attribute `@[to_additive_reorder n m ...]` to swap arguments `n` and `n+1`, arguments `m` and `m+1` etc. (start counting from 1).
* The only two attributes currently in use are:
```lean
attribute [to_additive_reorder 1] has_pow
attribute [to_additive_reorder 1 4] has_pow.pow
```
* It will  eta-expand all expressions that have as head a declaration with attribute `to_additive_reorder` until they have the required number of arguments. This is required to correctly deal with partially applied terms.
* Hack: if the first two arguments are reordered, then the first two universe variables are also reordered (this happens to be the correct behavior for `has_pow` and `has_pow.pow`). It might be cleaner to have a separate attribute for that, but that given the low amount of times that I expect that we use `to_additive_reorder`, this seems unnecessary.
* This PR also allows the user to write `@[to_additive?]` to trace the generated declaration.



Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>

src/algebra/big_operators/basic.lean

@@ -201,12 +201,9 @@ lemma prod_pair [decidable_eq α] {a b : α} (h : a ≠ b) :
   (∏ x in ({a, b} : finset α), f x) = f a * f b :=
 by rw [prod_insert (not_mem_singleton.2 h), prod_singleton]
 
-@[simp, priority 1100] lemma prod_const_one : (∏ x in s, (1 : β)) = 1 :=
+@[simp, priority 1100, to_additive]
+lemma prod_const_one : (∏ x in s, (1 : β)) = 1 :=
 by simp only [finset.prod, multiset.map_const, multiset.prod_repeat, one_pow]
-@[simp, priority 1100] lemma sum_const_zero {β α} {s : finset α} [add_comm_monoid β] :
-  (∑ x in s, (0 : β)) = 0 :=
-@prod_const_one (multiplicative β) _ _ _
-attribute [to_additive] prod_const_one
 
 @[simp, to_additive]
 lemma prod_image [decidable_eq α] {s : finset γ} {g : γ → α} :
@@ -820,15 +817,11 @@ lemma sum_multiset_map_count [decidable_eq α] (s : multiset α)
 @prod_multiset_map_count _ _ _ (multiplicative M) _ f
 attribute [to_additive] prod_multiset_map_count
 
+@[to_additive]
 lemma prod_multiset_count [decidable_eq α] [comm_monoid α] (s : multiset α) :
   s.prod = ∏ m in s.to_finset, m ^ (s.count m) :=
 by { convert prod_multiset_map_count s id, rw map_id }
 
-lemma sum_multiset_count [decidable_eq α] [add_comm_monoid α] (s : multiset α) :
-  s.sum = ∑ m in s.to_finset, s.count m • m :=
-@prod_multiset_count (multiplicative α) _ _ s
-attribute [to_additive] prod_multiset_count
-
 /--
 To prove a property of a product, it suffices to prove that
 the property is multiplicative and holds on factors.

src/algebra/big_operators/ring.lean

@@ -212,6 +212,7 @@ end
 
 /-- A product over `powerset s` is equal to the double product over
 sets of subsets of `s` with `card s = k`, for `k = 1, ... , card s`. -/
+@[to_additive]
 lemma prod_powerset [comm_monoid β] (s : finset α) (f : finset α → β) :
   ∏ t in powerset s, f t = ∏ j in range (card s + 1), ∏ t in powerset_len j s, f t :=
 begin
@@ -224,18 +225,4 @@ begin
   rwa ← hc,
 end
 
-/-- A sum over `powerset s` is equal to the double sum over
-sets of subsets of `s` with `card s = k`, for `k = 1, ... , card s`. -/
-lemma sum_powerset [add_comm_monoid β] (s : finset α) (f : finset α → β) :
-  ∑ t in powerset s, f t = ∑ j in range (card s + 1), ∑ t in powerset_len j s, f t :=
-begin
-  classical,
-  rw [powerset_card_bUnion, sum_bUnion],
-  intros i hi j hj hij,
-  rw [powerset_len_eq_filter, powerset_len_eq_filter, disjoint_filter],
-  intros x hx hc hnc,
-  apply hij,
-  rwa ← hc,
-end
-
 end finset

src/algebra/group/to_additive.lean

@@ -21,13 +21,11 @@ Usage information is contained in the doc string of `to_additive.attr`.
 
 * For structures, automatically generate theorems like `group α ↔
   add_group (additive α)`.
-
-* Rewrite rules for the last part of the name that work in more
-  cases. E.g., we can replace `monoid` with `add_monoid` etc.
 -/
 
 namespace to_additive
-open tactic exceptional
+open tactic
+setup_tactic_parser
 
 section performance_hack -- see Note [user attribute parameters]
 
@@ -60,10 +58,8 @@ end performance_hack
 
 section extra_attributes
 
-setup_tactic_parser
-
 /--
-n attribute that tells `@[to_additive]` that certain arguments of this definition are not
+An attribute that tells `@[to_additive]` that certain arguments of this definition are not
 involved when using `@[to_additive]`.
 This helps the heuristic of `@[to_additive]` by also transforming definitions if `ℕ` or another
 fixed type occurs as one of these arguments.
@@ -81,6 +77,30 @@ meta def ignore_args_attr : user_attribute (name_map $ list ℕ) (list ℕ) :=
       mk_name_map, []⟩,
   parser    := (lean.parser.small_nat)* }
 
+/--
+An attribute that stores all the declarations that needs their arguments reordered when
+applying `@[to_additive]`. Currently, we only support swapping consecutive arguments.
+The list of the natural numbers contains the positions of the first of the two arguments
+to be swapped.
+Example: `@[to_additive_reorder 1 4]` swaps the first two arguments and the arguments in
+positions 4 and 5.
+-/
+@[user_attribute]
+meta def reorder_attr : user_attribute (name_map $ list ℕ) (list ℕ) :=
+{ name      := `to_additive_reorder,
+  descr     :=
+    "Auxiliary attribute for `to_additive` that stores arguments that need to be reordered.",
+  cache_cfg :=
+    ⟨λ ns, ns.mfoldl
+      (λ dict n, do
+        param ← reorder_attr.get_param_untyped n, -- see Note [user attribute parameters]
+        return $ dict.insert n (param.to_list expr.to_nat).iget)
+      mk_name_map, []⟩,
+  parser    := do
+    l ← (lean.parser.small_nat)*,
+    guard (l.all (≠ 0)) <|> exceptional.fail "The reorder positions must be positive",
+    return l }
+
 end extra_attributes
 
 /-- A command that can be used to have future uses of `to_additive` change the `src` namespace
@@ -101,10 +121,18 @@ do let n := src.mk_string "_to_additive",
    aux_attr.set n tgt tt
 
 /-- `value_type` is the type of the arguments that can be provided to `to_additive`.
-`to_additive.parser` parses the provided arguments into `name` for the target and an
-optional doc string. -/
+`to_additive.parser` parses the provided arguments:
+* `replace_all`: replace all multiplicative declarations, do not use the heuristic.
+* `trace`: output the generated additive declaration.
+* `tgt : name`: the name of the target (the additive declaration).
+* `doc`: an optional doc string.
+-/
 @[derive has_reflect, derive inhabited]
-structure value_type : Type := (replace_all : bool) (tgt : name) (doc : option string)
+structure value_type : Type :=
+(replace_all : bool)
+(trace : bool)
+(tgt : name)
+(doc : option string)
 
 /-- `add_comm_prefix x s` returns `"comm_" ++ s` if `x = tt` and `s` otherwise. -/
 meta def add_comm_prefix : bool → string → string
@@ -166,18 +194,18 @@ meta def target_name (src tgt : name) (dict : name_map name) : tactic name :=
 Give the desired additive name explicitly using `@[to_additive additive_name]`. ")
   else pure res)
 
-setup_tactic_parser
-/-- the parser for the arguments to `to_additive` -/
+/-- the parser for the arguments to `to_additive`. -/
 meta def parser : lean.parser value_type :=
 do
-  b ← option.is_some <$> (tk "!")?,
+  bang ← option.is_some <$> (tk "!")?,
+  ques ← option.is_some <$> (tk "?")?,
   tgt ← ident?,
   e ← texpr?,
   doc ← match e with
       | some pe := some <$> ((to_expr pe >>= eval_expr string) : tactic string)
       | none := pure none
       end,
-  return ⟨b, tgt.get_or_else name.anonymous, doc⟩
+  return ⟨bang, ques, tgt.get_or_else name.anonymous, doc⟩
 
 private meta def proceed_fields_aux (src tgt : name) (prio : ℕ) (f : name → tactic (list string)) :
   command :=
@@ -365,13 +393,14 @@ protected meta def attr : user_attribute unit value_type :=
     val ← attr.get_param src,
     dict ← aux_attr.get_cache,
     ignore ← ignore_args_attr.get_cache,
+    reorder ← reorder_attr.get_cache,
     tgt ← target_name src val.tgt dict,
     aux_attr.set src tgt tt,
     let dict := dict.insert src tgt,
     if env.contains tgt
     then proceed_fields env src tgt prio
     else do
-      transform_decl_with_prefix_dict dict val.replace_all ignore src tgt
+      transform_decl_with_prefix_dict dict val.replace_all val.trace ignore reorder src tgt
         [`reducible, `_refl_lemma, `simp, `instance, `refl, `symm, `trans, `elab_as_eliminator,
          `no_rsimp, `measurability],
       mwhen (has_attribute' `simps src)