From c40f28fe5bfa74fc1fcef986c03fc960793902a5 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 13 Jun 2009 19:00:52 +0000
Subject: [PATCH] we removed some coercion detours and we added some coercions
 we really would like to see

---
 .../matita/library/algebra/finite_groups.ma   | 10 ++--
 .../software/matita/library/algebra/groups.ma | 51 ++++++++++---------
 .../matita/library/algebra/monoids.ma         | 50 +++++++++---------
 .../matita/library/algebra/semigroups.ma      | 26 +++++-----
 4 files changed, 68 insertions(+), 69 deletions(-)

diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma
index 6da0a7256..30408be37 100644
--- a/helm/software/matita/library/algebra/finite_groups.ma
+++ b/helm/software/matita/library/algebra/finite_groups.ma
@@ -327,7 +327,7 @@ theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_
  ∀G:finite_enumerable_SemiGroup.
   left_cancellable ? (op G) →
   right_cancellable ? (op G) →
-   ∃e:G. isMonoid (mk_PreMonoid 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);
@@ -346,24 +346,24 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
     clearbody GOGO;
     rewrite < HH in GOGO;
     rewrite < HH in GOGO:(? ? % ?);
-    rewrite > (op_associative ? G) in GOGO;
+    rewrite > (op_is_associative ? G) in GOGO;
     letin GaGa ≝(H ? ? ? GOGO);
     clearbody GaGa;
     clear GOGO;
     constructor 1;
     [ simplify;
-      apply (semigroup_properties G)
+      apply (is_semi_group G)
     | unfold is_left_unit; intro;
       letin GaxGax ≝(refl_eq ? (G \sub a ·x));
       clearbody GaxGax; (* demo *)
       rewrite < GaGa in GaxGax:(? ? % ?);
-      rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
+      rewrite > (op_is_associative ? 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 < (op_associative ? (semigroup_properties G)) in GaxGax;
+      rewrite < (op_is_associative ? G) in GaxGax;
       apply (H1 ? ? ? GaxGax)
     ]
   ]
diff --git a/helm/software/matita/library/algebra/groups.ma b/helm/software/matita/library/algebra/groups.ma
index bfb639af7..fd08a95da 100644
--- a/helm/software/matita/library/algebra/groups.ma
+++ b/helm/software/matita/library/algebra/groups.ma
@@ -18,22 +18,27 @@ include "datatypes/bool.ma".
 include "nat/compare.ma".
 
 record PreGroup : Type ≝
