feat(attribute/to_additive): apply to_additive recursively

algebra/big_operators.lean

@@ -27,7 +27,6 @@ variables {s s₁ s₂ : finset α} {a : α} {f g : α → β}
 /-- `prod s f` is the product of `f x` as `x` ranges over the elements of the finite set `s`. -/
 @[to_additive finset.sum]
 protected def prod [comm_monoid β] (s : finset α) (f : α → β) : β := (s.1.map f).prod
-attribute [to_additive finset.sum.equations._eqn_1] finset.prod.equations._eqn_1
 
 @[to_additive finset.sum_eq_fold]
 theorem prod_eq_fold [comm_monoid β] (s : finset α) (f : α → β) : s.prod f = s.fold (*) 1 f := rfl

algebra/group.lean

@@ -13,6 +13,23 @@ section pending_1857
 section transport
 open tactic
 
+meta def prefixes : name → list name
+| (name.mk_string s p) := p :: prefixes p
+| name.anonymous := []
+| _ := []
+
+meta def set_to_additive_attr : name_set → name → name → name_map name → tactic (name_map name)
+| pre src tgt dict :=
+(get_decl tgt >> pure dict) <|>
+do d ← get_decl src,
+   let ns := (d.value.list_constant).filter
+     (λ n, ∃ p ∈ prefixes n, pre.contains p),
+   dict ← ns.to_list.mfoldl (λ (dict : name_map _) n,
+     set_to_additive_attr (pre.insert n) n (n.update_prefix tgt) dict ) dict,
+   transport_with_dict dict src tgt,
+   let dict := dict.insert src tgt,
+   pure dict
+
 @[user_attribute]
 meta def to_additive_attr : user_attribute (name_map name) name :=
 { name      := `to_additive,
@@ -22,11 +39,16 @@ meta def to_additive_attr : user_attribute (name_map name) name :=
     pure $ dict.insert n val) mk_name_map, []⟩,
   parser    := lean.parser.ident,
   after_set := some $ λ src _ _, do
-    env ← get_env,
-    dict ← to_additive_attr.get_cache,
     tgt ← to_additive_attr.get_param src,
     (get_decl tgt >> skip) <|>
-      transport_with_dict dict src tgt }
+      do dict ← to_additive_attr.get_cache,
+         dict ← set_to_additive_attr (name_set.of_list [src]) src tgt dict,
+         ls ← get_eqn_lemmas_for tt src,
+         dict ← ls.mfoldl (λ (dict : name_map _) src',
+           do let tgt' := (src'.replace_prefix src tgt),
+              transport_with_dict dict src' tgt',
+              pure $ dict.insert src' tgt') dict,
+         dict.to_list.mmap' $ λ ⟨src,tgt⟩, to_additive_attr.set src tgt tt }
 
 end transport
 
@@ -282,9 +304,6 @@ instance [semigroup α] : monoid (with_one α) :=
   one_mul   := (option.lift_or_get_is_left_id _).1,
   mul_one   := (option.lift_or_get_is_right_id _).1 }
 
-attribute [to_additive with_zero.add_monoid._proof_1] with_one.monoid._proof_1
-attribute [to_additive with_zero.add_monoid._proof_2] with_one.monoid._proof_2
-attribute [to_additive with_zero.add_monoid._proof_3] with_one.monoid._proof_3
 attribute [to_additive with_zero.add_monoid] with_one.monoid
 
 instance [semigroup α] : mul_zero_class (with_zero α) :=

data/finsupp.lean

@@ -224,7 +224,6 @@ f.support.sum (λa, g a (f a))
 @[to_additive finsupp.sum]
 def prod [has_zero β] [comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ :=
 f.support.prod (λa, g a (f a))
-attribute [to_additive finsupp.sum.equations._eqn_1] finsupp.prod.equations._eqn_1
 
 @[to_additive finsupp.sum_map_range_index]
 lemma prod_map_range_index [has_zero β₁] [has_zero β₂] [comm_monoid γ] [decidable_eq β₂]

data/list/basic.lean

@@ -1289,7 +1289,6 @@ end
 /-- Product of a list. `prod [a, b, c] = ((1 * a) * b) * c` -/
 @[to_additive list.sum]
 def prod [has_mul α] [has_one α] : list α → α := foldl (*) 1
-attribute [to_additive list.sum.equations._eqn_1] list.prod.equations._eqn_1
 
 section monoid
 variables [monoid α] {l l₁ l₂ : list α} {a : α}

data/multiset.lean

@@ -693,7 +693,6 @@ theorem foldl_swap (f : β → α → β) (H : right_commutative f) (b : β) (s
   `prod {a, b, c} = a * b * c` -/
 def prod [comm_monoid α] : multiset α → α :=
 foldr (*) (λ x y z, by simp [mul_left_comm]) 1
-attribute [to_additive multiset.sum._proof_1] prod._proof_1
 attribute [to_additive multiset.sum] prod
 
 @[to_additive multiset.sum_eq_foldr]

group_theory/coset.lean

@@ -10,11 +10,9 @@ variable {α : Type*}
 
 @[to_additive left_add_coset]
 def left_coset [has_mul α] (a : α) (s : set α) : set α := (λ x, a * x) '' s
-attribute [to_additive left_add_coset.equations._eqn_1] left_coset.equations._eqn_1
 
 @[to_additive right_add_coset]
 def right_coset [has_mul α] (s : set α) (a : α) : set α := (λ x, x * a) '' s
-attribute [to_additive right_add_coset.equations._eqn_1] right_coset.equations._eqn_1
 
 local infix ` *l `:70 := left_coset
 local infix ` +l `:70 := left_add_coset
@@ -151,22 +149,18 @@ def left_rel [group α] (s : set α) [is_subgroup s] : setoid α :=
   assume x y z hxy hyz,
   have x⁻¹ * y * (y⁻¹ * z) ∈ s, from is_submonoid.mul_mem hxy hyz,
   by simpa [mul_assoc] using this⟩
-attribute [to_additive quotient_add_group.left_rel._proof_1] left_rel._proof_1
 attribute [to_additive quotient_add_group.left_rel] left_rel
-attribute [to_additive quotient_add_group.left_rel.equations._eqn_1] left_rel.equations._eqn_1
 
 /-- `quotient s` is the quotient type representing the left cosets of `s`.
   If `s` is a normal subgroup, `quotient s` is a group -/
 def quotient [group α] (s : set α) [is_subgroup s] : Type* := quotient (left_rel s)
 attribute [to_additive quotient_add_group.quotient] quotient
-attribute [to_additive quotient_add_group.quotient.equations._eqn_1] quotient.equations._eqn_1
 
 variables [group α] {s : set α} [is_subgroup s]
 
 @[to_additive quotient_add_group.mk]
 def mk (a : α) : quotient s :=
 quotient.mk' a
-attribute [to_additive quotient_add_group.mk.equations._eqn_1] mk.equations._eqn_1
 
 @[elab_as_eliminator, elab_strategy, to_additive quotient_add_group.induction_on]
 lemma induction_on {C : quotient s → Prop} (x : quotient s)
@@ -176,7 +170,6 @@ attribute [elab_as_eliminator, elab_strategy] quotient_add_group.induction_on
 
 @[to_additive quotient_add_group.has_coe]
 instance : has_coe α (quotient s) := ⟨mk⟩
-attribute [to_additive quotient_add_group.has_coe.equations._eqn_1] has_coe.equations._eqn_1
 
 @[elab_as_eliminator, elab_strategy, to_additive quotient_add_group.induction_on']
 lemma induction_on' {C : quotient s → Prop} (x : quotient s)
@@ -187,7 +180,6 @@ attribute [elab_as_eliminator, elab_strategy] quotient_add_group.induction_on'
 @[to_additive quotient_add_group.inhabited]
 instance [group α] (s : set α) [is_subgroup s] : inhabited (quotient s) :=
 ⟨((1 : α) : quotient s)⟩
-attribute [to_additive quotient_add_group.inhabited.equations._eqn_1] inhabited.equations._eqn_1
 
 @[to_additive quotient_add_group.eq]
 protected lemma eq {a b : α} : (a : quotient s) = b ↔ a⁻¹ * b ∈ s :=
@@ -209,16 +201,7 @@ def left_coset_equiv_subgroup (g : α) : left_coset g s ≃ s :=
  λ x, ⟨g * x.1, x.1, x.2, rfl⟩,
  λ ⟨x, hx⟩, subtype.eq $ by simp,
  λ ⟨g, hg⟩, subtype.eq $ by simp⟩
-attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._match_2] left_coset_equiv_subgroup._match_2
-attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._match_1] left_coset_equiv_subgroup._match_1
-attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._proof_4] left_coset_equiv_subgroup._proof_4
-attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._proof_3] left_coset_equiv_subgroup._proof_3
-attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._proof_2] left_coset_equiv_subgroup._proof_2
-attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._proof_1] left_coset_equiv_subgroup._proof_1
 attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup] left_coset_equiv_subgroup
-attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup.equations._eqn_1] left_coset_equiv_subgroup.equations._eqn_1
-attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._match_1.equations._eqn_1] left_coset_equiv_subgroup._match_1.equations._eqn_1
-attribute [to_additive is_add_subgroup.left_add_coset_equiv_subgroup._match_2.equations._eqn_1] left_coset_equiv_subgroup._match_2.equations._eqn_1
 
 noncomputable def group_equiv_quotient_times_subgroup (hs : is_subgroup s) :
   α ≃ (quotient s × s) :=
@@ -234,9 +217,6 @@ calc α ≃ Σ L : quotient s, {x : α // (x : quotient s)= L} :
   equiv.sigma_congr_right (λ L, left_coset_equiv_subgroup _)
     ... ≃ (quotient s × s) :
   equiv.sigma_equiv_prod _ _
-attribute [to_additive is_add_subgroup.add_group_equiv_quotient_times_subgroup._proof_2] group_equiv_quotient_times_subgroup._proof_2
-attribute [to_additive is_add_subgroup.add_group_equiv_quotient_times_subgroup._proof_1] group_equiv_quotient_times_subgroup._proof_1
 attribute [to_additive is_add_subgroup.add_group_equiv_quotient_times_subgroup] group_equiv_quotient_times_subgroup
-attribute [to_additive is_add_subgroup.add_group_equiv_quotient_times_subgroup.equations._eqn_1] group_equiv_quotient_times_subgroup.equations._eqn_1
 
-end is_subgroup
+end is_subgroup

group_theory/quotient_group.lean

@@ -37,32 +37,18 @@ instance : group (quotient N) :=
     end),
   mul_left_inv := λ a, quotient.induction_on' a
     (λ a, congr_arg mk (mul_left_inv a)) }
-attribute [to_additive quotient_add_group.add_group._proof_6] quotient_group.group._proof_6
-attribute [to_additive quotient_add_group.add_group._proof_5] quotient_group.group._proof_5
-attribute [to_additive quotient_add_group.add_group._proof_4] quotient_group.group._proof_4
-attribute [to_additive quotient_add_group.add_group._proof_3] quotient_group.group._proof_3
-attribute [to_additive quotient_add_group.add_group._proof_2] quotient_group.group._proof_2
-attribute [to_additive quotient_add_group.add_group._proof_1] quotient_group.group._proof_1
+
 attribute [to_additive quotient_add_group.add_group] quotient_group.group
-attribute [to_additive quotient_add_group.quotient.equations._eqn_1] quotient_group.quotient.equations._eqn_1
-attribute [to_additive quotient_add_group.add_group.equations._eqn_1] quotient_group.group.equations._eqn_1
 
 instance : is_group_hom (mk : G → quotient N) := ⟨λ _ _, rfl⟩
 attribute [to_additive quotient_add_group.is_add_group_hom] quotient_group.is_group_hom
-attribute [to_additive quotient_add_group.is_add_group_hom.equations._eqn_1] quotient_group.is_group_hom.equations._eqn_1
 
 instance {G : Type*} [comm_group G] (s : set G) [is_subgroup s] : comm_group (quotient s) :=
 { mul_comm := λ a b, quotient.induction_on₂' a b
     (λ a b, congr_arg mk (mul_comm a b)),
   ..@quotient_group.group _ _ s (normal_subgroup_of_comm_group s) }
-attribute [to_additive quotient_add_group.add_comm_group._proof_6] quotient_group.comm_group._proof_6
-attribute [to_additive quotient_add_group.add_comm_group._proof_5] quotient_group.comm_group._proof_5
-attribute [to_additive quotient_add_group.add_comm_group._proof_4] quotient_group.comm_group._proof_4
-attribute [to_additive quotient_add_group.add_comm_group._proof_3] quotient_group.comm_group._proof_3
-attribute [to_additive quotient_add_group.add_comm_group._proof_2] quotient_group.comm_group._proof_2
-attribute [to_additive quotient_add_group.add_comm_group._proof_1] quotient_group.comm_group._proof_1
+
 attribute [to_additive quotient_add_group.add_comm_group] quotient_group.comm_group
-attribute [to_additive quotient_add_group.add_comm_group.equations._eqn_1] quotient_group.comm_group.equations._eqn_1
 
 @[simp] lemma coe_one : ((1 : G) : quotient N) = 1 := rfl
 @[simp] lemma coe_mul (a b : G) : ((a * b : G) : quotient N) = a * b := rfl
@@ -82,17 +68,14 @@ local notation ` Q ` := quotient N
 instance is_group_hom_quotient_group_mk : is_group_hom (mk : G → Q) :=
 by refine {..}; intros; refl
 attribute [to_additive quotient_add_group.is_add_group_hom_quotient_add_group_mk] quotient_group.is_group_hom_quotient_group_mk
-attribute [to_additive quotient_add_group.is_add_group_hom_quotient_add_group_mk.equations._eqn_1] quotient_group.is_group_hom_quotient_group_mk.equations._eqn_1
 
 def lift (φ : G → H) [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (q : Q) : H :=
 q.lift_on' φ $ assume a b (hab : a⁻¹ * b ∈ N),
 (calc φ a = φ a * 1           : by simp
 ...       = φ a * φ (a⁻¹ * b) : by rw HN (a⁻¹ * b) hab
 ...       = φ (a * (a⁻¹ * b)) : by rw is_group_hom.mul φ a (a⁻¹ * b)
 ...       = φ b               : by simp)
-attribute [to_additive quotient_add_group.lift._proof_1] lift._proof_1
 attribute [to_additive quotient_add_group.lift] lift
-attribute [to_additive quotient_add_group.lift.equations._eqn_1] lift.equations._eqn_1
 
 @[simp] lemma lift_mk {φ : G → H} [is_group_hom φ] (HN : ∀x∈N, φ x = 1) (g : G) :
   lift N φ HN (g : Q) = φ g := rfl
@@ -124,7 +107,6 @@ instance is_group_hom_quotient_lift  :
 ⟨λ q r, quotient.induction_on₂' q r $ λ a b,
   show φ (a * b) = φ a * φ b, from is_group_hom.mul φ a b⟩
 attribute [to_additive quotient_add_group.is_add_group_hom_quotient_lift] quotient_group.is_group_hom_quotient_lift
-attribute [to_additive quotient_add_group.is_add_group_hom_quotient_lift.equations._eqn_1] quotient_group.is_group_hom_quotient_lift.equations._eqn_1
 
 open function is_group_hom
 

group_theory/subgroup.lean

@@ -318,7 +318,6 @@ variables [group α] [group β]
 
 @[to_additive is_add_group_hom.ker]
 def ker (f : α → β) [is_group_hom f] : set α := preimage f (trivial β)
-attribute [to_additive is_add_group_hom.ker.equations._eqn_1] ker.equations._eqn_1
 
 @[to_additive is_add_group_hom.mem_ker]
 lemma mem_ker (f : α → β) [is_group_hom f] {x : α} : x ∈ ker f ↔ f x = 1 :=
@@ -350,38 +349,27 @@ instance image_subgroup (f : α → β) [is_group_hom f] (s : set α) [is_subgro
              ⟨b₁ * b₂, mul_mem hb₁ hb₂, by simp [eq₁, eq₂, mul f]⟩,
   one_mem := ⟨1, one_mem s, one f⟩,
   inv_mem := assume a ⟨b, hb, eq⟩, ⟨b⁻¹, inv_mem hb, by rw inv f; simp *⟩ }
-attribute [to_additive is_add_group_hom.image_add_subgroup._match_1] is_group_hom.image_subgroup._match_1
-attribute [to_additive is_add_group_hom.image_add_subgroup._match_2] is_group_hom.image_subgroup._match_2
-attribute [to_additive is_add_group_hom.image_add_subgroup._match_3] is_group_hom.image_subgroup._match_3
 attribute [to_additive is_add_group_hom.image_add_subgroup] is_group_hom.image_subgroup
-attribute [to_additive is_add_group_hom.image_add_subgroup._match_1.equations._eqn_1] is_group_hom.image_subgroup._match_1.equations._eqn_1
-attribute [to_additive is_add_group_hom.image_add_subgroup._match_2.equations._eqn_1] is_group_hom.image_subgroup._match_2.equations._eqn_1
-attribute [to_additive is_add_group_hom.image_add_subgroup._match_3.equations._eqn_1] is_group_hom.image_subgroup._match_3.equations._eqn_1
-attribute [to_additive is_add_group_hom.image_add_subgroup.equations._eqn_1] is_group_hom.image_subgroup.equations._eqn_1
 
 instance range_subgroup (f : α → β) [is_group_hom f] : is_subgroup (set.range f) :=
 @set.image_univ _ _ f ▸ is_group_hom.image_subgroup f set.univ
 attribute [to_additive is_add_group_hom.range_add_subgroup] is_group_hom.range_subgroup
-attribute [to_additive is_add_group_hom.range_add_subgroup.equations._eqn_1] is_group_hom.range_subgroup.equations._eqn_1
 
 local attribute [simp] one_mem inv_mem mul_mem normal_subgroup.normal
 
 instance preimage (f : α → β) [is_group_hom f] (s : set β) [is_subgroup s] :
   is_subgroup (f ⁻¹' s) :=
 by refine {..}; simp [mul f, one f, inv f, @inv_mem β _ s] {contextual:=tt}
 attribute [to_additive is_add_group_hom.preimage] is_group_hom.preimage
-attribute [to_additive is_add_group_hom.preimage.equations._eqn_1] is_group_hom.preimage.equations._eqn_1
 
 instance preimage_normal (f : α → β) [is_group_hom f] (s : set β) [normal_subgroup s] :
   normal_subgroup (f ⁻¹' s) :=
 ⟨by simp [mul f, inv f] {contextual:=tt}⟩
 attribute [to_additive is_add_group_hom.preimage_normal] is_group_hom.preimage_normal
-attribute [to_additive is_add_group_hom.preimage_normal.equations._eqn_1] is_group_hom.preimage_normal.equations._eqn_1
 
 instance normal_subgroup_ker (f : α → β) [is_group_hom f] : normal_subgroup (ker f) :=
 is_group_hom.preimage_normal f (trivial β)
 attribute [to_additive is_add_group_hom.normal_subgroup_ker] is_group_hom.normal_subgroup_ker
-attribute [to_additive is_add_group_hom.normal_subgroup_ker.equations._eqn_1] is_group_hom.normal_subgroup_ker.equations._eqn_1
 
 lemma inj_of_trivial_ker (f : α → β) [is_group_hom f] (h : ker f = trivial α) :
   function.injective f :=

group_theory/submonoid.lean

@@ -109,11 +109,6 @@ end is_submonoid
 instance subtype.monoid {s : set α} [is_submonoid s] : monoid s :=
 by subtype_instance
 
-attribute [to_additive subtype.add_monoid._proof_1] subtype.monoid._proof_1
-attribute [to_additive subtype.add_monoid._proof_2] subtype.monoid._proof_2
-attribute [to_additive subtype.add_monoid._proof_3] subtype.monoid._proof_3
-attribute [to_additive subtype.add_monoid._proof_4] subtype.monoid._proof_4
-attribute [to_additive subtype.add_monoid._proof_5] subtype.monoid._proof_5
 attribute [to_additive subtype.add_monoid] subtype.monoid
 
 @[simp, to_additive is_add_submonoid.coe_zero]