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.