CoRN.model.monoids.Nmonoid

Require Export Nsemigroup.
Require Import CMonoids.

Example of a monoid: ⟨nat,[+]⟩

Zero is an unit for the addition.

Lemma O_as_rht_unit : is_rht_unit (S:=nat_as_CSetoid) plus_is_bin_fun 0.
Proof.
red in |- ×.
simpl in |- ×.
intro x.
symmetry in |- ×.
apply plus_n_O.
Qed.

Lemma O_as_lft_unit : is_lft_unit (S:=nat_as_CSetoid) plus_is_bin_fun 0.
Proof.
red in |- ×.
simpl in |- ×.
intro x.
reflexivity.
Qed.

Definition nat_is_CMonoid := Build_is_CMonoid
nat_as_CSemiGroup _ O_as_rht_unit O_as_lft_unit.

Whence we can define the monoid of natural numbers:

Definition nat_as_CMonoid := Build_CMonoid nat_as_CSemiGroup _ nat_is_CMonoid.

Canonical Structure nat_as_CMonoid.

Lemma SO_as_rht_unit : is_rht_unit (S:=nat_as_CSetoid) mult_as_bin_fun 1.
Proof.
red in |- ×.
simpl.
auto with arith.
Qed.

Lemma SO_as_lft_unit : is_lft_unit (S:=nat_as_CSetoid) mult_as_bin_fun 1.
Proof.
red in |- ×.
simpl.
auto with arith.
Qed.

Definition Nmult_is_CMonoid := Build_is_CMonoid
Nmult_as_CSemiGroup _ SO_as_rht_unit SO_as_lft_unit.

Definition Nmult_as_CMonoid := Build_CMonoid Nmult_as_CSemiGroup _ Nmult_is_CMonoid.