1. The last commit that fixed unification of compound coercions with

[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 bec57fb4c2ca845a9d49bcd511c74b15a44e81bb..ae6b525e3906d9b6f5b153b0c767ed6c47faed08 100644 (file)
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -17,24 +17,27 @@ 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"
+(*notation < "G"
 for @{ 'monoid $G }.
 
 interpretation "Monoid coercion" 'monoid G =
- (cic:/matita/algebra/groups/monoid.con G).
+ (cic:/matita/algebra/groups/monoid.con G).*)
 
 notation < "G"
 for @{ 'type_of_group $G }.
@@ -43,10 +46,10 @@ interpretation "Type_of_group coercion" 'type_of_group G =
  (cic:/matita/algebra/groups/Type_of_Group.con G).
 
 notation < "G"
-for @{ 'semigroup_of_group $G }.
+for @{ 'magma_of_group $G }.
 
-interpretation "Semigroup_of_group coercion" 'semigroup_of_group G =
- (cic:/matita/algebra/groups/SemiGroup_of_Group.con 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 }.
@@ -68,11 +71,11 @@ intros;
 unfold left_cancellable;
 unfold injective;
 intros (x y z);
-rewrite < (e_is_left_unit ? ? (monoid_properties G));
-rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
-rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
-rewrite > (semigroup_properties G);
-rewrite > (semigroup_properties G);
+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.
@@ -85,11 +88,11 @@ unfold right_cancellable;
 unfold injective;
 simplify;fold simplify (op G); 
 intros (x y z);
-rewrite < (e_is_right_unit ? ? (monoid_properties G));
-rewrite < (e_is_right_unit ? ? (monoid_properties G) z);
-rewrite < (opp_is_right_inverse ? ? (group_properties G) x);
-rewrite < (semigroup_properties G);
-rewrite < (semigroup_properties G);
+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.
@@ -119,13 +122,10 @@ 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
+ { semigroup:> SemiGroup;
+   is_finite_enumerable:> finite_enumerable semigroup
  }.
 
-coercion cic:/matita/algebra/groups/semigroup.con.
-coercion cic:/matita/algebra/groups/is_finite_enumerable.con.
-
 notation < "S"
 for @{ 'semigroup_of_finite_enumerable_semigroup $S }.
 
@@ -134,6 +134,14 @@ interpretation "Semigroup_of_finite_enumerable_semigroup"
 =
  (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 }.
 
@@ -159,7 +167,7 @@ theorem foo:
  ∀G:finite_enumerable_SemiGroup.
   left_cancellable ? (op G) →
   right_cancellable ? (op G) →
-   ∃e:G. isMonoid G e.
+   ∃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);
@@ -178,23 +186,26 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
     clearbody GOGO;
     rewrite < HH in GOGO;
     rewrite < HH in GOGO:(? ? % ?);
-    rewrite > (semigroup_properties G) in GOGO;
+    rewrite > (associative ? G) in GOGO;
     letin GaGa ≝ (H ? ? ? GOGO);
     clearbody GaGa;
     clear GOGO;
     constructor 1;
-    [ unfold is_left_unit; intro;
+    [ 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 > (semigroup_properties G) 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 < (semigroup_properties G) in GaxGax;
+      rewrite < (associative ? (semigroup_properties G)) in GaxGax;
       apply (H1 ? ? ? GaxGax)
+    ]
   ]
 |
-].
\ No newline at end of file
+].