X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Falgebra%2Fgroups.ma;h=ae6b525e3906d9b6f5b153b0c767ed6c47faed08;hb=ec13ac23f555f04b0a546d0e8ae464d9b5806d9b;hp=a9164a927bde9cf2f937d77a2b8f0dabadd64428;hpb=1561ac998b6823c9e763617fcb9cf3c063bb5e3b;p=helm.git

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index a9164a927..ae6b525e3 100644
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -15,19 +15,41 @@
 set "baseuri" "cic:/matita/algebra/groups/".
 
 include "algebra/monoids.ma".
+include "nat/le_arith.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 PreGroup : Type ≝
+ { premonoid:> PreMonoid;
+   opp: premonoid -> premonoid
+ }.
+
+record isGroup (G:PreGroup) : Prop ≝
+ { is_monoid: isMonoid G;
+   opp_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (opp G);
+   opp_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (opp G)
  }.
  
 record Group : Type ≝
- { monoid: Monoid;
-   opp: monoid -> monoid;
-   group_properties: isGroup ? opp
+ { pregroup:> PreGroup;
+   group_properties:> isGroup pregroup
  }.
- 
-coercion cic:/matita/algebra/groups/monoid.con.
+
+(*notation < "G"
+for @{ 'monoid $G }.
+
+interpretation "Monoid coercion" 'monoid G =
+ (cic:/matita/algebra/groups/monoid.con G).*)
+
+notation < "G"
+for @{ 'type_of_group $G }.
+
+interpretation "Type_of_group coercion" 'type_of_group G =
+ (cic:/matita/algebra/groups/Type_of_Group.con G).
+
+notation < "G"
+for @{ 'magma_of_group $G }.
+
+interpretation "magma_of_group coercion" 'magma_of_group G =
+ (cic:/matita/algebra/groups/Magma_of_Group.con G).
 
 notation "hvbox(x \sup (-1))" with precedence 89
 for @{ 'gopp $x }.
@@ -35,43 +57,155 @@ 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 left_cancellable ≝
+ λT:Type. λop: T -> T -> T.
+  ∀x. injective ? ? (op x).
   
-definition right_cancellable :=
- \lambda T:Type. \lambda op: T -> T -> T.
-  \forall x,y,z. op y x = op z x -> y = z.
+definition right_cancellable ≝
+ λT:Type. λop: T -> T -> T.
+  ∀x. injective ? ? (λz.op z x).
   
 theorem eq_op_x_y_op_x_z_to_eq:
- \forall G:Group. left_cancellable G (op G).
+ ∀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);
+unfold injective;
+intros (x y z);
+rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G)));
+rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G)) z);
+rewrite < (opp_is_left_inverse ? (group_properties G) x);
+rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
+rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
 apply eq_f;
 assumption.
 qed.
 
-(*
+
 theorem eq_op_x_y_op_z_y_to_eq:
- \forall G:Group. right_cancellable G (op G).
+ ∀G:Group. right_cancellable G (op G).
+intros;
+unfold right_cancellable;
+unfold injective;
+simplify;fold simplify (op G); 
+intros (x y z);
+rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G)));
+rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G)) z);
+rewrite < (opp_is_right_inverse ? (group_properties G) x);
+rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
+rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
+rewrite > H;
+reflexivity.
 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<
