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
 106 theorem eq_opp_plus_plus_opp_opp: ∀G:abelian_group.∀x,y:G. -(x+y) = -x + -y.
 107  intros;
 108  apply (cancellationlaw ? (x+y));
 109  rewrite < plus_comm;
 110  rewrite > opp_inverse;
 111  rewrite > plus_assoc;
 112  rewrite > plus_comm in ⊢ (? ? ? (? ? ? (? ? ? %)));
 113  rewrite < plus_assoc in ⊢ (? ? ? (? ? ? %));
 114  rewrite > plus_comm;
 115  rewrite > plus_comm in ⊢ (? ? ? (? ? (? ? % ?) ?));
 116  rewrite > opp_inverse;
 117  rewrite > zero_neutral;
 118  rewrite > opp_inverse;
 119  reflexivity.
 120 qed.
 121
 122 theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x=x.
 123  intros;
 124  apply (cancellationlaw ? (-x));
 125  rewrite > opp_inverse;
 126  rewrite > plus_comm;
 127  rewrite > opp_inverse;
 128  reflexivity.
 129 qed.
 130
 131 theorem eq_zero_opp_zero: ∀G:abelian_group.0=-0.
 132  [ assumption
 133  | intros;
 134    apply (cancellationlaw ? 0);
 135    rewrite < plus_comm in ⊢ (? ? ? %);
 136    rewrite > opp_inverse;
 137    rewrite > zero_neutral;
 138    reflexivity
 139  ].
 140 qed.