Library mathcomp.boot.monoid

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice ssrnat seq.
From mathcomp Require Import bigop fintype finfun.

Group-like structures NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. This file defines the following algebraic structures: magmaType == magma The HB class is called Magma. ChoiceMagma.type == join of magmaType and choiceType The HB class is called ChoiceMagma. semigroupType == associative magma The HB class is called Semigroup. baseUMagmaType == pointed magma The HB class is called BaseUMagma. ChoiceBaseUMagma.type == join of baseUMagmaType and choiceType The HB class is called ChoiceBaseUMagma. umagmaType == unitary magma The HB class is called UMagma. monoidType == monoid The HB class is called Monoid. baseGroupType == pointed magma with an inversion operator The HB class is called BaseGroup. starMonoidType == *-monoid, i.e. monoid with an involutive antiautomorphism The HB class is called BaseGroup. groupType == group The HB class is called Group. and their joins with subType: subMagmaType V P == join of magmaType and subType (P : pred V) such that val is multiplicative The HB class is called SubMagma. subSemigroupType V P == join of semigroupType and subType (P : pred V) such that val is multiplicative The HB class is called SubSemigroup. subBaseUMagmaType V P == join of baseUMagmaType and subType (P : pred V) such that val is multiplicative and preserves 1 The HB class is called SubBaseUMagma. subUMagmaType V P == join of UMagmaType and subType (P : pred V) such that val is multiplicative and preserves 1 The HB class is called SubUMagma. subMonoidType V P == join of monoidType and subType (P : pred V) such that val is multiplicative and preserves 1 The HB class is called SubMonoid. subGroupType V P == join of groupType and subType (P : pred V) such that val is multiplicative and preserves 1 The HB class is called SubGroup. Morphisms between the above structures: Multiplicative.type G H == multiplicative functions between magmaType instances G and H UMagmaMorphism.type G H == multiplicative functions preserving 1 between baseUMagmaType instances G and H Closedness predicates for the algebraic structures: mulgClosed V == predicate closed under multiplication on G : magmaType The HB class is called MulClosed. umagmaClosed V == predicate closed under multiplication and containing 1 on G : baseUMagmaType The HB class is called UMagmaClosed. invgClosed V == predicate closed under inversion on G : baseGroupType The HB class is called InvClosed. groupClosed V == predicate closed under multiplication and inversion and containing 1 on G : baseGroupType The HB class is called InvClosed. Canonical properties of the algebraic structures:

magmaType (magmas):

x * y == the product of x and y commute x y <-> x and y commute (i.e. x * y = y * x) mulg_closed S <-> collective predicate S is closed under multiplication

baseUMagmaType (pointed magmas):

1 == the unit of a unitary magma x ^+ n == x to the power n, with n in nat (non-negative), i.e. x * (x * .. (x * x)..) (n terms); x ^+ 1 is thus convertible to x, and x ^+ 2 to x * x \prod<range> e == iterated product for a baseUMagmaType (cf bigop.v) umagma_closed S <-> collective predicate S is closed under multiplication and contains 1

monoidType (monoids):

monoid_closed S := umagma_closed S

baseGroupType (pointed magmas with an inversion operator):

