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 include "algebra/groups.ma".
17 record finite_enumerable (T:Type) : Type≝
21 index_of_sur: ∀x.index_of x ≤ order;
22 index_of_repr: ∀n. n≤order → index_of (repr n) = n;
23 repr_index_of: ∀x. repr (index_of x) = x
26 notation "hvbox(C \sub i)" with precedence 89
29 (* CSC: multiple interpretations in the same file are not considered in the
31 interpretation "Finite_enumerable representation" 'repr C i =
32 (cic:/matita/algebra/finite_groups/repr.con C _ i).*)
34 interpretation "Finite_enumerable order" 'card C =
35 (cic:/matita/algebra/finite_groups/order.con C _).
37 record finite_enumerable_SemiGroup : Type≝
38 { semigroup:> SemiGroup;
39 is_finite_enumerable:> finite_enumerable semigroup
42 interpretation "Finite_enumerable representation" 'repr S i =
43 (cic:/matita/algebra/finite_groups/repr.con S
44 (cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i).
46 notation "hvbox(\iota e)" with precedence 60
47 for @{ 'index_of_finite_enumerable_semigroup $e }.
49 interpretation "Index_of_finite_enumerable representation"
50 'index_of_finite_enumerable_semigroup e
52 (cic:/matita/algebra/finite_groups/index_of.con _
53 (cic:/matita/algebra/finite_groups/is_finite_enumerable.con _) e).
56 (* several definitions/theorems to be moved somewhere else *)
60 (∀x,y.x≤n → y≤n → f x = f y → x=y) →
61 (∀m. m ≤ n → f m ≤ n) →
62 ∀x. x≤n → ∃y.f y = x ∧ y ≤ n.
65 [ apply (ex_intro ? ? O);
67 [ rewrite < (le_n_O_to_eq ? H2);
68 rewrite < (le_n_O_to_eq ? (H1 O ?));
79 match ltb fSn1 fx with
83 cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
84 [ cut (∀x. x ≤ n1 → f' x ≤ n1);
85 [ apply (nat_compare_elim (f (S n1)) x);
87 elim (H f' ? ? (pred x));
95 apply (ex_intro ? ? a);
97 [ generalize in match (eq_f ? ? S ? ? H6);
100 rewrite < S_pred in H5;
101 [ generalize in match H4;
105 apply (ltb_elim (f (S n1)) (f a));
110 | apply (ltn_to_ltO ? ? H4)
114 generalize in match (not_lt_to_le ? ? H4);
117 generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
119 generalize in match (H1 ? ? ? ? H4);
121 generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
123 generalize in match (H1 ? ? ? ? H9);
126 elim (not_le_Sn_n ? H7)
136 | apply (ltn_to_ltO ? ? H4)
143 | apply le_S_S_to_le;
146 | apply (ltn_to_ltO ? ? H4)
150 apply (ex_intro ? ? (S n1));
164 apply (ex_intro ? ? a);
166 [ generalize in match H4;
170 apply (ltb_elim (f (S n1)) (f a));
173 generalize in match (lt_to_lt_S_S ? ? H5);
175 rewrite < S_pred in H6;
176 [ elim (lt_n_m_to_not_lt_m_Sn ? ? H4 H6)
177 | apply (ltn_to_ltO ? ? H4)
188 | rewrite > (pred_Sn n1);
190 generalize in match (H2 (S n1));
192 generalize in match (lt_to_le_to_lt ? ? ? H4 (H5 (le_n ?)));
202 apply (ltb_elim (f (S n1)) (f x1));
205 [ generalize in match (H2 x1);
207 change in match n1 with (pred (S n1));
212 | generalize in match (H2 (S n1) (le_n ?));
214 generalize in match (not_lt_to_le ? ? H4);
216 generalize in match (transitive_le ? ? ? H7 H6);
218 cut (f x1 ≠ f (S n1));
219 [ generalize in match (not_eq_to_le_to_lt ? ? Hcut1 H7);
222 generalize in match (transitive_le ? ? ? H9 H6);
228 generalize in match (H1 ? ? ? ? H9);
231 apply (not_le_Sn_n ? H5)
242 apply (ltb_elim (f (S n1)) (f x1));
244 apply (ltb_elim (f (S n1)) (f y));
248 [ apply (H1 ? ? ? ? Hcut);
251 | alias id "eq_pred_to_eq" = "cic:/matita/nat/relevant_equations/eq_pred_to_eq.con".
253 [ apply (ltn_to_ltO ? ? H7)
254 | apply (ltn_to_ltO ? ? H6)
258 | (* pred (f x1) = f y absurd since y ≠ S n1 and thus f y ≠ f (S n1)
259 so that f y < f (S n1) < f x1; hence pred (f x1) = f y is absurd *)
261 [ generalize in match (lt_to_not_eq ? ? Hcut);
263 cut (f y ≠ f (S n1));
264 [ cut (f y < f (S n1));
265 [ rewrite < H8 in Hcut2;
268 generalize in match (le_S_S ? ? Hcut2);
270 generalize in match (transitive_le ? ? ? H10 H7);
272 rewrite < (S_pred (f x1)) in H11;
273 [ elim (not_le_Sn_n ? H11)
274 | fold simplify ((f (S n1)) < (f x1)) in H7;
275 apply (ltn_to_ltO ? ? H7)
277 | apply not_eq_to_le_to_lt;
279 | apply not_lt_to_le;
286 apply (H1 ? ? ? ? H10);
296 | (* f x1 = pred (f y) absurd since it implies S (f x1) = f y and
297 f x1 ≤ f (S n1) < f y = S (f x1) so that f x1 = f (S n1); by
298 injectivity x1 = S n1 that is absurd since x1 ≤ n1 *)
299 generalize in match (eq_f ? ? S ? ? H8);
301 rewrite < S_pred in H9;
302 [ rewrite < H9 in H6;
303 generalize in match (not_lt_to_le ? ? H7);
306 generalize in match (le_S_S ? ? H10);
308 generalize in match (antisym_le ? ? H11 H6);
310 generalize in match (inj_S ? ? H12);
312 generalize in match (H1 ? ? ? ? H13);
315 elim (not_le_Sn_n ? H4)
320 | apply (ltn_to_ltO ? ? H6)
322 | apply (H1 ? ? ? ? H8);
330 theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid:
331 ∀G:finite_enumerable_SemiGroup.
332 left_cancellable ? (op G) →
333 right_cancellable ? (op G) →
334 ∃e:G. isMonoid (mk_PreMonoid G e).
336 letin f ≝(λn.ι(G \sub O · G \sub n));
337 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
338 [ letin EX ≝(Hcut O ?);
345 letin HH ≝(eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
347 rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
348 apply (ex_intro ? ? (G \sub a));
349 letin GOGO ≝(refl_eq ? (repr ? (is_finite_enumerable G) O));
351 rewrite < HH in GOGO;
352 rewrite < HH in GOGO:(? ? % ?);
353 rewrite > (op_associative ? G) in GOGO;
354 letin GaGa ≝(H ? ? ? GOGO);
359 apply (semigroup_properties G)
360 | unfold is_left_unit; intro;
361 letin GaxGax ≝(refl_eq ? (G \sub a ·x));
362 clearbody GaxGax; (* demo *)
363 rewrite < GaGa in GaxGax:(? ? % ?);
364 rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
365 apply (H ? ? ? GaxGax)
366 | unfold is_right_unit; intro;
367 letin GaxGax ≝(refl_eq ? (x·G \sub a));
369 rewrite < GaGa in GaxGax:(? ? % ?);
370 rewrite < (op_associative ? (semigroup_properties G)) in GaxGax;
371 apply (H1 ? ? ? GaxGax)
375 elim (pigeonhole (order ? G) f ? ? ? H2);
376 [ apply (ex_intro ? ? a);
381 cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
382 [ rewrite > (repr_index_of ? ? (G \sub O · G \sub x)) in Hcut;
383 rewrite > (repr_index_of ? ? (G \sub O · G \sub y)) in Hcut;
384 generalize in match (H ? ? ? Hcut);
386 generalize in match (eq_f ? ? (index_of ? G) ? ? H6);
388 rewrite > index_of_repr in H7;
389 rewrite > index_of_repr in H7;