Library Groups

Require Import EnsembleFacts.

Require Import Setoid.

Section Groups.

Variable U:Type.
Variable f:Operation U.

Definition LeftIdentity (e:U):=forall a:U, f e a= a.
Definition RightIdentity (e:U):=forall a:U, f a e= a.
Definition Identity (e:U):=LeftIdentity e /\ RightIdentity e.
Definition HasIdentity:=exists e:U, Identity e.

Definition LeftInverse (b a:U):=exists e:U, Identity e /\ f a b=e.

Definition RightInverse (b a:U):=LeftInverse a b.

Definition Inverse (b a:U):=LeftInverse b a /\ RightInverse b a.

Definition HasInverses:=forall a:U, exists b:U, Inverse a b.

End Groups.


Definition Group (U:Type) (f:Operation U):=
Associativity U f /\
HasIdentity U f /\
HasInverses U f.

Definition AbelianGroup (U:Type) (f:Operation U):=
Group U f /\ Commutativity U f.

Definition Monoid (U:Type) (f:Operation U):=
Associativity U f /\
HasIdentity U f.

Lemma Group_is_Monoid: forall (U:Type) (f:Operation U),
Group U f -> Monoid U f.

Theorem uniqueidentity : forall (U:Type) (f:Operation U)
(e1 e2:U),
Identity U f e1 -> Identity U f e2 -> e1=e2.

Theorem Group_uniqueidentity : forall (U:Type) (f:Operation U),
Group U f-> forall (e1 e2:U),
Identity U f e1 -> Identity U f e2 -> e1=e2.

Theorem Monoid_uniqueinverse : forall (U:Type) (f:Operation U),
Monoid U f-> forall (a l r:U),
Inverse U f a l -> Inverse U f a r -> l=r.

Theorem Group_uniqueinverse : forall (U:Type) (f:Operation U),
Group U f-> forall (a l r:U),
Inverse U f a l -> Inverse U f a r -> l=r.

Lemma Group_inversesidentity : forall (U:Type) (f:Operation U)
(a b:U), Inverse U f a b -> Identity U f (f a b).

Lemma Group_existsidentity : forall (U:Type) (f:Operation U)
(a:U), Group U f-> exists e:U, Identity U f e.

Lemma Group_inversesref : forall (U:Type) (f:Operation U)
(a b:U), Inverse U f a b-> Inverse U f b a.

Lemma Group_existsinverse : forall (U:Type) (f:Operation U)
(a:U), Group U f-> exists b:U, Inverse U f a b.

Lemma Group_leftsimplifyinverses :
forall (U:Type) (f:Operation U) (a ia b:U),
Group U f-> Inverse U f a ia ->
f (f a ia) b=b.

Lemma Group_rightsimplifyinverses :
forall (U:Type) (f:Operation U) (a ia b:U),
Group U f-> Inverse U f a ia ->
f b (f a ia)=b.

Lemma Group_refinverses :
forall (U:Type) (f:Operation U) (a b:U),
Inverse U f a b-> Inverse U f b a.

Lemma Group_inversesareidentity:
forall (U:Type) (f:Operation U) (a ia:U),
Group U f -> Inverse U f a ia -> Identity U f (f a ia).

Lemma Group_inversescommute:
forall (U:Type) (f:Operation U) (a ia:U),
Group U f -> Inverse U f a ia -> f a ia = f ia a.

Lemma Group_indentityinverse :
forall (U:Type) (f:Operation U) (e ie:U),
Group U f->
Identity U f e -> Inverse U f e ie -> Identity U f ie.

Theorem Group_additioninverse :
forall (U:Type) (f:Operation U) (a b ia ib:U),
Group U f->
Inverse U f a ia -> Inverse U f b ib ->
Inverse U f (f a b) (f ib ia).

Theorem Group_leftadd : forall (U:Type) (f:Operation U)
(l a b:U), a=b -> f l a=f l b.

Theorem Group_rightadd : forall (U:Type) (f:Operation U)
(r a b:U), a=b -> f a r=f b r.

Theorem Group_leftsimplify : forall (U:Type) (f:Operation U),
Group U f-> forall (l a b:U), f l a= f l b-> a=b.