x ^-1 == the inverse of x x / y == x * (y ^- 1) x ^- n == (x ^+ n)^-1 x ^ y := y^-1 * (x * y) == the conjugate of x by y [~ x, y] := x^-1 * (y^-1 * (x * y) == the commutator of x and y invg_closed S <-> collective predicate S is closed under inversion divg_closed S <-> collective predicate S is closed under division group_closed S <-> collective predicate S is closed under division and contains 1 In addition to this structure hierarchy, we also develop a separate,

Multiplicative (magma morphisms):

{multiplicative U -> V} == the interface type for magma morphisms, i.e. functions from U to V which maps * in U to * in V; both U and V must have magmaType instances := GRing.RMorphism.type R S

UMagmaMorphism (unitary magma morphisms):

monoid_morphism f <-> f of type U -> V is a multiplicative monoid morphism, i.e., f maps 1 and * in U to 1 and

in V, respectively. U and V must have

canonical baseUMagmaType instances. Algebra.UMagmaMorphism.type == the interface type for unitary magma morphisms; both U and V must have magmaType instances Notations are defined in scope group_scope (delimiter %g) This library also extends the conventional suffixes described in library ssrbool.v with the following: 1 -- unitary magma 1, as in mulg1 : x * 1 = x M -- magma multiplication, as in conjgM : x ^ (y * z) = (x ^ y) ^ z Mn -- ring by nat multiplication, as in expgMn : (x * y) ^+ n = x ^+ n * y ^+ n V -- group inverse, as in expVgn : (x^-1) ^+ n = x ^- n F -- group division, as in invgF : (x / y)^-1 = y / x X -- unitary magma exponentiation, as in conjXg : (x ^+ n) ^ y = (x ^ y) ^+ n J -- group conjugation, as in conjJg : (x ^ y) ^ z = (x ^ z) ^ y ^ z R -- group commutator, as in conjRg : [~ x, y] ^ z = [~ x ^ z, y ^ z] The operator suffixes D, B, M and X are also used for the corresponding operations on nat, as in expgnDr : x ^+ (m + n) = x ^+ m * x ^+ n. For the binary power operator, a trailing "n" suffix is used to indicate the operator suffix applies to the left-hand group argument, as in expg1n : 1 ^+ n = 1 vs. expg1 : x ^+ 1 = x.

Set Implicit Arguments.

Reserved Notation "*%g" (at level 0).
Reserved Notation "\1" (at level 0).
Reserved Notation "f \* g" (at level 40, left associativity).

Reserved Notation "'{' 'multiplicative' G '->' H '}'"
  (at level 0, G at level 98, H at level 99,
   format "{ 'multiplicative' G -> H }").

Declare Scope group_scope.
Delimit Scope group_scope with g.
Local Open Scope group_scope.

#[short (type ="magmaType")]
HB.structure Definition Magma := {G of hasMul G }.

Bind Scope group_scope with Magma.sort.

Bind Scope group_scope with ChoiceMagma.sort.

Local Notation "*%g" := (@mul _) : function_scope.
Local Notation "x * y" := (mul x y) : group_scope.

Section MagmaTheory.

Variable G : magmaType.
Implicit Types x y : G.

Definition commute x y := x × y = y × x.

Lemma commute_refl x : commute x x.

Lemma commute_sym x y : commute x y → commute y x.

Section ClosedPredicates.

Variable S : {pred G }.

Definition mulg_closed := {in S &, ∀ u v, u × v \in S }.

End ClosedPredicates.

End MagmaTheory.

#[short (type ="semigroupType")]
HB.structure Definition Semigroup := {G of Magma_isSemigroup G & ChoiceMagma G }.

Bind Scope group_scope with Semigroup.sort.

Section SemigroupTheory.
Variable G : semigroupType.
Implicit Types x y : G.

Lemma commuteM x y z : commute x y → commute x z → commute x (y × z).

End SemigroupTheory.

#[short (type ="baseUMagmaType")]
HB.structure Definition BaseUMagma := {G of hasOne G & Magma G }.

Bind Scope group_scope with BaseUMagma.sort.

Bind Scope group_scope with ChoiceBaseUMagma.sort.

Local Notation "1" := (@one _) : group_scope.
Local Notation "s `_ i" := (nth 1 s i) : group_scope.
Local Notation "\prod_ ( i <- r | P ) F" := (\big [*%g /1]_(i <- r | P) F).
Local Notation "\prod_ ( i | P ) F" := (\big [*%g /1]_(i | P) F).
Local Notation "\prod_ ( i 'in' A ) F" := (\big [*%g /1]_(i in A) F).
Local Notation "\prod_ ( m <= i < n ) F" := (\big [*%g /1%g]_(m ≤ i < n) F%g).

Definition natexp (G : baseUMagmaType) (x : G) n : G := iterop n *%g x 1.
Arguments natexp : simpl never.

Local Notation "x ^+ n" := (natexp x n) : group_scope.

Section baseUMagmaTheory.

Variable G : baseUMagmaType.
Implicit Types x : G.

Lemma expgnE x n : x ^+ n = iterop n mul x 1.
Lemma expg0 x : x ^+ 0 = 1.
Lemma expg1 x : x ^+ 1 = x.
Lemma expg2 x : x ^+ 2 = x × x.

Lemma expgSS x n : x ^+ n .+2 = x × x ^+ n .+1.

Lemma expgb x (b : bool) : x ^+ b = (if b then x else 1).

Section ClosedPredicates.

Variable S : {pred G }.

Definition umagma_closed := 1 \in S ∧ mulg_closed S.

End ClosedPredicates.

End baseUMagmaTheory.

#[warning ="-HB.no-new-instance"]
HB.instance Definition _ := BaseUMagma_isUMagma.Build G mul1g mulg1.

#[short (type ="umagmaType")]
HB.structure Definition UMagma := {G of Magma_isUMagma G & ChoiceMagma G }.

Bind Scope group_scope with UMagma.sort.

Section UMagmaTheory.

Variable G : umagmaType.
Implicit Types x y : G.

Lemma expgS x n : x ^+ n .+1 = x × x ^+ n.

Lemma expg1n n : 1 ^+ n = 1 :> G.

Lemma commute1 x : commute x 1.

End UMagmaTheory.

#[global] Hint Resolve commute1 : core.

#[short (type ="monoidType")]
HB.structure Definition Monoid := {G of Magma_isUMagma G & Semigroup G }.

#[export ]
HB.instance Definition _ (G : monoidType ) := Monoid.isLaw.Build G 1 *%g mulgA mul1g mulg1.

Bind Scope group_scope with Monoid.sort.

Section MonoidTheory.

Variable G : monoidType.
Implicit Types x y : G.

Lemma expgnDr x m n : x ^+ (m + n ) = x ^+ m × x ^+ n.

Lemma expgSr x n : x ^+ n .+1 = x ^+ n × x.

Lemma expgnA x m n : x ^+ (m × n ) = x ^+ m ^+ n.

Lemma expgnAC x m n : x ^+ m ^+ n = x ^+ n ^+ m.

Lemma iter_mulg n x y : iter n ( *%g x) y = x ^+ n × y.

Lemma iter_mulg_1 n x : iter n ( *%g x) 1 = x ^+ n.

Lemma prodg_const (I : finType) (A : pred I) x : \prod_(i in A ) x = x ^+ #|A |.

Lemma prodg_const_nat n m x : \prod_(n ≤ i < m ) x = x ^+ (m - n ).

Lemma prodgXr x I r P (F : I → nat) :
  \prod_(i <- r | P i ) x ^+ F i = x ^+ (\sum_(i <- r | P i ) F i ).

Lemma commute_prod (I : Type) (s : seq I) (P : pred I) (F : I → G) x :
  (∀ i, P i → commute x (F i)) → commute x (\prod_(i <- s | P i ) F i).

Lemma prodgM_commute {I : eqType} r (P : pred I) (F H : I → G) :
    (∀ i j, P i → P j → commute (F i) (H j)) →
  \prod_(i <- r | P i ) (F i × H i ) =
    \prod_(i <- r | P i ) F i × \prod_(i <- r | P i ) H i.

Lemma prodgMl_commute {I : finType} (A : pred I) (x : G) F :
    (∀ i, A i → commute x (F i)) →
  \prod_(i in A ) (x × F i ) = x ^+ #|A | × \prod_(i in A ) F i.

Lemma prodgMr_commute {I : finType} (A : pred I) (x : G) F :
    (∀ i, A i → commute x (F i)) →
  \prod_(i in A ) (F i × x ) = \prod_(i in A ) F i × x ^+ #|A |.

Lemma commuteX x y n : commute x y → commute x (y ^+ n).

Lemma commuteX2 x y m n : commute x y → commute (x ^+ m) (y ^+ n).

Lemma expgMn x y n : commute x y → (x × y ) ^+ n = x ^+ n × y ^+ n.

End MonoidTheory.

Notation monoid_closed := umagma_closed.

#[short (type ="baseGroupType")]
HB.structure Definition BaseGroup := {G of hasInv G & BaseUMagma G }.

Bind Scope group_scope with BaseGroup.sort.

Local Notation "x ^-1" := (inv x) : group_scope.
Local Notation "x / y" := (x × y^-1) : group_scope.
Local Notation "x ^- n" := ((x ^+ n)^-1) : group_scope.

Definition conjg (G : baseGroupType) (x y : G) := y ^-1 × (x × y ).
Local Notation "x ^ y" := (conjg x y) : group_scope.

Definition commg (G : baseGroupType) (x y : G) := x ^-1 × (conjg x y ).
Local Notation "[ ~ x1 , x2 , .. , xn ]" := (commg .. (commg x1 x2) .. xn)
  : group_scope.

#[short (type ="starMonoidType")]
HB.structure Definition StarMonoid :=
  { G of Monoid_isStarMonoid G & Monoid G & BaseGroup G }.

Bind Scope group_scope with StarMonoid.sort.

Lemma invg1 : inv one = one.

Lemma mulg1 : right_id one mul.

Section StarMonoidTheory.
Variable G : starMonoidType.
Implicit Types x y z : G.

Lemma invg_inj : injective (@inv G).

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

Lemma invgF x y : (x / y )^-1 = y / x.

Lemma prodgV I r (P : pred I) (E : I → G) :
  \prod_(i <- r | P i ) (E i )^-1 = (\prod_(i <- rev r | P i ) E i )^-1.

Lemma eqg_inv x y : (x ^-1 == y ^-1 ) = (x == y ).

Lemma eqg_invLR x y : (x ^-1 == y ) = (x == y ^-1 ).

Lemma invg_eq1 x : (x ^-1 == 1) = (x == 1).

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

Lemma conjgE x y : x ^ y = y ^-1 × (x × y ).

Lemma commgEl x y : [~ x , y ] = x ^-1 × x ^ y.

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

End StarMonoidTheory.

Arguments invg_inj {G} [x1 x2].

#[short (type ="groupType")]
HB.structure Definition Group :=
  {G of StarMonoid_isGroup G & BaseGroup G & StarMonoid G }.

Fact invgK : involutive (@inv G).

Fact mulKg : @left_loop G G inv *%g.

Fact invgM : {morph inv : x y / x × y >-> y × x : G }.

Bind Scope group_scope with Group.sort.

Section GroupTheory.
Variable G : groupType.
Implicit Types x y : G.

Lemma mulgV : right_inverse one inv (@mul G).
Definition divgg := mulgV.

Lemma mulKg : @left_loop G G (@inv G) *%g.

Lemma mulVKg : @rev_left_loop G G (@inv G) *%g.

Lemma mulgK : @right_loop G G (@inv G) *%g.

Lemma mulgVK : @rev_right_loop G G (@inv G) *%g.
Definition divgK := mulgVK.

Lemma mulgI : @right_injective G G G *%g.

Lemma mulIg : @left_injective G G G *%g.

Lemma divgI : @right_injective G G G (fun x y ⇒ x / y).

Lemma divIg : @left_injective G G G (fun x y ⇒ x / y).

Lemma divg1 x : x / 1 = x.

Lemma div1g x : 1 / x = x ^-1.

Lemma divKg x y : commute x y → x / (x / y ) = y.

TOTHINK : This does not have the same form as addrKA in ssralg.v

Lemma mulgKA z x y : (x × z ) / (y × z ) = x / y.

Lemma divgKA z x y : (x / z ) × (z × y ) = x × y.

Lemma mulg1_eq x y : x × y = 1 → x ^-1 = y.

Lemma divg1_eq x y : x / y = 1 → x = y.

Lemma divg_eq x y z : (x / z == y ) = (x == y × z ).

Lemma divg_eq1 x y : (x / y == 1) = (x == y ).

Lemma mulg_eq1 x y : (x × y == 1) = (x == y ^-1 ).

Lemma commuteV x y : commute x y → commute x y ^-1.

Lemma expgnFr x m n : n ≤ m → x ^+ (m - n ) = x ^+ m / x ^+ n.

Lemma expgnFl x y n : commute x y → (x / y ) ^+ n = x ^+ n / y ^+ n.

Lemma conjgC x y : x × y = y × x ^ y.

Lemma conjgCV x y : x × y = y ^ x ^-1 × x.

Lemma conjg1 x : x ^ 1 = x.

Lemma conj1g x : 1 ^ x = 1.

Lemma conjMg x y z : (x × y ) ^ z = x ^ z × y ^ z.

Lemma conjgM x y z : x ^ (y × z ) = (x ^ y ) ^ z.

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

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

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

Lemma conjgK : @right_loop G G (@inv G) (@conjg G).

Lemma conjgKV : @rev_right_loop G G (@inv G) (@conjg G).

Lemma conjg_inj : @left_injective G G G (@conjg G).

Lemma conjg_eq1 x y : (x ^ y == 1) = (x == 1).

Lemma conjg_prod I r (P : pred I) (F : I → G) z :
(\prod_(i <- r | P i ) F i ) ^ z = \prod_(i <- r | P i ) (F i ^ z ).

Lemma commgC x y : x × y = y × x × [~ x , y ].

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

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

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

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

Lemma conjg_fix x y : x ^ y == x = ([~ x , y ] == 1).

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

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

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

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

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

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

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

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

Section ClosedPredicates.

Variable S : {pred G }.

Definition invg_closed := {in S , ∀ u, u ^-1 \in S }.
Definition divg_closed := {in S &, ∀ u v, u / v \in S }.
Definition group_closed := 1 \in S ∧ divg_closed.

Lemma group_closedV : group_closed → invg_closed.

Lemma group_closedM : group_closed → mulg_closed S.

End ClosedPredicates.

End GroupTheory.

#[global] Hint Rewrite @mulg1 @mul1g invg1 @mulVg mulgV (@invgK) mulgK mulgVK
@invgM @mulgA : gsimpl.

Ltac gsimpl := autorewrite with gsimpl; try done.

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

Arguments mulgI [G].
Arguments mulIg [G].
Arguments conjg_inj {G} x [x1 x2].
Arguments commgP {G x y}.
Arguments conjg_fixP {G x y}.

Morphism hierarchy.

TODO: define pointedTypes and generalize this to pointedTypes.

Definition monoid_morphism (G H : baseUMagmaType) (f : G → H) : Prop :=
(f 1 = 1) × {morph f : x y / x × y }.

Local Lemma gmulf1 : apply 1 = 1.

Local Lemma gmulfM : {morph apply : x y / x × y }.

Module MultiplicativeExports.
Notation "{ 'multiplicative' U -> V }" :=
(Multiplicative.type U%type V%type) : type_scope.
End MultiplicativeExports.

FIXME: The instance below makes sure that the join instance between Multiplicative.type and UMagmaMorphism.type is declared in both directions. HB should do this automatically.

#[non_forgetful_inheritance ]
HB.instance Definition _ G H (f : UMagmaMorphism.type G H ) :=
  UMagmaMorphism.on (Multiplicative.sort f ).

Section LiftedMagma.
Variables (T : Type) (G : magmaType).
Definition mul_fun (f g : T → G) x := f x × g x.

End LiftedMagma.
Section LiftedBaseUMagma.
Variables (T : Type) (G : baseUMagmaType).
Definition one_fun : T → G := fun ⇒ 1.

End LiftedBaseUMagma.

Local Notation "\1" := (one_fun _) : function_scope.
Local Notation "f \* g" := (mul_fun f g) : function_scope.
Arguments one_fun {_} G _ /.
Arguments mul_fun {_ _} f g _ /.

Section MorphismTheory.

Section Magma.
Variables (G H : magmaType) (f : {multiplicative G → H }).

Lemma can2_gmulfM f' : cancel f f' → cancel f' f → {morph f' : x y / x × y }.

