Invoking monoid stuff in group definition

Stream: new members

[Iocta]

Is there something wrong with MyAdditiveGroup2? The add_neg and neg_add components at the bottom of this segment don't have the types I was expecting: it seems to want me to prove that all a b are each others inverses.

structure MyAddMonoid where
  zero : α
  add : α → α → α
  add_zero a : add a zero = a
  zero_add a : add zero a = a

def NatAdditiveMonoid : @MyAddMonoid ℕ :=
  ⟨(0:ℕ), HAdd.hAdd, add_zero, zero_add⟩

structure MyMultiplicativeMonoid where
  one : α
  mul : α → α → α
  mul_one a : mul a one = a
  one_mul a : mul one a = a

structure MyAdditiveGroup1 where
  zero : α
  add : α → α → α
  add_zero a : add a zero = a
  zero_add a : add zero a = a
  neg : α → α
  add_neg a : add a (neg a) = zero
  neg_add a : add (neg a) a = zero


structure MyAdditiveGroup2 where
  additive_monoid : @MyAddMonoid α
  neg : α → α
  add_neg a : additive_monoid.add a (neg a) = zero
  neg_add a : additive_monoid.add (neg a) a = zero

def MyAdditiveGroup.add {s : @MyAdditiveGroup1 α} (a b : α) : α :=
  s.add a b

def MyAdditiveGroup.sub {s : @MyAdditiveGroup1 α} (a b : α) : α :=
  s.add a (s.neg b)

theorem int_add_neg (a : ℤ) : a + (-a) = 0 := by
  linarith

theorem int_neg_add (a : ℤ) : -a + a = 0 := by
  linarith

def MyIntAdditiveGroup1 : @MyAdditiveGroup1 ℤ :=
  ⟨(0:ℤ), HAdd.hAdd, add_zero, zero_add, Neg.neg, int_add_neg, int_neg_add⟩

def MyIntAdditiveGroup2 : @MyAdditiveGroup2 ℤ :=
  ⟨⟨(0:ℤ), HAdd.hAdd, add_zero, zero_add⟩, Neg.neg, (by {
/-
α : Type
⊢ ∀ {zero : ℤ} (a : ℤ), { zero := 0, add := HAdd.hAdd, add_zero := ⋯, zero_add := ⋯ }.add a (-a) = zero
-/

  }), sorry⟩

[Eric Wieser]

set_option autoImplicit false