include "algebra/monoids.ma".
include "nat/le_arith.ma".
-record isGroup (M:Monoid) (opp: M -> M) : Prop ≝
- { opp_is_left_inverse: is_left_inverse M opp;
- opp_is_right_inverse: is_right_inverse M opp
+record PreGroup : Type ≝
+ { premonoid:> PreMonoid;
+ opp: premonoid -> premonoid
+ }.
+
+record isGroup (G:PreGroup) : Prop ≝
+ { is_monoid: isMonoid G;
+ opp_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (opp G);
+ opp_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (opp G)
}.
record Group : Type ≝
- { monoid: Monoid;
- opp: monoid -> monoid;
- group_properties: isGroup ? opp
+ { pregroup:> PreGroup;
+ group_properties:> isGroup pregroup
}.
-coercion cic:/matita/algebra/groups/monoid.con.
-
-notation < "G"
+(*notation < "G"
for @{ 'monoid $G }.
interpretation "Monoid coercion" 'monoid G =
- (cic:/matita/algebra/groups/monoid.con G).
+ (cic:/matita/algebra/groups/monoid.con G).*)
notation < "G"
for @{ 'type_of_group $G }.
(cic:/matita/algebra/groups/Type_of_Group.con G).
notation < "G"
-for @{ 'semigroup_of_group $G }.
+for @{ 'magma_of_group $G }.
-interpretation "Semigroup_of_group coercion" 'semigroup_of_group G =
- (cic:/matita/algebra/groups/SemiGroup_of_Group.con G).
+interpretation "magma_of_group coercion" 'magma_of_group G =
+ (cic:/matita/algebra/groups/Magma_of_Group.con G).
notation "hvbox(x \sup (-1))" with precedence 89
for @{ 'gopp $x }.
unfold left_cancellable;
unfold injective;
intros (x y z);
-rewrite < (e_is_left_unit ? ? (monoid_properties G));
-rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
-rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
-rewrite > (semigroup_properties G);
-rewrite > (semigroup_properties G);
+rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G)));
+rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G)) z);
+rewrite < (opp_is_left_inverse ? (group_properties G) x);
+rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
+rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
apply eq_f;
assumption.
qed.
unfold injective;
simplify;fold simplify (op G);
intros (x y z);
-rewrite < (e_is_right_unit ? ? (monoid_properties G));
-rewrite < (e_is_right_unit ? ? (monoid_properties G) z);
-rewrite < (opp_is_right_inverse ? ? (group_properties G) x);
-rewrite < (semigroup_properties G);
-rewrite < (semigroup_properties G);
+rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G)));
+rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G)) z);
+rewrite < (opp_is_right_inverse ? (group_properties G) x);
+rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
+rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
rewrite > H;
reflexivity.
qed.
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
+
+notation "hvbox(C \sub i)" with precedence 89
for @{ 'repr $C $i }.
+(* CSC: multiple interpretations in the same file are not considered in the
+ right order
interpretation "Finite_enumerable representation" 'repr C i =
- (cic:/matita/algebra/groups/repr.con C _ i).
+ (cic:/matita/algebra/groups/repr.con C _ i).*)
-notation < "hvbox(|C|)" with precedence 89
+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.
+record finite_enumerable_SemiGroup : Type ≝
+ { semigroup:> SemiGroup;
+ is_finite_enumerable:> finite_enumerable semigroup
+ }.
+
+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 @{ 'magma_of_finite_enumerable_semigroup $S }.
+
+interpretation "Magma_of_finite_enumerable_semigroup"
+ 'magma_of_finite_enumerable_semigroup S
+=
+ (cic:/matita/algebra/groups/Magma_of_finite_enumerable_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 (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);
[ 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 ? ? (G \sub 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);
+ rewrite > (associative ? G) in GOGO;
+ letin GaGa ≝ (H ? ? ? GOGO);
clearbody GaGa;
clear GOGO;
constructor 1;
- [ unfold is_left_unit; intro;
- letin GaxGax ≝ (refl_eq ? ((repr ? H a)·x));
+ [ simplify;
+ apply (semigroup_properties G)
+ | unfold is_left_unit; intro;
+ letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
- rewrite > (semigroup_properties G) in GaxGax;
- apply (H1 ? ? ? GaxGax)
+ rewrite > (associative ? (semigroup_properties G)) in GaxGax;
+ apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
- letin GaxGax ≝ (refl_eq ? (x·(repr ? H a)));
+ letin GaxGax ≝ (refl_eq ? (x·G \sub a));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
- rewrite < (semigroup_properties G) in GaxGax;
- apply (H2 ? ? ? GaxGax)
+ rewrite < (associative ? (semigroup_properties G)) in GaxGax;
+ apply (H1 ? ? ? GaxGax)
+ ]
]
|
-].
\ No newline at end of file
+].