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.