Theorem Group_rightsimplify : forall (U:Type) (f:Operation U),
Group U f-> forall (r a b:U), f a r= f b r-> a=b.

Lemma Group_identityfrominverses:
forall (U:Type) (f:Operation U) (a ia:U),
Group U f -> Identity U f (f a ia) -> Inverse U f a ia.

Theorem Group_addleftisbijection : forall (U:Type) (f:Operation U)
(a:U), Group U f-> Bijective U U (fun x:U=> f a x).

Theorem Group_addrightisbijection : forall (U:Type) (f:Operation U)
(a:U), Group U f-> Bijective U U (fun x:U=> f x a).

Definition Group_Inversion (U:Type) (f:Operation U) (s:U->U)
:= forall a:U, Inverse U f a (s a).

Theorem Group_existsInversion : forall (U:Type) (f:Operation U),
Group U f -> exists s, Group_Inversion U f s.

Theorem Group_InversionAsInverses :
forall (U:Type) (f:Operation U) (s:U->U) (a b:U),
Group U f -> Group_Inversion U f s ->
s a=b -> Inverse U f a b.

Theorem Group_InversionFromInverses :
forall (U:Type) (f:Operation U) (s:U->U) (a b:U),
Group U f -> Group_Inversion U f s ->
Inverse U f a b -> s a=b.

Theorem Group_SimplifyInversion:
forall (U:Type) (f:Operation U) (s:U->U) (a b:U),
Group U f -> Group_Inversion U f s ->
s a=s b -> a=b.

Theorem Group_InversionIsBijection :
forall (U:Type) (f:Operation U) (s:U->U),
Group U f -> Group_Inversion U f s -> Bijective U U s.

Theorem Group_InversionOfAdd :
forall (U:Type) (f:Operation U) (s:U->U) (a b:U),
Group U f -> Group_Inversion U f s -> s (f a b)=f (s b) (s a).

Theorem Group_DoubleInversion :
forall (U:Type) (f:Operation U) (s:U->U) (a:U),
Group U f -> Group_Inversion U f s -> s (s a)=a.

Theorem Group_ShiftInversion :
forall (U:Type) (f:Operation U) (s:U->U) (a b:U),
Group U f -> Group_Inversion U f s -> s a=b -> a=s b.

Theorem Group_ShiftRightTerm :
forall (U:Type) (f:Operation U) (s:U->U) (a b c:U),
Group U f -> Group_Inversion U f s -> f a b=c -> a=f c (s b).

Theorem Group_ShiftLeftTerm :
forall (U:Type) (f:Operation U) (s:U->U) (a b c:U),
Group U f -> Group_Inversion U f s -> f a b=c -> b=f (s a) c.

Theorem Group_ElimInversesRight :
forall (U:Type) (f:Operation U) (s:U->U) (zero a:U),
Group U f -> Group_Inversion U f s -> Identity U f zero ->
f a (s a)=zero.

Theorem Group_ElimInversesLeft :
forall (U:Type) (f:Operation U) (s:U->U) (zero a:U),
Group U f -> Group_Inversion U f s -> Identity U f zero ->
f (s a) a=zero.

Theorem Group_ElimInverseIdentity :
forall (U:Type) (f:Operation U) (s:U->U) (zero:U),
Group U f -> Group_Inversion U f s -> Identity U f zero ->
s zero=zero.

Fixpoint Group_AddMult (U:Type) (f:Operation U) (z a:U) (n:nat):U:=
match n with
| 0 => z
| S p => f (Group_AddMult U f z a p) a
end.

Theorem Group_AddMult_Extract:
forall (U:Type) (f:Operation U) (zero x a:U) (n:nat),
Group U f -> Identity U f zero ->
Group_AddMult U f x a n=f x (Group_AddMult U f zero a n).

Theorem Group_AddMult_Shift:
forall (U:Type) (f:Operation U) (x a:U) (n:nat),
Group U f ->
Group_AddMult U f x a (S n)= Group_AddMult U f (f x a) a n.

Theorem Group_AddMult_Step:
forall (U:Type) (f:Operation U) (x a:U) (n:nat),
Group U f ->
Group_AddMult U f x a (S n)= f (Group_AddMult U f x a n) a.