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 6eb0054c2fcb81fc93bd6c52cc5a70b5fe84d216..a9164a927bde9cf2f937d77a2b8f0dabadd64428 100644 (file)
--- 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 c85d1ebc1842df1e80af57928ca936766ef83f46..7c40db1fd89bffad6aefb0b284c01f10e4f1b169 100644 (file)
--- 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 93a139ca760e5113f6b87d00a8f09d5552861e48..64c2d13c9670f4e66a94448fb414895a1dfaeb34 100644 (file)
--- 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.