include "algebra/groups.ma".
-record finite_enumerable (T:Type) : Type ≝
+record finite_enumerable (T:Type) : Type≝
{ order: nat;
repr: nat → T;
index_of: T → nat;
interpretation "Finite_enumerable order" 'card C =
(cic:/matita/algebra/finite_groups/order.con C _).
-record finite_enumerable_SemiGroup : Type ≝
+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/finite_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/finite_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/finite_groups/Type_of_finite_enumerable_SemiGroup.con S).
-
interpretation "Finite_enumerable representation" 'repr S i =
(cic:/matita/algebra/finite_groups/repr.con S
(cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i).
(* several definitions/theorems to be moved somewhere else *)
-definition ltb ≝ λn,m. leb n m ∧ notb (eqb n m).
+definition ltb ≝λn,m. leb n m ∧ notb (eqb n m).
theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
intros;
apply (le_S_S ? ? H).
qed.
+(* moved to nat/order.ma
theorem lt_O_S: ∀n. O < S n.
intro;
unfold lt;
apply le_S_S;
apply le_O_n.
-qed.
+qed. *)
theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
intros;
| clear n;
letin f' ≝
(λx.
- let fSn1 ≝ f (S n1) in
- let fx ≝ f x in
+ let fSn1 ≝f (S n1) in
+ let fx ≝f x in
match ltb fSn1 fx with
[ true ⇒ pred fx
| false ⇒ fx
]
].
qed.
-
+(* demo *)
theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid:
∀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));
+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 ?);
+[ letin EX ≝(Hcut O ?);
[ apply le_O_n
| clearbody EX;
clear Hcut;
unfold f in EX;
elim EX;
clear EX;
- letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
+ letin HH ≝(eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
clearbody HH;
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));
+ letin GOGO ≝(refl_eq ? (repr ? (is_finite_enumerable G) O));
clearbody GOGO;
rewrite < HH in GOGO;
rewrite < HH in GOGO:(? ? % ?);
- rewrite > (associative ? G) in GOGO;
- letin GaGa ≝ (H ? ? ? GOGO);
+ rewrite > (op_associative ? G) in GOGO;
+ letin GaGa ≝(H ? ? ? GOGO);
clearbody GaGa;
clear GOGO;
constructor 1;
[ simplify;
apply (semigroup_properties G)
| unfold is_left_unit; intro;
- letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
- clearbody GaxGax;
+ letin GaxGax ≝(refl_eq ? (G \sub a ·x));
+ clearbody GaxGax; (* demo *)
rewrite < GaGa in GaxGax:(? ? % ?);
- rewrite > (associative ? (semigroup_properties G)) in GaxGax;
+ rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
apply (H ? ? ? GaxGax)
| unfold is_right_unit; intro;
- letin GaxGax ≝ (refl_eq ? (x·G \sub a));
+ letin GaxGax ≝(refl_eq ? (x·G \sub a));
clearbody GaxGax;
rewrite < GaGa in GaxGax:(? ? % ?);
- rewrite < (associative ? (semigroup_properties G)) in GaxGax;
+ rewrite < (op_associative ? (semigroup_properties G)) in GaxGax;
apply (H1 ? ? ? GaxGax)
]
]
elim H3;
assumption
| intros;
- change in H5 with (ι(G \sub O · G \sub x) = ι(G \sub O · G \sub y));
+ simplify in H5;
cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
[ rewrite > (repr_index_of ? ? (G \sub O · G \sub x)) in Hcut;
rewrite > (repr_index_of ? ? (G \sub O · G \sub y)) in Hcut;