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