opp: monoid -> monoid;
group_properties: isGroup ? opp
}.
-
+
coercion cic:/matita/algebra/groups/monoid.con.
+notation < "G"
+for @{ 'monoid $G }.
+
+interpretation "Monoid coercion" 'monoid G =
+ (cic:/matita/algebra/groups/monoid.con G).
+
+notation < "G"
+for @{ 'type_of_group $G }.
+
+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 }.
+
+interpretation "Semigroup_of_group coercion" 'semigroup_of_group G =
+ (cic:/matita/algebra/groups/SemiGroup_of_Group.con G).
+
notation "hvbox(x \sup (-1))" with precedence 89
for @{ 'gopp $x }.
reflexivity.
qed.
-(*
-record enumerable (T:Type) : Type ≝
+
+record finite_enumerable (T:Type) : Type ≝
{ order: nat;
repr: nat → T;
- repr_inj: ∀n,n'. n≤order → n'≤order → repr n ≠ repr n';
- repr_sur: ∀x.∃n.n≤order ∧ repr n = x
+ index_of: T → nat;
+ index_of_sur: ∀x.index_of x ≤ order;
+ 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 representation" 'repr C i =
+ (cic:/matita/algebra/groups/repr.con C _ i).
+notation < "hvbox(|C|)" with precedence 89
+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.
theorem foo:
∀G:SemiGroup.
- enumerable (carrier G) →
+ finite_enumerable (carrier G) →
left_cancellable (carrier G) (op G) →
right_cancellable (carrier G) (op G) →
- ∃e:G. is_left_unit ? e.
+ ∃e:G. isMonoid ? e.
intros (G H);
-unfold left_cancellable in H1;
-letin x ≝ (repr ? H O);
-letin f ≝ (λy.x·(repr ? H y));
-generalize in match (H1 x);
-intro;
-*)
\ No newline at end of file
+letin f ≝ (λn.index_of ? H ((repr ? H O)·(repr ? H n)));
+cut (∀n.n ≤ order ? H → ∃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);
+ clearbody HH;
+ rewrite > (repr_index_of ? H) in HH;
+ apply (ex_intro ? ? (repr ? H a));
+ letin GOGO ≝ (refl_eq ? (repr ? H O));
+ clearbody GOGO;
+ rewrite < HH in GOGO;
+ rewrite < HH in GOGO:(? ? % ?);
+ rewrite > (semigroup_properties G) in GOGO;
+ letin GaGa ≝ (H1 ? ? ? GOGO);
+ clearbody GaGa;
+ clear GOGO;
+ constructor 1;
+ [ unfold is_left_unit; intro;
+ letin GaxGax ≝ (refl_eq ? ((repr ? H a)·x));
+ clearbody GaxGax;
+ rewrite < GaGa in GaxGax:(? ? % ?);
+ rewrite > (semigroup_properties G) in GaxGax;
+ apply (H1 ? ? ? GaxGax)
+ | unfold is_right_unit; intro;
+ letin GaxGax ≝ (refl_eq ? (x·(repr ? H a)));
+ clearbody GaxGax;
+ rewrite < GaGa in GaxGax:(? ? % ?);
+ rewrite < (semigroup_properties G) in GaxGax;
+ apply (H2 ? ? ? GaxGax)
+ ]
+|
+].
\ No newline at end of file