1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/algebra/finite_groups/".
17 include "algebra/groups.ma".
19 record finite_enumerable (T:Type) : Type ≝
23 index_of_sur: ∀x.index_of x ≤ order;
24 index_of_repr: ∀n. n≤order → index_of (repr n) = n;
25 repr_index_of: ∀x. repr (index_of x) = x
28 notation "hvbox(C \sub i)" with precedence 89
31 (* CSC: multiple interpretations in the same file are not considered in the
33 interpretation "Finite_enumerable representation" 'repr C i =
34 (cic:/matita/algebra/finite_groups/repr.con C _ i).*)
36 notation < "hvbox(|C|)" with precedence 89
39 interpretation "Finite_enumerable order" 'card C =
40 (cic:/matita/algebra/finite_groups/order.con C _).
42 record finite_enumerable_SemiGroup : Type ≝
43 { semigroup:> SemiGroup;
44 is_finite_enumerable:> finite_enumerable semigroup
48 for @{ 'semigroup_of_finite_enumerable_semigroup $S }.
50 interpretation "Semigroup_of_finite_enumerable_semigroup"
51 'semigroup_of_finite_enumerable_semigroup S
53 (cic:/matita/algebra/finite_groups/semigroup.con S).
56 for @{ 'magma_of_finite_enumerable_semigroup $S }.
58 interpretation "Magma_of_finite_enumerable_semigroup"
59 'magma_of_finite_enumerable_semigroup S
61 (cic:/matita/algebra/finite_groups/Magma_of_finite_enumerable_SemiGroup.con S).
64 for @{ 'type_of_finite_enumerable_semigroup $S }.
66 interpretation "Type_of_finite_enumerable_semigroup"
67 'type_of_finite_enumerable_semigroup S
69 (cic:/matita/algebra/finite_groups/Type_of_finite_enumerable_SemiGroup.con S).
71 interpretation "Finite_enumerable representation" 'repr S i =
72 (cic:/matita/algebra/finite_groups/repr.con S
73 (cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i).
75 notation "hvbox(ι e)" with precedence 60
76 for @{ 'index_of_finite_enumerable_semigroup $e }.
78 interpretation "Index_of_finite_enumerable representation"
79 'index_of_finite_enumerable_semigroup e
81 (cic:/matita/algebra/finite_groups/index_of.con _
82 (cic:/matita/algebra/finite_groups/is_finite_enumerable.con _) e).
85 (* several definitions/theorems to be moved somewhere else *)
87 definition ltb ≝ λn,m. leb n m ∧ notb (eqb n m).
89 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
91 elim (le_to_or_lt_eq ? ? H1);
112 | apply (not_eq_to_le_to_lt ? ? H H1)
116 | apply le_to_not_lt;
117 generalize in match (not_le_to_lt ? ? H1);
125 theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
126 (n < m → (P true)) → (n ≮ m → (P false)) →
130 (match (ltb n m) with
132 | false ⇒ n ≮ m] → (P (ltb n m))).
133 apply Hcut.apply ltb_to_Prop.
139 theorem Not_lt_n_n: ∀n. n ≮ n.
144 apply (not_le_Sn_n ? H).
147 theorem eq_pred_to_eq:
148 ∀n,m. O < n → O < m → pred n = pred m → n = m.
150 generalize in match (eq_f ? ? S ? ? H2);
152 rewrite < S_pred in H3;
153 rewrite < S_pred in H3;
157 theorem le_pred_to_le:
158 ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
163 rewrite > (S_pred m);
171 theorem le_to_le_pred:
172 ∀n,m. n ≤ m → pred n ≤ pred m.
178 generalize in match H1;
181 [ elim (not_le_Sn_O ? H1)
189 theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
195 generalize in match (le_S_S ? ? H);
197 generalize in match (transitive_le ? ? ? H2 H1);
199 apply (not_le_Sn_n ? H3).
202 theorem lt_S_S: ∀n,m. n < m → S n < S m.
205 apply (le_S_S ? ? H).
208 theorem lt_O_S: ∀n. O < S n.
215 theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
218 generalize in match (le_S_S_to_le ? ? H1);
220 apply cic:/matita/nat/orders/antisym_le.con;
226 (∀x,y.x≤n → y≤n → f x = f y → x=y) →
227 (∀m. m ≤ n → f m ≤ n) →
228 ∀x. x≤n → ∃y.f y = x ∧ y ≤ n.
231 [ apply (ex_intro ? ? O);
233 [ rewrite < (le_n_O_to_eq ? H2);
234 rewrite < (le_n_O_to_eq ? (H1 O ?));
243 let fSn1 ≝ f (S n1) in
245 match ltb fSn1 fx with
249 cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
250 [ cut (∀x. x ≤ n1 → f' x ≤ n1);
251 [ apply (nat_compare_elim (f (S n1)) x);
253 elim (H f' ? ? (pred x));
260 apply (ex_intro ? ? a);
262 [ generalize in match (eq_f ? ? S ? ? H6);
265 rewrite < S_pred in H5;
266 [ generalize in match H4;
270 apply (ltb_elim (f (S n1)) (f a));
275 | apply (ltn_to_ltO ? ? H4)
279 generalize in match (not_lt_to_le ? ? H4);
282 generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
284 generalize in match (H1 ? ? ? ? H4);
286 generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
288 generalize in match (H1 ? ? ? ? H9);
291 elim (not_le_Sn_n ? H7)
301 | apply (ltn_to_ltO ? ? H4)
308 | apply le_S_S_to_le;
311 | apply (ltn_to_ltO ? ? H4)
315 apply (ex_intro ? ? (S n1));
328 apply (ex_intro ? ? a);
330 [ generalize in match H4;
334 apply (ltb_elim (f (S n1)) (f a));
337 generalize in match (lt_S_S ? ? H5);
339 rewrite < S_pred in H6;
340 [ elim (lt_n_m_to_not_lt_m_Sn ? ? H4 H6)
341 | apply (ltn_to_ltO ? ? H4)
352 | rewrite > (pred_Sn n1);
354 generalize in match (H2 (S n1));
356 generalize in match (lt_to_le_to_lt ? ? ? H4 (H5 (le_n ?)));
366 apply (ltb_elim (f (S n1)) (f x1));
369 [ generalize in match (H2 x1);
371 change in match n1 with (pred (S n1));
376 | generalize in match (H2 (S n1) (le_n ?));
378 generalize in match (not_lt_to_le ? ? H4);
380 generalize in match (transitive_le ? ? ? H7 H6);
382 cut (f x1 ≠ f (S n1));
383 [ generalize in match (not_eq_to_le_to_lt ? ? Hcut1 H7);
386 generalize in match (transitive_le ? ? ? H9 H6);
392 generalize in match (H1 ? ? ? ? H9);
395 apply (not_le_Sn_n ? H5)
406 apply (ltb_elim (f (S n1)) (f x1));
408 apply (ltb_elim (f (S n1)) (f y));
412 [ apply (H1 ? ? ? ? Hcut);
415 | apply eq_pred_to_eq;
416 [ apply (ltn_to_ltO ? ? H7)
417 | apply (ltn_to_ltO ? ? H6)
421 | (* pred (f x1) = f y absurd since y ≠ S n1 and thus f y ≠ f (S n1)
422 so that f y < f (S n1) < f x1; hence pred (f x1) = f y is absurd *)
424 [ generalize in match (lt_to_not_eq ? ? Hcut);
426 cut (f y ≠ f (S n1));
427 [ cut (f y < f (S n1));
428 [ rewrite < H8 in Hcut2;
431 generalize in match (le_S_S ? ? Hcut2);
433 generalize in match (transitive_le ? ? ? H10 H7);
435 rewrite < (S_pred (f x1)) in H11;
436 [ elim (not_le_Sn_n ? H11)
437 | fold simplify ((f (S n1)) < (f x1)) in H7;
438 apply (ltn_to_ltO ? ? H7)
440 | apply not_eq_to_le_to_lt;
442 | apply not_lt_to_le;
449 apply (H1 ? ? ? ? H10);
459 | (* f x1 = pred (f y) absurd since it implies S (f x1) = f y and
460 f x1 ≤ f (S n1) < f y = S (f x1) so that f x1 = f (S n1); by
461 injectivity x1 = S n1 that is absurd since x1 ≤ n1 *)
462 generalize in match (eq_f ? ? S ? ? H8);
464 rewrite < S_pred in H9;
465 [ rewrite < H9 in H6;
466 generalize in match (not_lt_to_le ? ? H7);
469 generalize in match (le_S_S ? ? H10);
471 generalize in match (antisym_le ? ? H11 H6);
473 generalize in match (inj_S ? ? H12);
475 generalize in match (H1 ? ? ? ? H13);
478 elim (not_le_Sn_n ? H4)
483 | apply (ltn_to_ltO ? ? H6)
485 | apply (H1 ? ? ? ? H8);
493 theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid:
494 ∀G:finite_enumerable_SemiGroup.
495 left_cancellable ? (op G) →
496 right_cancellable ? (op G) →
497 ∃e:G. isMonoid (mk_PreMonoid G e).
499 letin f ≝ (λn.ι(G \sub O · G \sub n));
500 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
501 [ letin EX ≝ (Hcut O ?);
508 letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
510 rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
511 apply (ex_intro ? ? (G \sub a));
512 letin GOGO ≝ (refl_eq ? (repr ? (is_finite_enumerable G) O));
514 rewrite < HH in GOGO;
515 rewrite < HH in GOGO:(? ? % ?);
516 rewrite > (associative ? G) in GOGO;
517 letin GaGa ≝ (H ? ? ? GOGO);
522 apply (semigroup_properties G)
523 | unfold is_left_unit; intro;
524 letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
526 rewrite < GaGa in GaxGax:(? ? % ?);
527 rewrite > (associative ? (semigroup_properties G)) in GaxGax;
528 apply (H ? ? ? GaxGax)
529 | unfold is_right_unit; intro;
530 letin GaxGax ≝ (refl_eq ? (x·G \sub a));
532 rewrite < GaGa in GaxGax:(? ? % ?);
533 rewrite < (associative ? (semigroup_properties G)) in GaxGax;
534 apply (H1 ? ? ? GaxGax)
538 elim (pigeonhole (order ? G) f ? ? ? H2);
539 [ apply (ex_intro ? ? a);
543 change in H5 with (ι(G \sub O · G \sub x) = ι(G \sub O · G \sub y));
544 cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
545 [ rewrite > (repr_index_of ? ? (G \sub O · G \sub x)) in Hcut;
546 rewrite > (repr_index_of ? ? (G \sub O · G \sub y)) in Hcut;
547 generalize in match (H ? ? ? Hcut);
549 generalize in match (eq_f ? ? (index_of ? G) ? ? H6);
551 rewrite > index_of_repr in H7;
552 rewrite > index_of_repr in H7;