8
\$\begingroup\$

Part of the 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 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.

\$\endgroup\$
1
  • \$\begingroup\$ You say addition is not a pong, but over the booleans addition can be defined just as xor \$\endgroup\$
    – qwr
    Oct 15 '21 at 14:28
6
\$\begingroup\$

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
\$\endgroup\$
3
  • \$\begingroup\$ You can shave off a few bytes with V(A:Type u) -> V(A) \$\endgroup\$ Oct 24 '21 at 23:02
  • \$\begingroup\$ Also, by allowing some metavariables while rewriting, this shaves off a few more bytes: rw[<-right_id(a+b),<-P,P a,<-P b,left_id,left_id]. \$\endgroup\$ Oct 24 '21 at 23:06
  • \$\begingroup\$ Oh my, you can do something even worse to shave off two bytes: a+b=b+a -> a+b=_. This is relying on the way Lean elaborates a def vs a theorem, which is that definitions are allowed to have metavariables in their types before typechecking what comes after the :=. Theorems don't allow this so that it can typecheck proofs in parallel. (This verifies it still has the right type: example (A : Type*) [pong A] (a b : A) : a + b = b + a := V A a b, in addition to #check V.) \$\endgroup\$ Oct 25 '21 at 23:07
4
\$\begingroup\$

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.

\$\endgroup\$
5
  • 1
    \$\begingroup\$ Since you don't split your goal at any point you can replace all the ,s with ;s and get rid of the brackets to save a byte. \$\endgroup\$
    – Wheat Wizard
    Oct 16 '21 at 16:52
  • \$\begingroup\$ @WheatWitch Thanks! I was going to try that before, but Lean started erroring as soon as I replaced one comma with a semicolon. I guess it needs all of them to be replaced to work properly \$\endgroup\$
    – user
    Oct 16 '21 at 18:04
  • 1
    \$\begingroup\$ 122 bytes with def V(A)[pong A](a b:A):a+b=b+a:=by rw<-l b(a+b);repeat{rw<-s};rw[l,s,right_id,s(a+b),l] \$\endgroup\$ Oct 24 '21 at 23:22
  • 1
    \$\begingroup\$ and 121 bytes with 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] \$\endgroup\$ Oct 24 '21 at 23:31
  • \$\begingroup\$ @KyleMiller Wow, thanks! \$\endgroup\$
    – user
    Oct 25 '21 at 22:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.