Lemma gmulf_commute x y : commute x y → commute (f x) (f y).

End Magma.

Section UMagma.
Variables (G H : umagmaType) (f : UMagmaMorphism.type G H).

Lemma gmulf_eq1 x : injective f → (f x == 1) = (x == 1).

Lemma can2_gmulf1 f' : cancel f f' → cancel f' f → f' 1 = 1.

Lemma gmulfXn n : {morph f : x / x ^+ n }.

Lemma gmulf_prod I r (P : pred I) E :
  f (\prod_(i <- r | P i ) E i) = \prod_(i <- r | P i ) f (E i).

End UMagma.

Section Group.
Variables (G H : groupType) (f : UMagmaMorphism.type G H).

Lemma gmulfV : {morph f : x / x ^-1 }.

Lemma gmulfF : {morph f : x y / x / y }.

Lemma gmulf_inj : (∀ x, f x = 1 → x = 1) → injective f.

Lemma gmulfXVn n : {morph f : x / x ^- n }.

Lemma gmulfJ : {morph f : x y / x ^ y }.

Lemma gmulfR : {morph f : x y / [~ x , y ]}.
End Group.

Section MulFun.
Variables (G H K : magmaType).
Variables (f g : {multiplicative H → K }) (h : {multiplicative G → H }).

