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 PreMonoid : Type ≝
24 notation < "M" for @{ 'pmmagma $M }.
25 interpretation "premonoid magma coercion" 'pmmagma M =
26 (cic:/matita/algebra/monoids/magma.con M).
28 record isMonoid (M:PreMonoid) : Prop ≝
29 { is_semi_group: isSemiGroup M;
31 is_left_unit (mk_SemiGroup ? is_semi_group) (e M);
33 is_right_unit (mk_SemiGroup ? is_semi_group) (e M)
36 record Monoid : Type ≝
37 { premonoid:> PreMonoid;
38 monoid_properties:> isMonoid premonoid
41 notation < "M" for @{ 'semigroup $M }.
42 interpretation "premonoid coercion" 'premonoid M =
43 (cic:/matita/algebra/monoids/premonoid.con M).
45 notation < "M" for @{ 'typeofmonoid $M }.
46 interpretation "premonoid coercion" 'typeofmonoid M =
47 (cic:/matita/algebra/monoids/Type_of_Monoid.con M).
49 notation < "M" for @{ 'magmaofmonoid $M }.
50 interpretation "premonoid coercion" 'magmaofmonoid M =
51 (cic:/matita/algebra/monoids/Magma_of_Monoid.con M).
53 notation "1" with precedence 89
56 interpretation "Monoid unit" 'munit =
57 (cic:/matita/algebra/monoids/e.con _).
59 definition is_left_inverse ≝
64 definition is_right_inverse ≝
69 theorem is_left_inverse_to_is_right_inverse_to_eq:
71 is_left_inverse M l → is_right_inverse M r →
74 generalize in match (H x); intro;
75 generalize in match (eq_f ? ? (λy.y·(r x)) ? ? H2);
76 simplify; fold simplify (op M);
78 generalize in match (associative ? (is_semi_group ? (monoid_properties M)));
80 rewrite > H2 in H3; clear H2;
82 rewrite > (e_is_left_unit ? (monoid_properties M)) in H3;
83 rewrite > (e_is_right_unit ? (monoid_properties M)) in H3;