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