-*)
+record finite_enumerable (T:Type) : Type ≝
+ { order: nat;
+   repr: nat → T;
+   index_of: T → nat;
+   index_of_sur: ∀x.index_of x ≤ order;
+   index_of_repr: ∀n. n≤order → index_of (repr n) = n;
+   repr_index_of: ∀x. repr (index_of x) = x
+ }.
+ 
+notation "hvbox(C \sub i)" with precedence 89
+for @{ 'repr $C $i }.
+
+(* CSC: multiple interpretations in the same file are not considered in the
+ right order
+interpretation "Finite_enumerable representation" 'repr C i =
+ (cic:/matita/algebra/groups/repr.con C _ i).*)
+ 
+notation "hvbox(|C|)" with precedence 89
+for @{ 'card $C }.
+
+interpretation "Finite_enumerable order" 'card C =
+ (cic:/matita/algebra/groups/order.con C _).
+
+record finite_enumerable_SemiGroup : Type ≝
+ { semigroup:> SemiGroup;
+   is_finite_enumerable:> finite_enumerable semigroup
+ }.
+
+notation < "S"
+for @{ 'semigroup_of_finite_enumerable_semigroup $S }.
+
+interpretation "Semigroup_of_finite_enumerable_semigroup"
+ 'semigroup_of_finite_enumerable_semigroup S
+=
+ (cic:/matita/algebra/groups/semigroup.con S).
+
+notation < "S"
+for @{ 'magma_of_finite_enumerable_semigroup $S }.
+
+interpretation "Magma_of_finite_enumerable_semigroup"
+ 'magma_of_finite_enumerable_semigroup S
+=
+ (cic:/matita/algebra/groups/Magma_of_finite_enumerable_SemiGroup.con S).
+ 
+notation < "S"
+for @{ 'type_of_finite_enumerable_semigroup $S }.
+
+interpretation "Type_of_finite_enumerable_semigroup"
+ 'type_of_finite_enumerable_semigroup S
+=
+ (cic:/matita/algebra/groups/Type_of_finite_enumerable_SemiGroup.con S).
+
+interpretation "Finite_enumerable representation" 'repr S i =
+ (cic:/matita/algebra/groups/repr.con S
+  (cic:/matita/algebra/groups/is_finite_enumerable.con S) i).
+
+notation "hvbox(ι e)" with precedence 60
+for @{ 'index_of_finite_enumerable_semigroup $e }.
+
+interpretation "Index_of_finite_enumerable representation"
+ 'index_of_finite_enumerable_semigroup e
+=
+ (cic:/matita/algebra/groups/index_of.con _
+  (cic:/matita/algebra/groups/is_finite_enumerable.con _) e).
+ 
+theorem foo:
+ ∀G:finite_enumerable_SemiGroup.
+  left_cancellable ? (op G) →
+  right_cancellable ? (op G) →
+   ∃e:G. isMonoid (mk_PreMonoid G e).
+intros;
+letin f ≝ (λn.ι(G \sub O · G \sub n));
+cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
+[ letin EX ≝ (Hcut O ?);
+  [ apply le_O_n
+  | clearbody EX;
+    clear Hcut;
+    unfold f in EX;
+    elim EX;
+    clear EX;
+    letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
+    clearbody HH;
+    rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
+    apply (ex_intro ? ? (G \sub a));
+    letin GOGO ≝ (refl_eq ? (repr ? (is_finite_enumerable G) O));
+    clearbody GOGO;
+    rewrite < HH in GOGO;
+    rewrite < HH in GOGO:(? ? % ?);
+    rewrite > (associative ? G) in GOGO;
+    letin GaGa ≝ (H ? ? ? GOGO);
+    clearbody GaGa;
+    clear GOGO;
+    constructor 1;
+    [ simplify;
+      apply (semigroup_properties G)
+    | unfold is_left_unit; intro;
+      letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
+      clearbody GaxGax;
+      rewrite < GaGa in GaxGax:(? ? % ?);
+      rewrite > (associative ? (semigroup_properties G)) in GaxGax;
+      apply (H ? ? ? GaxGax)
+    | unfold is_right_unit; intro;
+      letin GaxGax ≝ (refl_eq ? (x·G \sub a));
+      clearbody GaxGax;
+      rewrite < GaGa in GaxGax:(? ? % ?);
+      rewrite < (associative ? (semigroup_properties G)) in GaxGax;
+      apply (H1 ? ? ? GaxGax)
+    ]
+  ]
+|
+].