- { premonoid:> PreMonoid;
-   inv: premonoid -> premonoid
+ { pre_monoid:> PreMonoid;
+   inv: pre_monoid -> pre_monoid
  }.
 
+interpretation "Group inverse" 'invert x = (inv ? x).
+
 record isGroup (G:PreGroup) : Prop ≝
- { is_monoid:> isMonoid G;
-   inv_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (inv G);
-   inv_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (inv G)
+ { is_monoid           :> IsMonoid G;
+   inv_is_left_inverse :  is_left_inverse G (inv G);
+   inv_is_right_inverse:  is_right_inverse G (inv G)
  }.
- 
+
 record Group : Type ≝
- { pregroup:> PreGroup;
-   group_properties:> isGroup pregroup
+ { pre_group:> PreGroup;
+   is_group:> isGroup pre_group
  }.
 
-interpretation "Group inverse" 'invert x = (inv ? x).
+definition Monoid_of_Group: Group → Monoid ≝
+ λG. mk_Monoid ? (is_group G).
+
+coercion Monoid_of_Group nocomposites.
 
 definition left_cancellable ≝
  λT:Type. λop: T -> T -> T.
@@ -52,25 +57,23 @@ intros (x y z);
 rewrite < (e_is_left_unit ? G);
 rewrite < (e_is_left_unit ? G z);
 rewrite < (inv_is_left_inverse ? G x);
-rewrite > (op_associative ? G);
-rewrite > (op_associative ? G);
+rewrite > (op_is_associative ? G);
+rewrite > (op_is_associative ? G);
 apply eq_f;
 assumption.
 qed.
 
-
 theorem eq_op_x_y_op_z_y_to_eq:
  ∀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 ? G);
 rewrite < (e_is_right_unit ? G z);
 rewrite < (inv_is_right_inverse ? G x);
-rewrite < (op_associative ? G);
-rewrite < (op_associative ? G);
+rewrite < (op_is_associative ? G);
+rewrite < (op_is_associative ? G);
 rewrite > H;
 reflexivity.
 qed.
@@ -104,7 +107,7 @@ theorem eq_opxy_z_to_eq_x_opzinvy:
  ∀G:Group. ∀x,y,z:G. x·y=z → x = z·y \sup -1.
 intros;
 apply (eq_op_x_y_op_z_y_to_eq ? y);
-rewrite > (op_associative ? G);
+rewrite > (op_is_associative ? G);
 rewrite > (inv_is_left_inverse ? G);
 rewrite > (e_is_right_unit ? G);
 assumption.
@@ -114,7 +117,7 @@ theorem eq_opxy_z_to_eq_y_opinvxz:
  ∀G:Group. ∀x,y,z:G. x·y=z → y = x \sup -1·z.
 intros;
 apply (eq_op_x_y_op_x_z_to_eq ? x);
-rewrite < (op_associative ? G);
+rewrite < (op_is_associative ? G);
 rewrite > (inv_is_right_inverse ? G);
 rewrite > (e_is_left_unit ? G);
 assumption.
@@ -125,8 +128,8 @@ theorem eq_inv_op_x_y_op_inv_y_inv_x:
 intros;
 apply (eq_op_x_y_op_z_y_to_eq ? (x·y));
 rewrite > (inv_is_left_inverse ? G);
-rewrite < (op_associative ? G);
-rewrite > (op_associative ? G (y \sup -1));
+rewrite < (op_is_associative ? G);
+rewrite > (op_is_associative ? G (y \sup -1));
 rewrite > (inv_is_left_inverse ? G);
 rewrite > (e_is_right_unit ? G);
 rewrite > (inv_is_left_inverse ? G);
@@ -246,8 +249,8 @@ exists;
   rewrite < H2;
   rewrite > eq_inv_op_x_y_op_inv_y_inv_x;
   rewrite > eq_inv_inv_x_x;
-  rewrite < (op_associative ? G);
-  rewrite < (op_associative ? G);
+  rewrite < (op_is_associative ? G);
+  rewrite < (op_is_associative ? G);
   rewrite > (inv_is_right_inverse ? G);
   rewrite > (e_is_left_unit ? G);
   reflexivity
@@ -266,12 +269,12 @@ elim H2;
 apply (ex_intro ? ? (x'·a \sup -1));
 rewrite > f_morph; 
 apply (eq_op_x_y_op_z_y_to_eq ? (a \sub H));
-rewrite > (op_associative ? G);
+rewrite > (op_is_associative ? G);
 rewrite < H3;
-rewrite > (op_associative ? G);
+rewrite > (op_is_associative ? G);
 rewrite < f_morph;
 rewrite > (inv_is_left_inverse ? H);
-rewrite < (op_associative ? G);
+rewrite < (op_is_associative ? G);
 rewrite > (inv_is_left_inverse ? G);
 rewrite > (e_is_left_unit ? G);
 rewrite < (f_morph ? ? H);
diff --git a/helm/software/matita/library/algebra/monoids.ma b/helm/software/matita/library/algebra/monoids.ma
index 36de5a369..71e9a7c59 100644
--- a/helm/software/matita/library/algebra/monoids.ma
+++ b/helm/software/matita/library/algebra/monoids.ma
@@ -15,33 +15,35 @@
 include "algebra/semigroups.ma".
 
 record PreMonoid : Type ≝
- { magma:> Magma;
-   e: magma
- }.
+{ pre_semi_group :> PreSemiGroup;
+  e              :  pre_semi_group 
+}.
 
-(* FG: the interpretation goes just after its definition *)
 interpretation "Monoid unit" 'neutral = (e ?).
 
-record isMonoid (M:PreMonoid) : Prop ≝
- { is_semi_group:> isSemiGroup M;
-   e_is_left_unit:
-    is_left_unit (mk_SemiGroup ? is_semi_group) (e M);
-   e_is_right_unit:
-    is_right_unit (mk_SemiGroup ? is_semi_group) (e M)
+record IsMonoid (M:PreMonoid): Prop ≝
+ { is_pre_semi_group :> IsSemiGroup M;
+   e_is_left_unit    :  is_left_unit M ⅇ;
+   e_is_right_unit   :  is_right_unit M ⅇ
  }.
- 
+
 record Monoid : Type ≝
- { premonoid:> PreMonoid;
-   monoid_properties:> isMonoid premonoid 
+ { pre_monoid :> PreMonoid;
+   is_monoid  :> IsMonoid pre_monoid 
  }.
-  
+
+definition SemiGroup_of_Monoid: Monoid → SemiGroup ≝
+ λM. mk_SemiGroup ? (is_monoid M).
+
+coercion SemiGroup_of_Monoid nocomposites.
+
 definition is_left_inverse ≝
- λM:Monoid.
+ λM:PreMonoid.
   λopp: M → M.
    ∀x:M. (opp x)·x = ⅇ.
-   
+
 definition is_right_inverse ≝
- λM:Monoid.
+ λM:PreMonoid.
   λopp: M → M.
    ∀x:M. x·(opp x) = ⅇ.
 
@@ -50,15 +52,11 @@ theorem is_left_inverse_to_is_right_inverse_to_eq:
   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.y·(r x)) ? ? H2);
- simplify; fold simplify (op M);
- intro; clear H2;
- generalize in match (op_associative ? (is_semi_group ? (monoid_properties M)));
- intro;
- rewrite > H2 in H3; clear H2;
+ lapply (H x) as H2;
+ lapply (eq_f ? ? (λy.y·(r x)) ? ? H2) as H3; clear H2;
+ rewrite > (op_is_associative ? M) in H3.
  rewrite > H1 in H3;
- rewrite > (e_is_left_unit ? (monoid_properties M)) in H3;
- rewrite > (e_is_right_unit ? (monoid_properties M)) in H3;
+ rewrite > (e_is_left_unit ? M) in H3;
+ rewrite > (e_is_right_unit ? M) in H3;
  assumption.
 qed.
diff --git a/helm/software/matita/library/algebra/semigroups.ma b/helm/software/matita/library/algebra/semigroups.ma
index 7d68dbb36..18d73b619 100644
--- a/helm/software/matita/library/algebra/semigroups.ma
+++ b/helm/software/matita/library/algebra/semigroups.ma
@@ -14,33 +14,31 @@
 
 include "higher_order_defs/functions.ma".
 
-(* Magmas *)
+(* Semigroups *)
 
-record Magma : Type≝
+record PreSemiGroup : Type≝
  { carrier:> Type;
    op: carrier → carrier → carrier
  }.
 
-interpretation "magma operation" 'middot a b = (op ? a b).
-
-(* Semigroups *)
+interpretation "Semigroup operation" 'middot a b = (op ? a b).
 
-record isSemiGroup (M:Magma) : Prop≝
- { op_associative: associative ? (op M) }.
+record IsSemiGroup (S:PreSemiGroup) : Prop ≝
+ { op_is_associative: associative ? (op S) }.
 
 record SemiGroup : Type≝
- { magma:> Magma;
-   semigroup_properties:> isSemiGroup magma
+ { pre_semi_group:> PreSemiGroup;
+   is_semi_group :> IsSemiGroup pre_semi_group
  }.
- 
+
 definition is_left_unit ≝
- λS:SemiGroup. λe:S. ∀x:S. e·x = x.
- 
+ λS:PreSemiGroup. λe:S. ∀x:S. e·x = x.
+
 definition is_right_unit ≝
- λS:SemiGroup. λe:S. ∀x:S. x·e = x.
+ λS:PreSemiGroup. λe:S. ∀x:S. x·e = x.
 
 theorem is_left_unit_to_is_right_unit_to_eq:
- ∀S:SemiGroup. ∀e,e':S.
+ ∀S:PreSemiGroup. ∀e,e':S.
   is_left_unit ? e → is_right_unit ? e' → e=e'.
  intros;
  rewrite < (H e');
-- 
2.39.2