X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2Fmonoids.ma;h=71e9a7c594a609d335a13501695cc657564881b9;hb=395bcb2796cb9edcdb792579341c2271a8d1adaf;hp=36de5a369d47eae97a210e6d0f7c8c64362e38a1;hpb=a14157957532b731330492388ab32909b4147758;p=helm.git diff --git a/helm/software/matita/library/algebra/monoids.ma b/helm/software/matita/library/algebra/monoids.ma index 36de5a369..71e9a7c59 100644 --- a/helm/software/matita/library/algebra/monoids.ma +++ b/helm/software/matita/library/algebra/monoids.ma @@ -15,33 +15,35 @@ 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) = ⅇ. @@ -50,15 +52,11 @@ theorem is_left_inverse_to_is_right_inverse_to_eq: 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.