Fact idfun_gmulfM : {morph @idfun G : x y / x × y }.

Fact comp_gmulfM : {morph f \o h : x y / x × y }.
End MulFun.

Section Mul1Fun.
Variables (G : magmaType) (H : umagmaType).

Fact idfun_gmulf1 : idfun 1 = 1 :> H.

Fact one_fun_gmulfM : {morph @one_fun G H : x y / x × y }.
End Mul1Fun.

Section Mul11Fun.
Variables (G H K : umagmaType).
Variables (f g : UMagmaMorphism.type H K) (h : UMagmaMorphism.type G H).

Fact comp_gmulf1 : (f \o h ) 1 = 1.
#[warning ="-HB.no-new-instance"]
HB.instance Definition _ :=
  Multiplicative_isUMagmaMorphism.Build G K (f \o h ) comp_gmulf1.

Fact one_fun_gmulf1 : @one_fun G H 1 = 1.

Fact mul_fun_gmulf1 : (f \* g ) 1 = 1.

End Mul11Fun.
End MorphismTheory.

Mixins for stability properties

Structures for stability properties

#[short (type ="mulgClosed")]
HB.structure Definition MulClosed G := {S of isMulClosed G S }.

#[short (type ="umagmaClosed")]
HB.structure Definition UMagmaClosed G :=
  {S of isMul1Closed G S & isMulClosed G S }.

