From 1561ac998b6823c9e763617fcb9cf3c063bb5e3b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 19 Jan 2006 18:30:42 +0000 Subject: [PATCH] 1. Back to nicer (and more comprehensible) notation (that cannot be used when more than one structure is in use at once). 2. The first definitions and theorems over groups. --- helm/matita/library/algebra/groups.ma | 61 +++++++++++++++++++++++ helm/matita/library/algebra/monoids.ma | 36 +++++++------ helm/matita/library/algebra/semigroups.ma | 27 ++++++---- 3 files changed, 98 insertions(+), 26 deletions(-) diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma index 6eb0054c2..a9164a927 100644 --- a/helm/matita/library/algebra/groups.ma +++ b/helm/matita/library/algebra/groups.ma @@ -14,3 +14,64 @@ set "baseuri" "cic:/matita/algebra/groups/". +include "algebra/monoids.ma". + +record isGroup (M:Monoid) (opp: M -> M) : Prop ≝ + { opp_is_left_inverse: is_left_inverse M opp; + opp_is_right_inverse: is_right_inverse M opp + }. + +record Group : Type ≝ + { monoid: Monoid; + opp: monoid -> monoid; + group_properties: isGroup ? opp + }. + +coercion cic:/matita/algebra/groups/monoid.con. + +notation "hvbox(x \sup (-1))" with precedence 89 +for @{ 'gopp $x }. + +interpretation "Group inverse" 'gopp x = + (cic:/matita/algebra/groups/opp.con _ x). + +definition left_cancellable := + \lambda T:Type. \lambda op: T -> T -> T. + \forall x,y,z. op x y = op x z -> y = z. + +definition right_cancellable := + \lambda T:Type. \lambda op: T -> T -> T. + \forall x,y,z. op y x = op z x -> y = z. + +theorem eq_op_x_y_op_x_z_to_eq: + \forall G:Group. left_cancellable G (op G). +intros; +unfold left_cancellable; +intros; +rewrite < (e_is_left_unit ? ? (monoid_properties G)); +fold simplify (e G); +rewrite < (e_is_left_unit ? ? (monoid_properties G) z); +fold simplify (e G); +rewrite < (opp_is_left_inverse ? ? (group_properties G) x); +fold simplify (opp G); +rewrite > (semigroup_properties G); +fold simplify (op G); +rewrite > (semigroup_properties G); +fold simplify (op G); +apply eq_f; +assumption. +qed. + +(* +theorem eq_op_x_y_op_z_y_to_eq: + \forall G:Group. right_cancellable G (op G). +qed. + +definition has_cardinality := + \lambda T:Type. \lambda n:nat. + \exists f. injective T nat f. + +definition finite := + \lambda T:Type. + \exists f: T -> {n|n< +*) diff --git a/helm/matita/library/algebra/monoids.ma b/helm/matita/library/algebra/monoids.ma index c85d1ebc1..7c40db1fd 100644 --- a/helm/matita/library/algebra/monoids.ma +++ b/helm/matita/library/algebra/monoids.ma @@ -24,17 +24,24 @@ record isMonoid (SS:SemiGroup) (e:SS) : Prop ≝ record Monoid : Type ≝ { semigroup: SemiGroup; e: semigroup; - properties: isMonoid ? e + monoid_properties: isMonoid ? e }. coercion cic:/matita/algebra/monoids/semigroup.con. -notation "hvbox(! \sub S)" +(* too ugly +notation "hvbox(1 \sub S)" with precedence 89 for @{ 'munit $S }. interpretation "Monoid unit" 'munit S = - (cic:/matita/algebra/monoids/e.con S). - + (cic:/matita/algebra/monoids/e.con S). *) + +notation "1" with precedence 89 +for @{ 'munit }. + +interpretation "Monoid unit" 'munit = + (cic:/matita/algebra/monoids/e.con _). + notation < "M" for @{ 'semigroup $M }. @@ -44,30 +51,29 @@ interpretation "Semigroup coercion" 'semigroup M = definition is_left_inverse ≝ λM:Monoid. λopp: M → M. - ∀x:M. op M (opp x) x = ! \sub M. - + ∀x:M. op M (opp x) x = 1. + definition is_right_inverse ≝ λM:Monoid. λopp: M → M. - ∀x:M. op M x (opp x) = ! \sub M. + ∀x:M. op M x (opp x) = 1. theorem is_left_inverse_to_is_right_inverse_to_eq: - ∀M:Monoid. ∀oppL,oppR. - is_left_inverse M oppL → is_right_inverse M oppR → - ∀x:M. oppL x = oppR x. + ∀M:Monoid. ∀l,r. + 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. op M y (oppR x)) ? ? H2); + generalize in match (eq_f ? ? (λy. op M y (r x)) ? ? H2); simplify; fold simplify (op M); intro; clear H2; - generalize in match (properties (semigroup M)); + generalize in match (semigroup_properties M); fold simplify (Type_of_Monoid M); intro; unfold isSemiGroup in H2; unfold associative in H2; rewrite > H2 in H3; clear H2; rewrite > H1 in H3; - rewrite > (e_is_left_unit ? ? (properties M)) in H3; - rewrite > (e_is_right_unit ? ? (properties M)) in H3; + rewrite > (e_is_left_unit ? ? (monoid_properties M)) in H3; + rewrite > (e_is_right_unit ? ? (monoid_properties M)) in H3; assumption. qed. - diff --git a/helm/matita/library/algebra/semigroups.ma b/helm/matita/library/algebra/semigroups.ma index 93a139ca7..64c2d13c9 100644 --- a/helm/matita/library/algebra/semigroups.ma +++ b/helm/matita/library/algebra/semigroups.ma @@ -22,32 +22,37 @@ definition isSemiGroup ≝ record SemiGroup : Type ≝ { carrier: Type; op: carrier → carrier → carrier; - properties: isSemiGroup carrier op + semigroup_properties: isSemiGroup carrier op }. coercion cic:/matita/algebra/semigroups/carrier.con. -notation "hvbox(a break * \sub S b)" +notation "hvbox(a break \middot \sub S b)" left associative with precedence 55 for @{ 'ptimes $S $a $b }. -interpretation "Semigroup operation" 'times a b = +notation "hvbox(a break \middot b)" + left associative with precedence 55 +for @{ 'ptimesi $a $b }. + +interpretation "Semigroup operation" 'ptimesi a b = (cic:/matita/algebra/semigroups/op.con _ a b). +(* too ugly interpretation "Semigroup operation" 'ptimes S a b = - (cic:/matita/algebra/semigroups/op.con S a b). + (cic:/matita/algebra/semigroups/op.con S a b). *) definition is_left_unit ≝ - λS:SemiGroup. λe:S. ∀x:S. e * x = x. + λS:SemiGroup. λe:S. ∀x:S. e·x = x. definition is_right_unit ≝ - λS:SemiGroup. λe:S. ∀x:S. x * e = x. + λS:SemiGroup. λe:S. ∀x:S. x·e = x. theorem is_left_unit_to_is_right_unit_to_eq: - ∀S:SemiGroup. ∀e1,e2:S. - is_left_unit ? e1 → is_right_unit ? e2 → e1=e2. + ∀S:SemiGroup. ∀e,e':S. + is_left_unit ? e → is_right_unit ? e' → e=e'. intros; - rewrite < (H e2); - rewrite < (H1 e1) in \vdash (? ? % ?); + rewrite < (H e'); + rewrite < (H1 e) in \vdash (? ? % ?); reflexivity. -qed. \ No newline at end of file +qed. -- 2.39.2