]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/algebra/finite_groups.ma
Scripts fixed because of:
[helm.git] / helm / software / 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 theorem pigeonhole:
64  ∀n:nat.∀f:nat→nat.
65   (∀x,y.x≤n → y≤n → f x = f y → x=y) →
66   (∀m. m ≤ n → f m ≤ n) →
67    ∀x. x≤n → ∃y.f y = x ∧ y ≤ n.
68 intro;
69 elim n;
70 [ apply (ex_intro ? ? O);
71   split;
72   [ rewrite < (le_n_O_to_eq ? H2);
73     rewrite < (le_n_O_to_eq ? (H1 O ?));
74     [ reflexivity
75     | apply le_n
76     ]
77   | apply le_n
78   ]
79 | clear n;
80   letin f' ≝
81    (λx.
82     let fSn1 ≝f (S n1) in
83      let fx ≝f x in
84       match ltb fSn1 fx with
85       [ true ⇒ pred fx
86       | false ⇒ fx
87       ]);
88   cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
89   [ cut (∀x. x ≤ n1 → f' x ≤ n1);
90     [ apply (nat_compare_elim (f (S n1)) x);
91       [ intro;
92         elim (H f' ? ? (pred x));
93         [ simplify in H5;
94           clear Hcut;
95           clear Hcut1;
96           unfold f' in H5;
97           clear f';
98           elim H5;
99           clear H5;
100           apply (ex_intro ? ? a);
101           split;
102           [ generalize in match (eq_f ? ? S ? ? H6);
103             clear H6;
104             intro;
105             rewrite < S_pred in H5;
106             [ generalize in match H4;
107               clear H4;
108               rewrite < H5;
109               clear H5;
110               apply (ltb_elim (f (S n1)) (f a));
111               [ simplify;
112                 intros;
113                 rewrite < S_pred;
114                 [ reflexivity
115                 | apply (ltn_to_ltO ? ? H4)
116                 ]
117               | simplify;
118                 intros;
119                 generalize in match (not_lt_to_le ? ? H4);
120                 clear H4;
121                 intro;
122                 generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
123                 intro;
124                 generalize in match (H1 ? ? ? ? H4);
125                 [ intro;
126                   generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
127                   intro;
128                   generalize in match (H1 ? ? ? ? H9);
129                   [ intro;
130                     rewrite > H10 in H7;
131                     elim (not_le_Sn_n ? H7)
132                   | rewrite > H8;
133                     apply le_n
134                   | apply le_n
135                   ]
136                 | apply le_S;
137                   assumption
138                 | apply le_n
139                 ]
140               ]
141             | apply (ltn_to_ltO ? ? H4)
142             ]
143           | apply le_S;
144             assumption
145           ]
146         | apply Hcut
147         | apply Hcut1
148         | apply le_S_S_to_le;
149           rewrite < S_pred;
150           [ assumption
151           | apply (ltn_to_ltO ? ? H4)
152           ]
153         ]    
154       | intros;
155         apply (ex_intro ? ? (S n1));
156         split;
157         [ assumption
158         | constructor 1
159         ] 
160       | intro;
161         elim (H f' ? ? x);
162         [ simplify in H5;
163           clear Hcut;
164           clear Hcut1;
165           unfold f' in H5;
166           clear f';
167           elim H5;
168           clear H5;
169           apply (ex_intro ? ? a);
170           split;
171           [ generalize in match H4;
172             clear H4;
173             rewrite < H6;
174             clear H6;
175             apply (ltb_elim (f (S n1)) (f a));
176             [ simplify;
177               intros;
178               generalize in match (lt_to_lt_S_S ? ? H5);
179               intro;
180               rewrite < S_pred in H6;
181               [ elim (lt_n_m_to_not_lt_m_Sn ? ? H4 H6)
182               | apply (ltn_to_ltO ? ? H4)
183               ]
184             | simplify;
185               intros;
186               reflexivity
187             ]        
188           | apply le_S;
189             assumption
190           ]
191         | apply Hcut    
192         | apply Hcut1
193         | rewrite > (pred_Sn n1);
194           simplify;
195           generalize in match (H2 (S n1));
196           intro;
197           generalize in match (lt_to_le_to_lt ? ? ? H4 (H5 (le_n ?)));
198           intro;
199           unfold lt in H6;
200           apply le_S_S_to_le;
201           assumption
202         ]
203       ]
204     | unfold f';
205       simplify;
206       intro;
207       apply (ltb_elim (f (S n1)) (f x1));
208       simplify;
209       intros;
210       [ generalize in match (H2 x1);
211         intro;
212         change in match n1 with (pred (S n1));
213         apply le_to_le_pred;
214         apply H6;
215         apply le_S;
216         assumption
217       | generalize in match (H2 (S n1) (le_n ?));
218         intro;
219         generalize in match (not_lt_to_le ? ? H4);
220         intro;
221         generalize in match (transitive_le ? ? ? H7 H6);
222         intro;
223         cut (f x1 ≠ f (S n1));
224         [ generalize in match (not_eq_to_le_to_lt ? ? Hcut1 H7);
225           intro;
226           unfold lt in H9;
227           generalize in match (transitive_le ? ? ? H9 H6);
228           intro;
229           apply le_S_S_to_le;
230           assumption
231         | unfold Not;
232           intro;
233           generalize in match (H1 ? ? ? ? H9);
234           [ intro;
235             rewrite > H10 in H5;
236             apply (not_le_Sn_n ? H5)
237           | apply le_S;
238             assumption
239           | apply le_n
240           ]
241         ] 
242       ]
243     ]
244   | intros 4;
245     unfold f';
246     simplify;
247     apply (ltb_elim (f (S n1)) (f x1));
248     simplify;
249     apply (ltb_elim (f (S n1)) (f y));
250     simplify;
251     intros;
252     [ cut (f x1 = f y);
253       [ apply (H1 ? ? ? ? Hcut);
254         apply le_S;
255         assumption
256       | alias id "eq_pred_to_eq" = "cic:/matita/nat/relevant_equations/eq_pred_to_eq.con".
257 apply eq_pred_to_eq;
258         [ apply (ltn_to_ltO ? ? H7)
259         | apply (ltn_to_ltO ? ? H6)
260         | assumption
261         ]
262       ]         
263     | (* pred (f x1) = f y absurd since y ≠ S n1 and thus f y ≠ f (S n1)
264          so that f y < f (S n1) < f x1; hence pred (f x1) = f y is absurd *)
265        cut (y < S n1);
266        [ generalize in match (lt_to_not_eq ? ? Hcut);
267          intro;
268          cut (f y ≠ f (S n1));
269          [ cut (f y < f (S n1));
270            [ rewrite < H8 in Hcut2;
271              unfold lt in Hcut2;
272              unfold lt in H7;
273              generalize in match (le_S_S ? ? Hcut2);
274              intro;
275              generalize in match (transitive_le ? ? ? H10 H7);
276              intros;
277              rewrite < (S_pred (f x1)) in H11;
278               [ elim (not_le_Sn_n ? H11)
279               | fold simplify ((f (S n1)) < (f x1)) in H7;
280                 apply (ltn_to_ltO ? ? H7)
281               ]
282            | apply not_eq_to_le_to_lt;
283              [ assumption
284              | apply not_lt_to_le;
285                assumption
286              ]
287            ]
288          | unfold Not;
289            intro;
290            apply H9;
291            apply (H1 ? ? ? ? H10);
292            [ apply lt_to_le;
293              assumption
294            | constructor 1
295            ]
296          ]
297        | unfold lt;
298          apply le_S_S;
299          assumption
300        ]
301     | (* f x1 = pred (f y) absurd since it implies S (f x1) = f y and
302          f x1 ≤ f (S n1) < f y = S (f x1) so that f x1 = f (S n1); by
303          injectivity x1 = S n1 that is absurd since x1 ≤ n1 *)
304        generalize in match (eq_f ? ? S ? ? H8);
305        intro;
306        rewrite < S_pred in H9;
307        [ rewrite < H9 in H6;
308          generalize in match (not_lt_to_le ? ? H7);
309          intro;
310          unfold lt in H6;
311          generalize in match (le_S_S ? ? H10);
312          intro;
313          generalize in match (antisym_le ? ? H11 H6);
314          intro;
315          generalize in match (inj_S ? ? H12);
316          intro;
317          generalize in match (H1 ? ? ? ? H13);
318          [ intro;
319            rewrite > H14 in H4;
320            elim (not_le_Sn_n ? H4)
321          | apply le_S;
322            assumption
323          | apply le_n
324          ]
325        | apply (ltn_to_ltO ? ? H6) 
326        ]
327     | apply (H1 ? ? ? ? H8);
328       apply le_S;
329       assumption
330     ]
331   ]
332 ].
333 qed.
334 (* demo *)
335 theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid:
336  ∀G:finite_enumerable_SemiGroup.
337   left_cancellable ? (op G) →
338   right_cancellable ? (op G) →
339    ∃e:G. isMonoid (mk_PreMonoid G e).
340 intros;
341 letin f ≝(λn.ι(G \sub O · G \sub n));
342 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
343 [ letin EX ≝(Hcut O ?);
344   [ apply le_O_n
345   | clearbody EX;
346     clear Hcut;
347     unfold f in EX;
348     elim EX;
349     clear EX;
350     letin HH ≝(eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
351     clearbody HH;
352     rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
353     apply (ex_intro ? ? (G \sub a));
354     letin GOGO ≝(refl_eq ? (repr ? (is_finite_enumerable G) O));
355     clearbody GOGO;
356     rewrite < HH in GOGO;
357     rewrite < HH in GOGO:(? ? % ?);
358     rewrite > (op_associative ? G) in GOGO;
359     letin GaGa ≝(H ? ? ? GOGO);
360     clearbody GaGa;
361     clear GOGO;
362     constructor 1;
363     [ simplify;
364       apply (semigroup_properties G)
365     | unfold is_left_unit; intro;
366       letin GaxGax ≝(refl_eq ? (G \sub a ·x));
367       clearbody GaxGax; (* demo *)
368       rewrite < GaGa in GaxGax:(? ? % ?);
369       rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
370       apply (H ? ? ? GaxGax)
371     | unfold is_right_unit; intro;
372       letin GaxGax ≝(refl_eq ? (x·G \sub a));
373       clearbody GaxGax;
374       rewrite < GaGa in GaxGax:(? ? % ?);
375       rewrite < (op_associative ? (semigroup_properties G)) in GaxGax;
376       apply (H1 ? ? ? GaxGax)
377     ]
378   ]
379 | intros;
380   elim (pigeonhole (order ? G) f ? ? ? H2);
381   [ apply (ex_intro ? ? a);
382     elim H3;
383     assumption
384   | intros;
385     simplify in H5;
386     cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
387     [ rewrite > (repr_index_of ? ? (G \sub O · G \sub x))  in Hcut;
388       rewrite > (repr_index_of ? ? (G \sub O · G \sub y))  in Hcut;
389       generalize in match (H ? ? ? Hcut);
390       intro;
391       generalize in match (eq_f ? ? (index_of ? G) ? ? H6);
392       intro;
393       rewrite > index_of_repr in H7;
394       rewrite > index_of_repr in H7;
395       assumption
396     | apply eq_f;
397       assumption
398     ]
399   | intros;
400     unfold f;
401     apply index_of_sur
402   ] 
403 ].
404 qed.