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 notation < "S"
  48 for @{ 'semigroup_of_finite_enumerable_semigroup $S }.
  49
  50 interpretation "Semigroup_of_finite_enumerable_semigroup"
  51  'semigroup_of_finite_enumerable_semigroup S
  52 =
  53  (cic:/matita/algebra/finite_groups/semigroup.con S).
  54
  55 notation < "S"
  56 for @{ 'magma_of_finite_enumerable_semigroup $S }.
  57
  58 interpretation "Magma_of_finite_enumerable_semigroup"
  59  'magma_of_finite_enumerable_semigroup S
  60 =
  61  (cic:/matita/algebra/finite_groups/Magma_of_finite_enumerable_SemiGroup.con S).
  62
  63 notation < "S"
  64 for @{ 'type_of_finite_enumerable_semigroup $S }.
  65
  66 interpretation "Type_of_finite_enumerable_semigroup"
  67  'type_of_finite_enumerable_semigroup S
  68 =
  69  (cic:/matita/algebra/finite_groups/Type_of_finite_enumerable_SemiGroup.con S).
  70
  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).
  74
  75 notation "hvbox(ι e)" with precedence 60
  76 for @{ 'index_of_finite_enumerable_semigroup $e }.
  77
  78 interpretation "Index_of_finite_enumerable representation"
  79  'index_of_finite_enumerable_semigroup e
  80 =
  81  (cic:/matita/algebra/finite_groups/index_of.con _
  82   (cic:/matita/algebra/finite_groups/is_finite_enumerable.con _) e).
  83
  84
  85 (* several definitions/theorems to be moved somewhere else *)
  86
  87 definition ltb ≝ λn,m. leb n m ∧ notb (eqb n m).
  88
  89 theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
  90 intros;
  91 elim (le_to_or_lt_eq ? ? H1);
  92 [ assumption
  93 | elim (H H2)
  94 ].
  95 qed.
  96
  97 theorem ltb_to_Prop :
  98  ∀n,m.
  99   match ltb n m with
 100   [ true ⇒ n < m
 101   | false ⇒ n ≮ m
 102   ].
 103 intros;
 104 unfold ltb;
 105 apply leb_elim;
 106 apply eqb_elim;
 107 intros;
 108 simplify;
 109 [ rewrite < H;
 110   apply le_to_not_lt;
 111   constructor 1
 112 | apply (not_eq_to_le_to_lt ? ? H H1)
 113 | rewrite < H;
 114   apply le_to_not_lt;
 115   constructor 1
 116 | apply le_to_not_lt;
 117   generalize in match (not_le_to_lt ? ? H1);
 118   clear H1;
 119   intro;
 120   apply lt_to_le;
 121   assumption
 122 ].
 123 qed.
 124
 125 theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
 126 (n < m → (P true)) → (n ≮ m → (P false)) →
 127 P (ltb n m).
 128 intros.
 129 cut
 130 (match (ltb n m) with
 131 [ true  ⇒ n < m
 132 | false ⇒ n ≮ m] → (P (ltb n m))).
 133 apply Hcut.apply ltb_to_Prop.
 134 elim (ltb n m).
 135 apply ((H H2)).
 136 apply ((H1 H2)).
 137 qed.
 138
 139 theorem Not_lt_n_n: ∀n. n ≮ n.
 140 intro;
 141 unfold Not;
 142 intro;
 143 unfold lt in H;
 144 apply (not_le_Sn_n ? H).
 145 qed.
 146
 147 theorem eq_pred_to_eq:
 148  ∀n,m. O < n → O < m → pred n = pred m → n = m.
 149 intros;
 150 generalize in match (eq_f ? ? S ? ? H2);
 151 intro;
 152 rewrite < S_pred in H3;
 153 rewrite < S_pred in H3;
 154 assumption.
 155 qed.
 156
 157 theorem le_pred_to_le:
 158  ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
 159 intros 2;
 160 elim n;
 161 [ apply le_O_n
 162 | simplify in H2;
 163   rewrite > (S_pred m);
 164   [ apply le_S_S;
 165     assumption
 166   | assumption
 167   ]
 168 ].
 169 qed.
 170
 171 theorem le_to_le_pred:
 172  ∀n,m. n ≤ m → pred n ≤ pred m.
 173 intros 2;
 174 elim n;
 175 [ simplify;
 176   apply le_O_n
 177 | simplify;
 178   generalize in match H1;
 179   clear H1;
 180   elim m;
 181   [ elim (not_le_Sn_O ? H1)
 182   | simplify;
 183     apply le_S_S_to_le;
 184     assumption
 185   ]
 186 ].
 187 qed.
 188
 189 theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
 190 intros;
 191 unfold Not;
 192 intro;
 193 unfold lt in H;
 194 unfold lt in H1;
 195 generalize in match (le_S_S ? ? H);
 196 intro;
 197 generalize in match (transitive_le ? ? ? H2 H1);
 198 intro;
 199 apply (not_le_Sn_n ? H3).
 200 qed.
 201
 202 theorem lt_S_S: ∀n,m. n < m → S n < S m.
 203 intros;
 204 unfold lt in H;
 205 apply (le_S_S ? ? H).
 206 qed.
 207
 208 theorem lt_O_S: ∀n. O < S n.
 209 intro;
 210 unfold lt;
 211 apply le_S_S;
 212 apply le_O_n.
 213 qed.
 214
 215 theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
 216 intros;
 217 unfold lt in H1;
 218 generalize in match (le_S_S_to_le ? ? H1);
 219 intro;
 220 apply cic:/matita/nat/orders/antisym_le.con;
 221 assumption.
 222 qed.
 223
 224 theorem pigeonhole:
 225  ∀n:nat.∀f:nat→nat.
 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.
 229 intro;
 230 elim n;
 231 [ apply (ex_intro ? ? O);
 232   split;
 233   [ rewrite < (le_n_O_to_eq ? H2);
 234     rewrite < (le_n_O_to_eq ? (H1 O ?));
 235     [ reflexivity
 236     | apply le_n
 237     ]
 238   | apply le_n
 239   ]
 240 | clear n;
 241   letin f' ≝
 242    (λx.
 243     let fSn1 ≝ f (S n1) in
 244      let fx ≝ f x in
 245       match ltb fSn1 fx with
 246       [ true ⇒ pred fx
 247       | false ⇒ fx
 248       ]);
 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);
 252       [ intro;
 253         elim (H f' ? ? (pred x));
 254         [ simplify in H5;
 255           clear Hcut;
 256           clear Hcut1;
 257           clear f';
 258           elim H5;
 259           clear H5;
 260           apply (ex_intro ? ? a);
 261           split;
 262           [ generalize in match (eq_f ? ? S ? ? H6);
 263             clear H6;
 264             intro;
 265             rewrite < S_pred in H5;
 266             [ generalize in match H4;
 267               clear H4;
 268               rewrite < H5;
 269               clear H5;
 270               apply (ltb_elim (f (S n1)) (f a));
 271               [ simplify;
 272                 intros;
 273                 rewrite < S_pred;
 274                 [ reflexivity
 275                 | apply (ltn_to_ltO ? ? H4)
 276                 ]
 277               | simplify;
 278                 intros;
 279                 generalize in match (not_lt_to_le ? ? H4);
 280                 clear H4;
 281                 intro;
 282                 generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
 283                 intro;
 284                 generalize in match (H1 ? ? ? ? H4);
 285                 [ intro;
 286                   generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
 287                   intro;
 288                   generalize in match (H1 ? ? ? ? H9);
 289                   [ intro;
 290                     rewrite > H10 in H7;
 291                     elim (not_le_Sn_n ? H7)
 292                   | rewrite > H8;
 293                     apply le_n
 294                   | apply le_n
 295                   ]
 296                 | apply le_S;
 297                   assumption
 298                 | apply le_n
 299                 ]
 300               ]
 301             | apply (ltn_to_ltO ? ? H4)
 302             ]
 303           | apply le_S;
 304             assumption
 305           ]
 306         | apply Hcut
 307         | apply Hcut1
 308         | apply le_S_S_to_le;
 309           rewrite < S_pred;
 310           [ assumption
 311           | apply (ltn_to_ltO ? ? H4)
 312           ]
 313         ]
 314       | intros;
 315         apply (ex_intro ? ? (S n1));
 316         split;
 317         [ assumption
 318         | constructor 1
 319         ]
 320       | intro;
 321         elim (H f' ? ? x);
 322         [ simplify in H5;
 323           clear Hcut;
 324           clear Hcut1;
 325           clear f';
 326           elim H5;
 327           clear H5;
 328           apply (ex_intro ? ? a);
 329           split;
 330           [ generalize in match H4;
 331             clear H4;
 332             rewrite < H6;
 333             clear H6;
 334             apply (ltb_elim (f (S n1)) (f a));
 335             [ simplify;
 336               intros;
 337               generalize in match (lt_S_S ? ? H5);
 338               intro;
 339               rewrite < S_pred in H6;
 340               [ elim (lt_n_m_to_not_lt_m_Sn ? ? H4 H6)
 341               | apply (ltn_to_ltO ? ? H4)
 342               ]
 343             | simplify;
 344               intros;
 345               reflexivity
 346             ]
 347           | apply le_S;
 348             assumption
 349           ]
 350         | apply Hcut
 351         | apply Hcut1
 352         | rewrite > (pred_Sn n1);
 353           simplify;
 354           generalize in match (H2 (S n1));
 355           intro;
 356           generalize in match (lt_to_le_to_lt ? ? ? H4 (H5 (le_n ?)));
 357           intro;
 358           unfold lt in H6;
 359           apply le_S_S_to_le;
 360           assumption
 361         ]
 362       ]
 363     | unfold f';
 364       simplify;
 365       intro;
 366       apply (ltb_elim (f (S n1)) (f x1));
 367       simplify;
 368       intros;
 369       [ generalize in match (H2 x1);
 370         intro;
 371         change in match n1 with (pred (S n1));
 372         apply le_to_le_pred;
 373         apply H6;
 374         apply le_S;
 375         assumption
 376       | generalize in match (H2 (S n1) (le_n ?));
 377         intro;
 378         generalize in match (not_lt_to_le ? ? H4);
 379         intro;
 380         generalize in match (transitive_le ? ? ? H7 H6);
 381         intro;
 382         cut (f x1 ≠ f (S n1));
 383         [ generalize in match (not_eq_to_le_to_lt ? ? Hcut1 H7);
 384           intro;
 385           unfold lt in H9;
 386           generalize in match (transitive_le ? ? ? H9 H6);
 387           intro;
 388           apply le_S_S_to_le;
 389           assumption
 390         | unfold Not;
 391           intro;
 392           generalize in match (H1 ? ? ? ? H9);
 393           [ intro;
 394             rewrite > H10 in H5;
 395             apply (not_le_Sn_n ? H5)
 396           | apply le_S;
 397             assumption
 398           | apply le_n
 399           ]
 400         ]
 401       ]
 402     ]
 403   | intros 4;
 404     unfold f';
 405     simplify;
 406     apply (ltb_elim (f (S n1)) (f x1));
 407     simplify;
 408     apply (ltb_elim (f (S n1)) (f y));
 409     simplify;
 410     intros;
 411     [ cut (f x1 = f y);
 412       [ apply (H1 ? ? ? ? Hcut);
 413         apply le_S;
 414         assumption
 415       | apply eq_pred_to_eq;
 416         [ apply (ltn_to_ltO ? ? H7)
 417         | apply (ltn_to_ltO ? ? H6)
 418         | assumption
 419         ]
 420       ]
 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 *)
 423        cut (y < S n1);
 424        [ generalize in match (lt_to_not_eq ? ? Hcut);
 425          intro;
 426          cut (f y ≠ f (S n1));
 427          [ cut (f y < f (S n1));
 428            [ rewrite < H8 in Hcut2;
 429              unfold lt in Hcut2;
 430              unfold lt in H7;
 431              generalize in match (le_S_S ? ? Hcut2);
 432              intro;
 433              generalize in match (transitive_le ? ? ? H10 H7);
 434              intros;
 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)
 439               ]
 440            | apply not_eq_to_le_to_lt;
 441              [ assumption
 442              | apply not_lt_to_le;
 443                assumption
 444              ]
 445            ]
 446          | unfold Not;
 447            intro;
 448            apply H9;
 449            apply (H1 ? ? ? ? H10);
 450            [ apply lt_to_le;
 451              assumption
 452            | constructor 1
 453            ]
 454          ]
 455        | unfold lt;
 456          apply le_S_S;
 457          assumption
 458        ]
 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);
 463        intro;
 464        rewrite < S_pred in H9;
 465        [ rewrite < H9 in H6;
 466          generalize in match (not_lt_to_le ? ? H7);
 467          intro;
 468          unfold lt in H6;
 469          generalize in match (le_S_S ? ? H10);
 470          intro;
 471          generalize in match (antisym_le ? ? H11 H6);
 472          intro;
 473          generalize in match (inj_S ? ? H12);
 474          intro;
 475          generalize in match (H1 ? ? ? ? H13);
 476          [ intro;
 477            rewrite > H14 in H4;
 478            elim (not_le_Sn_n ? H4)
 479          | apply le_S;
 480            assumption
 481          | apply le_n
 482          ]
 483        | apply (ltn_to_ltO ? ? H6)
 484        ]
 485     | apply (H1 ? ? ? ? H8);
 486       apply le_S;
 487       assumption
 488     ]
 489   ]
 490 ].
 491 qed.
 492
 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).
 498 intros;
 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 ?);
 502   [ apply le_O_n
 503   | clearbody EX;
 504     clear Hcut;
 505     unfold f in EX;
 506     elim EX;
 507     clear EX;
 508     letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
 509     clearbody HH;
 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));
 513     clearbody GOGO;
 514     rewrite < HH in GOGO;
 515     rewrite < HH in GOGO:(? ? % ?);
 516     rewrite > (associative ? G) in GOGO;
 517     letin GaGa ≝ (H ? ? ? GOGO);
 518     clearbody GaGa;
 519     clear GOGO;
 520     constructor 1;
 521     [ simplify;
 522       apply (semigroup_properties G)
 523     | unfold is_left_unit; intro;
 524       letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
 525       clearbody GaxGax;
 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));
 531       clearbody GaxGax;
 532       rewrite < GaGa in GaxGax:(? ? % ?);
 533       rewrite < (associative ? (semigroup_properties G)) in GaxGax;
 534       apply (H1 ? ? ? GaxGax)
 535     ]
 536   ]
 537 | intros;
 538   elim (pigeonhole (order ? G) f ? ? ? H2);
 539   [ apply (ex_intro ? ? a);
 540     elim H3;
 541     assumption
 542   | intros;
 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);
 548       intro;
 549       generalize in match (eq_f ? ? (index_of ? G) ? ? H6);
 550       intro;
 551       rewrite > index_of_repr in H7;
 552       rewrite > index_of_repr in H7;
 553       assumption
 554     | apply eq_f;
 555       assumption
 556     ]
 557   | intros;
 558     apply index_of_sur
 559   ]
 560 ].
 561 qed.