helm/matita/library/algebra/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/groups/".
  16
  17 include "algebra/monoids.ma".
  18 include "nat/le_arith.ma".
  19
  20 record PreGroup : Type ≝
  21  { premonoid:> PreMonoid;
  22    opp: premonoid -> premonoid
  23  }.
  24
  25 record isGroup (G:PreGroup) : Prop ≝
  26  { is_monoid: isMonoid G;
  27    opp_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (opp G);
  28    opp_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (opp G)
  29  }.
  30
  31 record Group : Type ≝
  32  { pregroup:> PreGroup;
  33    group_properties:> isGroup pregroup
  34  }.
  35
  36 (*notation < "G"
  37 for @{ 'monoid $G }.
  38
  39 interpretation "Monoid coercion" 'monoid G =
  40  (cic:/matita/algebra/groups/monoid.con G).*)
  41
  42 notation < "G"
  43 for @{ 'type_of_group $G }.
  44
  45 interpretation "Type_of_group coercion" 'type_of_group G =
  46  (cic:/matita/algebra/groups/Type_of_Group.con G).
  47
  48 notation < "G"
  49 for @{ 'magma_of_group $G }.
  50
  51 interpretation "magma_of_group coercion" 'magma_of_group G =
  52  (cic:/matita/algebra/groups/Magma_of_Group.con G).
  53
  54 notation "hvbox(x \sup (-1))" with precedence 89
  55 for @{ 'gopp $x }.
  56
  57 interpretation "Group inverse" 'gopp x =
  58  (cic:/matita/algebra/groups/opp.con _ x).
  59
  60 definition left_cancellable ≝
  61  λT:Type. λop: T -> T -> T.
  62   ∀x. injective ? ? (op x).
  63
  64 definition right_cancellable ≝
  65  λT:Type. λop: T -> T -> T.
  66   ∀x. injective ? ? (λz.op z x).
  67
  68 theorem eq_op_x_y_op_x_z_to_eq:
  69  ∀G:Group. left_cancellable G (op G).
  70 intros;
  71 unfold left_cancellable;
  72 unfold injective;
  73 intros (x y z);
  74 rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G)));
  75 rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G)) z);
  76 rewrite < (opp_is_left_inverse ? (group_properties G) x);
  77 rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
  78 rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
  79 apply eq_f;
  80 assumption.
  81 qed.
  82
  83
  84 theorem eq_op_x_y_op_z_y_to_eq:
  85  ∀G:Group. right_cancellable G (op G).
  86 intros;
  87 unfold right_cancellable;
  88 unfold injective;
  89 simplify;fold simplify (op G);
  90 intros (x y z);
  91 rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G)));
  92 rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G)) z);
  93 rewrite < (opp_is_right_inverse ? (group_properties G) x);
  94 rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
  95 rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
  96 rewrite > H;
  97 reflexivity.
  98 qed.
  99
 100
 101 record finite_enumerable (T:Type) : Type ≝
 102  { order: nat;
 103    repr: nat → T;
 104    index_of: T → nat;
 105    index_of_sur: ∀x.index_of x ≤ order;
 106    index_of_repr: ∀n. n≤order → index_of (repr n) = n;
 107    repr_index_of: ∀x. repr (index_of x) = x
 108  }.
 109
 110 notation "hvbox(C \sub i)" with precedence 89
 111 for @{ 'repr $C $i }.
 112
 113 (* CSC: multiple interpretations in the same file are not considered in the
 114  right order
 115 interpretation "Finite_enumerable representation" 'repr C i =
 116  (cic:/matita/algebra/groups/repr.con C _ i).*)
 117
 118 notation "hvbox(|C|)" with precedence 89
 119 for @{ 'card $C }.
 120
 121 interpretation "Finite_enumerable order" 'card C =
 122  (cic:/matita/algebra/groups/order.con C _).
 123
 124 record finite_enumerable_SemiGroup : Type ≝
 125  { semigroup:> SemiGroup;
 126    is_finite_enumerable:> finite_enumerable semigroup
 127  }.
 128
 129 notation < "S"
 130 for @{ 'semigroup_of_finite_enumerable_semigroup $S }.
 131
 132 interpretation "Semigroup_of_finite_enumerable_semigroup"
 133  'semigroup_of_finite_enumerable_semigroup S
 134 =
 135  (cic:/matita/algebra/groups/semigroup.con S).
 136
 137 notation < "S"
 138 for @{ 'magma_of_finite_enumerable_semigroup $S }.
 139
 140 interpretation "Magma_of_finite_enumerable_semigroup"
 141  'magma_of_finite_enumerable_semigroup S
 142 =
 143  (cic:/matita/algebra/groups/Magma_of_finite_enumerable_SemiGroup.con S).
 144
 145 notation < "S"
 146 for @{ 'type_of_finite_enumerable_semigroup $S }.
 147
 148 interpretation "Type_of_finite_enumerable_semigroup"
 149  'type_of_finite_enumerable_semigroup S
 150 =
 151  (cic:/matita/algebra/groups/Type_of_finite_enumerable_SemiGroup.con S).
 152
 153 interpretation "Finite_enumerable representation" 'repr S i =
 154  (cic:/matita/algebra/groups/repr.con S
 155   (cic:/matita/algebra/groups/is_finite_enumerable.con S) i).
 156
 157 notation "hvbox(ι e)" with precedence 60
 158 for @{ 'index_of_finite_enumerable_semigroup $e }.
 159
 160 interpretation "Index_of_finite_enumerable representation"
 161  'index_of_finite_enumerable_semigroup e
 162 =
 163  (cic:/matita/algebra/groups/index_of.con _
 164   (cic:/matita/algebra/groups/is_finite_enumerable.con _) e).
 165
 166 theorem foo:
 167  ∀G:finite_enumerable_SemiGroup.
 168   left_cancellable ? (op G) →
 169   right_cancellable ? (op G) →
 170    ∃e:G. isMonoid (mk_PreMonoid G e).
 171 intros;
 172 letin f ≝ (λn.ι(G \sub O · G \sub n));
 173 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
 174 [ letin EX ≝ (Hcut O ?);
 175   [ apply le_O_n
 176   | clearbody EX;
 177     clear Hcut;
 178     unfold f in EX;
 179     elim EX;
 180     clear EX;
 181     letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
 182     clearbody HH;
 183     rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
 184     apply (ex_intro ? ? (G \sub a));
 185     letin GOGO ≝ (refl_eq ? (repr ? (is_finite_enumerable G) O));
 186     clearbody GOGO;
 187     rewrite < HH in GOGO;
 188     rewrite < HH in GOGO:(? ? % ?);
 189     rewrite > (associative ? G) in GOGO;
 190     letin GaGa ≝ (H ? ? ? GOGO);
 191     clearbody GaGa;
 192     clear GOGO;
 193     constructor 1;
 194     [ simplify;
 195       apply (semigroup_properties G)
 196     | unfold is_left_unit; intro;
 197       letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
 198       clearbody GaxGax;
 199       rewrite < GaGa in GaxGax:(? ? % ?);
 200       rewrite > (associative ? (semigroup_properties G)) in GaxGax;
 201       apply (H ? ? ? GaxGax)
 202     | unfold is_right_unit; intro;
 203       letin GaxGax ≝ (refl_eq ? (x·G \sub a));
 204       clearbody GaxGax;
 205       rewrite < GaGa in GaxGax:(? ? % ?);
 206       rewrite < (associative ? (semigroup_properties G)) in GaxGax;
 207       apply (H1 ? ? ? GaxGax)
 208     ]
 209   ]
 210 |
 211 ].