1. Back to nicer (and more comprehensible) notation (that cannot be used

[helm.git] / helm / matita / library / algebra / groups.ma

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<
+*)