helm/software/matita/contribs/CoRN-Decl/algebra/CGroups.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/CGroups".
  18
  19 (* $Id: CGroups.v,v 1.9 2004/04/23 10:00:52 lcf Exp $ *)
  20
  21 (*#* printing [-] %\ensuremath-% #&minus;# *)
  22
  23 (*#* printing [--] %\ensuremath-% #&minus;# *)
  24
  25 (*#* printing {-} %\ensuremath-% #&minus;# *)
  26
  27 (*#* printing {--} %\ensuremath-% #&minus;# *)
  28
  29 (* INCLUDE
  30 CMonoids
  31 *)
  32
  33 (* Begin_SpecReals *)
  34
  35 (*#*
  36 * Groups
  37 ** Definition of the notion of Group
  38 *)
  39
  40 inline cic:/CoRN/algebra/CGroups/is_inverse.con.
  41
  42 (* UNEXPORTED
  43 Implicit Arguments is_inverse [S].
  44 *)
  45
  46 inline cic:/CoRN/algebra/CGroups/is_CGroup.con.
  47
  48 inline cic:/CoRN/algebra/CGroups/CGroup.ind.
  49
  50 (* End_SpecReals *)
  51
  52 (* Begin_SpecReals *)
  53
  54 (* UNEXPORTED
  55 Implicit Arguments cg_inv [c].
  56 *)
  57
  58 inline cic:/CoRN/algebra/CGroups/cg_minus.con.
  59
  60 (*#*
  61 %\begin{nameconvention}%
  62 In the names of lemmas, we will denote [[--] ] with [inv],
  63 and [ [-] ] with [minus].
  64 %\end{nameconvention}%
  65 *)
  66
  67 (* UNEXPORTED
  68 Implicit Arguments cg_minus [G].
  69 *)
  70
  71 (* End_SpecReals *)
  72
  73 (*#*
  74 ** Group axioms
  75 %\begin{convention}% Let [G] be a group.
  76 %\end{convention}%
  77 *)
  78
  79 (* UNEXPORTED
  80 Section CGroup_axioms.
  81 *)
  82
  83 inline cic:/CoRN/algebra/CGroups/G.var.
  84
  85 inline cic:/CoRN/algebra/CGroups/cg_inverse.con.
  86
  87 (* UNEXPORTED
  88 End CGroup_axioms.
  89 *)
  90
  91 (*#*
  92 ** Group basics
  93 General properties of groups.
  94 %\begin{convention}% Let [G] be a group.
  95 %\end{convention}%
  96 *)
  97
  98 (* UNEXPORTED
  99 Section CGroup_basics.
 100 *)
 101
 102 inline cic:/CoRN/algebra/CGroups/G.var.
 103
 104 inline cic:/CoRN/algebra/CGroups/cg_rht_inv_unfolded.con.
 105
 106 inline cic:/CoRN/algebra/CGroups/cg_lft_inv_unfolded.con.
 107
 108 inline cic:/CoRN/algebra/CGroups/cg_minus_correct.con.
 109
 110 (* UNEXPORTED
 111 Hint Resolve cg_rht_inv_unfolded cg_lft_inv_unfolded cg_minus_correct:
 112   algebra.
 113 *)
 114
 115 inline cic:/CoRN/algebra/CGroups/cg_inverse'.con.
 116
 117 (* Hints for Auto *)
 118
 119 inline cic:/CoRN/algebra/CGroups/cg_minus_unfolded.con.
 120
 121 (* UNEXPORTED
 122 Hint Resolve cg_minus_unfolded: algebra.
 123 *)
 124
 125 inline cic:/CoRN/algebra/CGroups/cg_minus_wd.con.
 126
 127 (* UNEXPORTED
 128 Hint Resolve cg_minus_wd: algebra_c.
 129 *)
 130
 131 inline cic:/CoRN/algebra/CGroups/cg_minus_strext.con.
 132
 133 inline cic:/CoRN/algebra/CGroups/cg_minus_is_csetoid_bin_op.con.
 134
 135 inline cic:/CoRN/algebra/CGroups/grp_inv_assoc.con.
 136
 137 (* UNEXPORTED
 138 Hint Resolve grp_inv_assoc: algebra.
 139 *)
 140
 141 inline cic:/CoRN/algebra/CGroups/cg_inv_unique.con.
 142
 143 inline cic:/CoRN/algebra/CGroups/cg_inv_inv.con.
 144
 145 (* UNEXPORTED
 146 Hint Resolve cg_inv_inv: algebra.
 147 *)
 148
 149 inline cic:/CoRN/algebra/CGroups/cg_cancel_lft.con.
 150
 151 inline cic:/CoRN/algebra/CGroups/cg_cancel_rht.con.
 152
 153 inline cic:/CoRN/algebra/CGroups/cg_inv_unique'.con.
 154
 155 inline cic:/CoRN/algebra/CGroups/cg_inv_unique_2.con.
 156
 157 inline cic:/CoRN/algebra/CGroups/cg_zero_inv.con.
 158
 159 (* UNEXPORTED
 160 Hint Resolve cg_zero_inv: algebra.
 161 *)
 162
 163 inline cic:/CoRN/algebra/CGroups/cg_inv_zero.con.
 164
 165 inline cic:/CoRN/algebra/CGroups/cg_inv_op.con.
 166
 167 (*#*
 168 Useful for interactive proof development.
 169 *)
 170
 171 inline cic:/CoRN/algebra/CGroups/x_minus_x.con.
 172
 173 (*#*
 174 ** Sub-groups
 175 %\begin{convention}% Let [P] be a predicate on [G] containing
 176 [Zero] and closed under [[+]] and [[--] ].
 177 %\end{convention}%
 178 *)
 179
 180 (* UNEXPORTED
 181 Section SubCGroups.
 182 *)
 183
 184 inline cic:/CoRN/algebra/CGroups/P.var.
 185
 186 inline cic:/CoRN/algebra/CGroups/Punit.var.
 187
 188 inline cic:/CoRN/algebra/CGroups/op_pres_P.var.
 189
 190 inline cic:/CoRN/algebra/CGroups/inv_pres_P.var.
 191
 192 inline cic:/CoRN/algebra/CGroups/subcrr.con.
 193
 194 inline cic:/CoRN/algebra/CGroups/subinv.con.
 195
 196 inline cic:/CoRN/algebra/CGroups/isgrp_scrr.con.
 197
 198 inline cic:/CoRN/algebra/CGroups/Build_SubCGroup.con.
 199
 200 (* UNEXPORTED
 201 End SubCGroups.
 202 *)
 203
 204 (* UNEXPORTED
 205 End CGroup_basics.
 206 *)
 207
 208 (* UNEXPORTED
 209 Hint Resolve cg_rht_inv_unfolded cg_lft_inv_unfolded: algebra.
 210 *)
 211
 212 (* UNEXPORTED
 213 Hint Resolve cg_inv_inv cg_minus_correct cg_zero_inv cg_inv_zero: algebra.
 214 *)
 215
 216 (* UNEXPORTED
 217 Hint Resolve cg_minus_unfolded grp_inv_assoc cg_inv_op: algebra.
 218 *)
 219
 220 (* UNEXPORTED
 221 Hint Resolve cg_minus_wd: algebra_c.
 222 *)
 223
 224 (*#*
 225 ** Associative properties of groups
 226 %\begin{convention}% Let [G] be a group.
 227 %\end{convention}%
 228 *)
 229
 230 (* UNEXPORTED
 231 Section Assoc_properties.
 232 *)
 233
 234 inline cic:/CoRN/algebra/CGroups/G.var.
 235
 236 inline cic:/CoRN/algebra/CGroups/assoc_2.con.
 237
 238 inline cic:/CoRN/algebra/CGroups/zero_minus.con.
 239
 240 inline cic:/CoRN/algebra/CGroups/cg_cancel_mixed.con.
 241
 242 inline cic:/CoRN/algebra/CGroups/plus_resp_eq.con.
 243
 244 (* UNEXPORTED
 245 End Assoc_properties.
 246 *)
 247
 248 (* UNEXPORTED
 249 Hint Resolve assoc_2 minus_plus zero_minus cg_cancel_mixed plus_resp_eq:
 250   algebra.
 251 *)
 252
 253 (*#*
 254 ** Apartness in Constructive Groups
 255 Specific properties of apartness.
 256 %\begin{convention}% Let [G] be a group.
 257 %\end{convention}%
 258 *)
 259
 260 (* UNEXPORTED
 261 Section cgroups_apartness.
 262 *)
 263
 264 inline cic:/CoRN/algebra/CGroups/G.var.
 265
 266 inline cic:/CoRN/algebra/CGroups/cg_add_ap_zero.con.
 267
 268 inline cic:/CoRN/algebra/CGroups/op_rht_resp_ap.con.
 269
 270 inline cic:/CoRN/algebra/CGroups/cg_ap_cancel_rht.con.
 271
 272 inline cic:/CoRN/algebra/CGroups/plus_cancel_ap_rht.con.
 273
 274 inline cic:/CoRN/algebra/CGroups/minus_ap_zero.con.
 275
 276 inline cic:/CoRN/algebra/CGroups/zero_minus_apart.con.
 277
 278 inline cic:/CoRN/algebra/CGroups/inv_resp_ap_zero.con.
 279
 280 inline cic:/CoRN/algebra/CGroups/inv_resp_ap.con.
 281
 282 inline cic:/CoRN/algebra/CGroups/minus_resp_ap_rht.con.
 283
 284 inline cic:/CoRN/algebra/CGroups/minus_resp_ap_lft.con.
 285
 286 inline cic:/CoRN/algebra/CGroups/minus_cancel_ap_rht.con.
 287
 288 (* UNEXPORTED
 289 End cgroups_apartness.
 290 *)
 291
 292 (* UNEXPORTED
 293 Hint Resolve op_rht_resp_ap: algebra.
 294 *)
 295
 296 (* UNEXPORTED
 297 Hint Resolve minus_ap_zero zero_minus_apart inv_resp_ap_zero: algebra.
 298 *)
 299
 300 (* UNEXPORTED
 301 Section CGroup_Ops.
 302 *)
 303
 304 (*#*
 305 ** Functional operations
 306
 307 As before, we lift our group operations to the function space of the group.
 308
 309 %\begin{convention}%
 310 Let [G] be a group and [F,F':(PartFunct G)] with domains given respectively
 311 by [P] and [Q].
 312 %\end{convention}%
 313 *)
 314
 315 inline cic:/CoRN/algebra/CGroups/G.var.
 316
 317 inline cic:/CoRN/algebra/CGroups/F.var.
 318
 319 inline cic:/CoRN/algebra/CGroups/F'.var.
 320
 321 (* begin hide *)
 322
 323 inline cic:/CoRN/algebra/CGroups/P.con.
 324
 325 inline cic:/CoRN/algebra/CGroups/Q.con.
 326
 327 (* end hide *)
 328
 329 (* UNEXPORTED
 330 Section Part_Function_Inv.
 331 *)
 332
 333 inline cic:/CoRN/algebra/CGroups/part_function_inv_strext.con.
 334
 335 inline cic:/CoRN/algebra/CGroups/Finv.con.
 336
 337 (* UNEXPORTED
 338 End Part_Function_Inv.
 339 *)
 340
 341 (* UNEXPORTED
 342 Section Part_Function_Minus.
 343 *)
 344
 345 inline cic:/CoRN/algebra/CGroups/part_function_minus_strext.con.
 346
 347 inline cic:/CoRN/algebra/CGroups/Fminus.con.
 348
 349 (* UNEXPORTED
 350 End Part_Function_Minus.
 351 *)
 352
 353 (*#*
 354 %\begin{convention}% Let [R:G->CProp].
 355 %\end{convention}%
 356 *)
 357
 358 inline cic:/CoRN/algebra/CGroups/R.var.
 359
 360 inline cic:/CoRN/algebra/CGroups/included_FInv.con.
 361
 362 inline cic:/CoRN/algebra/CGroups/included_FInv'.con.
 363
 364 inline cic:/CoRN/algebra/CGroups/included_FMinus.con.
 365
 366 inline cic:/CoRN/algebra/CGroups/included_FMinus'.con.
 367
 368 inline cic:/CoRN/algebra/CGroups/included_FMinus''.con.
 369
 370 (* UNEXPORTED
 371 End CGroup_Ops.
 372 *)
 373
 374 (* UNEXPORTED
 375 Implicit Arguments Finv [G].
 376 *)
 377
 378 (* UNEXPORTED
 379 Implicit Arguments Fminus [G].
 380 *)
 381
 382 (* UNEXPORTED
 383 Hint Resolve included_FInv included_FMinus : included.
 384 *)
 385
 386 (* UNEXPORTED
 387 Hint Immediate included_FInv' included_FMinus' included_FMinus'' : included.
 388 *)
 389