# ∀ a b. a + b = b + a

This question is a part of the LotM.

A ring is a type of structure that takes the rules of addition and multiplication we are familiar with and abstracts them, so we can reason about them. To do this we state a number of expected properties as axioms and see what we can say about systems that follow these axioms. For example $$\a + (b + c) = (a + b) + c\$$, is one of the axioms commonly given.

But exactly what the ring axioms are depends on whom you ask. Because, rings can be defined in a number of equivalent ways. Often one of the given axioms is that for any $$\a\$$ and $$\b\$$ then $$\a + b = b + a\$$. We call this additive commutativity. However this axiom is not needed! Usually we can prove it from more basic axioms.

In this challenge I will give a minimal axiom set for rings in the Lean programming language and your task is to prove commutativity.

The ring class is defined as follows:

universe u

class ring (α : Type u) extends has_add α, has_mul α, has_one α, has_zero α, has_neg α :=
( add_assoc : ∀ a b c : α, a + (b + c) = (a + b) + c )
( mul_assoc : ∀ a b c : α, a * (b * c) = (a * b) * c )
( add_left_id : ∀ a : α, 0 + a = a )
( mul_left_id : ∀ a : α, 1 * a = a )
( mul_right_id : ∀ a : α, a * 1 = a )
( add_left_inv : ∀ a : α, (-a) + a = 0 )
( left_distribute : ∀ a b c : α, a * (b + c) = a * b + a * c )
( right_distribute : ∀ a b c : α, (a + b) * c = a * c + b * c)

open ring

Your goal is to create an object with the same type as:

axiom add_comm {α : Type*} [ring α] : ∀ a b : α, a + b = b + a

This is the same as proving the claim.

You may rename things here however you want as long as the underlying type is correct. So the following is a smaller but perfectly valid header for your proof:

def k{A:Type*}[ring A]:∀a b:A,a+b=b+a

You can't use different but similar looking types. So for example redefining the notation of = to make the proof trivial:

local notation a = b := true
def k{A:Type*}[ring A]:∀a b:A,a+b=b+a := λ x y, trivial

is not a valid answer, even though the type looks identical. (Thanks to Eric for pointing this possible exploit out.)

You must actually prove the claim, so you may not use sorry or axiom in your proof.

This is so answers will be scored in bytes with fewer bytes being the goal.

If you want to do this challenge but don't know where to get started just use the links in the LotM post. I'll be happy to help anyway I can in chat.

• Should we be counting characters and not bytes since Lean is UTF8? If so, should that be added to the list of per-language rules here?
– Eric
Oct 7, 2021 at 11:59
• @Eric You should be counting bytes on disc just as in most other challenges. I don't think there is any reason to special case this. Oct 7, 2021 at 12:01
• You might want to look at this loophole proposal. Oct 8, 2021 at 0:04