Zulip Chat Archive

Stream: maths

Topic: additive group game


view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 01:56):

@[class, priority 100]
structure add_group : Type u  Type u
fields:
add_group.add : Π {α : Type u} [c : add_group α], α  α  α
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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 01:56):

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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 01:57):

And I think one of them follows from the others

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 01:57):

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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 01:57):

Is that right?

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 01:57):

I wanted to prove this myself:

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 01:57):

variables {α : Type}
theorem add_group.add_zero
(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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 01:58):

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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 01:58):

because it doesn't know what + means yet

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 01:59):

I just wanted to make myself a toy abelian group

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 01:59):

but then start taking away the axioms by editing the definition

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 02:02):

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

view this post on Zulip Kevin Buzzard (Apr 28 2018 at 02:03):

Is there a trick?

view this post on Zulip 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