]> matita.cs.unibo.it Git - helm.git/blob - matita/library/algebra/finite_groups.ma
More documentation committed.
[helm.git] / matita / library / algebra / finite_groups.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/algebra/finite_groups/".
16
17 include "algebra/groups.ma".
18
19 record finite_enumerable (T:Type) : Type≝
20  { order: nat;
21    repr: nat → T;
22    index_of: T → nat;
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
26  }.
27  
28 notation "hvbox(C \sub i)" with precedence 89
29 for @{ 'repr $C $i }.
30
31 (* CSC: multiple interpretations in the same file are not considered in the
32  right order
33 interpretation "Finite_enumerable representation" 'repr C i =
34  (cic:/matita/algebra/finite_groups/repr.con C _ i).*)
35  
36 notation < "hvbox(|C|)" with precedence 89
37 for @{ 'card $C }.
38
39 interpretation "Finite_enumerable order" 'card C =
40  (cic:/matita/algebra/finite_groups/order.con C _).
41
42 record finite_enumerable_SemiGroup : Type≝
43  { semigroup:> SemiGroup;
44    is_finite_enumerable:> finite_enumerable semigroup
45  }.
46
47 interpretation "Finite_enumerable representation" 'repr S i =
48  (cic:/matita/algebra/finite_groups/repr.con S
49   (cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i).
50
51 notation "hvbox(ι e)" with precedence 60
52 for @{ 'index_of_finite_enumerable_semigroup $e }.
53
54 interpretation "Index_of_finite_enumerable representation"
55  'index_of_finite_enumerable_semigroup e
56 =
57  (cic:/matita/algebra/finite_groups/index_of.con _
58   (cic:/matita/algebra/finite_groups/is_finite_enumerable.con _) e).
59
60
61 (* several definitions/theorems to be moved somewhere else *)
62
63 definition ltb ≝λn,m. leb n m ∧ notb (eqb n m).
64
65 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
66 intros;
67 elim (le_to_or_lt_eq ? ? H1);
68 [ assumption
69 | elim (H H2)
70 ].
71 qed.
72
73 theorem ltb_to_Prop :
74  ∀n,m.
75   match ltb n m with
76   [ true ⇒ n < m
77   | false ⇒ n ≮ m
78   ].
79 intros;
80 unfold ltb;
81 apply leb_elim;
82 apply eqb_elim;
83 intros;
84 simplify;
85 [ rewrite < H;
86   apply le_to_not_lt;
87   constructor 1
88 | apply (not_eq_to_le_to_lt ? ? H H1)
89 | rewrite < H;
90   apply le_to_not_lt;
91   constructor 1
92 | apply le_to_not_lt;
93   generalize in match (not_le_to_lt ? ? H1);
94   clear H1;
95   intro;
96   apply lt_to_le;
97   assumption
98 ].
99 qed.
100
101 theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
102 (n < m → (P true)) → (n ≮ m → (P false)) →
103 P (ltb n m).
104 intros.
105 cut
106 (match (ltb n m) with
107 [ true  ⇒ n < m
108 | false ⇒ n ≮ m] → (P (ltb n m))).
109 apply Hcut.apply ltb_to_Prop.
110 elim (ltb n m).
111 apply ((H H2)).
112 apply ((H1 H2)).
113 qed.
114
115 theorem Not_lt_n_n: ∀n. n ≮ n.
116 intro;
117 unfold Not;
118 intro;
119 unfold lt in H;
120 apply (not_le_Sn_n ? H).
121 qed.
122
123 theorem eq_pred_to_eq:
124  ∀n,m. O < n → O < m → pred n = pred m → n = m.
125 intros;
126 generalize in match (eq_f ? ? S ? ? H2);
127 intro;
128 rewrite < S_pred in H3;
129 rewrite < S_pred in H3;
130 assumption.
131 qed.
132
133 theorem le_pred_to_le:
134  ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
135 intros 2;
136 elim n;
137 [ apply le_O_n
138 | simplify in H2;
139   rewrite > (S_pred m);
140   [ apply le_S_S;
141     assumption
142   | assumption
143   ]
144 ].
145 qed.
146
147 theorem le_to_le_pred:
148  ∀n,m. n ≤ m → pred n ≤ pred m.
149 intros 2;
150 elim n;
151 [ simplify;
152   apply le_O_n
153 | simplify;
154   generalize in match H1;
155   clear H1;
156   elim m;
157   [ elim (not_le_Sn_O ? H1)
158   | simplify;
159     apply le_S_S_to_le;
160     assumption
161   ]
162 ].
163 qed.
164
165 theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
166 intros;
167 unfold Not;
168 intro;
169 unfold lt in H;
170 unfold lt in H1;
171 generalize in match (le_S_S ? ? H);
172 intro;
173 generalize in match (transitive_le ? ? ? H2 H1);
174 intro;
175 apply (not_le_Sn_n ? H3).
176 qed.
177
178 theorem lt_S_S: ∀n,m. n < m → S n < S m.
179 intros;
180 unfold lt in H;
181 apply (le_S_S ? ? H).
182 qed.
183
184 theorem lt_O_S: ∀n. O < S n.
185 intro;
186 unfold lt;
187 apply le_S_S;
188 apply le_O_n.
189 qed.
190
191 theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
192 intros;
193 unfold lt in H1;
194 generalize in match (le_S_S_to_le ? ? H1);
195 intro;
196 apply cic:/matita/nat/orders/antisym_le.con;
197 assumption.
198 qed.
199
200 theorem pigeonhole:
201  ∀n:nat.∀f:nat→nat.
202   (∀x,y.x≤n → y≤n → f x = f y → x=y) →
203   (∀m. m ≤ n → f m ≤ n) →
204    ∀x. x≤n → ∃y.f y = x ∧ y ≤ n.
205 intro;
206 elim n;
207 [ apply (ex_intro ? ? O);
208   split;
209   [ rewrite < (le_n_O_to_eq ? H2);
210     rewrite < (le_n_O_to_eq ? (H1 O ?));
211     [ reflexivity
212     | apply le_n
213     ]
214   | apply le_n
215   ]
216 | clear n;
217   letin f' ≝
218    (λx.
219     let fSn1 ≝f (S n1) in
220      let fx ≝f x in
221       match ltb fSn1 fx with
222       [ true ⇒ pred fx
223       | false ⇒ fx
224       ]);
225   cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
226   [ cut (∀x. x ≤ n1 → f' x ≤ n1);
227     [ apply (nat_compare_elim (f (S n1)) x);
228       [ intro;
229         elim (H f' ? ? (pred x));
230         [ simplify in H5;
231           clear Hcut;
232           clear Hcut1;
233           clear f';
234           elim H5;
235           clear H5;
236           apply (ex_intro ? ? a);
237           split;
238           [ generalize in match (eq_f ? ? S ? ? H6);
239             clear H6;
240             intro;
241             rewrite < S_pred in H5;
242             [ generalize in match H4;
243               clear H4;
244               rewrite < H5;
245               clear H5;
246               apply (ltb_elim (f (S n1)) (f a));
247               [ simplify;
248                 intros;
249                 rewrite < S_pred;
250                 [ reflexivity
251                 | apply (ltn_to_ltO ? ? H4)
252                 ]
253               | simplify;
254                 intros;
255                 generalize in match (not_lt_to_le ? ? H4);
256                 clear H4;
257                 intro;
258                 generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
259                 intro;
260                 generalize in match (H1 ? ? ? ? H4);
261                 [ intro;
262                   generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
263                   intro;
264                   generalize in match (H1 ? ? ? ? H9);
265                   [ intro;
266                     rewrite > H10 in H7;
267                     elim (not_le_Sn_n ? H7)
268                   | rewrite > H8;
269                     apply le_n
270                   | apply le_n
271                   ]
272                 | apply le_S;
273                   assumption
274                 | apply le_n
275                 ]
276               ]
277             | apply (ltn_to_ltO ? ? H4)
278             ]
279           | apply le_S;
280             assumption
281           ]
282         | apply Hcut
283         | apply Hcut1
284         | apply le_S_S_to_le;
285           rewrite < S_pred;
286           [ assumption
287           | apply (ltn_to_ltO ? ? H4)
288           ]
289         ]    
290       | intros;
291         apply (ex_intro ? ? (S n1));
292         split;
293         [ assumption
294         | constructor 1
295         ] 
296       | intro;
297         elim (H f' ? ? x);
298         [ simplify in H5;
299           clear Hcut;
300           clear Hcut1;
301           clear f';
302           elim H5;
303           clear H5;
304           apply (ex_intro ? ? a);
305           split;
306           [ generalize in match H4;
307             clear H4;
308             rewrite < H6;
309             clear H6;
310             apply (ltb_elim (f (S n1)) (f a));
311             [ simplify;
312               intros;
313               generalize in match (lt_S_S ? ? H5);
314               intro;
315               rewrite < S_pred in H6;
316               [ elim (lt_n_m_to_not_lt_m_Sn ? ? H4 H6)
317               | apply (ltn_to_ltO ? ? H4)
318               ]
319             | simplify;
320               intros;
321               reflexivity
322             ]        
323           | apply le_S;
324             assumption
325           ]
326         | apply Hcut    
327         | apply Hcut1
328         | rewrite > (pred_Sn n1);
329           simplify;
330           generalize in match (H2 (S n1));
331           intro;
332           generalize in match (lt_to_le_to_lt ? ? ? H4 (H5 (le_n ?)));
333           intro;
334           unfold lt in H6;
335           apply le_S_S_to_le;
336           assumption
337         ]
338       ]
339     | unfold f';
340       simplify;
341       intro;
342       apply (ltb_elim (f (S n1)) (f x1));
343       simplify;
344       intros;
345       [ generalize in match (H2 x1);
346         intro;
347         change in match n1 with (pred (S n1));
348         apply le_to_le_pred;
349         apply H6;
350         apply le_S;
351         assumption
352       | generalize in match (H2 (S n1) (le_n ?));
353         intro;
354         generalize in match (not_lt_to_le ? ? H4);
355         intro;
356         generalize in match (transitive_le ? ? ? H7 H6);
357         intro;
358         cut (f x1 ≠ f (S n1));
359         [ generalize in match (not_eq_to_le_to_lt ? ? Hcut1 H7);
360           intro;
361           unfold lt in H9;
362           generalize in match (transitive_le ? ? ? H9 H6);
363           intro;
364           apply le_S_S_to_le;
365           assumption
366         | unfold Not;
367           intro;
368           generalize in match (H1 ? ? ? ? H9);
369           [ intro;
370             rewrite > H10 in H5;
371             apply (not_le_Sn_n ? H5)
372           | apply le_S;
373             assumption
374           | apply le_n
375           ]
376         ] 
377       ]
378     ]
379   | intros 4;
380     unfold f';
381     simplify;
382     apply (ltb_elim (f (S n1)) (f x1));
383     simplify;
384     apply (ltb_elim (f (S n1)) (f y));
385     simplify;
386     intros;
387     [ cut (f x1 = f y);
388       [ apply (H1 ? ? ? ? Hcut);
389         apply le_S;
390         assumption
391       | apply eq_pred_to_eq;
392         [ apply (ltn_to_ltO ? ? H7)
393         | apply (ltn_to_ltO ? ? H6)
394         | assumption
395         ]
396       ]         
397     | (* pred (f x1) = f y absurd since y ≠ S n1 and thus f y ≠ f (S n1)
398          so that f y < f (S n1) < f x1; hence pred (f x1) = f y is absurd *)
399        cut (y < S n1);
400        [ generalize in match (lt_to_not_eq ? ? Hcut);
401          intro;
402          cut (f y ≠ f (S n1));
403          [ cut (f y < f (S n1));
404            [ rewrite < H8 in Hcut2;
405              unfold lt in Hcut2;
406              unfold lt in H7;
407              generalize in match (le_S_S ? ? Hcut2);
408              intro;
409              generalize in match (transitive_le ? ? ? H10 H7);
410              intros;
411              rewrite < (S_pred (f x1)) in H11;
412               [ elim (not_le_Sn_n ? H11)
413               | fold simplify ((f (S n1)) < (f x1)) in H7;
414                 apply (ltn_to_ltO ? ? H7)
415               ]
416            | apply not_eq_to_le_to_lt;
417              [ assumption
418              | apply not_lt_to_le;
419                assumption
420              ]
421            ]
422          | unfold Not;
423            intro;
424            apply H9;
425            apply (H1 ? ? ? ? H10);
426            [ apply lt_to_le;
427              assumption
428            | constructor 1
429            ]
430          ]
431        | unfold lt;
432          apply le_S_S;
433          assumption
434        ]
435     | (* f x1 = pred (f y) absurd since it implies S (f x1) = f y and
436          f x1 ≤ f (S n1) < f y = S (f x1) so that f x1 = f (S n1); by
437          injectivity x1 = S n1 that is absurd since x1 ≤ n1 *)
438        generalize in match (eq_f ? ? S ? ? H8);
439        intro;
440        rewrite < S_pred in H9;
441        [ rewrite < H9 in H6;
442          generalize in match (not_lt_to_le ? ? H7);
443          intro;
444          unfold lt in H6;
445          generalize in match (le_S_S ? ? H10);
446          intro;
447          generalize in match (antisym_le ? ? H11 H6);
448          intro;
449          generalize in match (inj_S ? ? H12);
450          intro;
451          generalize in match (H1 ? ? ? ? H13);
452          [ intro;
453            rewrite > H14 in H4;
454            elim (not_le_Sn_n ? H4)
455          | apply le_S;
456            assumption
457          | apply le_n
458          ]
459        | apply (ltn_to_ltO ? ? H6) 
460        ]
461     | apply (H1 ? ? ? ? H8);
462       apply le_S;
463       assumption
464     ]
465   ]
466 ].
467 qed.
468 (* demo *)
469 theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid:
470  ∀G:finite_enumerable_SemiGroup.
471   left_cancellable ? (op G) →
472   right_cancellable ? (op G) →
473    ∃e:G. isMonoid (mk_PreMonoid G e).
474 intros;
475 letin f ≝(λn.ι(G \sub O · G \sub n));
476 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
477 [ letin EX ≝(Hcut O ?);
478   [ apply le_O_n
479   | clearbody EX;
480     clear Hcut;
481     unfold f in EX;
482     elim EX;
483     clear EX;
484     letin HH ≝(eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
485     clearbody HH;
486     rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
487     apply (ex_intro ? ? (G \sub a));
488     letin GOGO ≝(refl_eq ? (repr ? (is_finite_enumerable G) O));
489     clearbody GOGO;
490     rewrite < HH in GOGO;
491     rewrite < HH in GOGO:(? ? % ?);
492     rewrite > (op_associative ? G) in GOGO;
493     letin GaGa ≝(H ? ? ? GOGO);
494     clearbody GaGa;
495     clear GOGO;
496     constructor 1;
497     [ simplify;
498       apply (semigroup_properties G)
499     | unfold is_left_unit; intro;
500       letin GaxGax ≝(refl_eq ? (G \sub a ·x));
501       clearbody GaxGax; (* demo *)
502       rewrite < GaGa in GaxGax:(? ? % ?);
503       rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
504       apply (H ? ? ? GaxGax)
505     | unfold is_right_unit; intro;
506       letin GaxGax ≝(refl_eq ? (x·G \sub a));
507       clearbody GaxGax;
508       rewrite < GaGa in GaxGax:(? ? % ?);
509       rewrite < (op_associative ? (semigroup_properties G)) in GaxGax;
510       apply (H1 ? ? ? GaxGax)
511     ]
512   ]
513 | intros;
514   elim (pigeonhole (order ? G) f ? ? ? H2);
515   [ apply (ex_intro ? ? a);
516     elim H3;
517     assumption
518   | intros;
519     simplify in H5;
520     cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
521     [ rewrite > (repr_index_of ? ? (G \sub O · G \sub x))  in Hcut;
522       rewrite > (repr_index_of ? ? (G \sub O · G \sub y))  in Hcut;
523       generalize in match (H ? ? ? Hcut);
524       intro;
525       generalize in match (eq_f ? ? (index_of ? G) ? ? H6);
526       intro;
527       rewrite > index_of_repr in H7;
528       rewrite > index_of_repr in H7;
529       assumption
530     | apply eq_f;
531       assumption
532     ]
533   | intros;
534     apply index_of_sur
535   ] 
536 ].
537 qed.