Skip to content

Instantly share code, notes, and snippets.

@nyuichi
Last active December 14, 2016 10:24
Show Gist options
  • Save nyuichi/c5f0e51b1320f4cb52358dcdddd8f26f to your computer and use it in GitHub Desktop.
Save nyuichi/c5f0e51b1320f4cb52358dcdddd8f26f to your computer and use it in GitHub Desktop.
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment