helm/software/matita/library/algebra/monoids.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "algebra/semigroups.ma".
  16
  17 record PreMonoid : Type ≝
  18 { pre_semi_group :> PreSemiGroup;
  19   e              :  pre_semi_group
  20 }.
  21
  22 interpretation "Monoid unit" 'neutral = (e ?).
  23
  24 record IsMonoid (M:PreMonoid): Prop ≝
  25  { is_pre_semi_group :> IsSemiGroup M;
  26    e_is_left_unit    :  is_left_unit M ⅇ;
  27    e_is_right_unit   :  is_right_unit M ⅇ
  28  }.
  29
  30 record Monoid : Type ≝
  31  { pre_monoid :> PreMonoid;
  32    is_monoid  :> IsMonoid pre_monoid
  33  }.
  34
  35 definition SemiGroup_of_Monoid: Monoid → SemiGroup ≝
  36  λM. mk_SemiGroup ? (is_monoid M).
  37
  38 coercion SemiGroup_of_Monoid nocomposites.
  39
  40 definition is_left_inverse ≝
  41  λM:PreMonoid.
  42   λopp: M → M.
  43    ∀x:M. (opp x)·x = ⅇ.
  44
  45 definition is_right_inverse ≝
  46  λM:PreMonoid.
  47   λopp: M → M.
  48    ∀x:M. x·(opp x) = ⅇ.
  49
  50 theorem is_left_inverse_to_is_right_inverse_to_eq:
  51  ∀M:Monoid. ∀l,r.
  52   is_left_inverse M l → is_right_inverse M r →
  53    ∀x:M. l x = r x.
  54  intros;
  55  lapply (H x) as H2;
  56  lapply (eq_f ? ? (λy.y·(r x)) ? ? H2) as H3; clear H2;
  57  rewrite > (op_is_associative ? M) in H3.
  58  rewrite > H1 in H3;
  59  rewrite > (e_is_left_unit ? M) in H3;
  60  rewrite > (e_is_right_unit ? M) in H3;
  61  assumption.
  62 qed.