#[short (type ="invgClosed")]
HB.structure Definition InvClosed G := {S of isInvClosed G S }.

#[short (type ="groupClosed")]
HB.structure Definition GroupClosed G :=
  {S of isInvClosed G S & isMul1Closed G S & isMulClosed G S }.

Section UMagmaPred.
Variables (G : baseUMagmaType).

Section UMagma.
Variables S : umagmaClosed G.

Lemma gpred_prod I r (P : pred I) F :
  (∀ i, P i → F i \in S ) → \prod_(i <- r | P i ) F i \in S.

Lemma gpredXn n : {in S , ∀ u, u ^+ n \in S }.

End UMagma.
End UMagmaPred.

Section GroupPred.
Variables (G : groupType).

Lemma gpredV (S : invgClosed G) : {mono (@inv G ): u / u \in S }.

Section Group.
Variables S : groupClosed G.

Lemma gpredF : {in S &, ∀ u v, u / v \in S }.

Lemma gpredFC u v : u / v \in S = (v / u \in S ).

Lemma gpredXNn n: {in S , ∀ u, u ^- n \in S }.

Lemma gpredMr x y : x \in S → (y × x \in S ) = (y \in S ).

Lemma gpredMl x y : x \in S → (x × y \in S ) = (y \in S ).

Lemma gpredFr x y : x \in S → (y / x \in S ) = (y \in S ).

