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