∀ a b. a + b = b + a

Question

This question is a part of the lean 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 code-golf 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.

Answer 1

Lean, 451 449 445 439 414 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

Answer 2

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