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