]> matita.cs.unibo.it Git - helm.git/blob - matita/dama/groups.ma
fix dependences for matita
[helm.git] / 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.