Lemma gpredFl x y : x \in S → (x / y \in S ) = (y \in S ).

Lemma gpredJ x y : x \in S → y \in S → x ^ y \in S.

Lemma gpredR x y : x \in S → y \in S → [~ x , y ] \in S.

End Group.
End GroupPred.

#[short (type ="subMagmaType")]
HB.structure Definition SubMagma (G : magmaType ) S :=
  { H of SubChoice G S H & Magma H & isSubMagma G S H }.

Section subMagma.
Context (G : magmaType) (S : pred G) (H : subMagmaType S).
Notation val := (val : H → G).
Lemma valM : {morph val : x y / x × y }.
End subMagma.

Let inH v Sv : H := Sub v Sv.
Let mulH (u1 u2 : H) := inH (gpredM _ _ (valP u1) (valP u2)).

Lemma valM : {morph (val : H → G ) : x y / x × y }.

#[short (type ="subSemigroupType")]
HB.structure Definition SubSemigroup (G : semigroupType ) S :=
  { H of SubMagma G S H & Semigroup H }.

Lemma mulgA : associative (@mul H).

#[short (type ="subBaseUMagmaType")]
HB.structure Definition SubBaseUMagma (G : umagmaType ) S :=
  { H of SubMagma G S H & BaseUMagma H & isSubBaseUMagma G S H }.

