83 lines
3.1 KiB
Text
83 lines
3.1 KiB
Text
import macros
|
|
|
|
definition associative {A : (Type U)} (f : A → A → A) := ∀ x y z, f (f x y) z = f x (f y z)
|
|
definition commutative {A : (Type U)} (f : A → A → A) := ∀ x y, f x y = f y x
|
|
definition is_identity {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, f x id = x
|
|
definition inverse_ex {A : (Type U)} (f : A → A → A) (id : A) := ∀ x, ∃ y, f x y = id
|
|
|
|
definition struct := Type
|
|
definition carrier (s : struct) := s
|
|
|
|
definition mul_struct
|
|
:= sig s : struct, carrier s → carrier s → carrier s
|
|
|
|
definition mul_to_s (m : mul_struct) : struct := proj1 m
|
|
coercion mul_to_s
|
|
|
|
definition mul {m : mul_struct} : carrier m → carrier m → carrier m
|
|
:= proj2 m
|
|
|
|
infixl 70 * : mul
|
|
|
|
definition semi_group
|
|
:= sig m : mul_struct, associative (@mul m)
|
|
|
|
definition sg_to_mul (sg : semi_group) : mul_struct := proj1 sg
|
|
definition sg_to_s (sg : semi_group) : struct := mul_to_s (sg_to_mul sg)
|
|
coercion sg_to_s
|
|
coercion sg_to_mul
|
|
|
|
theorem sg_assoc {m : semi_group} (x y z : carrier m) : (x * y) * z = x * (y * z)
|
|
:= proj2 m x y z
|
|
|
|
definition monoid
|
|
:= sig sg : semi_group, sig id : carrier sg, is_identity (@mul sg) id
|
|
|
|
definition monoid_to_sg (m : monoid) : semi_group := proj1 m
|
|
definition monoid_to_mul (m : monoid) : mul_struct := sg_to_mul (monoid_to_sg m)
|
|
definition monoid_to_s (m : monoid) : struct := mul_to_s (monoid_to_mul m)
|
|
coercion monoid_to_sg
|
|
coercion monoid_to_mul
|
|
coercion monoid_to_s
|
|
|
|
definition one {m : monoid} : carrier m
|
|
:= proj1 (proj2 m)
|
|
theorem monoid_id {m : monoid} (x : carrier m) : x * one = x
|
|
:= proj2 (proj2 m) x
|
|
|
|
definition group
|
|
:= sig m : monoid, inverse_ex (@mul m) (@one m)
|
|
|
|
definition group_to_monoid (g : group) : monoid := proj1 g
|
|
definition group_to_sg (g : group) : semi_group := monoid_to_sg (group_to_monoid g)
|
|
definition group_to_mul (g : group) : mul_struct := sg_to_mul (group_to_sg g)
|
|
definition group_to_s (g : group) : struct := mul_to_s (group_to_mul g)
|
|
coercion group_to_monoid
|
|
coercion group_to_sg
|
|
coercion group_to_mul
|
|
coercion group_to_s
|
|
|
|
theorem group_inv {g : group} (x : carrier g) : ∃ y, x * y = one
|
|
:= proj2 g x
|
|
|
|
definition abelian_group
|
|
:= sig g : group, commutative (@mul g)
|
|
|
|
definition abelian_to_group (ag : abelian_group) : group := proj1 ag
|
|
definition abelian_to_monoid (ag : abelian_group) : monoid := group_to_monoid (abelian_to_group ag)
|
|
definition abelian_to_sg (ag : abelian_group) : semi_group := monoid_to_sg (abelian_to_monoid ag)
|
|
definition abelian_to_mul (ag : abelian_group) : mul_struct := sg_to_mul (abelian_to_sg ag)
|
|
definition abelian_to_s (ag : abelian_group) : struct := mul_to_s (abelian_to_mul ag)
|
|
coercion abelian_to_group
|
|
coercion abelian_to_monoid
|
|
coercion abelian_to_sg
|
|
coercion abelian_to_mul
|
|
coercion abelian_to_s
|
|
|
|
theorem abelian_comm {ag : abelian_group} (x y : carrier ag) : x * y = y * x
|
|
:= proj2 ag x y
|
|
|
|
theorem abelian_left_comm {ag : abelian_group} (x y z : carrier ag) : x * (y * z) = y * (x * z)
|
|
:= calc x * (y * z) = (x * y) * z : symm (sg_assoc x y z)
|
|
... = (y * x) * z : { abelian_comm x y }
|
|
... = y * (x * z) : sg_assoc y x z
|