Definition is_CSemiGroup A (op : CSetoid_bin_op A) := associative op.
Record CSemiGroup : Type :=
{csg_crr :> CSetoid;
csg_op : CSetoid_bin_op csg_crr;
csg_proof : is_CSemiGroup csg_crr csg_op}.
In the names of lemmas, we will denote + with plus.
Section CSemiGroup_axioms.
Variable G : CSemiGroup.
Lemma CSemiGroup_is_CSemiGroup : is_CSemiGroup G csg_op.
Lemma plus_assoc : associative (csg_op (c:=G)).
End CSemiGroup_axioms.
Variable G : CSemiGroup.
Lemma CSemiGroup_is_CSemiGroup : is_CSemiGroup G csg_op.
Lemma plus_assoc : associative (csg_op (c:=G)).
End CSemiGroup_axioms.
Section CSemiGroup_basics.
Variable G : CSemiGroup.
Lemma plus_assoc_unfolded : forall (G : CSemiGroup) (x y z : G), x[+] (y[+]z) [=] x[+]y[+]z.
End CSemiGroup_basics.
Section p71R1.
Variable G : CSemiGroup.
Lemma plus_assoc_unfolded : forall (G : CSemiGroup) (x y z : G), x[+] (y[+]z) [=] x[+]y[+]z.
End CSemiGroup_basics.
Section p71R1.
Variable S1:CSemiGroup.
Variable S2:CSemiGroup.
Definition morphism_of_CSemiGroups (f:(CSetoid_fun S1 S2)):CProp:=
forall (a b:S1), (f (a[+]b))[=] (f a)[+](f b).
End p71R1.
Definition is_rht_unit S (op : CSetoid_bin_op S) Zero : Prop := forall x, op x Zero [=] x.
Definition is_lft_unit S (op : CSetoid_bin_op S) Zero : Prop := forall x, op Zero x [=] x.
An alternative definition:
Definition is_unit (S:CSemiGroup): S -> Prop :=
fun e => forall (a:S), e[+]a [=] a /\ a[+]e [=]a.
Lemma cs_unique_unit : forall (S:CSemiGroup) (e f:S),
(is_unit S e) /\ (is_unit S f) -> e[=]f.
Functional operations
We can also define a similar addition operator, which will be denoted by {+}, on partial functions.Whenever possible, we will denote the functional construction corresponding to an algebraic operation by the same symbol enclosed in curly braces.
At this stage, we will always consider automorphisms; we could treat this in a more general setting, but we feel that it wouldn't really be a useful effort.
Let G:CSemiGroup and F,F':(PartFunct G) and denote by P and Q, respectively, the predicates characterizing their domains.
Section Part_Function_Plus.
Variable G : CSemiGroup.
Variables F F' : PartFunct G.
Lemma part_function_plus_strext : forall x y (Hx : Conj P Q x) (Hy : Conj P Q y),
F x (Prj1 Hx) [+]F' x (Prj2 Hx) [#] F y (Prj1 Hy) [+]F' y (Prj2 Hy) -> x [#] y.
Definition Fplus := Build_PartFunct G _ (conj_wd (dom_wd _ F) (dom_wd _ F'))
(fun x Hx => F x (Prj1 Hx) [+]F' x (Prj2 Hx)) part_function_plus_strext.
Let R:G->CProp.
Variable R : G -> CProp.
Lemma included_FPlus : ⊆ R P -> ⊆ R Q -> ⊆ R (Dom Fplus).
Lemma included_FPlus' : ⊆ R (Dom Fplus) -> ⊆ R P.
Lemma included_FPlus'' : ⊆ R (Dom Fplus) -> ⊆ R Q.
End Part_Function_Plus.
Infix "{+}" := Fplus (at level 50, left associativity).
Subsemigroups
Let csg a semi-group and P a non-empty predicate on the semi-group which is preserved by +.
Section SubCSemiGroups.
Variable csg : CSemiGroup.
Variable P : csg -> CProp.
Variable op_pres_P : bin_op_pres_pred _ P csg_op.
Let subcrr : CSetoid := Build_SubCSetoid _ P.
Definition Build_SubCSemiGroup : CSemiGroup := Build_CSemiGroup
subcrr (Build_SubCSetoid_bin_op _ _ _ op_pres_P)
(restr_f_assoc _ _ _ op_pres_P (plus_assoc csg)).
End SubCSemiGroups.
Section D9S.
Variable csg : CSemiGroup.
Variable P : csg -> CProp.
Variable op_pres_P : bin_op_pres_pred _ P csg_op.
Let subcrr : CSetoid := Build_SubCSetoid _ P.
Definition Build_SubCSemiGroup : CSemiGroup := Build_CSemiGroup
subcrr (Build_SubCSetoid_bin_op _ _ _ op_pres_P)
(restr_f_assoc _ _ _ op_pres_P (plus_assoc csg)).
End SubCSemiGroups.
Section D9S.
Variable M1 M2: CSemiGroup.
Definition dprod (x:ProdCSetoid M1 M2)(y:ProdCSetoid M1 M2):
(ProdCSetoid M1 M2):=
let (x1, x2):= x in
let (y1, y2):= y in
(pairT (x1[+]y1) (x2 [+] y2)).
Lemma dprod_strext:(bin_fun_strext (ProdCSetoid M1 M2)(ProdCSetoid M1 M2)
(ProdCSetoid M1 M2)dprod).
Definition dprod_as_csb_fun:
CSetoid_bin_fun (ProdCSetoid M1 M2) (ProdCSetoid M1 M2)(ProdCSetoid M1 M2):=
(Build_CSetoid_bin_fun (ProdCSetoid M1 M2)(ProdCSetoid M1 M2)
(ProdCSetoid M1 M2) dprod dprod_strext).
Lemma direct_product_is_CSemiGroup:
(is_CSemiGroup (ProdCSetoid M1 M2) dprod_as_csb_fun).
Definition direct_product_as_CSemiGroup:=
(Build_CSemiGroup (ProdCSetoid M1 M2) dprod_as_csb_fun
direct_product_is_CSemiGroup).
End D9S.
Lemma FS_is_CSemiGroup:
forall (X:CSetoid),(is_CSemiGroup (FS_as_CSetoid X X) (comp_as_bin_op X )).
Definition FS_as_CSemiGroup (A : CSetoid) :=
Build_CSemiGroup (FS_as_CSetoid A A) (comp_as_bin_op A) (assoc_comp A).
Section p66E2b4.
Variable A:CSetoid.
Lemma Astar_is_CSemiGroup:
(is_CSemiGroup (free_csetoid_as_csetoid A) (app_as_csb_fun A)).
Definition Astar_as_CSemiGroup:=
(Build_CSemiGroup (free_csetoid_as_csetoid A) (app_as_csb_fun A)
Astar_is_CSemiGroup).
End p66E2b4.