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

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

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.
-