eckmann_hilton.lean

open eq

section eckmann_hilton
  universe variables u
  parameter {α : Type u}
  parameters plus mult : α → α → α
  parameters one zero : α
  local notation a + b := plus a b
  local notation a * b := mult a b

  parameter plus_left_identity : ∀{a}, zero + a = a
  parameter plus_right_identity : ∀{a}, a + zero = a
  parameter mult_left_identity : ∀{a}, one * a = a
  parameter mult_right_identity : ∀{a}, a * one = a
  parameter plus_x_mult    : ∀{a b c d}, (a + b) * (c + d) = (a * c) + (b * d)

  include plus_left_identity plus_right_identity mult_left_identity mult_right_identity plus_x_mult

  theorem one_eq_zero : one = zero :=
    calc
      one = one * one                   : by rw [mult_left_identity]
      ... = (one + zero) * (zero + one) : by rw [plus_right_identity, plus_left_identity]
      ... = (one * zero) + (zero * one) : plus_x_mult
      ... = zero + zero                 : by rw [mult_right_identity, mult_left_identity]
      ... = zero                        : by rw [plus_left_identity]

  theorem mult_eq_plus : mult = plus :=
    have H0 : ∀x, mult x = plus x, from assume x,
      have H1 : ∀y, x * y = x + y, from assume y,
        calc x * y = (x + zero) * (zero + y)       : by rw [plus_right_identity, plus_left_identity]
              ...  = (x * zero) + (zero * y)       : by rw [plus_x_mult]
              ...  = (x * zero) + (one * y)        : congr_arg (λc, (x * zero) + c) (congr_arg (λc, c * y) (eq.symm one_eq_zero))
              ...  = (x * one) + (one * y)         : congr_arg (λc, c + (one * y)) (congr_arg (λc, x * c) (eq.symm one_eq_zero))
              ...  = x + y                         : by rw [mult_left_identity, mult_right_identity],
      funext H1,
    funext H0

  private lemma interchange' : ∀a b c d, (a + b) + (c + d) = (a + c) + (b + d) :=
    assume a b c d,
    calc (a + b) + (c + d) = (a + b) * (c + d)   : congr_fun (congr_fun (eq.symm mult_eq_plus) (a + b)) (c + d)
                   ...     = (a * c) + (b * d)   : by rw [plus_x_mult]
                   ...     = (a + c) + (b * d)   : congr_arg (λx, x + (b * d)) (congr_fun (congr_fun mult_eq_plus a) c)
                   ...     = (a + c) + (b + d)   : congr_arg (λx, (a + c) + x) (congr_fun (congr_fun mult_eq_plus b) d)

  theorem commutativity : ∀x y, x + y = y + x :=
    assume x y,
    calc x + y = (zero + x) + (y + zero) : by rw [plus_left_identity, plus_right_identity]
         ...   = (zero + y) + (x + zero) : interchange' zero x y zero
         ...   = y + x                   : by rw [plus_right_identity, plus_left_identity]

  theorem associativity : ∀x y z, x + (y + z) = (x + y) + z :=
    assume x y z,
    calc x + (y + z) = (zero + x) + (y + z)   : by rw [plus_left_identity]
               ...   = (zero + x) + (z + y)   : congr_arg (λc, (zero + x) + c) (commutativity y z)
               ...   = (zero + z) + (x + y)   : interchange' zero x z y
               ...   = z + (x + y)            : by rw [plus_left_identity]
               ...   = (x + y) + z            : commutativity z _

end eckmann_hilton