#[short (type ="subUMagmaType")]
HB.structure Definition SubUMagma (G : umagmaType ) S :=
  { H of SubMagma G S H & UMagma H & isSubBaseUMagma G S H }.

Section subUMagma.
Context (G : umagmaType) (S : pred G) (H : subUMagmaType S).
Notation val := (val : H → G).
Lemma val1 : val 1 = 1.
End subUMagma.

Let inH v Sv : H := Sub v Sv.
Let oneH := inH (fst umagma_closed_subproof).

Lemma val1 : (val : H → G) 1 = 1.

Lemma mul1g : left_id 1 (@mul H).
Lemma mulg1 : right_id 1 (@mul H).

#[short (type ="subMonoidType")]
HB.structure Definition SubMonoid (G : monoidType ) S :=
  { H of SubUMagma G S H & Monoid H }.

#[short (type ="subGroupType")]
HB.structure Definition SubGroup (G : groupType ) S :=
  { H of SubUMagma G S H & Group H }.

Lemma umagma_closed : umagma_closed S.

Let inH v Sv : H := Sub v Sv.
Let invH (u : H) := inH (gpredVr _ (valP u)).

Lemma mulVg : left_inverse 1%g invH *%g.
Lemma mulgV : right_inverse 1%g invH *%g.

Notation "*%g" := (@mul _) : function_scope.
Notation "x * y" := (mul x y) : group_scope.
Notation "1" := (@one _) : group_scope.
Notation "s `_ i" := (nth 1 s i) : group_scope.
Notation "\prod_ ( i <- r | P ) F" :=
  (\big [*%g /1]_(i <- r | P%B) F%g) : group_scope.
Notation "\prod_ ( i <- r ) F" :=
  (\big [*%g /1]_(i <- r) F%g) : group_scope.
Notation "\prod_ ( m <= i < n | P ) F" :=
  (\big [*%g /1]_(m ≤ i < n | P%B) F%g) : group_scope.
Notation "\prod_ ( m <= i < n ) F" :=
  (\big [*%g /1]_(m ≤ i < n) F%g) : group_scope.
Notation "\prod_ ( i | P ) F" :=
  (\big [*%g /1]_(i | P%B) F%g) : group_scope.
Notation "\prod_ i F" :=
  (\big [*%g /1]_i F%g) : group_scope.
Notation "\prod_ ( i : t | P ) F" :=
  (\big [*%g /1]_(i : t | P%B) F%g) (only parsing) : group_scope.
Notation "\prod_ ( i : t ) F" :=
  (\big [*%g /1]_(i : t) F%g) (only parsing) : group_scope.
Notation "\prod_ ( i < n | P ) F" :=
  (\big [*%g /1]_(i < n | P%B) F%g) : group_scope.
Notation "\prod_ ( i < n ) F" :=
  (\big [*%g /1]_(i < n) F%g) : group_scope.
