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