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