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