CoRN.algebra.CAbMonoids

Require Export CMonoids.

Require Import SetoidPermutation Setoid Morphisms.

Section Abelian_Monoids.

Abelian Monoids

Now we introduce commutativity and add some results.

Definition is_CAbMonoid (G : CMonoid) := commutes (csg_op (c:=G)).

Record CAbMonoid : Type :=
 {cam_crr :> CMonoid;
  cam_proof : is_CAbMonoid cam_crr}.

Section AbMonoid_Axioms.

Variable M : CAbMonoid.
Let M be an abelian monoid.

Lemma CAbMonoid_is_CAbMonoid : is_CAbMonoid M.
Proof.
 elim M; auto.
Qed.

Lemma cam_commutes : commutes (csg_op (c:=M)).
Proof.
 exact CAbMonoid_is_CAbMonoid.
Qed.

Lemma cam_commutes_unfolded : ∀ x y : M, x[+]y [=] y[+]x.
Proof cam_commutes.

End AbMonoid_Axioms.

Global Instance cm_Sum_AbMonoid_Proper: ∀ {M: CAbMonoid},
 Proper (SetoidPermutation (@st_eq M) ==> @st_eq M) cm_Sum.
Proof.
 repeat intro.
 apply cm_Sum_Proper.
  apply cam_proof.
 assumption.
Qed.

Section SubCAbMonoids.

Subgroups of an Abelian Monoid

Variable M : CAbMonoid.
Variable P : M → CProp.
Variable Punit : P [0].
Variable op_pres_P : bin_op_pres_pred _ P csg_op.

Let M be an Abelian Monoid and P be a (CProp-valued) predicate on M that contains Zero and is closed under [+] and [--].

Let subcrr : CMonoid := Build_SubCMonoid _ _ Punit op_pres_P.

Lemma isabgrp_scrr : is_CAbMonoid subcrr.
Proof.
 red in |- ×. intros x y. case x. case y. intros.
 simpl in |- ×. apply cam_commutes_unfolded.
Qed.

Definition Build_SubCAbMonoid : CAbMonoid := Build_CAbMonoid _ isabgrp_scrr.

End SubCAbMonoids.

End Abelian_Monoids.

Hint Resolve cam_commutes_unfolded: algebra.