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.