# ∀ 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 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 at 12:01
• You might want to look at this loophole proposal. Oct 8 at 0:04

## Lean, 451449445439414 407 bytes

def k{A}[ring A](a b:A):a+b=b+a:=let
L:=@add_left_inv A,I:=@add_left_id A,K:=@congr_arg,c:=λx y,K(+y)$L x in by{let C:=add_assoc,simp[I]at*,let e:=λb,(λ(a:A)h:a+a=a,(eq.trans(by rw[<-I a,<-L,<-C,h])$L _:a=0))(b+-b)$by simp[<-C]at*;rw c,let d:=K(λx,-b+x+-a)(left_distribute(1+1)b a),simp[c,C,right_distribute,mul_left_id,mul_right_id,λa b,(by rw[<-C,e,λa:A,(by rw[<-L,C,e,I]:a+0=a)]:b+a+-a=b)]at*,rw d}  Unpacked: def add_comm {A} [ring A] (a b : A) : a + b = b + a := let L := @add_left_inv A, I := @add_left_id A, K := @congr_arg, c := λ x y, K (+ y) (L x) in begin have C := add_assoc, simp [I] at c, -- c: ∀ (x y : A), -x + x + y = y have e : ∀ (b : A), b + -b = 0 := λ b, have ∀ (a : A), a + a = a → a = 0 := λ (a : A) (h : a + a = a), show a = 0, from eq.trans (by rw [← I a, ← L, ← C, h]) (L _), this (b + -b) (by simp [← C] at c ⊢; rw c), have d : -b + ((1 + 1) * (b + a)) + -a = -b + ((1 + 1) * b + (1 + 1) * a) + -a := K (λ x, -b + x + -a) (left_distribute (1+1) b a), simp [c, C, right_distribute, mul_left_id, mul_right_id, have ∀ (a b : A), b + a + -a = b := λ a b : A, show b + a + -a = b, by rw [← C, e, have ∀ (a : A), a + 0 = a, from λ a : A, show a + 0 = a, by rw [← L, C, e, I], this], this] at d, -- d : a + b = b + a rw d end  • how does the first by rw in the eq.trans work? If I say: let asd : a = _ := (by rw [← I a, ← L, ← C, h]) in eq.trans asd (L _), it's fine, but if I give it its real type instead of the placeholder (supposedly a = -a + a) then it fails Oct 8 at 11:09 • @It'sNotALie The trick is that after the eq.trans, the first subgoal is something like a = ?m, and rewriting a to something only acts on the lhs, even though eventually the ?m becomes an expression involving a. If you give it the full type, with a on the rhs too, then the rw will rewrite those a's as well, which breaks the proof. It's basically a cheap way to do conv {to_lhs, rw ...}. Oct 9 at 12:04 # Lean, 268 bytes import tactic.cache def k{A}[r:ring A](a b:A):a+b=b+a:=by{casesI r with _ _ _ _ _ c _ d _ _ e f,let g:=λa:A,trans(by simp*:_=-(a+-a)+(a+-a+a+-a))$by
simp[<-c,*],let:=λa,trans(by
rw[<-c,e,g]:a+b+_=a+(-a+a))\$by
rw[c,g,d],transitivity-a+(1+1)*(a+b)+-b,rw f,simp*,simp*}


Run with Lean Web Editor

• I think mathlib is allowed, so you can use import tactic and then casesI instead of tactic.unfreeze_local_instances,cases Oct 12 at 2:23
• @MarioCarneiro import tactic brings a conflicting ring into scope. I’m not entirely sure if import is allowed at all, since imports have to be at the top of the file, but I’ll assume for now that import tactic.cache is okay. Oct 12 at 4:25