## Stream: maths

#### Kevin Buzzard (Apr 28 2018 at 01:56):

The additive group add_group in Lean is defined in core Lean, which means it's hard to change. The definition is this:

#### Kevin Buzzard (Apr 28 2018 at 01:56):

@[class, priority 100]
structure add_group : Type u → Type u
fields:
add_group.add_assoc : ∀ {α : Type u} [c : add_group α] (a b c_1 : α), a + b + c_1 = a + (b + c_1)
add_group.zero : Π (α : Type u) [c : add_group α], α
add_group.zero_add : ∀ {α : Type u} [c : add_group α] (a : α), 0 + a = a
add_group.add_zero : ∀ {α : Type u} [c : add_group α] (a : α), a + 0 = a
add_group.neg : Π {α : Type u} [c : add_group α], α → α
add_group.add_left_neg : ∀ {α : Type u} [c : add_group α] (a : α), -a + a = 0


#### Kevin Buzzard (Apr 28 2018 at 01:56):

It's a class, with a bunch of axioms.

#### Kevin Buzzard (Apr 28 2018 at 01:57):

And I think one of them follows from the others

#### Kevin Buzzard (Apr 28 2018 at 01:57):

which means that add_group can be made to go faster, I think.

Is that right?

#### Kevin Buzzard (Apr 28 2018 at 01:57):

I wanted to prove this myself:

#### Kevin Buzzard (Apr 28 2018 at 01:57):

variables {α : Type}
(add : α → α → α)
(add_assoc : ∀ a b c : α, a + b + c = a + (b + c))
(zero : α)
(zero_add : ∀ a : α, 0 + a = a)
(neg : α → α)
(add_left_neg : ∀ a : α, -a + a = 0)
: ∀ a : α, a + 0 = a := sorry


#### Kevin Buzzard (Apr 28 2018 at 01:58):

I just faffed around and cut and pasted that from Lean output, it was pretty painful, it would have been much easier to do in emacs.

#### Kevin Buzzard (Apr 28 2018 at 01:58):

And at the end of it all, it didn't work anyway

#### Kevin Buzzard (Apr 28 2018 at 01:58):

because it doesn't know what + means yet

#### Kevin Buzzard (Apr 28 2018 at 01:59):

I just wanted to make myself a toy abelian group

#### Kevin Buzzard (Apr 28 2018 at 01:59):

but then start taking away the axioms by editing the definition

#### Kevin Buzzard (Apr 28 2018 at 02:02):

All I want to do is to create an additive group but with one axiom missing.

#### Kevin Buzzard (Apr 28 2018 at 02:03):

Is there a trick?

#### Kevin Buzzard (Apr 28 2018 at 02:03):

Can I create one with type class inference and then write over the axiom with a sorry?

Last updated: May 10 2021 at 08:14 UTC