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 (* moved to nat/order.ma
 185 theorem lt_O_S: ∀n. O < S n.
 186 intro;
 187 unfold lt;
 188 apply le_S_S;
 189 apply le_O_n.
 190 qed. *)
 191
 192 theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
 193 intros;
 194 unfold lt in H1;
 195 generalize in match (le_S_S_to_le ? ? H1);
 196 intro;
 197 apply cic:/matita/nat/orders/antisym_le.con;
 198 assumption.
 199 qed.
 200
 201 theorem pigeonhole:
 202  ∀n:nat.∀f:nat→nat.
 203   (∀x,y.x≤n → y≤n → f x = f y → x=y) →
 204   (∀m. m ≤ n → f m ≤ n) →
 205    ∀x. x≤n → ∃y.f y = x ∧ y ≤ n.
 206 intro;
 207 elim n;
 208 [ apply (ex_intro ? ? O);
 209   split;
 210   [ rewrite < (le_n_O_to_eq ? H2);
 211     rewrite < (le_n_O_to_eq ? (H1 O ?));
 212     [ reflexivity
 213     | apply le_n
 214     ]
 215   | apply le_n
 216   ]
 217 | clear n;
 218   letin f' ≝
 219    (λx.
 220     let fSn1 ≝f (S n1) in
 221      let fx ≝f x in
 222       match ltb fSn1 fx with
 223       [ true ⇒ pred fx
 224       | false ⇒ fx
 225       ]);
 226   cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
 227   [ cut (∀x. x ≤ n1 → f' x ≤ n1);
 228     [ apply (nat_compare_elim (f (S n1)) x);
 229       [ intro;
 230         elim (H f' ? ? (pred x));
 231         [ simplify in H5;
 232           clear Hcut;
 233           clear Hcut1;
 234           clear f';
 235           elim H5;
 236           clear H5;
 237           apply (ex_intro ? ? a);
 238           split;
 239           [ generalize in match (eq_f ? ? S ? ? H6);
 240             clear H6;
 241             intro;
 242             rewrite < S_pred in H5;
 243             [ generalize in match H4;
 244               clear H4;
 245               rewrite < H5;
 246               clear H5;
 247               apply (ltb_elim (f (S n1)) (f a));
 248               [ simplify;
 249                 intros;
 250                 rewrite < S_pred;
 251                 [ reflexivity
 252                 | apply (ltn_to_ltO ? ? H4)
 253                 ]
 254               | simplify;
 255                 intros;
 256                 generalize in match (not_lt_to_le ? ? H4);
 257                 clear H4;
 258                 intro;
 259                 generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
 260                 intro;
 261                 generalize in match (H1 ? ? ? ? H4);
 262                 [ intro;
 263                   generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
 264                   intro;
 265                   generalize in match (H1 ? ? ? ? H9);
 266                   [ intro;
 267                     rewrite > H10 in H7;
 268                     elim (not_le_Sn_n ? H7)
 269                   | rewrite > H8;
 270                     apply le_n
 271                   | apply le_n
 272                   ]
 273                 | apply le_S;
 274                   assumption
 275                 | apply le_n
 276                 ]
 277               ]
 278             | apply (ltn_to_ltO ? ? H4)
 279             ]
 280           | apply le_S;
 281             assumption
 282           ]
 283         | apply Hcut
 284         | apply Hcut1
 285         | apply le_S_S_to_le;
 286           rewrite < S_pred;
 287           [ assumption
 288           | apply (ltn_to_ltO ? ? H4)
 289           ]
 290         ]
 291       | intros;
 292         apply (ex_intro ? ? (S n1));
 293         split;
 294         [ assumption
 295         | constructor 1
 296         ]
 297       | intro;
 298         elim (H f' ? ? x);
 299         [ simplify in H5;
 300           clear Hcut;
 301           clear Hcut1;
 302           clear f';
 303           elim H5;
 304           clear H5;
 305           apply (ex_intro ? ? a);
 306           split;
 307           [ generalize in match H4;
 308             clear H4;
 309             rewrite < H6;
 310             clear H6;
 311             apply (ltb_elim (f (S n1)) (f a));
 312             [ simplify;
 313               intros;
 314               generalize in match (lt_S_S ? ? H5);
 315               intro;
 316               rewrite < S_pred in H6;
 317               [ elim (lt_n_m_to_not_lt_m_Sn ? ? H4 H6)
 318               | apply (ltn_to_ltO ? ? H4)
 319               ]
 320             | simplify;
 321               intros;
 322               reflexivity
 323             ]
 324           | apply le_S;
 325             assumption
 326           ]
 327         | apply Hcut
 328         | apply Hcut1
 329         | rewrite > (pred_Sn n1);
 330           simplify;
 331           generalize in match (H2 (S n1));
 332           intro;
 333           generalize in match (lt_to_le_to_lt ? ? ? H4 (H5 (le_n ?)));
 334           intro;
 335           unfold lt in H6;
 336           apply le_S_S_to_le;
 337           assumption
 338         ]
 339       ]
 340     | unfold f';
 341       simplify;
 342       intro;
 343       apply (ltb_elim (f (S n1)) (f x1));
 344       simplify;
 345       intros;
 346       [ generalize in match (H2 x1);
 347         intro;
 348         change in match n1 with (pred (S n1));
 349         apply le_to_le_pred;
 350         apply H6;
 351         apply le_S;
 352         assumption
 353       | generalize in match (H2 (S n1) (le_n ?));
 354         intro;
 355         generalize in match (not_lt_to_le ? ? H4);
 356         intro;
 357         generalize in match (transitive_le ? ? ? H7 H6);
 358         intro;
 359         cut (f x1 ≠ f (S n1));
 360         [ generalize in match (not_eq_to_le_to_lt ? ? Hcut1 H7);
 361           intro;
 362           unfold lt in H9;
 363           generalize in match (transitive_le ? ? ? H9 H6);
 364           intro;
 365           apply le_S_S_to_le;
 366           assumption
 367         | unfold Not;
 368           intro;
 369           generalize in match (H1 ? ? ? ? H9);
 370           [ intro;
 371             rewrite > H10 in H5;
 372             apply (not_le_Sn_n ? H5)
 373           | apply le_S;
 374             assumption
 375           | apply le_n
 376           ]
 377         ]
 378       ]
 379     ]
 380   | intros 4;
 381     unfold f';
 382     simplify;
 383     apply (ltb_elim (f (S n1)) (f x1));
 384     simplify;
 385     apply (ltb_elim (f (S n1)) (f y));
 386     simplify;
 387     intros;
 388     [ cut (f x1 = f y);
 389       [ apply (H1 ? ? ? ? Hcut);
 390         apply le_S;
 391         assumption
 392       | apply eq_pred_to_eq;
 393         [ apply (ltn_to_ltO ? ? H7)
 394         | apply (ltn_to_ltO ? ? H6)
 395         | assumption
 396         ]
 397       ]
 398     | (* pred (f x1) = f y absurd since y ≠ S n1 and thus f y ≠ f (S n1)
 399          so that f y < f (S n1) < f x1; hence pred (f x1) = f y is absurd *)
 400        cut (y < S n1);
 401        [ generalize in match (lt_to_not_eq ? ? Hcut);
 402          intro;
 403          cut (f y ≠ f (S n1));
 404          [ cut (f y < f (S n1));
 405            [ rewrite < H8 in Hcut2;
 406              unfold lt in Hcut2;
 407              unfold lt in H7;
 408              generalize in match (le_S_S ? ? Hcut2);
 409              intro;
 410              generalize in match (transitive_le ? ? ? H10 H7);
 411              intros;
 412              rewrite < (S_pred (f x1)) in H11;
 413               [ elim (not_le_Sn_n ? H11)
 414               | fold simplify ((f (S n1)) < (f x1)) in H7;
 415                 apply (ltn_to_ltO ? ? H7)
 416               ]
 417            | apply not_eq_to_le_to_lt;
 418              [ assumption
 419              | apply not_lt_to_le;
 420                assumption
 421              ]
 422            ]
 423          | unfold Not;
 424            intro;
 425            apply H9;
 426            apply (H1 ? ? ? ? H10);
 427            [ apply lt_to_le;
 428              assumption
 429            | constructor 1
 430            ]
 431          ]
 432        | unfold lt;
 433          apply le_S_S;
 434          assumption
 435        ]
 436     | (* f x1 = pred (f y) absurd since it implies S (f x1) = f y and
 437          f x1 ≤ f (S n1) < f y = S (f x1) so that f x1 = f (S n1); by
 438          injectivity x1 = S n1 that is absurd since x1 ≤ n1 *)
 439        generalize in match (eq_f ? ? S ? ? H8);
 440        intro;
 441        rewrite < S_pred in H9;
 442        [ rewrite < H9 in H6;
 443          generalize in match (not_lt_to_le ? ? H7);
 444          intro;
 445          unfold lt in H6;
 446          generalize in match (le_S_S ? ? H10);
 447          intro;
 448          generalize in match (antisym_le ? ? H11 H6);
 449          intro;
 450          generalize in match (inj_S ? ? H12);
 451          intro;
 452          generalize in match (H1 ? ? ? ? H13);
 453          [ intro;
 454            rewrite > H14 in H4;
 455            elim (not_le_Sn_n ? H4)
 456          | apply le_S;
 457            assumption
 458          | apply le_n
 459          ]
 460        | apply (ltn_to_ltO ? ? H6)
 461        ]
 462     | apply (H1 ? ? ? ? H8);
 463       apply le_S;
 464       assumption
 465     ]
 466   ]
 467 ].
 468 qed.
 469 (* demo *)
 470 theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid:
 471  ∀G:finite_enumerable_SemiGroup.
 472   left_cancellable ? (op G) →
 473   right_cancellable ? (op G) →
 474    ∃e:G. isMonoid (mk_PreMonoid G e).
 475 intros;
 476 letin f ≝(λn.ι(G \sub O · G \sub n));
 477 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
 478 [ letin EX ≝(Hcut O ?);
 479   [ apply le_O_n
 480   | clearbody EX;
 481     clear Hcut;
 482     unfold f in EX;
 483     elim EX;
 484     clear EX;
 485     letin HH ≝(eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
 486     clearbody HH;
 487     rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
 488     apply (ex_intro ? ? (G \sub a));
 489     letin GOGO ≝(refl_eq ? (repr ? (is_finite_enumerable G) O));
 490     clearbody GOGO;
 491     rewrite < HH in GOGO;
 492     rewrite < HH in GOGO:(? ? % ?);
 493     rewrite > (op_associative ? G) in GOGO;
 494     letin GaGa ≝(H ? ? ? GOGO);
 495     clearbody GaGa;
 496     clear GOGO;
 497     constructor 1;
 498     [ simplify;
 499       apply (semigroup_properties G)
 500     | unfold is_left_unit; intro;
 501       letin GaxGax ≝(refl_eq ? (G \sub a ·x));
 502       clearbody GaxGax; (* demo *)
 503       rewrite < GaGa in GaxGax:(? ? % ?);
 504       rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
 505       apply (H ? ? ? GaxGax)
 506     | unfold is_right_unit; intro;
 507       letin GaxGax ≝(refl_eq ? (x·G \sub a));
 508       clearbody GaxGax;
 509       rewrite < GaGa in GaxGax:(? ? % ?);
 510       rewrite < (op_associative ? (semigroup_properties G)) in GaxGax;
 511       apply (H1 ? ? ? GaxGax)
 512     ]
 513   ]
 514 | intros;
 515   elim (pigeonhole (order ? G) f ? ? ? H2);
 516   [ apply (ex_intro ? ? a);
 517     elim H3;
 518     assumption
 519   | intros;
 520     simplify in H5;
 521     cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
 522     [ rewrite > (repr_index_of ? ? (G \sub O · G \sub x))  in Hcut;
 523       rewrite > (repr_index_of ? ? (G \sub O · G \sub y))  in Hcut;
 524       generalize in match (H ? ? ? Hcut);
 525       intro;
 526       generalize in match (eq_f ? ? (index_of ? G) ? ? H6);
 527       intro;
 528       rewrite > index_of_repr in H7;
 529       rewrite > index_of_repr in H7;
 530       assumption
 531     | apply eq_f;
 532       assumption
 533     ]
 534   | intros;
 535     apply index_of_sur
 536   ]
 537 ].
 538 qed.