Every Pong is Abelian

Question

Part of the lean Language of the Month

A pong* is a set \$P\$ with an operation \$+\$, that satisfies the following properties:

\$ \forall a, b \in P : (b + b) + a = a\\ \forall a, b \in P : a + (b + b) = a\\ \forall a, b, c \in P: a + (b + c) = (a + b) + c \\ \$

This makes a pong*, just a group where every element is it's own inverse.

Now most operations we know of are not pongs. Addition is clearly not a pong. However you should be familiar with some. Exclusive or on booleans is a pong, since \$\mathrm{True}\oplus\mathrm{True} = \mathrm{False}\$ and \$\mathrm{False}\oplus\mathrm{False} = \mathrm{False}\$, and by extension bitwise xor on integers is also a pong.

A beginner level proof in Abstract Algebra is to show that every pong is an Abelian group. That is given the axioms prove

\$ \forall a,b : a + b = b + a \$

So as I thought it would be fun to tackle this problem as a beginner lean problem. Here's a pong class:

universe u

class pong (A : Type u) extends has_add A :=
  ( add_assoc : ∀ a b c : A, (a + b) + c = a + (b + c) )
  ( left_id : ∀ a b : A, (b + b) + a = a )
  ( right_id : ∀ a b : A, a + (b + b) = a )

open pong

Your task is to prove the following theorem:

theorem add_comm (A : Type u) [pong A] : ∀ a b : A, a + b = b + a

As is standard now you may rename the function and golf declaration as long as the underlying type remains the same.

You may not use any of the theorem proving sidesteps.

This is code-golf answers will be scored in bytes with fewer bytes being the goal.

I ask that if you are experienced in Lean you give a little time for beginners to have a go at this. Feel free to post your score below as a motivator. You can also post a hash of your program as proof.

^{* A term I just made up, because saying "Group where every element is its own inverse" gets tiring real quick.}

Answer 1

Lean, ^{115 103} 100 bytes

def P:=@add_assoc
def V(A)[pong A](a b:A):a+b=_:=by rw[<-right_id$a+b,<-P,P a,<-P b,left_id,left_id]

Try it on Lean Web Editor!

-14 bytes thanks to Kyle Miller.

Proof outline

a + b
= (a + b) + ((b + a) + (b + a)) -- by right_id
= ((a + b) + (b + a)) + (b + a) -- by add_assoc
= (a + (b + (b + a))) + (b + a) -- by add_assoc
= (a + ((b + b) + a)) + (b + a) -- by add_assoc
= (a + a) + (b + a) -- by left_id
= b + a -- by left_id

Answer 2

Lean, 141 140 121 bytes

• Saved one byte thanks to Wheat Witch/Wheat Wizard
• Saved 19 bytes thanks to Kyle Miller!

def s:=@add_assoc
def V(A)[pong A](a b:A):a+b=b+a:=by rw<-left_id b(a+b);repeat{rw<-s};rw s;simp[right_id,s(a+b),left_id]

Try it online

Bubbler's is much better, but I'm just throwing my hat into the ring anyway.