include "algebra/semigroups.ma".
record PreMonoid : Type ≝
- { magma:> Magma;
- e: magma
- }.
+{ pre_semi_group :> PreSemiGroup;
+ e : pre_semi_group
+}.
-(* FG: the interpretation goes just after its definition *)
interpretation "Monoid unit" 'neutral = (e ?).
-record isMonoid (M:PreMonoid) : Prop ≝
- { is_semi_group:> isSemiGroup M;
- e_is_left_unit:
- is_left_unit (mk_SemiGroup ? is_semi_group) (e M);
- e_is_right_unit:
- is_right_unit (mk_SemiGroup ? is_semi_group) (e M)
+record IsMonoid (M:PreMonoid): Prop ≝
+ { is_pre_semi_group :> IsSemiGroup M;
+ e_is_left_unit : is_left_unit M ⅇ;
+ e_is_right_unit : is_right_unit M ⅇ
}.
-
+
record Monoid : Type ≝
- { premonoid:> PreMonoid;
- monoid_properties:> isMonoid premonoid
+ { pre_monoid :> PreMonoid;
+ is_monoid :> IsMonoid pre_monoid
}.
-
+
+definition SemiGroup_of_Monoid: Monoid → SemiGroup ≝
+ λM. mk_SemiGroup ? (is_monoid M).
+
+coercion SemiGroup_of_Monoid nocomposites.
+
definition is_left_inverse ≝
- λM:Monoid.
+ λM:PreMonoid.
λopp: M → M.
∀x:M. (opp x)·x = ⅇ.
-
+
definition is_right_inverse ≝
- λM:Monoid.
+ λM:PreMonoid.
λopp: M → M.
∀x:M. x·(opp x) = ⅇ.
is_left_inverse M l → is_right_inverse M r →
∀x:M. l x = r x.
intros;
- generalize in match (H x); intro;
- generalize in match (eq_f ? ? (λy.y·(r x)) ? ? H2);
- simplify; fold simplify (op M);
- intro; clear H2;
- generalize in match (op_associative ? (is_semi_group ? (monoid_properties M)));
- intro;
- rewrite > H2 in H3; clear H2;
+ lapply (H x) as H2;
+ lapply (eq_f ? ? (λy.y·(r x)) ? ? H2) as H3; clear H2;
+ rewrite > (op_is_associative ? M) in H3.
rewrite > H1 in H3;
- rewrite > (e_is_left_unit ? (monoid_properties M)) in H3;
- rewrite > (e_is_right_unit ? (monoid_properties M)) in H3;
+ rewrite > (e_is_left_unit ? M) in H3;
+ rewrite > (e_is_right_unit ? M) in H3;
assumption.
qed.