From 6f5127e717e9022c8e63495fe65d09547a09137c Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 25 Jan 2006 18:00:05 +0000
Subject: [PATCH] New formulation of finite_enumerable_SemiGroups to allow the
 \iota notation to be invertible. However, this does not work (yet) in
 practice due to unification between a coercion and a composite coercion. E.g.
  (composite x) vs (f (g ?1))

---
 helm/matita/library/algebra/groups.ma | 86 ++++++++++++++++++---------
 1 file changed, 58 insertions(+), 28 deletions(-)

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index 15361b6c9..c93c9d94c 100644
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -103,7 +103,7 @@ record finite_enumerable (T:Type) : Type ≝
    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 }.
 
@@ -116,57 +116,87 @@ for @{ 'card $C }.
 interpretation "Finite_enumerable order" 'card C =
  (cic:/matita/algebra/groups/order.con C _).
 
-theorem repr_inj:
- ∀T:Type. ∀H:finite_enumerable T.
-  ∀n,n'. n ≤ order ? H → n' ≤ order ? H →
-   repr ? H n = repr ? H n' → n=n'.
-intros;
-rewrite < (index_of_repr ? ? ? H1);
-rewrite > H3;
-apply index_of_repr;
-assumption.
-qed.
+record finite_enumerable_SemiGroup : Type ≝
+ { 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 }.
+
+interpretation "Semigroup_of_finite_enumerable_semigroup"
+ 'semigroup_of_finite_enumerable_semigroup S
+=
+ (cic:/matita/algebra/groups/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:SemiGroup.
-  finite_enumerable (carrier G) →
-   left_cancellable (carrier G) (op G) →
-    right_cancellable (carrier G) (op G) →
-     ∃e:G. isMonoid ? e.
-intros (G H);
-letin f ≝ (λn.index_of ? H ((repr ? H O)·(repr ? H n)));
-cut (∀n.n ≤ order ? H → ∃m.f m = n);
+ ∀G:finite_enumerable_SemiGroup.
+  left_cancellable ? (op G) →
+  right_cancellable ? (op G) →
+   ∃e:G. isMonoid G e.
+intros;
+letin f ≝
+ (λn.index_of G (is_finite_enumerable G)
+  (op G
+   (repr (Type_of_finite_enumerable_SemiGroup G) (is_finite_enumerable G) O)
+   (repr (Type_of_finite_enumerable_SemiGroup G) (is_finite_enumerable G) 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;
-    letin HH ≝ (eq_f ? ? (repr ? H) ? ? H3);
+    clear EX;
+    letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
     clearbody HH;
-    rewrite > (repr_index_of ? H) in HH;
-    apply (ex_intro ? ? (repr ? H a));
-    letin GOGO ≝ (refl_eq ? (repr ? H O));
+    rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
+    apply (ex_intro ? ? (repr ? (is_finite_enumerable G) a));
+    letin GOGO ≝ (refl_eq ? (repr ? (is_finite_enumerable G) O));
     clearbody GOGO;
     rewrite < HH in GOGO;
     rewrite < HH in GOGO:(? ? % ?);
     rewrite > (semigroup_properties G) in GOGO;
-    letin GaGa ≝ (H1 ? ? ? GOGO);
+    letin GaGa ≝ (H ? ? ? GOGO);
     clearbody GaGa;
     clear GOGO;
     constructor 1;
     [ unfold is_left_unit; intro;
-      letin GaxGax ≝ (refl_eq ? ((repr ? H a)·x));
+      letin GaxGax ≝ (refl_eq ? ((repr ? (is_finite_enumerable G) a)·x));
       clearbody GaxGax;
       rewrite < GaGa in GaxGax:(? ? % ?);
       rewrite > (semigroup_properties G) in GaxGax;
-      apply (H1 ? ? ? GaxGax)
+      apply (H ? ? ? GaxGax)
     | unfold is_right_unit; intro;
-      letin GaxGax ≝ (refl_eq ? (x·(repr ? H a)));
+      letin GaxGax ≝ (refl_eq ? (x·(repr ? (is_finite_enumerable G) a)));
       clearbody GaxGax;
       rewrite < GaGa in GaxGax:(? ? % ?);
       rewrite < (semigroup_properties G) in GaxGax;
-      apply (H2 ? ? ? GaxGax)
+      apply (H1 ? ? ? GaxGax)
   ]
 |
 ].
\ No newline at end of file
-- 
2.39.2