fix(algebra/pi_instances): improve definitions of pi.* (#3116)

The new `test/pi_simp.lean` fails with current `master`. Note that
this is a workaround, not a proper fix for `tactic.pi_instance`.

See also [Zulip chat](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60id.60.20in.20pi_instances)

Also use `@[to_additive]` to generate additive definitions, add ordered multiplicative monoids, and add `semimodule (Π i, f i) (Π, g i)`.

Author: urkud

src/algebra/category/Group/biproducts.lean

@@ -54,8 +54,8 @@ to the cartesian product of those groups.
 def lift (s : cone F) :
   s.X ⟶ AddCommGroup.of (Π j, F.obj j) :=
 { to_fun := λ x j, s.π.app j x,
-  map_zero' := by { ext, dsimp, simp, refl, },
-  map_add' := λ x y, by { ext, dsimp, simp, refl, }, }
+  map_zero' := by { ext, simp },
+  map_add' := λ x y, by { ext, simp }, }
 
 @[simp] lemma lift_apply (s : cone F) (x : s.X) (j : J) : (lift F s) x j = s.π.app j x := rfl
 

src/algebra/pi_instances.lean

@@ -11,6 +11,16 @@ open_locale big_operators
 
 /-!
 # Pi instances for algebraic structures
+
+## Implementation notes
+
+We don't use `by pi_instance` directly because currently instances generated by this tactic have
+slightly wrong definitions (extra `id`s and `group.mul` instead of `has_mul.mul`). These little
+bugs prevent Lean from applying a `simp` lemma about `pi.has_one` to `1` coming from `pi.group`.
+
+## TODO
+
+Properly fix `tactic.pi_instance`.
 -/
 
 namespace pi
@@ -19,64 +29,99 @@ variable {I : Type u}     -- The indexing type
 variable {f : I → Type v} -- The family of types already equipped with instances
 variables (x y : Π i, f i) (i : I)
 
-instance has_zero [∀ i, has_zero $ f i] : has_zero (Π i : I, f i) := ⟨λ i, 0⟩
-@[simp] lemma zero_apply [∀ i, has_zero $ f i] : (0 : Π i, f i) i = 0 := rfl
+@[to_additive] instance has_one [∀ i, has_one $ f i] : has_one (Π i : I, f i) := ⟨λ _, 1⟩
+@[simp, to_additive] lemma one_apply [∀ i, has_one $ f i] : (1 : Π i, f i) i = 1 := rfl
+
+@[to_additive]
+instance has_mul [∀ i, has_mul $ f i] : has_mul (Π i : I, f i) := ⟨λ f g i, f i * g i⟩
+@[simp, to_additive] lemma mul_apply [∀ i, has_mul $ f i] : (x * y) i = x i * y i := rfl
+
+@[to_additive] instance has_inv [∀ i, has_inv $ f i] : has_inv (Π i : I, f i) := ⟨λ f i, (f i)⁻¹⟩
+@[simp, to_additive] lemma inv_apply [∀ i, has_inv $ f i] : x⁻¹ i = (x i)⁻¹ := rfl
+
+instance has_scalar {α : Type*} [Π i, has_scalar α $ f i] :
+  has_scalar α (Π i : I, f i) :=
+⟨λ s x, λ i, s • (x i)⟩
+
+@[simp] lemma smul_apply {α : Type*} [Π i, has_scalar α $ f i] (s : α) : (s • x) i = s • x i := rfl
+
+instance has_scalar' {g : I → Type*} [Π i, has_scalar (f i) (g i)] :
+  has_scalar (Π i, f i) (Π i : I, g i) :=
+⟨λ s x, λ i, (s i) • (x i)⟩
+
+@[simp]
+lemma smul_apply' {g : I → Type*} [∀ i, has_scalar (f i) (g i)] (s : Π i, f i) (x : Π i, g i) :
+  (s • x) i = s i • x i :=
+rfl
+
+@[to_additive add_semigroup]
+instance semigroup [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
+by refine_struct { mul := (*), .. }; tactic.pi_instance_derive_field
 
-instance has_one [∀ i, has_one $ f i] : has_one (Π i : I, f i) := ⟨λ i, 1⟩
-@[simp] lemma one_apply [∀ i, has_one $ f i] : (1 : Π i, f i) i = 1 := rfl
+@[to_additive add_comm_semigroup]
+instance comm_semigroup [∀ i, comm_semigroup $ f i] : comm_semigroup (Π i : I, f i) :=
+by refine_struct { mul := (*), .. }; tactic.pi_instance_derive_field
 
-attribute [to_additive] pi.has_one
-attribute [to_additive] pi.one_apply
+@[to_additive add_monoid]
+instance monoid [∀ i, monoid $ f i] : monoid (Π i : I, f i) :=
+by refine_struct { one := (1 : Π i, f i), mul := (*), .. }; tactic.pi_instance_derive_field
 
-instance has_add [∀ i, has_add $ f i] : has_add (Π i : I, f i) := ⟨λ x y, λ i, x i + y i⟩
-@[simp] lemma add_apply [∀ i, has_add $ f i] : (x + y) i = x i + y i := rfl
+@[to_additive add_comm_monoid]
+instance comm_monoid [∀ i, comm_monoid $ f i] : comm_monoid (Π i : I, f i) :=
+by refine_struct { one := (1 : Π i, f i), mul := (*), .. }; tactic.pi_instance_derive_field
 
-instance has_mul [∀ i, has_mul $ f i] : has_mul (Π i : I, f i) := ⟨λ x y, λ i, x i * y i⟩
-@[simp] lemma mul_apply [∀ i, has_mul $ f i] : (x * y) i = x i * y i := rfl
+@[to_additive add_group]
+instance group [∀ i, group $ f i] : group (Π i : I, f i) :=
+by refine_struct { one := (1 : Π i, f i), mul := (*), inv := has_inv.inv, .. };
+  tactic.pi_instance_derive_field
 
-attribute [to_additive] pi.has_mul
-attribute [to_additive] pi.mul_apply
+@[to_additive add_comm_group]
+instance comm_group [∀ i, comm_group $ f i] : comm_group (Π i : I, f i) :=
+by refine_struct { one := (1 : Π i, f i), mul := (*), inv := has_inv.inv, .. };
+  tactic.pi_instance_derive_field
 
-instance has_inv [∀ i, has_inv $ f i] : has_inv (Π i : I, f i) := ⟨λ x, λ i, (x i)⁻¹⟩
-@[simp] lemma inv_apply [∀ i, has_inv $ f i] : x⁻¹ i = (x i)⁻¹ := rfl
+instance mul_zero_class [Π i, mul_zero_class $ f i] : mul_zero_class (Π i : I, f i) :=
+by refine_struct { zero := (0 : Π i, f i), mul := (*), .. }; tactic.pi_instance_derive_field
 
-instance has_neg [∀ i, has_neg $ f i] : has_neg (Π i : I, f i) := ⟨λ x, λ i, -(x i)⟩
-@[simp] lemma neg_apply [∀ i, has_neg $ f i] : (-x) i = -x i := rfl
+instance distrib [Π i, distrib $ f i] : distrib (Π i : I, f i) :=
+by refine_struct { add := (+), mul := (*), .. }; tactic.pi_instance_derive_field
 
-attribute [to_additive] pi.has_inv
-attribute [to_additive] pi.inv_apply
+instance semiring [∀ i, semiring $ f i] : semiring (Π i : I, f i) :=
+by refine_struct { zero := (0 : Π i, f i), one := 1, add := (+), mul := (*), .. };
+  tactic.pi_instance_derive_field
 
-instance has_scalar {α : Type*} [∀ i, has_scalar α $ f i] : has_scalar α (Π i : I, f i) := ⟨λ s x, λ i, s • (x i)⟩
-@[simp] lemma smul_apply {α : Type*} [∀ i, has_scalar α $ f i] (s : α) : (s • x) i = s • x i := rfl
+instance ring [∀ i, ring $ f i] : ring (Π i : I, f i) :=
+by refine_struct { zero := (0 : Π i, f i), one := 1, add := (+), mul := (*),
+  neg := has_neg.neg, .. }; tactic.pi_instance_derive_field
 
-instance semigroup          [∀ i, semigroup          $ f i] : semigroup          (Π i : I, f i) := by pi_instance
-instance comm_semigroup     [∀ i, comm_semigroup     $ f i] : comm_semigroup     (Π i : I, f i) := by pi_instance
-instance monoid             [∀ i, monoid             $ f i] : monoid             (Π i : I, f i) := by pi_instance
-instance comm_monoid        [∀ i, comm_monoid        $ f i] : comm_monoid        (Π i : I, f i) := by pi_instance
-instance group              [∀ i, group              $ f i] : group              (Π i : I, f i) := by pi_instance
-instance comm_group         [∀ i, comm_group         $ f i] : comm_group         (Π i : I, f i) := by pi_instance
-instance add_semigroup      [∀ i, add_semigroup      $ f i] : add_semigroup      (Π i : I, f i) := by pi_instance
-instance add_comm_semigroup [∀ i, add_comm_semigroup $ f i] : add_comm_semigroup (Π i : I, f i) := by pi_instance
-instance add_monoid         [∀ i, add_monoid         $ f i] : add_monoid         (Π i : I, f i) := by pi_instance
-instance add_comm_monoid    [∀ i, add_comm_monoid    $ f i] : add_comm_monoid    (Π i : I, f i) := by pi_instance
-instance add_group          [∀ i, add_group          $ f i] : add_group          (Π i : I, f i) := by pi_instance
-instance add_comm_group     [∀ i, add_comm_group     $ f i] : add_comm_group     (Π i : I, f i) := by pi_instance
-instance semiring           [∀ i, semiring           $ f i] : semiring           (Π i : I, f i) := by pi_instance
-instance ring               [∀ i, ring               $ f i] : ring               (Π i : I, f i) := by pi_instance
-instance comm_ring          [∀ i, comm_ring          $ f i] : comm_ring          (Π i : I, f i) := by pi_instance
+instance comm_ring [∀ i, comm_ring $ f i] : comm_ring (Π i : I, f i) :=
+by refine_struct { zero := (0 : Π i, f i), one := 1, add := (+), mul := (*),
+  neg := has_neg.neg, .. }; tactic.pi_instance_derive_field
 
-instance mul_action (α) {m : monoid α} [∀ i, mul_action α $ f i] :
+instance mul_action (α) {m : monoid α} [Π i, mul_action α $ f i] :
   @mul_action α (Π i : I, f i) m :=
-{ smul := λ c f i, c • f i,
+{ smul := (•),
   mul_smul := λ r s f, funext $ λ i, mul_smul _ _ _,
   one_smul := λ f, funext $ λ i, one_smul α _ }
 
+instance mul_action' {g : I → Type*} {m : Π i, monoid (f i)} [Π i, mul_action (f i) (g i)] :
+  @mul_action (Π i, f i) (Π i : I, g i) (@pi.monoid I f m) :=
+{ smul := (•),
+  mul_smul := λ r s f, funext $ λ i, mul_smul _ _ _,
+  one_smul := λ f, funext $ λ i, one_smul _ _ }
+
 instance distrib_mul_action (α) {m : monoid α} {n : ∀ i, add_monoid $ f i} [∀ i, distrib_mul_action α $ f i] :
   @distrib_mul_action α (Π i : I, f i) m (@pi.add_monoid I f n) :=
 { smul_zero := λ c, funext $ λ i, smul_zero _,
   smul_add := λ c f g, funext $ λ i, smul_add _ _ _,
   ..pi.mul_action _ }
 
+instance distrib_mul_action' {g : I → Type*} {m : Π i, monoid (f i)} {n : Π i, add_monoid $ g i}
+  [Π i, distrib_mul_action (f i) (g i)] :
+  @distrib_mul_action (Π i, f i) (Π i : I, g i) (@pi.monoid I f m) (@pi.add_monoid I g n) :=
+{ smul_add := by { intros, ext x, apply smul_add },
+  smul_zero := by { intros, ext x, apply smul_zero } }
+
 variables (I f)
 
 instance semimodule (α) {r : semiring α} {m : ∀ i, add_comm_monoid $ f i} [∀ i, semimodule α $ f i] :
@@ -87,41 +132,35 @@ instance semimodule (α) {r : semiring α} {m : ∀ i, add_comm_monoid $ f i} [
 
 variables {I f}
 
+instance semimodule' {g : I → Type*} {r : Π i, semiring (f i)} {m : Π i, add_comm_monoid (g i)}
+  [Π i, semimodule (f i) (g i)] :
+  semimodule (Π i, f i) (Π i, g i) :=
+{ add_smul := by { intros, ext1, apply add_smul },
+  zero_smul := by { intros, ext1, apply zero_smul } }
+
+@[to_additive add_left_cancel_semigroup]
 instance left_cancel_semigroup [∀ i, left_cancel_semigroup $ f i] :
   left_cancel_semigroup (Π i : I, f i) :=
-by pi_instance
-
-instance add_left_cancel_semigroup [∀ i, add_left_cancel_semigroup $ f i] :
-  add_left_cancel_semigroup (Π i : I, f i) :=
-by pi_instance
+by refine_struct { mul := (*) }; tactic.pi_instance_derive_field
 
+@[to_additive add_right_cancel_semigroup]
 instance right_cancel_semigroup [∀ i, right_cancel_semigroup $ f i] :
   right_cancel_semigroup (Π i : I, f i) :=
-by pi_instance
-
-instance add_right_cancel_semigroup [∀ i, add_right_cancel_semigroup $ f i] :
-  add_right_cancel_semigroup (Π i : I, f i) :=
-by pi_instance
-
-instance ordered_cancel_comm_monoid [∀ i, ordered_cancel_add_comm_monoid $ f i] :
-  ordered_cancel_add_comm_monoid (Π i : I, f i) :=
-by pi_instance
-
-instance ordered_add_comm_group [∀ i, ordered_add_comm_group $ f i] :
-  ordered_add_comm_group (Π i : I, f i) :=
-{ add_le_add_left := λ x y hxy c i, add_le_add_left (hxy i) _,
-  ..pi.add_comm_group,
+by refine_struct { mul := (*) }; tactic.pi_instance_derive_field
+
+@[to_additive ordered_cancel_add_comm_monoid]
+instance ordered_cancel_comm_monoid [∀ i, ordered_cancel_comm_monoid $ f i] :
+  ordered_cancel_comm_monoid (Π i : I, f i) :=
+by refine_struct { mul := (*), one := (1 : Π i, f i), le := (≤), lt := (<), .. pi.partial_order };
+  tactic.pi_instance_derive_field
+
+@[to_additive ordered_add_comm_group]
+instance ordered_comm_group [∀ i, ordered_comm_group $ f i] :
+  ordered_comm_group (Π i : I, f i) :=
+{ mul_le_mul_left := λ x y hxy c i, mul_le_mul_left' (hxy i),
+  ..pi.comm_group,
   ..pi.partial_order }
 
-attribute [to_additive add_semigroup]              pi.semigroup
-attribute [to_additive add_comm_semigroup]         pi.comm_semigroup
-attribute [to_additive add_monoid]                 pi.monoid
-attribute [to_additive add_comm_monoid]            pi.comm_monoid
-attribute [to_additive add_group]                  pi.group
-attribute [to_additive add_comm_group]             pi.comm_group
-attribute [to_additive add_left_cancel_semigroup]  pi.left_cancel_semigroup
-attribute [to_additive add_right_cancel_semigroup] pi.right_cancel_semigroup
-
 @[simp] lemma sub_apply [∀ i, add_group $ f i] : (x - y) i = x i - y i := rfl
 
 @[to_additive]
@@ -309,16 +348,14 @@ section
 variables {f}
 variables [Π i, semiring (f i)]
 
--- it is somewhat unfortunate that we can't easily use `add_monoid_hom.functions_ext` here
+-- we need `apply`+`convert` because Lean fails to unify different `add_monoid` instances
+-- on `Π i, f i`
 @[ext]
 lemma ring_hom.functions_ext [fintype I] (G : Type*) [semiring G] (g h : (Π i, f i) →+* G)
   (w : ∀ (i : I) (x : f i), g (single i x) = h (single i x)) : g = h :=
 begin
-  ext k,
-  rw [←finset.univ_sum_single k, ring_hom.map_sum, ring_hom.map_sum],
-  apply finset.sum_congr rfl,
-  intros,
-  apply w,
+  apply ring_hom.coe_add_monoid_hom_injective,
+  convert add_monoid_hom.functions_ext _ _ _ _; assumption
 end
 end
 end

src/topology/metric_space/pi_Lp.lean

@@ -221,7 +221,7 @@ protected lemma dist {p : ℝ} {hp : 1 ≤ p} {α : ι → Type*}
 /-- normed group instance on the product of finitely many normed groups, using the `L^p` norm. -/
 instance normed_group [∀i, normed_group (α i)] : normed_group (pi_Lp p hp α) :=
 { norm := λf, (∑ (i : ι), norm (f i) ^ p) ^ (1/p),
-  dist_eq := λ x y, by { simp [pi_Lp.dist, dist_eq_norm], refl },
+  dist_eq := λ x y, by { simp [pi_Lp.dist, dist_eq_norm] },
   .. pi.add_comm_group }
 
 lemma norm_eq {p : ℝ} {hp : 1 ≤ p} {α : ι → Type*}

test/pi_simp.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Yury G. Kudryashov
+-/
+import algebra.pi_instances
+
+/-!
+Test if `simp` can use a lemma about `pi.has_one` to simplify `1` coming from `pi.group`
+-/
+
+variables {I : Type*} {f : Π i : I, Type*}
+
+namespace test
+
+def eval_default [inhabited I] (F : Π i, f i) : f (default I) := F (default I)
+
+@[simp] lemma eval_default_one [inhabited I] [Π i, has_one (f i)] :
+  eval_default (1 : Π i, f i) = 1 := rfl
+
+example [inhabited I] [Π i, group (f i)] (F : Π i, f i) : eval_default (F⁻¹ * F) = 1 := by simp
+
+end test