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 "hvbox(x \sup (-1))" with precedence 89
  34 for @{ 'gopp $x }.
  35
  36 interpretation "Group inverse" 'gopp x =
  37  (cic:/matita/algebra/groups/opp.con _ x).
  38
  39 definition left_cancellable ≝
  40  λT:Type. λop: T -> T -> T.
  41   ∀x. injective ? ? (op x).
  42
  43 definition right_cancellable ≝
  44  λT:Type. λop: T -> T -> T.
  45   ∀x. injective ? ? (λz.op z x).
  46
  47 theorem eq_op_x_y_op_x_z_to_eq:
  48  ∀G:Group. left_cancellable G (op G).
  49 intros;
  50 unfold left_cancellable;
  51 unfold injective;
  52 intros (x y z);
  53 rewrite < (e_is_left_unit ? ? (monoid_properties G));
  54 rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
  55 rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
  56 rewrite > (semigroup_properties G);
  57 rewrite > (semigroup_properties G);
  58 apply eq_f;
  59 assumption.
  60 qed.
  61
  62
  63 theorem eq_op_x_y_op_z_y_to_eq:
  64  ∀G:Group. right_cancellable G (op G).
  65 intros;
  66 unfold right_cancellable;
  67 unfold injective;
  68 simplify;fold simplify (op G);
  69 intros (x y z);
  70 rewrite < (e_is_right_unit ? ? (monoid_properties G));
  71 rewrite < (e_is_right_unit ? ? (monoid_properties G) z);
  72 rewrite < (opp_is_right_inverse ? ? (group_properties G) x);
  73 rewrite < (semigroup_properties G);
  74 rewrite < (semigroup_properties G);
  75 rewrite > H;
  76 reflexivity.
  77 qed.
  78
  79 (*
  80 record enumerable (T:Type) : Type ≝
  81  { order: nat;
  82    repr: nat → T;
  83    repr_inj: ∀n,n'. n≤order → n'≤order → repr n ≠ repr n';
  84    repr_sur: ∀x.∃n.n≤order ∧ repr n = x
  85  }.
  86
  87
  88 theorem foo:
  89  ∀G:SemiGroup.
  90   enumerable (carrier G) →
  91    left_cancellable (carrier G) (op G) →
  92     right_cancellable (carrier G) (op G) →
  93      ∃e:G. is_left_unit ? e.
  94 intros (G H);
  95 unfold left_cancellable in H1;
  96 letin x ≝ (repr ? H O);
  97 letin f ≝ (λy.x·(repr ? H y));
  98 generalize in match (H1 x);
  99 intro;
 100 *)