helm/software/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 include "algebra/groups.ma".
  16
  17 record finite_enumerable (T:Type) : Type≝
  18  { order: nat;
  19    repr: nat → T;
  20    index_of: T → nat;
  21    index_of_sur: ∀x.index_of x ≤ order;
  22    index_of_repr: ∀n. n≤order → index_of (repr n) = n;
  23    repr_index_of: ∀x. repr (index_of x) = x
  24  }.
  25
  26 notation "hvbox(C \sub i)" with precedence 89
  27 for @{ 'repr $C $i }.
  28
  29 (* CSC: multiple interpretations in the same file are not considered in the
  30  right order
  31 interpretation "Finite_enumerable representation" 'repr C i =
  32  (cic:/matita/algebra/finite_groups/repr.con C _ i).*)
  33
  34 interpretation "Finite_enumerable order" 'card C =
  35  (cic:/matita/algebra/finite_groups/order.con C _).
  36
  37 record finite_enumerable_SemiGroup : Type≝
  38  { semigroup:> SemiGroup;
  39    is_finite_enumerable:> finite_enumerable semigroup
  40  }.
  41
  42 interpretation "Finite_enumerable representation" 'repr S i =
  43  (cic:/matita/algebra/finite_groups/repr.con S
  44   (cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i).
  45
  46 notation "hvbox(\iota e)" with precedence 60
  47 for @{ 'index_of_finite_enumerable_semigroup $e }.
  48
  49 interpretation "Index_of_finite_enumerable representation"
  50  'index_of_finite_enumerable_semigroup e
  51 =
  52  (cic:/matita/algebra/finite_groups/index_of.con _
  53   (cic:/matita/algebra/finite_groups/is_finite_enumerable.con _) e).
  54
  55
  56 (* several definitions/theorems to be moved somewhere else *)
  57
  58 theorem pigeonhole:
  59  ∀n:nat.∀f:nat→nat.
  60   (∀x,y.x≤n → y≤n → f x = f y → x=y) →
  61   (∀m. m ≤ n → f m ≤ n) →
  62    ∀x. x≤n → ∃y.f y = x ∧ y ≤ n.
  63 intro;
  64 elim n;
  65 [ apply (ex_intro ? ? O);
  66   split;
  67   [ rewrite < (le_n_O_to_eq ? H2);
  68     rewrite < (le_n_O_to_eq ? (H1 O ?));
  69     [ reflexivity
  70     | apply le_n
  71     ]
  72   | apply le_n
  73   ]
  74 | clear n;
  75   letin f' ≝
  76    (λx.
  77     let fSn1 ≝f (S n1) in
  78      let fx ≝f x in
  79       match ltb fSn1 fx with
  80       [ true ⇒ pred fx
  81       | false ⇒ fx
  82       ]);
  83   cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
  84   [ cut (∀x. x ≤ n1 → f' x ≤ n1);
  85     [ apply (nat_compare_elim (f (S n1)) x);
  86       [ intro;
  87         elim (H f' ? ? (pred x));
  88         [ simplify in H5;
  89           clear Hcut;
  90           clear Hcut1;
  91           unfold f' in H5;
  92           clear f';
  93           elim H5;
  94           clear H5;
  95           apply (ex_intro ? ? a);
  96           split;
  97           [ generalize in match (eq_f ? ? S ? ? H6);
  98             clear H6;
  99             intro;
 100             rewrite < S_pred in H5;
 101             [ generalize in match H4;
 102               clear H4;
 103               rewrite < H5;
 104               clear H5;
 105               apply (ltb_elim (f (S n1)) (f a));
 106               [ simplify;
 107                 intros;
 108                 rewrite < S_pred;
 109                 [ reflexivity
 110                 | apply (ltn_to_ltO ? ? H4)
 111                 ]
 112               | simplify;
 113                 intros;
 114                 generalize in match (not_lt_to_le ? ? H4);
 115                 clear H4;
 116                 intro;
 117                 generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
 118                 intro;
 119                 generalize in match (H1 ? ? ? ? H4);
 120                 [ intro;
 121                   generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
 122                   intro;
 123                   generalize in match (H1 ? ? ? ? H9);
 124                   [ intro;
 125                     rewrite > H10 in H7;
 126                     elim (not_le_Sn_n ? H7)
 127                   | rewrite > H8;
 128                     apply le_n
 129                   | apply le_n
 130                   ]
 131                 | apply le_S;
 132                   assumption
 133                 | apply le_n
 134                 ]
 135               ]
 136             | apply (ltn_to_ltO ? ? H4)
 137             ]
 138           | apply le_S;
 139             assumption
 140           ]
 141         | apply Hcut
 142         | apply Hcut1
 143         | apply le_S_S_to_le;
 144           rewrite < S_pred;
 145           [ assumption
 146           | apply (ltn_to_ltO ? ? H4)
 147           ]
 148         ]
 149       | intros;
 150         apply (ex_intro ? ? (S n1));
 151         split;
 152         [ assumption
 153         | constructor 1
 154         ]
 155       | intro;
 156         elim (H f' ? ? x);
 157         [ simplify in H5;
 158           clear Hcut;
 159           clear Hcut1;
 160           unfold f' in H5;
 161           clear f';
 162           elim H5;
 163           clear H5;
 164           apply (ex_intro ? ? a);
 165           split;
 166           [ generalize in match H4;
 167             clear H4;
 168             rewrite < H6;
 169             clear H6;
 170             apply (ltb_elim (f (S n1)) (f a));
 171             [ simplify;
 172               intros;
 173               generalize in match (lt_to_lt_S_S ? ? H5);
 174               intro;
 175               rewrite < S_pred in H6;
 176               [ elim (lt_n_m_to_not_lt_m_Sn ? ? H4 H6)
 177               | apply (ltn_to_ltO ? ? H4)
 178               ]
 179             | simplify;
 180               intros;
 181               reflexivity
 182             ]
 183           | apply le_S;
 184             assumption
 185           ]
 186         | apply Hcut
 187         | apply Hcut1
 188         | rewrite > (pred_Sn n1);
 189           simplify;
 190           generalize in match (H2 (S n1));
 191           intro;
 192           generalize in match (lt_to_le_to_lt ? ? ? H4 (H5 (le_n ?)));
 193           intro;
 194           unfold lt in H6;
 195           apply le_S_S_to_le;
 196           assumption
 197         ]
 198       ]
 199     | unfold f';
 200       simplify;
 201       intro;
 202       apply (ltb_elim (f (S n1)) (f x1));
 203       simplify;
 204       intros;
 205       [ generalize in match (H2 x1);
 206         intro;
 207         change in match n1 with (pred (S n1));
 208         apply le_to_le_pred;
 209         apply H6;
 210         apply le_S;
 211         assumption
 212       | generalize in match (H2 (S n1) (le_n ?));
 213         intro;
 214         generalize in match (not_lt_to_le ? ? H4);
 215         intro;
 216         generalize in match (transitive_le ? ? ? H7 H6);
 217         intro;
 218         cut (f x1 ≠ f (S n1));
 219         [ generalize in match (not_eq_to_le_to_lt ? ? Hcut1 H7);
 220           intro;
 221           unfold lt in H9;
 222           generalize in match (transitive_le ? ? ? H9 H6);
 223           intro;
 224           apply le_S_S_to_le;
 225           assumption
 226         | unfold Not;
 227           intro;
 228           generalize in match (H1 ? ? ? ? H9);
 229           [ intro;
 230             rewrite > H10 in H5;
 231             apply (not_le_Sn_n ? H5)
 232           | apply le_S;
 233             assumption
 234           | apply le_n
 235           ]
 236         ]
 237       ]
 238     ]
 239   | intros 4;
 240     unfold f';
 241     simplify;
 242     apply (ltb_elim (f (S n1)) (f x1));
 243     simplify;
 244     apply (ltb_elim (f (S n1)) (f y));
 245     simplify;
 246     intros;
 247     [ cut (f x1 = f y);
 248       [ apply (H1 ? ? ? ? Hcut);
 249         apply le_S;
 250         assumption
 251       | alias id "eq_pred_to_eq" = "cic:/matita/nat/relevant_equations/eq_pred_to_eq.con".
 252 apply eq_pred_to_eq;
 253         [ apply (ltn_to_ltO ? ? H7)
 254         | apply (ltn_to_ltO ? ? H6)
 255         | assumption
 256         ]
 257       ]
 258     | (* pred (f x1) = f y absurd since y ≠ S n1 and thus f y ≠ f (S n1)
 259          so that f y < f (S n1) < f x1; hence pred (f x1) = f y is absurd *)
 260        cut (y < S n1);
 261        [ generalize in match (lt_to_not_eq ? ? Hcut);
 262          intro;
 263          cut (f y ≠ f (S n1));
 264          [ cut (f y < f (S n1));
 265            [ rewrite < H8 in Hcut2;
 266              unfold lt in Hcut2;
 267              unfold lt in H7;
 268              generalize in match (le_S_S ? ? Hcut2);
 269              intro;
 270              generalize in match (transitive_le ? ? ? H10 H7);
 271              intros;
 272              rewrite < (S_pred (f x1)) in H11;
 273               [ elim (not_le_Sn_n ? H11)
 274               | fold simplify ((f (S n1)) < (f x1)) in H7;
 275                 apply (ltn_to_ltO ? ? H7)
 276               ]
 277            | apply not_eq_to_le_to_lt;
 278              [ assumption
 279              | apply not_lt_to_le;
 280                assumption
 281              ]
 282            ]
 283          | unfold Not;
 284            intro;
 285            apply H9;
 286            apply (H1 ? ? ? ? H10);
 287            [ apply lt_to_le;
 288              assumption
 289            | constructor 1
 290            ]
 291          ]
 292        | unfold lt;
 293          apply le_S_S;
 294          assumption
 295        ]
 296     | (* f x1 = pred (f y) absurd since it implies S (f x1) = f y and
 297          f x1 ≤ f (S n1) < f y = S (f x1) so that f x1 = f (S n1); by
 298          injectivity x1 = S n1 that is absurd since x1 ≤ n1 *)
 299        generalize in match (eq_f ? ? S ? ? H8);
 300        intro;
 301        rewrite < S_pred in H9;
 302        [ rewrite < H9 in H6;
 303          generalize in match (not_lt_to_le ? ? H7);
 304          intro;
 305          unfold lt in H6;
 306          generalize in match (le_S_S ? ? H10);
 307          intro;
 308          generalize in match (antisym_le ? ? H11 H6);
 309          intro;
 310          generalize in match (inj_S ? ? H12);
 311          intro;
 312          generalize in match (H1 ? ? ? ? H13);
 313          [ intro;
 314            rewrite > H14 in H4;
 315            elim (not_le_Sn_n ? H4)
 316          | apply le_S;
 317            assumption
 318          | apply le_n
 319          ]
 320        | apply (ltn_to_ltO ? ? H6)
 321        ]
 322     | apply (H1 ? ? ? ? H8);
 323       apply le_S;
 324       assumption
 325     ]
 326   ]
 327 ].
 328 qed.
 329 (* demo *)
 330 theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid:
 331  ∀G:finite_enumerable_SemiGroup.
 332   left_cancellable ? (op G) →
 333   right_cancellable ? (op G) →
 334    ∃e:G. isMonoid (mk_PreMonoid G e).
 335 intros;
 336 letin f ≝(λn.ι(G \sub O · G \sub n));
 337 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
 338 [ letin EX ≝(Hcut O ?);
 339   [ apply le_O_n
 340   | clearbody EX;
 341     clear Hcut;
 342     unfold f in EX;
 343     elim EX;
 344     clear EX;
 345     letin HH ≝(eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
 346     clearbody HH;
 347     rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
 348     apply (ex_intro ? ? (G \sub a));
 349     letin GOGO ≝(refl_eq ? (repr ? (is_finite_enumerable G) O));
 350     clearbody GOGO;
 351     rewrite < HH in GOGO;
 352     rewrite < HH in GOGO:(? ? % ?);
 353     rewrite > (op_associative ? G) in GOGO;
 354     letin GaGa ≝(H ? ? ? GOGO);
 355     clearbody GaGa;
 356     clear GOGO;
 357     constructor 1;
 358     [ simplify;
 359       apply (semigroup_properties G)
 360     | unfold is_left_unit; intro;
 361       letin GaxGax ≝(refl_eq ? (G \sub a ·x));
 362       clearbody GaxGax; (* demo *)
 363       rewrite < GaGa in GaxGax:(? ? % ?);
 364       rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
 365       apply (H ? ? ? GaxGax)
 366     | unfold is_right_unit; intro;
 367       letin GaxGax ≝(refl_eq ? (x·G \sub a));
 368       clearbody GaxGax;
 369       rewrite < GaGa in GaxGax:(? ? % ?);
 370       rewrite < (op_associative ? (semigroup_properties G)) in GaxGax;
 371       apply (H1 ? ? ? GaxGax)
 372     ]
 373   ]
 374 | intros;
 375   elim (pigeonhole (order ? G) f ? ? ? H2);
 376   [ apply (ex_intro ? ? a);
 377     elim H3;
 378     assumption
 379   | intros;
 380     simplify in H5;
 381     cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
 382     [ rewrite > (repr_index_of ? ? (G \sub O · G \sub x))  in Hcut;
 383       rewrite > (repr_index_of ? ? (G \sub O · G \sub y))  in Hcut;
 384       generalize in match (H ? ? ? Hcut);
 385       intro;
 386       generalize in match (eq_f ? ? (index_of ? G) ? ? H6);
 387       intro;
 388       rewrite > index_of_repr in H7;
 389       rewrite > index_of_repr in H7;
 390       assumption
 391     | apply eq_f;
 392       assumption
 393     ]
 394   | intros;
 395     unfold f;
 396     apply index_of_sur
 397   ]
 398 ].
 399 qed.