matita/dama/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/groups/".
  16
  17 include "higher_order_defs/functions.ma".
  18 include "nat/nat.ma".
  19 include "nat/orders.ma".
  20
  21 definition left_neutral \def λC,op.λe:C. ∀x:C. op e x = x.
  22
  23 definition right_neutral \def λC,op. λe:C. ∀x:C. op x e=x.
  24
  25 definition left_inverse \def λC,op.λe:C.λinv:C→C. ∀x:C. op (inv x) x = e.
  26
  27 definition right_inverse \def λC,op.λe:C.λ inv: C→ C. ∀x:C. op x (inv x)=e.
  28
  29 definition distributive_left ≝
  30  λA:Type.λf:A→A→A.λg:A→A→A.
  31   ∀x,y,z. f x (g y z) = g (f x y) (f x z).
  32
  33 definition distributive_right ≝
  34  λA:Type.λf:A→A→A.λg:A→A→A.
  35   ∀x,y,z. f (g x y) z = g (f x z) (f y z).
  36
  37 record is_abelian_group (C:Type) (plus:C→C→C) (zero:C) (opp:C→C) : Prop \def
  38  { (* abelian additive semigroup properties *)
  39     plus_assoc_: associative ? plus;
  40     plus_comm_: symmetric ? plus;
  41     (* additive monoid properties *)
  42     zero_neutral_: left_neutral ? plus zero;
  43     (* additive group properties *)
  44     opp_inverse_: left_inverse ? plus zero opp
  45  }.
  46
  47 record abelian_group : Type \def
  48  { carrier:> Type;
  49    plus: carrier → carrier → carrier;
  50    zero: carrier;
  51    opp: carrier → carrier;
  52    ag_abelian_group_properties: is_abelian_group ? plus zero opp
  53  }.
  54
  55 notation "0" with precedence 89
  56 for @{ 'zero }.
  57
  58 interpretation "Abelian group zero" 'zero =
  59  (cic:/matita/groups/zero.con _).
  60
  61 interpretation "Abelian group plus" 'plus a b =
  62  (cic:/matita/groups/plus.con _ a b).
  63
  64 interpretation "Abelian group opp" 'uminus a =
  65  (cic:/matita/groups/opp.con _ a).
  66
  67 definition minus ≝
  68  λG:abelian_group.λa,b:G. a + -b.
  69
  70 interpretation "Abelian group minus" 'minus a b =
  71  (cic:/matita/groups/minus.con _ a b).
  72
  73 theorem plus_assoc: ∀G:abelian_group. associative ? (plus G).
  74  intro;
  75  apply (plus_assoc_ ? ? ? ? (ag_abelian_group_properties G)).
  76 qed.
  77
  78 theorem plus_comm: ∀G:abelian_group. symmetric ? (plus G).
  79  intro;
  80  apply (plus_comm_ ? ? ? ? (ag_abelian_group_properties G)).
  81 qed.
  82
  83 theorem zero_neutral: ∀G:abelian_group. left_neutral ? (plus G) 0.
  84  intro;
  85  apply (zero_neutral_ ? ? ? ? (ag_abelian_group_properties G)).
  86 qed.
  87
  88 theorem opp_inverse: ∀G:abelian_group. left_inverse ? (plus G) 0 (opp G).
  89  intro;
  90  apply (opp_inverse_ ? ? ? ? (ag_abelian_group_properties G)).
  91 qed.
  92
  93 lemma cancellationlaw: ∀G:abelian_group.∀x,y,z:G. x+y=x+z → y=z.
  94 intros;
  95 generalize in match (eq_f ? ? (λa.-x +a) ? ? H);
  96 intros; clear H;
  97 rewrite < plus_assoc in H1;
  98 rewrite < plus_assoc in H1;
  99 rewrite > opp_inverse in H1;
 100 rewrite > zero_neutral in H1;
 101 rewrite > zero_neutral in H1;
 102 assumption.
 103 qed.
 104