1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/algebra/monoids/".
17 include "algebra/semigroups.ma".
19 record isMonoid (SS:SemiGroup) (e:SS) : Prop ≝
20 { e_is_left_unit: is_left_unit SS e;
21 e_is_right_unit: is_right_unit SS e
24 record Monoid : Type ≝
25 { semigroup: SemiGroup;
27 monoid_properties: isMonoid ? e
30 coercion cic:/matita/algebra/monoids/semigroup.con.
33 notation "hvbox(1 \sub S)" with precedence 89
36 interpretation "Monoid unit" 'munit S =
37 (cic:/matita/algebra/monoids/e.con S). *)
39 notation "1" with precedence 89
42 interpretation "Monoid unit" 'munit =
43 (cic:/matita/algebra/monoids/e.con _).
46 for @{ 'semigroup $M }.
48 interpretation "Semigroup coercion" 'semigroup M =
49 (cic:/matita/algebra/monoids/semigroup.con M).
51 definition is_left_inverse ≝
56 definition is_right_inverse ≝
61 theorem is_left_inverse_to_is_right_inverse_to_eq:
63 is_left_inverse M l → is_right_inverse M r →
66 generalize in match (H x); intro;
67 generalize in match (eq_f ? ? (λy.y·(r x)) ? ? H2);
68 simplify; fold simplify (op M);
70 generalize in match (semigroup_properties M);
71 fold simplify (Type_of_Monoid M);
73 unfold isSemiGroup in H2; unfold associative in H2;
74 rewrite > H2 in H3; clear H2;
76 rewrite > (e_is_left_unit ? ? (monoid_properties M)) in H3;
77 rewrite > (e_is_right_unit ? ? (monoid_properties M)) in H3;