Library groups

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
This file defines the main interface for finite groups :                  
         finGroupType == the structure for finite types with a group law  
          {group gT}  == type of groups with elements of type gT          
If gT implements finGroupType, then we can form {set gT}, the type of     
finite sets with elements of type gT (as finGroupType extends finType).   
The group law extends pointwise to {set gT}, which thus implements a sub- 
interface baseFinGroupType of finGroupType. To be consistent with the     
predType interface, this is done by coercion to FinGroup.arg_sort, an     
alias for FinGroup.sort. Accordingly, all pointwise group operations      
below have arguments of type (FinGroup.arg_sort) gT and return results    
of type FinGroup.sort gT.                                                 
  The notations below are declared in two scopes:                         
     group_scope (delimiter %g) for point operations and set constructs   
  subgroup_scope (delimiter %G) for explicit {group gT} structures        
These scopes should not be opened globally, athough group_scope is often  
opened locally in group-theory files (via Import GroupScope).             
 {group gT} is an interface structure for {set gT} (as well as a subtype) 
so the fact that a given G : {set gT} is a group can (and usually should) 
be inferred by type inference with Canonical Structures. This means that  
all "group" constructions (e.g., the normaliser 'N_G(H)) actually define  
sets with a canonical {group gT} structure; the %G delimiter can be used  
to specify the actual {group gT} structure (e.g., 'N_G(H)%G).             
 Operations on elements of a group                                        
           x * y     == internal group operation                          
           x ^+ n    == power operation                                   
           x^-1      == inverse group operation                           
           x ^- n    == inverse power operation                           
           1         == unit element                                      
          x ^ y      == the conjugate of x by y                           
 \prod_(i ...) x i   == product of the x i (order-sensitive)              
        commute x y  <=> x and y commute                                  
     centralises x A <=> x centralises A                                  
          'C[x]      == the set of elements that commutes with x          
          'C_G[x]    == the set of elements of G that commutes with x     
           <[x]>     == cyclic subgroup generated by the element x        
           #[x]      == order of the element x                            
    [~ x1, ..., xn]  == commutator of x1, ..., xn                         
 Operations on sets of a finite group                                     
           H * G     == {xy | x \in H, y \in G}                           
  1 or [1] or [1 gT] == the unit group                                    
[setT]%G or [setT gT]%G == the group of all x : gT (in subgroup_scope)    
           subg_of G == the subtype of all x \in G                        
                        if G is a group, subg_of G is a finGroupType      
         subg, sgval == projection into, injection from subg_of G         
            [subg G] == the set (or group) of all u : subg_of G           
           H^#       == the set H minus the unit element                  
           repr H    == some element of H if 1 \notin H != set0, else 1   
         x *: H      == left coset of H by x                              
         lcosets H G == the set of the left cosets of H by elements of G  
         H :* x      == right coset of H by x                             
         rcosets H G == the set of the right cosets of H by elements of G 
          #|G : H|   == the index of H in G                               
           H :^ x    == the conjugate of H by x                           
           x ^: H    == the conjugate class of x in H                     
           G :^: H   == the set of all conjugate classes                  
   class_support G H == {x ^ y | x \in G, y \in H}                        
    [~: H1, ..., Hn] == commutator subgroup of H1, ..., Hn                
{in G, normalised H} <=> G normalises H                                   
                     <=> forall x, x \in G -> H :^ x = H                  
           'N(H)     == the normaliser of H                               
           'N_G(H)   == the normaliser of H in G                          
            H <| G   <=> H is normal in G                                 
           'C(H)     == the centraliser of H                              
           'C_G(H)   == the centraliser of H in G                         
            <<H>>    == subgroup generated by the set H                   
           H <*> G   == subgroup generated by H * G                       
(\prod_(i ...) H i)%G  == group generated by the H i                      
          abelian H  <=> H is abelian                                     
      [max G | P G ] <=> G is the largest group such that P holds         
 [max H of G | P G ] <=> H is the largest group such that P holds         
      [min G | P G ] <=> G is the smallest group such that P holds        
 [min H of G | P G ] <=> H is the smallest group such that P holds        

Import Prenex Implicits.

Delimit Scope group_scope with g.
Delimit Scope subgroup_scope with G.

This module can be imported to open the scope for group element 
operations locally to a file, without exporing the Open to      
clients of that file (as Open would do).                        
Module GroupScope.
Open Scope group_scope.
End GroupScope.
Import GroupScope.

Module FinGroup.

We split the group axiomatisation in two. We define a  
class of "base groups", which are basically monoids    
with an involutive antimorphism, from which we derive  
the class of groups proper. This allows use to reuse   
much of the group notation and algebraic axioms for    
group subsets, by defining a base group class on them. 
  We use class/mixins here rather than telescopes to   
be able to interoperate with the type coercions.       
Another potential benefit (not exploited here) would   
be to define a class for infinite groups, which could  
share all of the algebraic laws.                       
Record mixin_of (T : Type) : Type := BaseMixin {
  mul : T -> T -> T;
  one : T;
  inv : T -> T;
  _ : associative mul;
  _ : left_id one mul;
  _ : involutive inv;
  _ : {morph inv : x y / mul x y >-> mul y x}
}.

Structure base_type : Type := PackBase {
  sort : Type;
   _ : mixin_of sort;
   _ : Finite.class_of sort
}.

We want to use sort as a coercion class, both to infer         
argument scopes properly, and to allow groups and cosets to    
coerce to the base group of group subsets.                     
  However, the return type of group operations should NOT be a 
coercion class, since this would trump the real (head-normal)  
coercion class for concrete group types, thus spoiling the     
coercion of A * B to pred_sort in x \in A * B, or rho * tau to 
ffun and Funclass in (rho * tau) x, when rho tau : perm T.     
  Therefore we define an alias of sort for argument types, and 
make it the default coercion FinGroup.base_class >-> Sortclass 
so that arguments of a functions whose parameters are of type, 
say, gT : finGroupType, can be coerced to the coercion class   
of arg_sort. Care should be taken, however, to declare the     
return type of functions and operators as FinGroup.sort gT     
rather than gT, e.g., mulg : gT -> gT -> FinGroup.sort gT.     
Note that since we do this here and in normal.v for all the    
basic functions, the inferred return type should generally be  
correct.                                                       
Coercion arg_sort := sort.
Declaring sort as a Coercion is clearly redundant; it only     
serves the purpose of eliding FinGroup.sort in the display of  
return types. The warning could be eliminated by using the     
functor trick to replace Sortclass by a dummy target.          
Coercion sort : base_type >-> Sortclass.

Coercion mixin T :=
  let: PackBase _ m _ := T return mixin_of (sort T) in m.

Definition finClass T :=
  let: PackBase _ _ m := T return Finite.class_of (sort T) in m.

Structure type : Type := Pack {
  base :> base_type;
  _ : left_inverse (one base) (inv base) (mul base)
}.

We only need three axioms to make a true group. 

Section Mixin.

Variables (T : Type) (one : T) (mul : T -> T -> T) (inv : T -> T).

Hypothesis mulA : associative mul.
Hypothesis mul1 : left_id one mul.
Hypothesis mulV : left_inverse one inv mul.
Notation "1" := one.
Infix "*" := mul.
Notation "x ^-1" := (inv x).

Lemma mk_invgK : involutive inv.

Lemma mk_invMg : {morph inv : x y / x * y >-> y * x}.

Definition Mixin := BaseMixin mulA mul1 mk_invgK mk_invMg.

End Mixin.

Definition pack_base := let k T c m := PackBase m c in Finite.unpack k.

Definition repack_base gT :=
  let: PackBase _ m c := gT return {type of PackBase for sort gT} -> _ in
  fun k => k m c.

Definition repack gT :=
  let: Pack c ax := gT return {type of Pack for gT} -> _ in fun k => k ax.

Definition repack_arg gT of phant (sort gT) := @Pack gT.

End FinGroup.


Notation baseFinGroupType := FinGroup.base_type.
Notation BaseFinGroupType := FinGroup.pack_base.

Section InheritedClasses.

Variable T : baseFinGroupType.
Notation c := (FinGroup.finClass T).
Notation rT := (FinGroup.sort T).

Canonical Structure finGroup_eqType := Equality.Pack c rT.
Canonical Structure finGroup_choiceType := Choice.Pack c rT.
Canonical Structure finGroup_countType := Countable.Pack c rT.
Canonical Structure finGroup_finType := Finite.Pack c rT.
Canonical Structure finGroup_arg_eqType := Eval hnf in [eqType of T].
Canonical Structure finGroup_arg_choiceType := Eval hnf in [choiceType of T].
Canonical Structure finGroup_arg_countType := Eval hnf in [countType of T].
Canonical Structure finGroup_arg_finType := Eval hnf in [finType of T].

End InheritedClasses.

Coercion finGroup_arg_finType : baseFinGroupType >-> finType.

Notation "[ 'baseFinGroupType' 'of' T ]" :=
    (FinGroup.repack_base (fun m => @FinGroup.PackBase T m))
  (at level 0, format "[ 'baseFinGroupType' 'of' T ]") : form_scope.

Notation finGroupType := FinGroup.type.
Notation FinGroupType := FinGroup.Pack.

Notation "[ 'finGroupType' 'of' T ]" :=
    (FinGroup.repack (FinGroup.repack_arg (Phant T)))
  (at level 0, format "[ 'finGroupType' 'of' T ]") : form_scope.

Section ElementOps.

Variable T : baseFinGroupType.
Notation rT := (FinGroup.sort T).

Definition oneg : rT := FinGroup.one T.
Definition mulg : T -> T -> rT := FinGroup.mul T.
Definition invg : T -> rT := FinGroup.inv T.
Definition expgn_rec (x : T) n : rT := iterop n mulg x oneg.

End ElementOps.

Definition expgn := nosimpl expgn_rec.

Notation "1" := (oneg _) : group_scope.
Notation "x1 * x2" := (mulg x1 x2) : group_scope.
Notation "x ^-1" := (invg x) : group_scope.
Notation "x ^+ n" := (expgn x n) : group_scope.
Notation "x ^- n" := (x ^+ n)^-1 : group_scope.

Arguments of conjg are restricted to true groups to avoid an 
improper interpretation of A ^ B with A and B sets, namely:  
      {x^-1 * (y * z) | y \in A, x, z \in B}                 
Definition conjg (T : finGroupType) (x y : T) := y^-1 * (x * y).
Notation "x1 ^ x2" := (conjg x1 x2) : group_scope.

Definition commg (T : finGroupType) (x y : T) := x^-1 * x ^ y.
Notation "[ ~ x1 , x2 , .. , xn ]" := (commg ..


Notation "\prod_ ( <- r | P ) F" :=
  (\big[mulg/1]_(<- r | P%B) F%g) : group_scope.
Notation "\prod_ ( i <- r | P ) F" :=
  (\big[mulg/1]_(i <- r | P%B) F%g) : group_scope.
Notation "\prod_ ( i <- r ) F" :=
  (\big[mulg/1]_(i <- r) F%g) : group_scope.
Notation "\prod_ ( m <= i < n | P ) F" :=
  (\big[mulg/1]_(m <= i < n | P%B) F%g) : group_scope.
Notation "\prod_ ( m <= i < n ) F" :=
  (\big[mulg/1]_(m <= i < n) F%g) : group_scope.
Notation "\prod_ ( i | P ) F" :=
  (\big[mulg/1]_(i | P%B) F%g) : group_scope.
Notation "\prod_ i F" :=
  (\big[mulg/1]_i F%g) : group_scope.
Notation "\prod_ ( i : t | P ) F" :=
  (\big[mulg/1]_(i : t | P%B) F%g) (only parsing) : group_scope.
Notation "\prod_ ( i : t ) F" :=
  (\big[mulg/1]_(i : t) F%g) (only parsing) : group_scope.
Notation "\prod_ ( i < n | P ) F" :=
  (\big[mulg/1]_(i < n | P%B) F%g) : group_scope.
Notation "\prod_ ( i < n ) F" :=
  (\big[mulg/1]_(i < n) F%g) : group_scope.
Notation "\prod_ ( i \in A | P ) F" :=
  (\big[mulg/1]_(i \in A | P%B) F%g) : group_scope.
Notation "\prod_ ( i \in A ) F" :=
  (\big[mulg/1]_(i \in A) F%g) : group_scope.

Section PreGroupIdentities.

Variable T : baseFinGroupType.
Implicit Types x y z : T.

Lemma mulgA : @associative T mulg. Qed.

Lemma mul1g : @left_id T 1 mulg. Qed.

Lemma invgK : @involutive T invg. Qed.

Lemma invMg : forall x y, (x * y)^-1 = y^-1 * x^-1.

Lemma invg_inj : @injective T T invg. Qed.

Lemma eq_invg_sym : forall x y, (x^-1 == y :> T) = (x == y^-1).

Lemma invg1 : 1^-1 = 1 :> T.

Lemma eq_invg1 : forall x, (x^-1 == 1 :> T) = (x == 1).

Lemma mulg1 : @right_id T 1 mulg.

Canonical Structure finGroup_law := Monoid.Law mulgA mul1g mulg1.

Lemma expgnE : forall x n, x ^+ n = expgn_rec x n. Qed.

Lemma expg0 : forall x, x ^+ 0 = 1. Qed.

Lemma expg1 : forall x, x ^+ 1 = x. Qed.

Lemma expgS : forall x n, x ^+ n.+1 = x * x ^+ n.

Lemma exp1gn : forall n, 1 ^+ n = 1 :> T.

Lemma expgn_add : forall x n m, x ^+ (n + m) = x ^+ n * x ^+ m.

Lemma expgSr : forall x n, x ^+ n.+1 = x ^+ n * x.

Lemma expgn_mul : forall x n m, x ^+ (n * m) = x ^+ n ^+ m.

Definition commute x y := x * y = y * x.

Lemma commute_refl : forall x, commute x x.

Lemma commute_sym : forall x y, commute x y -> commute y x.

Lemma commute1 : forall x, commute x 1.

Lemma commuteM : forall x y z,
  commute x y -> commute x z -> commute x (y * z).

Lemma commuteX : forall x y n, commute x y -> commute x (y ^+ n).

Lemma commuteX2 : forall x y m n, commute x y -> commute (x ^+ m) (y ^+ n).

Lemma expVgn : forall x n, x^-1 ^+ n = x ^- n.

Lemma expMgn : forall x y n, commute x y -> (x * y) ^+ n = x ^+ n * y ^+ n.

End PreGroupIdentities.

Hint Resolve commute1.
Implicit Arguments invg_inj [T].

Section GroupIdentities.

Variable T : finGroupType.
Implicit Types x y z : T.

Lemma mulVg : @left_inverse T 1 invg mulg.

Lemma mulgV : @right_inverse T 1 invg mulg.

Lemma mulKg : forall x, cancel (mulg x) (mulg x^-1).

Lemma mulKVg : forall x, cancel (mulg x^-1) (mulg x).

Lemma mulgI : forall x, injective (mulg x).

Lemma mulgK : forall x, cancel (mulg^~ x) (mulg^~ x^-1).

Lemma mulgKV : forall x, cancel (mulg^~ x^-1) (mulg^~ x).

Lemma mulIg : forall x, injective (mulg^~ x).

Lemma eq_invg_mul : forall x y, (x^-1 == y :> T) = (x * y == 1 :> T).

Lemma eq_mulgV1 : forall x y, (x == y) = (x * y^-1 == 1 :> T).

Lemma eq_mulVg1 : forall x y, (x == y) = (x^-1 * y == 1 :> T).

Lemma commuteV : forall x y, commute x y -> commute x y^-1.

Lemma conjgE : forall x y, x ^ y = y^-1 * (x * y). Qed.

Lemma conjgC : forall x y, x * y = y * x ^ y.

Lemma conjgCV : forall x y, x * y = y ^ x^-1 * x.

Lemma conjg1 : forall x, x ^ 1 = x.

Lemma conj1g : forall x, 1 ^ x = 1.

Lemma conjMg : forall x y z, (x * y) ^ z = x ^ z * y ^ z.

Lemma conjgM : forall x y z, x ^ (y * z) = (x ^ y) ^ z.

Lemma conjVg : forall x y, x^-1 ^ y = (x ^ y)^-1.

Lemma conjJg : forall x y z, (x ^ y) ^ z = (x ^ z) ^ y ^ z.

Lemma conjXg : forall x y n, (x ^+ n) ^ y = (x ^ y) ^+ n.

Lemma conjgK : forall y, cancel (conjg^~ y) (conjg^~ y^-1).

Lemma conjgKV : forall y, cancel (conjg^~ y^-1) (conjg^~ y).

Lemma conjg_inj : forall y, injective (conjg^~ y).

Lemma commgEl : forall x y, [~ x, y] = x^-1 * x ^ y. Qed.

Lemma commgEr : forall x y, [~ x, y] = y^-1 ^ x * y.

Lemma commgC : forall x y, x * y = y * x * [~ x, y].

Lemma commgCV : forall x y, x * y = [~ x^-1, y^-1] * (y * x).

Lemma conjRg : forall x y z, [~ x, y] ^ z = [~ x ^ z, y ^ z].

Lemma invg_comm : forall x y, [~ x, y]^-1 = [~ y, x].

Lemma commgP : forall x y, reflect (commute x y) ([~ x, y] == 1 :> T).

Lemma conjg_fixP : forall x y, reflect (x ^ y = x) ([~ x, y] == 1 :> T).

Lemma commg1_sym : forall x y, ([~ x, y] == 1 :> T) = ([~ y, x] == 1 :> T).

Lemma commg1 : forall x, [~ x, 1] = 1.

Lemma comm1g : forall x, [~ 1, x] = 1.

Lemma commgg : forall x, [~ x, x] = 1.

Lemma commgXg : forall x n, [~ x, x ^+ n] = 1.

Lemma commgVg : forall x, [~ x, x^-1] = 1.

Lemma commgXVg : forall x n, [~ x, x ^- n] = 1.

Other commg identities should slot in here. 

End GroupIdentities.

Hint Rewrite mulg1 mul1g invg1 mulVg mulgV (@invgK) mulgK mulgKV
             invMg mulgA : gsimpl.

Ltac gsimpl := autorewrite with gsimpl; try done.

Definition gsimp := (mulg1 , mul1g, (invg1, @invgK), (mulgV, mulVg)).
Definition gnorm := (gsimp, (mulgK, mulgKV, (mulgA, invMg))).

Implicit Arguments mulgI [T].
Implicit Arguments mulIg [T].
Implicit Arguments conjg_inj [T].
Implicit Arguments commgP [T x y].
Implicit Arguments conjg_fixP [T x y].

Section SetMulDef.

Variable gT : finGroupType.
Notation Local sT := {set gT}.
Implicit Types A B : sT.
Implicit Type x y : gT.

Plucking a set representative. 

Definition repr A :=
  if 1 \in A then 1 else if [pick x \in A] is Some x then x else 1.

Lemma mem_repr : forall x A, x \in A -> repr A \in A.

Lemma card_mem_repr : forall A, #|A| > 0 -> repr A \in A.

Lemma repr_set1 : forall x : gT, repr [set x] = x.

Lemma repr_set0 : repr set0 = 1.

Set-lifted group operations. 

Definition set_mulg A B := mulg @2: (A, B).
Definition set_invg A := invg @^-1: A.

Definition lcoset A x := mulg x @: A.
Definition rcoset A x := mulg^~ x @: A.
Definition lcosets A B := lcoset A @: B.
Definition rcosets A B := rcoset A @: B.
Definition indexg B A := #|rcosets A B|.

Definition conjugate A x := conjg^~ x @: A.
Definition conjugates A B := conjugate A @: B.
Definition class x B := conjg x @: B.
Definition classes A := class^~ A @: A.
Definition class_support A B := conjg @2: (A, B).

Definition commg_set A B := commg @2: (A, B).

These will only be used later, but are defined here so that we can 
keep all the Notation together.                                    
Definition normaliser A := [set x | conjugate A x \subset A].
Definition centraliser A := \bigcap_(x \in A) normaliser [set x].
Definition abelian A := A \subset centraliser A.
Definition normal A B := (A \subset B) && (B \subset normaliser A).

"normalised" and "centralise[s|d]" are intended to be used with   
the {in ...} form, as in abelian below.                           
Definition normalised A := forall x, conjugate A x = A.
Definition centralises x A := forall y, y \in A -> commute x y.
Definition centralised A := forall x, centralises x A.

The pre-group structure of group subsets. 

Lemma set_mul1g : left_id [set 1] set_mulg.

Lemma set_mulgA : associative set_mulg.

Lemma set_invgK : involutive set_invg.

Lemma set_invgM : {morph set_invg : A B / set_mulg A B >-> set_mulg B A}.

Definition group_set_baseGroupMixin : FinGroup.mixin_of (set_type _) :=
  FinGroup.BaseMixin set_mulgA set_mul1g set_invgK set_invgM.

Canonical Structure group_set_baseGroupType :=
  Eval hnf in BaseFinGroupType group_set_baseGroupMixin.

Canonical Structure group_set_of_baseGroupType :=
  Eval hnf in [baseFinGroupType of {set gT}].

End SetMulDef.

Time to open the bag of dirty tricks. When we define groups down below 
as a subtype of {set gT}, we need them to be able to coerce to sets in 
both set-style contexts (x \in G) and monoid-style contexts (G * H),   
and we need the coercion function to be EXACTLY the structure          
projection in BOTH cases -- otherwise the canonical unification breaks.
  Alas, Coq doesn't let us use the same coercion function twice, even  
when the targets are convertible. Our workaround (ab)uses the module   
system to declare two different identity coercions on an alias class.  

Module GroupSet.
Definition sort (gT : finGroupType) := {set gT}.
Identity Coercion of_sort : sort >-> set_of.
End GroupSet.

Module Type GroupSetBaseGroupSig.
Definition sort gT := group_set_of_baseGroupType gT : Type.
End GroupSetBaseGroupSig.

Module MakeGroupSetBaseGroup (Gset_base : GroupSetBaseGroupSig).
Identity Coercion of_sort : Gset_base.sort >-> FinGroup.arg_sort.
End MakeGroupSetBaseGroup.

Module GroupSetBaseGroup := MakeGroupSetBaseGroup GroupSet.

Canonical Structure group_set_eqType gT :=
  Eval hnf in [eqType of GroupSet.sort gT].
Canonical Structure group_set_choiceType gT :=
  Eval hnf in [choiceType of GroupSet.sort gT].
Canonical Structure group_set_countType gT :=
  Eval hnf in [countType of GroupSet.sort gT].
Canonical Structure group_set_finType gT :=
  Eval hnf in [finType of GroupSet.sort gT].


Notation "[ 1 gT ]" := (1 : {set gT})
  (at level 0, format "[ 1 gT ]") : group_scope.
Notation "[ 1 ]" := [1 FinGroup.sort _]
  (at level 0, format "[ 1 ]") : group_scope.

Notation "A ^#" := (A :\ 1) (at level 2, format "A ^#") : group_scope.

Notation "x *: A" := ([set x%g] * A) (at level 40) : group_scope.
Notation "A :* x" := (A * [set x%g]) (at level 40) : group_scope.
Notation "A :^ x" := (conjugate A x) (at level 35) : group_scope.
Notation "x ^: B" := (class x B) (at level 35) : group_scope.
Notation "A :^: B" := (conjugates A B) (at level 35) : group_scope.

Notation "#| B : A |" := (indexg B A)
  (at level 0, B, A at level 99, format "#| B : A |") : group_scope.

No notation for lcoset and rcoset, which are to be used mostly  
in curried form; x *: B and A :* 1 denote singleton products,   
so thus we can use mulgA, mulg1, etc, on, say, A :* 1 * B :* x. 
No notation for the set commutator generator set set_commg.     

Notation "''N' ( A )" := (normaliser A)
  (at level 8, format "''N' ( A )") : group_scope.
Notation "''N_' G ( A )" := (G%g :&: 'N(A))
  (at level 8, G at level 2, format "''N_' G ( A )") : group_scope.
Notation "A <| B" := (normal A B)
  (at level 70) : group_scope.
Notation "''C' ( A )" := (centraliser A)
  (at level 8, format "''C' ( A )") : group_scope.
Notation "''C_' G ( A )" := (G%g :&: 'C(A))
  (at level 8, G at level 2, format "''C_' G ( A )") : group_scope.
Notation "''C' [ x ]" := 'N([set x%g])
  (at level 8, format "''C' [ x ]") : group_scope.
Notation "''C_' G [ x ]" := 'N_G([set x%g])
  (at level 8, G at level 2, format "''C_' G [ x ]") : group_scope.


Implicit Arguments mem_repr [gT A].

Section SmulProp.

Variable gT : finGroupType.
Notation sT := {set gT}.
Implicit Types A B C D : sT.
Implicit Type x y z : gT.

Set product. We already have all the pregroup identities, so we 
only need to add the monotonicity rules.                        

Lemma mulsgP : forall A B x,
  reflect (imset2_spec mulg (mem A) (fun _ => mem B) x) (x \in A * B).

Lemma mem_mulg : forall A B x y, x \in A -> y \in B -> x * y \in A * B.

Lemma mulSg : forall A B C, A \subset B -> A * C \subset B * C.

Lemma mulgS : forall A B C, B \subset C -> A * B \subset A * C.

Lemma mulgSS : forall A B C D,
  A \subset B -> C \subset D -> A * C \subset B * D.

Lemma mulg_subl : forall A B, 1 \in B -> A \subset A * B.

Lemma mulg_subr : forall A B, 1 \in A -> B \subset A * B.

Lemma mulUg : forall A B C, (A :|: B) * C = (A * C) :|: (B * C).

Lemma mulgU : forall A B C, A * (B :|: C) = (A * B) :|: (A * C).

Set (pointwise) inverse. 

Lemma invUg : forall A B, (A :|: B)^-1 = A^-1 :|: B^-1.

Lemma invIg : forall A B, (A :&: B)^-1 = A^-1 :&: B^-1.

Lemma invDg : forall A B, (A :\: B)^-1 = A^-1 :\: B^-1.

Lemma invCg : forall A, (~: A)^-1 = ~: A^-1.

Lemma invSg : forall A B, (A^-1 \subset B^-1) = (A \subset B).

Lemma mem_invg : forall x A, (x \in A^-1) = (x^-1 \in A).

Lemma memV_invg : forall x A, (x^-1 \in A^-1) = (x \in A).

Lemma card_invg : forall A, #|A^-1| = #|A|.

Product with singletons. 

Lemma set1gE : 1 = [set 1] :> sT. Qed.

Lemma set1gP : forall x : gT, reflect (x = 1) (x \in [1]).

Lemma mulg_set1 : forall x y, [set x] :* y = [set x * y].

Lemma invg_set1 : forall x, [set x]^-1 = [set x^-1].

Cosets, left and right. 

Lemma lcosetE : forall A x, lcoset A x = x *: A.

Lemma card_lcoset : forall A x, #|x *: A| = #|A|.

Lemma mem_lcoset : forall A x y, (y \in x *: A) = (x^-1 * y \in A).

Lemma lcosetP : forall A x y,
  reflect (exists2 a, a \in A & y = x * a) (y \in x *: A).

Lemma lcosetsP : forall A B C,
  reflect (exists2 x, x \in B & C = x *: A) (C \in lcosets A B).

Lemma lcosetM : forall A x y, (x * y) *: A = x *: (y *: A).

On to the right, adding some algebraic lemmas 

Lemma rcosetE : forall A x, rcoset A x = A :* x.

Lemma card_rcoset : forall A x, #|A :* x| = #|A|.

Lemma mem_rcoset : forall A x y, (y \in A :* x) = (y * x^-1 \in A).

Lemma rcosetP : forall A x y,
  reflect (exists2 a, a \in A & y = a * x) (y \in A :* x).

Lemma rcosetsP : forall A B C,
  reflect (exists2 x, x \in B & C = A :* x) (C \in rcosets A B).

Lemma rcosetM : forall A x y, A :* (x * y) = A :* x :* y.

Probably redundant 
Lemma rcoset1 : forall A, A :* 1 = A.

Lemma rcosetK : forall x, cancel (fun A => A :* x) (fun A => A :* x^-1).

Lemma rcosetKV : forall x, cancel (fun A => A :* x^-1) (fun A => A :* x).

Lemma rcoset_inj : forall x, injective (fun A => A :* x).

Inverse map lcosets to rcosets 

Lemma lcosets_invg : forall A B, lcosets A^-1 B^-1 = invg @^-1: rcosets A B.

Conjugates. 

Lemma conjg_preim : forall A x, A :^ x = (conjg^~ x^-1) @^-1: A.

Lemma conjIg : forall A B x, (A :&: B) :^ x = A :^ x :&: B :^ x.

Lemma conjUg : forall A B x, (A :|: B) :^ x = A :^ x :|: B :^ x.

Lemma cardJg : forall A x, #|A :^ x| = #|A|.

Lemma mem_conjg : forall A x y, (y \in A :^ x) = (y ^ x^-1 \in A).

Lemma mem_conjgV : forall A x y, (y \in A :^ x^-1) = (y ^ x \in A).

Lemma memJ_conjg : forall A x y, (y ^ x \in A :^ x) = (y \in A).

Lemma conjsgE : forall A x, A :^ x = x^-1 *: (A :* x).

Lemma conjsg1 : forall A, A :^ 1 = A.

Lemma conjsgM : forall A x y, A :^ (x * y) = (A :^ x) :^ y.

Lemma conjsgK : forall x, cancel (fun A => A :^ x) (fun A => A :^ x^-1).

Lemma conjsgKV : forall x, cancel (fun A => A :^ x^-1) (fun A => A :^ x).

Lemma conjsg_inj : forall x, injective (fun A => A :^ x).

Lemma conjSg : forall A B x, (A :^ x \subset B :^ x) = (A \subset B).

Lemma sub_conjg : forall A B x, (A :^ x \subset B) = (A \subset B :^ x^-1).

Lemma sub_conjgV : forall A B x, (A :^ x^-1 \subset B) = (A \subset B :^ x).

Lemma conjg_set1 : forall x y, [set x] :^ y = [set x ^ y].

Lemma conjs1g : forall x, 1 :^ x = 1.

Lemma conjsMg : forall A B x, (A * B) :^ x = A :^ x * B :^ x.

Classes; not much for now. 

Lemma memJ_class : forall x y A, y \in A -> x ^ y \in x ^: A.

Lemma classS : forall x A B, A \subset B -> x ^: A \subset x ^: B.

Lemma class_set1 : forall x y, x ^: [set y] = [set x ^ y].

Lemma class1g : forall x A, x \in A -> 1 ^: A = 1.

Lemma class_supportM : forall A B C,
  class_support A (B * C) = class_support (class_support A B) C.

Lemma class_support_set1l : forall A x, class_support [set x] A = x ^: A.

Lemma class_support_set1r : forall A x, class_support A [set x] = A :^ x.

Lemma classM : forall x A B, x ^: (A * B) = class_support (x ^: A) B.

Lemma class_lcoset : forall x y A, x ^: (y *: A) = (x ^ y) ^: A.

Lemma class_rcoset : forall x A y, x ^: (A :* y) = (x ^: A) :^ y.

Conjugate set. 

Lemma conjugatesS : forall A B C, B \subset C -> A :^: B \subset A :^: C.

Lemma conjugates_set1 : forall A x, A :^: [set x] = [set A :^ x].

Lemma class_supportEl : forall A B,
  class_support A B = \bigcup_(x \in A) x ^: B.

Lemma class_supportEr : forall A B,
  class_support A B = \bigcup_(x \in B) A :^ x.

Groups (at last!) 

Definition group_set A := (1 \in A) && (A * A \subset A).

Lemma group_setP : forall A,
  reflect (1 \in A /\ {in A & A, forall x y, x * y \in A}) (group_set A).

Structure group_type : Type := Group {
  gval :> GroupSet.sort gT;
  _ : group_set gval
}.

Definition group_of of phant gT : predArgType := group_type.
Notation Local groupT := (group_of (Phant gT)).
Identity Coercion type_of_group : group_of >-> group_type.

Canonical Structure group_subType :=
  Eval hnf in [subType for gval by group_type_rect].
Definition group_eqMixin := Eval hnf in [eqMixin of group_type by <:].
Canonical Structure group_eqType := Eval hnf in EqType group_eqMixin.
Definition group_choiceMixin := [choiceMixin of group_type by <:].
Canonical Structure group_choiceType :=
  Eval hnf in ChoiceType group_choiceMixin.
Definition group_countMixin := [countMixin of group_type by <:].
Canonical Structure group_countType := Eval hnf in CountType group_countMixin.
Canonical Structure group_subCountType :=
  Eval hnf in [subCountType of group_type].
Definition group_finMixin := [finMixin of group_type by <:].
Canonical Structure group_finType := Eval hnf in FinType group_finMixin.
Canonical Structure group_subFinType := Eval hnf in [subFinType of group_type].

No predType or baseFinGroupType structures, as these would hide the 
group-to-set coercion and thus spoil unification.                  

Canonical Structure group_of_subType := Eval hnf in [subType of groupT].
Canonical Structure group_of_eqType := Eval hnf in [eqType of groupT].
Canonical Structure group_of_choiceType := Eval hnf in [choiceType of groupT].
Canonical Structure group_of_countType := Eval hnf in [countType of groupT].
Canonical Structure group_of_subCountType :=
  Eval hnf in [subCountType of groupT].
Canonical Structure group_of_finType := Eval hnf in [finType of groupT].
Canonical Structure group_of_subFinType := Eval hnf in [subFinType of groupT].

Definition group (A : {set gT}) gA : groupT := @Group A gA.

Definition repack_group G :=
  let: Group _ gP := G return {type of Group for G} -> groupT in fun k => k gP.

Lemma group_inj : injective gval. Qed.

Lemma groupP : forall G : groupT, group_set G. Qed.

Lemma congr_group : forall H K : groupT, H = K -> H :=: K.

Lemma isgroupP : forall A, reflect (exists G : groupT, A = G) (group_set A).

Lemma group_set_one : group_set 1.

Canonical Structure one_group := group group_set_one.
Canonical Structure set1_group := @group [set 1] group_set_one.

Lemma group_setT : group_set setT.

Canonical Structure setT_group := group group_setT.

These definitions come early so we can establish the Notation. 
Definition generated A := \bigcap_(G : groupT | A \subset G) G.
Definition mulgen A B := generated (A :|: B).
Definition commutator A B := generated (commg_set A B).
Definition cycle x := generated [set x].
Definition order x := #|cycle x|.

End SmulProp.

Implicit Arguments mulsgP [gT A B x].
Implicit Arguments set1gP [gT x].
Implicit Arguments lcosetP [gT A x y].
Implicit Arguments lcosetsP [gT A B C].
Implicit Arguments rcosetP [gT A x y].
Implicit Arguments rcosetsP [gT A B C].
Implicit Arguments group_setP [gT A].


Notation "{ 'group' gT }" := (group_of (Phant gT))
  (at level 0, format "{ 'group' gT }") : type_scope.

Notation "[ 'group' 'of' G ]" := (repack_group (fun gP => @group _ G gP))
  (at level 0, format "[ 'group' 'of' G ]") : form_scope.

Notation "1" := (one_group _) : subgroup_scope.
Notation "[ 1 gT ]" := (1%G : {group gT})
  (at level 0, format "[ 1 gT ]") : subgroup_scope.
Notation "[ 'setT' ]" := (setT_group _)
  (at level 0, format "[ 'setT' ]") : subgroup_scope.
Notation "[ 'setT' gT ]" := ([setT]%G : {group gT})
  (at level 0, format "[ 'setT' gT ]") : subgroup_scope.

Notation "<< A >>" := (generated A)
  (at level 0, format "<< A >>") : group_scope.

Notation "<[ x ] >" := (cycle x)
  (at level 0, format "<[ x ] >") : group_scope.

Notation "#[ x ]" := (order x) (at level 0, format "#[ x ]") : group_scope.

Notation "A <*> B" := (mulgen A B) (at level 40) : group_scope.

Notation "[ ~: A1 , A2 , .. , An ]" := (commutator ..


Section GroupProp.

Variable gT : finGroupType.
Notation sT := {set gT}.
Implicit Types A B C D : sT.
Implicit Types x y z : gT.
Implicit Types G H K : {group gT}.

Section OneGroup.

Variable G : {group gT}.

Lemma valG : val G = G. Qed.

Non-triviality. 

Lemma group1 : 1 \in G. Qed.

Hint Resolve group1.

Loads of silly variants to placate the incompleteness of trivial. 
An alternative would be to upgrade done, pending better support   
in the ssreflect ML code.                                         
Notation gTr := (FinGroup.sort gT).
Notation Gcl := (pred_of_set G : pred gTr).
Lemma group1_class1 : (1 : gTr) \in G. Qed.

Lemma group1_class2 : 1 \in Gcl. Qed.

Lemma group1_class12 : (1 : gTr) \in Gcl. Qed.

Lemma group1_eqType : (1 : gT : eqType) \in G. Qed.

Lemma group1_finType : (1 : gT : finType) \in G. Qed.

Lemma sub1G : [1 gT] \subset G. Qed.

Lemma subG1 : (G \subset [1]) = (G :==: 1).

Lemma repr_group : repr G = 1. Qed.

Lemma cardG_gt0 : 0 < #|G|.

Lemma indexg_gt0 : forall A, 0 < #|G : A|.

Lemma trivgP : reflect (G :=: 1) (G \subset [1]).

Lemma trivGP : reflect (G = 1%G) (G \subset [1]).

Lemma proper1G : ([1] \proper G) = (G :!=: 1).

Lemma trivgPn : reflect (exists2 x, x \in G & x != 1) (G :!=: 1).

Lemma trivg_card_le1 : (G :==: 1) = (#|G| <= 1).

Lemma trivg_card1 : (G :==: 1) = (#|G| == 1%N).

Lemma card_le1_trivg : #|G| <= 1 -> G :=: 1.

Lemma card1_trivg : #|G| = 1%N -> G :=: 1.

Inclusion and product. 

Lemma mulG_subl : forall A, A \subset A * G.

Lemma mulG_subr : forall A, A \subset G * A.

Lemma mulGid : G * G = G.

Lemma mulGS : forall A B, (G * A \subset G * B) = (A \subset G * B).

Lemma mulSG : forall A B, (A * G \subset B * G) = (A \subset B * G).

Lemma mul_subG : forall A B, A \subset G -> B \subset G -> A * B \subset G.

Membership lemmas 

Lemma groupM : forall x y, x \in G -> y \in G -> x * y \in G.

Lemma groupX : forall x n, x \in G -> x ^+ n \in G.

Lemma groupVr : forall x, x \in G -> x^-1 \in G.

Lemma groupVl : forall x, x^-1 \in G -> x \in G.

Lemma groupV : forall x, (x^-1 \in G) = (x \in G).

Lemma groupMl : forall x y, x \in G -> (x * y \in G) = (y \in G).

Lemma groupMr : forall x y, x \in G -> (y * x \in G) = (y \in G).

Definition in_group := (group1, groupV, (groupMl, groupX)).

Lemma groupJ : forall x y, x \in G -> y \in G -> x ^ y \in G.

Lemma groupJr : forall x y, y \in G -> (x ^ y \in G) = (x \in G).

Lemma groupR : forall x y, x \in G -> y \in G -> [~ x, y] \in G.

Inverse is an anti-morphism. 

Lemma invGid : G^-1 = G. Qed.

Lemma inv_subG : forall A, (A^-1 \subset G) = (A \subset G).

Lemma invg_lcoset : forall x, (x *: G)^-1 = G :* x^-1.

Lemma invg_rcoset : forall x, (G :* x)^-1 = x^-1 *: G.

Lemma memV_lcosetV : forall x y, (y^-1 \in x^-1 *: G) = (y \in G :* x).

Lemma memV_rcosetV : forall x y, (y^-1 \in G :* x^-1) = (y \in x *: G).

Product idempotence 

Lemma mulSgGid : forall A x, x \in A -> A \subset G -> A * G = G.

Lemma mulGSgid : forall A x, x \in A -> A \subset G -> G * A = G.

Left cosets 

Lemma lcoset_refl : forall x, x \in x *: G.

Lemma lcoset_sym : forall x y, (x \in y *: G) = (y \in x *: G).

Lemma lcoset_transl : forall x y, x \in y *: G -> x *: G = y *: G.

Lemma lcoset_transr : forall x y z,
  x \in y *: G -> (x \in z *: G) = (y \in z *: G).

Lemma lcoset_trans : forall x y z,
  x \in y *: G -> y \in z *: G -> x \in z *: G.

Lemma lcoset_id : forall x, x \in G -> x *: G = G.

Right cosets, with an elimination form for repr. 

Lemma rcoset_refl : forall x, x \in G :* x.

Lemma rcoset_sym : forall x y, (x \in G :* y) = (y \in G :* x).

Lemma rcoset_transl : forall x y, x \in G :* y -> G :* x = G :* y.

Lemma rcoset_transr : forall x y z,
  x \in G :* y -> (x \in G :* z) = (y \in G :* z).

Lemma rcoset_trans : forall x y z,
  y \in G :* x -> z \in G :* y -> z \in G :* x.

Lemma rcoset_id : forall x, x \in G -> G :* x = G.

Elimination form. 

CoInductive rcoset_repr_spec x : gT -> Type :=
  RcosetReprSpec g : g \in G -> rcoset_repr_spec x (g * x).

Lemma mem_repr_rcoset : forall x, repr (G :* x) \in G :* x.

This form sometimes fails because ssreflect 1.1 delegates matching to the 
(weaker) primitive Coq algorithm for general (co)inductive type families. 
Lemma repr_rcosetP : forall x, rcoset_repr_spec x (repr (G :* x)).

Lemma rcoset_repr : forall x, G :* (repr (G :* x)) = G :* x.

Coset spaces. 

Lemma mem_lcosets : forall A x, (x *: G \in lcosets G A) = (x \in A * G).

Lemma mem_rcosets : forall A x, (G :* x \in rcosets G A) = (x \in G * A).

Conjugates. 

Lemma group_set_conjG : forall x, group_set (G :^ x).

Canonical Structure conjG_group x := group (group_set_conjG x).

Lemma conjGid : {in G, normalised G}.

Lemma conj_subG : forall x A, x \in G -> A \subset G -> A :^ x \subset G.

Classes 

Lemma class1G : 1 ^: G = 1. Qed.

Lemma classGidl : forall x y, y \in G -> (x ^ y) ^: G = x ^: G.

Lemma classGidr : forall x, {in G, normalised (x ^: G)}.

Lemma class_refl : forall x, x \in x ^: G.
Hint Resolve class_refl.

Lemma class_transr : forall x y, x \in y ^: G -> x ^: G = y ^: G.

Lemma class_sym : forall x y, (x \in y ^: G) = (y \in x ^: G).

Lemma class_transl : forall x y z,
   x \in y ^: G -> (x \in z ^: G) = (y \in z ^: G).

Lemma class_trans : forall x y z,
   x \in y ^: G -> y \in z ^: G -> x \in z ^: G.

Lemma repr_class : forall x, {y | y \in G & repr (x ^: G) = x ^ y}.

Lemma class_subG : forall x A, x \in G -> A \subset G -> x ^: A \subset G.

Lemma class_supportGidl : forall A x,
  x \in G -> class_support (A :^ x) G = class_support A G.

Lemma class_supportGidr : forall A, {in G, normalised (class_support A G)}.

Subgroup Type construction. 
We only expect to use this for abstract groups, so we don't project 
the argument to a set.                                              

Inductive subg_of : predArgType := Subg x & x \in G.
Definition sgval u := let: Subg x _ := u in x.
Canonical Structure subg_subType :=
  Eval hnf in [subType for sgval by subg_of_rect].
Definition subg_eqMixin := Eval hnf in [eqMixin of subg_of by <:].
Canonical Structure subg_eqType := Eval hnf in EqType subg_eqMixin.
Definition subg_choiceMixin := [choiceMixin of subg_of by <:].
Canonical Structure subg_choiceType := Eval hnf in ChoiceType subg_choiceMixin.
Definition subg_countMixin := [countMixin of subg_of by <:].
Canonical Structure subg_countType := Eval hnf in CountType subg_countMixin.
Canonical Structure subg_subCountType := Eval hnf in [subCountType of subg_of].
Definition subg_finMixin := [finMixin of subg_of by <:].
Canonical Structure subg_finType := Eval hnf in FinType subg_finMixin.
Canonical Structure subg_subFinType := Eval hnf in [subFinType of subg_of].

Lemma subgP : forall u, sgval u \in G.
Lemma subg_inj : injective sgval.
Lemma congr_subg : forall u v, u = v -> sgval u = sgval v.

Definition subg_one := Subg group1.
Definition subg_inv u := Subg (groupVr (subgP u)).
Definition subg_mul u v := Subg (groupM (subgP u) (subgP v)).
Lemma subg_oneP : left_id subg_one subg_mul.
Lemma subg_invP : left_inverse subg_one subg_inv subg_mul.
Lemma subg_mulP : associative subg_mul.

Definition subFinGroupMixin := FinGroup.Mixin subg_mulP subg_oneP subg_invP.
Canonical Structure subBaseFinGroupType :=
  Eval hnf in BaseFinGroupType subFinGroupMixin.
Canonical Structure subFinGroupType := FinGroupType subg_invP.

Lemma sgvalM : {in setT &, {morph sgval : x y / x * y}}. Qed.

Lemma valgM : {in setT &, {morph val : x y / (x : subg_of) * y >-> x * y}}.

Definition subg : gT -> subg_of := insubd (1 : subg_of).
Lemma subgK : forall x, x \in G -> val (subg x) = x.
Lemma sgvalK : cancel sgval subg.
Lemma subg_default : forall x, (x \in G) = false -> val (subg x) = 1.
Lemma subgM : {in G &, {morph subg : x y / x * y}}.

End OneGroup.

Hint Resolve group1.

Lemma invMG : forall G H, (G * H)^-1 = H * G.

Lemma mulSGid : forall G H, H \subset G -> H * G = G.

Lemma mulGSid : forall G H, H \subset G -> G * H = G.

Lemma comm_group_setP : forall G H, reflect (commute G H) (group_set (G * H)).

Lemma card_lcosets : forall G H, #|lcosets H G| = #|G : H|.

Group Modularity equations 

Lemma group_modl : forall A B G, A \subset G -> A * (B :&: G) = A * B :&: G.

Lemma group_modr : forall A B G, B \subset G -> (G :&: A) * B = G :&: A * B.

End GroupProp.

Hint Resolve group1 group1_class1 group1_class12 group1_class12.
Hint Resolve group1_eqType group1_finType.
Hint Resolve cardG_gt0 indexg_gt0.

Notation "G :^ x" := (conjG_group G x) : subgroup_scope.

Notation "[ 'subg' G ]" := (@finset.setT (subg_finType G))
  (at level 0, format "[ 'subg' G ]") : group_scope.
Notation "[ 'subg' G ]" := (setT_group (subFinGroupType G)) : subgroup_scope.


Implicit Arguments trivgP [gT G].
Implicit Arguments trivGP [gT G].
Implicit Arguments comm_group_setP [gT G H].

Section GroupInter.

Variable gT : finGroupType.
Implicit Types A B : {set gT}.
Implicit Types G H : {group gT}.

Lemma group_setI : forall G H, group_set (G :&: H).

Canonical Structure setI_group G H := group (group_setI G H).

Section Nary.

Variables (I : finType) (P : pred I) (F : I -> {group gT}).

Lemma group_set_bigcap : group_set (\bigcap_(i | P i) F i).

Canonical Structure bigcap_group := group group_set_bigcap.

End Nary.

Canonical Structure generated_group A : {group _} :=
  Eval hnf in [group of <<A>>].
Canonical Structure commutator_group A B : {group _} :=
  Eval hnf in [group of [~: A, B]].
Canonical Structure mulgen_group A B : {group _} :=
  Eval hnf in [group of A <*> B].
Canonical Structure cycle_group x : {group _} :=
  Eval hnf in [group of <[x]>].

Lemma order_gt0 : forall x : gT, 0 < #[x].
Canonical Structure order_pos_nat x := PosNat (order_gt0 x).

End GroupInter.

Hint Resolve order_gt0.

Definition mulGen (gT : finGroupType) (G H : {group gT}) :=
  nosimpl (mulgen_group G H).


Notation "G :&: H" := (setI_group G H) : subgroup_scope.
Notation "<< A >>" := (generated_group A) : subgroup_scope.
Notation "<[ x ] >" := (cycle_group x) : subgroup_scope.
Notation "[ ~: A1 , A2 , .. , An ]" :=
  (commutator_group ..
Notation "G <*> H" := (mulGen G H) : subgroup_scope.

Notation "\prod_ ( <- r | P ) F" :=
  (\big[mulGen/1%G]_(<- r | P%B) F%G) : subgroup_scope.
Notation "\prod_ ( i <- r | P ) F" :=
  (\big[mulGen/1%G]_(i <- r | P%B) F%G) : subgroup_scope.
Notation "\prod_ ( i <- r ) F" :=
  (\big[mulGen/1%G]_(i <- r) F%G) : subgroup_scope.
Notation "\prod_ ( m <= i < n | P ) F" :=
  (\big[mulGen/1%G]_(m <= i < n | P%B) F%G) : subgroup_scope.
Notation "\prod_ ( m <= i < n ) F" :=
  (\big[mulGen/1%G]_(m <= i < n) F%G) : subgroup_scope.
Notation "\prod_ ( i | P ) F" :=
  (\big[mulGen/1%G]_(i | P%B) F%G) : subgroup_scope.
Notation "\prod_ i F" :=
  (\big[mulGen/1%G]_i F%G) : subgroup_scope.
Notation "\prod_ ( i : t | P ) F" :=
  (\big[mulGen/1%G]_(i : t | P%B) F%G) (only parsing) : subgroup_scope.
Notation "\prod_ ( i : t ) F" :=
  (\big[mulGen/1%G]_(i : t) F%G) (only parsing) : subgroup_scope.
Notation "\prod_ ( i < n | P ) F" :=
  (\big[mulGen/1%G]_(i < n | P%B) F%G) : subgroup_scope.
Notation "\prod_ ( i < n ) F" :=
  (\big[mulGen/1%G]_(i < n) F%G) : subgroup_scope.
Notation "\prod_ ( i \in A | P ) F" :=
  (\big[mulGen/1%G]_(i \in A | P%B) F%G) : subgroup_scope.
Notation "\prod_ ( i \in A ) F" :=
  (\big[mulGen/1%G]_(i \in A) F%G) : subgroup_scope.

Section LaGrange.

Variable gT : finGroupType.
Implicit Types G H K : {group gT}.

Lemma LaGrangeI : forall G H, (#|G :&: H| * #|G : H|)%N = #|G|.

Lemma divgI : forall G H, #|G| %/ #|G :&: H| = #|G : H|.

Lemma divg_index : forall G H, #|G| %/ #|G : H| = #|G :&: H|.

Lemma dvdn_indexg : forall G H, #|G : H| %| #|G|.

Theorem LaGrange : forall G H, H \subset G -> (#|H| * #|G : H|)%N = #|G|.

Lemma cardSg : forall G H, H \subset G -> #|H| %| #|G|.

Lemma divgS : forall G H, H \subset G -> #|G| %/ #|H| = #|G : H|.

Lemma indexJg : forall G H x, #|G :^ x : H :^ x| = #|G : H|.

Lemma indexgg : forall G, #|G : G| = 1%N.

Lemma LaGrange_index : forall G H K,
  H \subset G -> K \subset H -> (#|G : H| * #|H : K|)%N = #|G : K|.

Lemma indexgI : forall G H, #|G : G :&: H| = #|G : H|.

Lemma indexgS : forall G H K, H \subset K -> #|G : K| %| #|G : H|.

Lemma indexSg : forall G H K,
  H \subset K -> K \subset G -> #|K : H| %| #|G : H|.

Lemma index1g : forall G H, H \subset G -> #|G : H| = 1%N -> H = G.

Lemma indexg1 : forall G, #|G : 1| = #|G|.

Lemma mul_cardG : forall G H, (#|G| * #|H| = #|G * H|%g * #|G :&: H|)%N.

Lemma TI_cardMg : forall G H, G :&: H = 1 -> #|G * H| = (#|G| * #|H|)%N.

Lemma cardMg_TI : forall G H, #|G| * #|H| <= #|G * H| -> G :&: H = 1.

Lemma coprime_TIg : forall G H, coprime #|G| #|H| -> G :&: H = 1.

Lemma coprime_cardMg : forall G H,
  coprime #|G| #|H| -> #|G * H| = (#|G| * #|H|)%N.

End LaGrange.

Section GeneratedGroup.

Variable gT : finGroupType.
Notation sT := {set gT}.
Implicit Types x y z : gT.
Implicit Types A B C D : sT.
Implicit Types G H K : {group gT}.

Lemma subset_gen : forall A, A \subset <<A>>.

Lemma sub_gen : forall A B, A \subset B -> A \subset <<B>>.

Lemma mem_gen : forall x A, x \in A -> x \in <<A>>.

Lemma generatedP : forall x A,
  reflect (forall G, A \subset G -> x \in G) (x \in <<A>>).

Lemma gen_subG : forall A G, (<<A>> \subset G) = (A \subset G).

Lemma genGid : forall G, <<G>> = G.

Lemma genGidG : forall G, <<G>>%G = G.

Lemma gen_set_id : forall A, group_set A -> <<A>> = A.

Lemma genS : forall A B, A \subset B -> <<A>> \subset <<B>>.

Lemma gen0 : <<set0>> = 1 :> {set gT}.

Lemma genD : forall A B, A \subset <<A :\: B>> -> <<A :\: B>> = <<A>>.

Lemma genV : forall A, <<A^-1>> = <<A>>.

Lemma genJ : forall A z, <<A :^z>> = <<A>> :^ z.

Lemma genD1 : forall A x, x \in <<A :\ x>> -> <<A :\ x>> = <<A>>.

Notation mulgenT := (@mulgen gT) (only parsing).
Notation mulGenT := (@mulGen gT) (only parsing).

Lemma mulgenE : forall A B, A <*> B = <<A :|: B>>. Qed.

Lemma mulGenE : forall G H, (G <*> H)%G :=: G <*> H. Qed.

Lemma mulgenC : commutative mulgenT.

Lemma mulgen_idr : forall A B, A <*> <<B>> = A <*> B.

Lemma mulgen_idl : forall A B, <<A>> <*> B = A <*> B.

Lemma mulgen_subl : forall A B, A \subset A <*> B.

Lemma mulgen_subr : forall A B, B \subset A <*> B.

Lemma mulgen_subG : forall A B G,
  (A <*> B \subset G) = (A \subset G) && (B \subset G).

Lemma genDU : forall A B C,
  A \subset C -> <<C :\: A>> = <<B>> -> <<A :|: B>> = <<C>>.

Lemma mulgenA : associative mulgenT.

Lemma mulgen1G : forall G, 1 <*> G = G.

Lemma mulgenG1 : forall G, G <*> 1 = G.

Lemma genM_mulgen : forall G H, <<G * H>> = G <*> H.

Lemma trivMg : forall G H, (G * H == 1) = (G :==: 1) && (H :==: 1).

Lemma comm_mulgenE : forall G H, commute G H -> G <*> H = G * H.

Lemma mulGenC : commutative mulGenT.

Lemma mulGenA : associative mulGenT.

Lemma mulGen1G : left_id 1%G mulGenT.

Lemma mulGenG1 : right_id 1%G mulGenT.

Canonical Structure mulGen_law := Monoid.Law mulGenA mulGen1G mulGenG1.
Canonical Structure mulGen_abelaw := Monoid.ComLaw mulGenC.

Lemma bigprodGEgen : forall I r (P : pred I) (F : I -> {set gT}),
  (\prod_(i <- r | P i) <<F i>>)%G :=: << \bigcup_(i <- r | P i) F i >>.

Lemma bigprodGE : forall I r (P : pred I) (F : I -> {group gT}),
  (\prod_(i <- r | P i) F i)%G :=: << \bigcup_(i <- r | P i) F i >>.

Lemma mem_commg : forall A B x y, x \in A -> y \in B -> [~ x, y] \in [~: A, B].

Lemma commSg : forall A B C, A \subset B -> [~: A, C] \subset [~: B, C].

Lemma commgS : forall A B C, B \subset C -> [~: A, B] \subset [~: A, C].

Lemma commgSS : forall A B C D,
  A \subset B -> C \subset D -> [~: A, C] \subset [~: B, D].

Lemma der1_subG : forall G, [~: G, G] \subset G.

Lemma comm_subG : forall A B G,
  A \subset G -> B \subset G -> [~: A, B] \subset G.

Lemma commGC : forall A B, [~: A, B] = [~: B, A].

Lemma conjsRg : forall A B x, [~: A, B] :^ x = [~: A :^ x, B :^ x].

End GeneratedGroup.

Section Cycles.

Elementary properties of cycles and order, needed in perm.v.  
More advanced results on the structure of cyclic groups will  
be given in cyclic.v.                                         

Variable gT : finGroupType.
Implicit Types x y : gT.
Implicit Types G : {group gT}.

Import Monoid.Theory.

Lemma cycle1 : <[1]> = [1 gT].

Lemma order1 : #[1 : gT] = 1%N.

Lemma cycle_id : forall x, x \in <[x]>.

Lemma mem_cycle : forall x i, x ^+ i \in <[x]>.

Lemma cycle_subG : forall x G, (<[x]> \subset G) = (x \in G).

Lemma cycle_traject : forall x, <[x]> =i traject (mulg x) 1 #[x].

Lemma cyclePmin : forall x y,
  reflect (exists2 i, i < #[x] & y = x ^+ i) (y \in <[x]>).

Lemma cycleP : forall x y, reflect (exists i, y = x ^+ i) (y \in <[x]>).

Lemma expg_order : forall x, x ^+ #[x] = 1.

Lemma expg_mod_order : forall x i, x ^+ (i %% #[x]) = x ^+ i.

Lemma invg_expg : forall x, x^-1 = x ^+ #[x].-1.

Lemma cycleX : forall x i, <[x ^+ i]> \subset <[x]>.

Lemma cycleV : forall x, <[x^-1]> = <[x]>.

Lemma orderV : forall x, #[x^-1] = #[x].

Lemma cycleJ : forall x y, <[x ^ y]> = <[x]> :^ y.

Lemma orderJ : forall x y, #[x ^ y] = #[x].

End Cycles.

Section Normaliser.

Variable gT : finGroupType.
Notation sT := {set gT}.
Implicit Types x y z : gT.
Implicit Types A B C D : sT.
Implicit Type G H K : {group gT}.

Lemma normP : forall x A, reflect (A :^ x = A) (x \in 'N(A)).
Implicit Arguments normP [x A].

Lemma group_set_normaliser : forall A, group_set 'N(A).

Canonical Structure normaliser_group A := group (group_set_normaliser A).

Lemma normsP : forall A B, reflect {in A, normalised B} (A \subset 'N(B)).
Implicit Arguments normsP [A B].

Lemma memJ_norm : forall x y A, x \in 'N(A) -> (y ^ x \in A) = (y \in A).

Lemma norm1 : 'N(1) = setT :> {set gT}.

Lemma norms1 : forall A, A \subset 'N(1).

Lemma normG : forall G, G \subset 'N(G).

Lemma normsG : forall A G, A \subset G -> A \subset 'N(G).

Lemma normC : forall A B, A \subset 'N(B) -> commute A B.

Lemma norm_mulgenEl : forall G H, G \subset 'N(H) -> G <*> H = G * H.

Lemma norm_mulgenEr : forall G H, H \subset 'N(G) -> G <*> H = G * H.

Lemma norm_rlcoset : forall G x, x \in 'N(G) -> G :* x = x *: G.

Lemma rcoset_mul : forall G x y,
  x \in 'N(G) -> (G :* x) * (G :* y) = G :* (x * y).

Lemma normJ : forall A x, 'N(A :^ x) = 'N(A) :^ x.

Lemma norm_gen : forall A, 'N(A) \subset 'N(<<A>>).

Lemma norm_class : forall x G, G \subset 'N(x ^: G).

Section norm_trans.

Variables A B C : {set gT}.
Hypotheses (nBA : A \subset 'N(B)) (nCA : A \subset 'N(C)).

Lemma norms_gen : A \subset 'N(<<B>>).

Lemma norms_norm : A \subset 'N('N(B)).

Lemma normsI : A \subset 'N(B :&: C).

Lemma normsM : A \subset 'N(B * C).

Lemma norms_mulgen : A \subset 'N(B <*> C).

Lemma normsR : A \subset 'N([~: B, C]).

End norm_trans.

Lemma normalP : forall A B,
  reflect (A \subset B /\ {in B, normalised A}) (A <| B).

Lemma normal_norm : forall A B, A <| B -> B \subset 'N(A).

Lemma normal_sub : forall A B, A <| B -> A \subset B.

Lemma normalS : forall G H K,
  K \subset H -> H \subset G -> K <| G -> K <| H.

Lemma normal1 : forall G, 1 <| G.

Lemma normal_refl : forall G, G <| G.

Lemma normalG : forall G, G <| 'N(G).

Lemma normalSG : forall G H, H \subset G -> H <| 'N_G(H).

Lemma normalM : forall G H K, H <| G -> K <| G -> H * K <| G.

Lemma normal_subnorm : forall G H, (H <| 'N_G(H)) = (H \subset G).

Lemma cent1P : forall x y, reflect (commute x y) (x \in 'C[y]).

Canonical Structure centraliser_group A : {group _} :=
  Eval hnf in [group of 'C(A)].

Lemma cent_set1 : forall x, 'C([set x]) = 'C[x].

Lemma centP : forall A x, reflect (centralises x A) (x \in 'C(A)).

Lemma centsP : forall A B, reflect {in A, centralised B} (A \subset 'C(B)).

Lemma centsC : forall A B, (A \subset 'C(B)) = (B \subset 'C(A)).

Lemma cents1 : forall A, A \subset 'C(1).

Lemma cent1T : 'C(1) = setT :> {set gT}.

Lemma cent11T : 'C[1] = setT :> {set gT}.

Lemma cent_sub : forall A, 'C(A) \subset 'N(A).

Lemma cents_norm : forall A B, A \subset 'C(B) -> A \subset 'N(B).

Lemma centC : forall A B, A \subset 'C(B) -> commute A B.

Lemma cent_mulgenEl : forall G H, G \subset 'C(H) -> G <*> H = G * H.

Lemma cent_mulgenEr : forall G H, H \subset 'C(G) -> G <*> H = G * H.

Lemma centJ : forall A x, 'C(A :^ x) = 'C(A) :^ x.

Lemma cent_norm : forall A, 'N(A) \subset 'N('C(A)).

Lemma norms_cent : forall A B, A \subset 'N(B) -> A \subset 'N('C(B)).

Lemma cent_normal : forall A, 'C(A) <| 'N(A).

Lemma centS : forall A B, B \subset A -> 'C(A) \subset 'C(B).

Lemma centsS : forall A B C, A \subset B -> C \subset 'C(B) -> C \subset 'C(A).

Lemma centSS : forall A B C D,
  A \subset C -> B \subset D -> C \subset 'C(D) -> A \subset 'C(B).

Lemma centI : forall A B, 'C(A) <*> 'C(B) \subset 'C(A :&: B).

Lemma centU : forall A B, 'C(A :|: B) = 'C(A) :&: 'C(B).

Lemma cent_gen : forall A, 'C(<<A>>) = 'C(A).

Lemma cent_mulgen : forall A B, 'C(A <*> B) = 'C(A) :&: 'C(B).

Lemma centM : forall G H, 'C(G * H) = 'C(G) :&: 'C(H).

Lemma cent_classP : forall x G, reflect (x ^: G = [set x]) (x \in 'C(G)).

Lemma commG1P : forall A B, reflect ([~: A, B] = 1) (A \subset 'C(B)).

Lemma abelianE : forall A, abelian A = (A \subset 'C(A)). Qed.

Lemma abelian1 : abelian [1 gT]. Qed.

Lemma abelianS : forall A B, A \subset B -> abelian B -> abelian A.

Lemma abelianJ : forall A x, abelian (A :^ x) = abelian A.

End Normaliser.

Implicit Arguments normP [gT x A].
Implicit Arguments centP [gT x A].
Implicit Arguments normsP [gT A B].
Implicit Arguments cent1P [gT x y].
Implicit Arguments normalP [gT A B].
Implicit Arguments centsP [gT A B].
Implicit Arguments commG1P [gT A B].



Notation "''N' ( A )" := (normaliser_group A) : subgroup_scope.
Notation "''C' ( A )" := (centraliser_group A) : subgroup_scope.
Notation "''C' [ x ]" := ('N([set x%g]))%G : subgroup_scope.
Notation "''N_' G ( A )" := (G :&: 'N(A))%G : subgroup_scope.
Notation "''C_' G ( A )" := (G :&: 'C(A))%G : subgroup_scope.
Notation "''C_' G [ x ]" := ('N_G([set x%g]))%G : subgroup_scope.

Hint Resolve normal_refl.

Section MinMaxGroup.

Variable gT : finGroupType.
Variable gP : pred {group gT}.

Definition maxgroup := maxset (fun A => group_set A && gP <<A>>).
Definition mingroup := minset (fun A => group_set A && gP <<A>>).

Lemma ex_maxgroup : (exists G, gP G) -> {G : {group gT} | maxgroup G}.

Lemma ex_mingroup : (exists G, gP G) -> {G : {group gT} | mingroup G}.

Variable G : {group gT}.

Lemma mingroupP :
  reflect (gP G /\ forall H, gP H -> H \subset G -> H :=: G) (mingroup G).

Lemma maxgroupP :
  reflect (gP G /\ forall H, gP H -> G \subset H -> H :=: G) (maxgroup G).

Lemma maxgroupp : maxgroup G -> gP G. Qed.

Lemma mingroupp : mingroup G -> gP G. Qed.

Hypothesis gPG : gP G.

Lemma maxgroup_exists : {H : {group gT} | maxgroup H & G \subset H}.

Lemma mingroup_exists : {H : {group gT} | mingroup H & H \subset G}.

End MinMaxGroup.

Notation "[ 'max' A 'of' G | gP ]" := (maxgroup (fun G : {group _} => gP) A)
  (at level 0, format "[ 'max' A 'of' G | gP ]") : group_scope.

Notation "[ 'max' G | gP ]" := [max gval G of G | gP]
  (at level 0, format "[ 'max' G | gP ]") : group_scope.

Notation "[ 'min' A 'of' G | gP ]" := (mingroup (fun G : {group _} => gP) A)
  (at level 0, format "[ 'min' A 'of' G | gP ]") : group_scope.

Notation "[ 'min' G | gP ]" := [min gval G of G | gP]
  (at level 0, format "[ 'min' G | gP ]") : group_scope.

Implicit Arguments mingroupP [gT gP G].
Implicit Arguments maxgroupP [gT gP G].