Notation "\prod_ ( i 'in' A | P ) F" :=
  (\big [*%g /1]_(i in A | P%B) F%g) : group_scope.
Notation "\prod_ ( i 'in' A ) F" :=
  (\big [*%g /1]_(i in A) F%g) : group_scope.
Notation "x ^+ n" := (natexp x n) : group_scope.
Notation "x ^-1" := (inv x) : group_scope.
Notation "x / y" := (x × y^-1) : group_scope.
Notation "x ^- n" := ((x ^+ n)^-1) : group_scope.
Notation "x ^ y" := (conjg x y) : group_scope.
Notation "[ ~ x1 , x2 , .. , xn ]" := (commg .. (commg x1 x2) .. xn)
  : group_scope.

Lifting Structure from the codomain of finfuns.

Section FinFunMagma.
Variable (aT : finType) (rT : magmaType).
Implicit Types f g : {ffun aT → rT }.

Definition ffun_mul f g := [ffun a ⇒ f a × g a ].

End FinFunMagma.

FIXME: HB.saturate

Section FinFunSemigroup.
Variable (aT : finType) (rT : semigroupType).
Implicit Types f g : {ffun aT → rT }.

Fact ffun_mulgA : associative (@ffun_mul aT rT).

End FinFunSemigroup.

Section FinFunBaseUMagma.
Variable (aT : finType) (rT : baseUMagmaType).
Implicit Types f g : {ffun aT → rT }.

Definition ffun_one := [ffun a : aT ⇒ (1 : rT )].

End FinFunBaseUMagma.

FIXME: HB.saturate

Section FinFunUMagma.
Variable (aT : finType) (rT : umagmaType).
Implicit Types f g : {ffun aT → rT }.

Fact ffun_mul1g : left_id (@ffun_one aT rT) *%g.
Fact ffun_mulg1 : right_id (@ffun_one aT rT) *%g.

End FinFunUMagma.

FIXME: HB.saturate

Section FinFunBaseGroup.

Variable (aT : finType) (rT : baseGroupType).
Implicit Types f g : {ffun aT → rT }.

Definition ffun_inv f := [ffun a ⇒ (f a )^-1 ].

End FinFunBaseGroup.

Section FinFunGroup.

Variable (aT : finType) (rT : groupType).
Implicit Types f g : {ffun aT → rT }.

Fact ffun_mulVg :
left_inverse (@ffun_one aT rT) (@ffun_inv _ _) (@ffun_mul _ _).
Fact ffun_mulgV :
right_inverse (@ffun_one aT rT) (@ffun_inv _ _) (@ffun_mul _ _).

End FinFunGroup.

External direct product

Section PairMagma.
Variables G H : magmaType.

Definition mul_pair (x y : G × H) := (x .1 × y .1 , x .2 × y .2 ).

Fact fst_is_multiplicative : {morph fst : x y / x × y }.

Fact snd_is_multiplicative : {morph snd : x y / x × y }.

End PairMagma.

Section PairSemigroup.
Variables G H : semigroupType.

Lemma pair_mulgA : associative (@mul (G × H)%type).

End PairSemigroup.

Section PairBaseUMagma.
Variables G H : baseUMagmaType.

Definition one_pair : G × H := (1, 1).

Fact fst_is_umagma_morphism : fst (1 : G × H) = 1.

Fact snd_is_umagma_morphism : snd (1 : G × H) = 1.

End PairBaseUMagma.

Section PairUMagma.
Variables G H : umagmaType.

Lemma pair_mul1g : left_id (@one_pair G H) *%g.
Lemma pair_mulg1 : right_id (@one_pair G H) *%g.

End PairUMagma.

FIXME: HB.saturate

/FIXME

Section PairBaseGroup.
Variables G H : baseGroupType.

Definition inv_pair (u : G × H) := (u .1 ^-1 , u .2 ^-1 ).

End PairBaseGroup.

Section PairGroup.
Variables G H : groupType.

Lemma pair_mulVg : left_inverse one (@inv_pair G H) mul.
Lemma pair_mulgV : right_inverse one (@inv_pair G H) mul.

End PairGroup.