From: Claudio Sacerdoti Coen Date: Thu, 19 Jan 2006 18:30:42 +0000 (+0000) Subject: 1. Back to nicer (and more comprehensible) notation (that cannot be used X-Git-Tag: make_still_working~7809 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1561ac998b6823c9e763617fcb9cf3c063bb5e3b;p=helm.git 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. --- 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.