CoRN.model.semigroups.CRsemigroup

Require Export CRGroupOps.
Require Export CRsetoid.
Require Export CGroups.
Require Import CRcorrect.
Require Import CornTac.

Open Local Scope uc_scope.

Lemma CRplus_strext : bin_op_strext CRasCSetoid (ucFun2 CRplus_uc).
Proof.
 intros x1 x2 y1 y2 H.
 simpl in ×.
 assert (X:(CRasCauchy_IR x1[+]CRasCauchy_IR y1)[#](CRasCauchy_IR x2[+]CRasCauchy_IR y2)).
  stepl (CRasCauchy_IR (x1+y1)%CR); [| apply eq_symmetric; apply CR_plus_as_Cauchy_IR_plus].
  stepr (CRasCauchy_IR (x2+y2)%CR); [| now apply eq_symmetric; apply CR_plus_as_Cauchy_IR_plus].
  apply CR_ap_as_Cauchy_IR_ap_1.
  assumption.
 destruct (bin_op_strext_unfolded _ _ _ _ _ _ X);[left|right];
   apply CR_ap_as_Cauchy_IR_ap_2; assumption.
Qed.

Definition CRplusasBinOp : CSetoid_bin_op CRasCSetoid :=
Build_CSetoid_bin_fun _ _ _ _ CRplus_strext.

Lemma CRisCSemiGroup : is_CSemiGroup _ CRplusasBinOp.
Proof.
 intros x y z.
 change (x + (y+z)==(x+y)+z)%CR.
 rewrite <- CR_eq_as_Cauchy_IR_eq.
 stepl ((CRasCauchy_IR x)[+](CRasCauchy_IR (y+z)%CR)); [| now apply CR_plus_as_Cauchy_IR_plus].
 stepl ((CRasCauchy_IR x)[+]((CRasCauchy_IR y)[+](CRasCauchy_IR z))); [| now
   apply plus_resp_eq; apply CR_plus_as_Cauchy_IR_plus].
 stepr ((CRasCauchy_IR (x+y)%CR)[+](CRasCauchy_IR z)); [| now apply CR_plus_as_Cauchy_IR_plus].
 stepr (((CRasCauchy_IR x)[+](CRasCauchy_IR y))[+](CRasCauchy_IR z)); [| now
   apply bin_op_is_wd_un_op_lft; apply CR_plus_as_Cauchy_IR_plus].
 apply plus_assoc_unfolded.
Qed.

Definition CRasCSemiGroup : CSemiGroup :=
Build_CSemiGroup _ _ CRisCSemiGroup.

Canonical Structure CRasCSemiGroup.