matita/contribs/CoRN-Decl/algebra/CAbGroups.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 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CAbGroups".
  18
  19 (* INCLUDE
  20 CGroups
  21 *)
  22
  23 (* UNEXPORTED
  24 Section Abelian_Groups.
  25 *)
  26
  27 (*#*
  28 * Abelian Groups
  29 Now we introduce commutativity and add some results.
  30 *)
  31
  32 inline cic:/CoRN/algebra/CAbGroups/is_CAbGroup.con.
  33
  34 inline cic:/CoRN/algebra/CAbGroups/CAbGroup.ind.
  35
  36 (* UNEXPORTED
  37 Section AbGroup_Axioms.
  38 *)
  39
  40 inline cic:/CoRN/algebra/CAbGroups/G.var.
  41
  42 (*#*
  43 %\begin{convention}% Let [G] be an Abelian Group.
  44 %\end{convention}%
  45 *)
  46
  47 inline cic:/CoRN/algebra/CAbGroups/CAbGroup_is_CAbGroup.con.
  48
  49 inline cic:/CoRN/algebra/CAbGroups/cag_commutes.con.
  50
  51 inline cic:/CoRN/algebra/CAbGroups/cag_commutes_unfolded.con.
  52
  53 (* UNEXPORTED
  54 End AbGroup_Axioms.
  55 *)
  56
  57 (* UNEXPORTED
  58 Section SubCAbGroups.
  59 *)
  60
  61 (*#*
  62 ** Subgroups of an Abelian Group
  63 *)
  64
  65 inline cic:/CoRN/algebra/CAbGroups/G.var.
  66
  67 inline cic:/CoRN/algebra/CAbGroups/P.var.
  68
  69 inline cic:/CoRN/algebra/CAbGroups/Punit.var.
  70
  71 inline cic:/CoRN/algebra/CAbGroups/op_pres_P.var.
  72
  73 inline cic:/CoRN/algebra/CAbGroups/inv_pres_P.var.
  74
  75 (*#*
  76 %\begin{convention}%
  77 Let [G] be an Abelian Group and [P] be a ([CProp]-valued) predicate on [G]
  78 that contains [Zero] and is closed under [[+]] and [[--]].
  79 %\end{convention}%
  80 *)
  81
  82 inline cic:/CoRN/algebra/CAbGroups/subcrr.con.
  83
  84 inline cic:/CoRN/algebra/CAbGroups/isabgrp_scrr.con.
  85
  86 inline cic:/CoRN/algebra/CAbGroups/Build_SubCAbGroup.con.
  87
  88 (* UNEXPORTED
  89 End SubCAbGroups.
  90 *)
  91
  92 (* UNEXPORTED
  93 Section Various.
  94 *)
  95
  96 (*#*
  97 ** Basic properties of Abelian groups
  98 *)
  99
 100 (* UNEXPORTED
 101 Hint Resolve cag_commutes_unfolded: algebra.
 102 *)
 103
 104 inline cic:/CoRN/algebra/CAbGroups/G.var.
 105
 106 (*#*
 107 %\begin{convention}% Let [G] be an Abelian Group.
 108 %\end{convention}%
 109 *)
 110
 111 inline cic:/CoRN/algebra/CAbGroups/cag_op_inv.con.
 112
 113 (* UNEXPORTED
 114 Hint Resolve cag_op_inv: algebra.
 115 *)
 116
 117 inline cic:/CoRN/algebra/CAbGroups/assoc_1.con.
 118
 119 inline cic:/CoRN/algebra/CAbGroups/minus_plus.con.
 120
 121 inline cic:/CoRN/algebra/CAbGroups/op_lft_resp_ap.con.
 122
 123 inline cic:/CoRN/algebra/CAbGroups/cag_ap_cancel_lft.con.
 124
 125 inline cic:/CoRN/algebra/CAbGroups/plus_cancel_ap_lft.con.
 126
 127 (* UNEXPORTED
 128 End Various.
 129 *)
 130
 131 (* UNEXPORTED
 132 End Abelian_Groups.
 133 *)
 134
 135 (* UNEXPORTED
 136 Hint Resolve cag_commutes_unfolded: algebra.
 137 *)
 138
 139 (* UNEXPORTED
 140 Hint Resolve cag_op_inv assoc_1 zero_minus minus_plus op_lft_resp_ap: algebra.
 141 *)
 142
 143 (* UNEXPORTED
 144 Section Nice_Char.
 145 *)
 146
 147 (*#*
 148 ** Building an abelian group
 149
 150 In order to actually define concrete abelian groups,
 151 it is not in general practical to construct first a semigroup,
 152 then a monoid, then a group and finally an abelian group.  The
 153 presence of commutativity, for example, makes many of the monoid
 154 proofs trivial.  In this section, we provide a constructor that
 155 will allow us to go directly from a setoid to an abelian group.
 156
 157 We start from a setoid S with an element [unit], a
 158 commutative and associative binary operation [plus] which
 159 is strongly extensional in its first argument and admits [unit]
 160 as a left unit, and a unary setoid
 161 function [inv] which inverts elements respective to [plus].
 162 *)
 163
 164 inline cic:/CoRN/algebra/CAbGroups/S.var.
 165
 166 inline cic:/CoRN/algebra/CAbGroups/unit.var.
 167
 168 inline cic:/CoRN/algebra/CAbGroups/plus.var.
 169
 170 (*#*
 171 %\begin{convention}%
 172 Let [S] be a Setoid and [unit:S], [plus:S->S->S] and [inv] a unary
 173 setoid operation on [S].
 174 Assume that [plus] is commutative, associative and `left-strongly-extensional
 175 ([(plus x z) [#] (plus y z) -> x [#] y]), that [unit] is a left-unit
 176 for [plus] and [(inv x)] is a right-inverse of [x] w.r.t.%\% [plus].
 177 %\end{convention}%
 178 *)
 179
 180 inline cic:/CoRN/algebra/CAbGroups/plus_lext.var.
 181
 182 inline cic:/CoRN/algebra/CAbGroups/plus_lunit.var.
 183
 184 inline cic:/CoRN/algebra/CAbGroups/plus_comm.var.
 185
 186 inline cic:/CoRN/algebra/CAbGroups/plus_assoc.var.
 187
 188 inline cic:/CoRN/algebra/CAbGroups/inv.var.
 189
 190 inline cic:/CoRN/algebra/CAbGroups/inv_inv.var.
 191
 192 inline cic:/CoRN/algebra/CAbGroups/plus_rext.con.
 193
 194 inline cic:/CoRN/algebra/CAbGroups/plus_runit.con.
 195
 196 inline cic:/CoRN/algebra/CAbGroups/plus_is_fun.con.
 197
 198 inline cic:/CoRN/algebra/CAbGroups/inv_inv'.con.
 199
 200 inline cic:/CoRN/algebra/CAbGroups/plus_fun.con.
 201
 202 inline cic:/CoRN/algebra/CAbGroups/Build_CSemiGroup'.con.
 203
 204 inline cic:/CoRN/algebra/CAbGroups/Build_CMonoid'.con.
 205
 206 inline cic:/CoRN/algebra/CAbGroups/Build_CGroup'.con.
 207
 208 inline cic:/CoRN/algebra/CAbGroups/Build_CAbGroup'.con.
 209
 210 (* UNEXPORTED
 211 End Nice_Char.
 212 *)
 213
 214 (*#* ** Iteration
 215
 216 For reflection the following is needed; hopefully it is also useful.
 217 *)
 218
 219 (* UNEXPORTED
 220 Section Group_Extras.
 221 *)
 222
 223 inline cic:/CoRN/algebra/CAbGroups/G.var.
 224
 225 inline cic:/CoRN/algebra/CAbGroups/nmult.con.
 226
 227 inline cic:/CoRN/algebra/CAbGroups/nmult_wd.con.
 228
 229 inline cic:/CoRN/algebra/CAbGroups/nmult_one.con.
 230
 231 inline cic:/CoRN/algebra/CAbGroups/nmult_Zero.con.
 232
 233 inline cic:/CoRN/algebra/CAbGroups/nmult_plus.con.
 234
 235 inline cic:/CoRN/algebra/CAbGroups/nmult_mult.con.
 236
 237 inline cic:/CoRN/algebra/CAbGroups/nmult_inv.con.
 238
 239 inline cic:/CoRN/algebra/CAbGroups/nmult_plus'.con.
 240
 241 (* UNEXPORTED
 242 Hint Resolve nmult_wd nmult_Zero nmult_inv nmult_plus nmult_plus': algebra.
 243 *)
 244
 245 inline cic:/CoRN/algebra/CAbGroups/zmult.con.
 246
 247 (*
 248 Lemma Zeq_imp_nat_eq : forall m n:nat, m = n -> m = n.
 249 auto.
 250 intro m; induction m.
 251 intro n; induction n; auto.
 252
 253 intro; induction n.
 254 intro. inversion H.
 255 intros.
 256 rewrite (IHm n).
 257 auto.
 258 repeat rewrite inj_S in H.
 259 auto with zarith.
 260 Qed.
 261 *)
 262
 263 inline cic:/CoRN/algebra/CAbGroups/zmult_char.con.
 264
 265 inline cic:/CoRN/algebra/CAbGroups/zmult_wd.con.
 266
 267 inline cic:/CoRN/algebra/CAbGroups/zmult_one.con.
 268
 269 inline cic:/CoRN/algebra/CAbGroups/zmult_min_one.con.
 270
 271 inline cic:/CoRN/algebra/CAbGroups/zmult_zero.con.
 272
 273 inline cic:/CoRN/algebra/CAbGroups/zmult_Zero.con.
 274
 275 (* UNEXPORTED
 276 Hint Resolve zmult_zero: algebra.
 277 *)
 278
 279 inline cic:/CoRN/algebra/CAbGroups/zmult_plus.con.
 280
 281 inline cic:/CoRN/algebra/CAbGroups/zmult_mult.con.
 282
 283 inline cic:/CoRN/algebra/CAbGroups/zmult_plus'.con.
 284
 285 (* UNEXPORTED
 286 End Group_Extras.
 287 *)
 288
 289 (* UNEXPORTED
 290 Hint Resolve nmult_wd nmult_one nmult_Zero nmult_plus nmult_inv nmult_mult
 291   nmult_plus' zmult_wd zmult_one zmult_min_one zmult_zero zmult_Zero
 292   zmult_plus zmult_mult zmult_plus': algebra.
 293 *)
 294
 295 (* UNEXPORTED
 296 Implicit Arguments nmult [G].
 297 *)
 298
 299 (* UNEXPORTED
 300 Implicit Arguments zmult [G].
 301 *)
 302