1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: CGroups.v,v 1.9 2004/04/23 10:00:52 lcf Exp $ *)
21 (*#* printing [-] %\ensuremath-% #−# *)
23 (*#* printing [--] %\ensuremath-% #−# *)
25 (*#* printing {-} %\ensuremath-% #−# *)
27 (*#* printing {--} %\ensuremath-% #−# *)
29 include "algebra/CMonoids.ma".
35 ** Definition of the notion of Group
38 inline procedural "cic:/CoRN/algebra/CGroups/is_inverse.con" as definition.
41 Implicit Arguments is_inverse [S].
44 inline procedural "cic:/CoRN/algebra/CGroups/is_CGroup.con" as definition.
46 inline procedural "cic:/CoRN/algebra/CGroups/CGroup.ind".
49 cic:/matita/CoRN-Procedural/algebra/CGroups/cg_crr.con
57 Implicit Arguments cg_inv [c].
61 Notation "[--] x" := (cg_inv x) (at level 2, right associativity).
64 inline procedural "cic:/CoRN/algebra/CGroups/cg_minus.con" as definition.
67 %\begin{nameconvention}%
68 In the names of lemmas, we will denote [[--] ] with [inv],
69 and [ [-] ] with [minus].
70 %\end{nameconvention}%
74 Implicit Arguments cg_minus [G].
78 Infix "[-]" := cg_minus (at level 50, left associativity).
85 %\begin{convention}% Let [G] be a group.
94 cic:/CoRN/algebra/CGroups/CGroup_axioms/G.var
97 inline procedural "cic:/CoRN/algebra/CGroups/cg_inverse.con" as lemma.
105 General properties of groups.
106 %\begin{convention}% Let [G] be a group.
111 Section CGroup_basics
115 cic:/CoRN/algebra/CGroups/CGroup_basics/G.var
118 inline procedural "cic:/CoRN/algebra/CGroups/cg_rht_inv_unfolded.con" as lemma.
120 inline procedural "cic:/CoRN/algebra/CGroups/cg_lft_inv_unfolded.con" as lemma.
122 inline procedural "cic:/CoRN/algebra/CGroups/cg_minus_correct.con" as lemma.
125 Hint Resolve cg_rht_inv_unfolded cg_lft_inv_unfolded cg_minus_correct:
129 inline procedural "cic:/CoRN/algebra/CGroups/cg_inverse'.con" as lemma.
133 inline procedural "cic:/CoRN/algebra/CGroups/cg_minus_unfolded.con" as lemma.
136 Hint Resolve cg_minus_unfolded: algebra.
139 inline procedural "cic:/CoRN/algebra/CGroups/cg_minus_wd.con" as lemma.
142 Hint Resolve cg_minus_wd: algebra_c.
145 inline procedural "cic:/CoRN/algebra/CGroups/cg_minus_strext.con" as lemma.
147 inline procedural "cic:/CoRN/algebra/CGroups/cg_minus_is_csetoid_bin_op.con" as definition.
149 inline procedural "cic:/CoRN/algebra/CGroups/grp_inv_assoc.con" as lemma.
152 Hint Resolve grp_inv_assoc: algebra.
155 inline procedural "cic:/CoRN/algebra/CGroups/cg_inv_unique.con" as lemma.
157 inline procedural "cic:/CoRN/algebra/CGroups/cg_inv_inv.con" as lemma.
160 Hint Resolve cg_inv_inv: algebra.
163 inline procedural "cic:/CoRN/algebra/CGroups/cg_cancel_lft.con" as lemma.
165 inline procedural "cic:/CoRN/algebra/CGroups/cg_cancel_rht.con" as lemma.
167 inline procedural "cic:/CoRN/algebra/CGroups/cg_inv_unique'.con" as lemma.
169 inline procedural "cic:/CoRN/algebra/CGroups/cg_inv_unique_2.con" as lemma.
171 inline procedural "cic:/CoRN/algebra/CGroups/cg_zero_inv.con" as lemma.
174 Hint Resolve cg_zero_inv: algebra.
177 inline procedural "cic:/CoRN/algebra/CGroups/cg_inv_zero.con" as lemma.
179 inline procedural "cic:/CoRN/algebra/CGroups/cg_inv_op.con" as lemma.
182 Useful for interactive proof development.
185 inline procedural "cic:/CoRN/algebra/CGroups/x_minus_x.con" as lemma.
189 %\begin{convention}% Let [P] be a predicate on [G] containing
190 [Zero] and closed under [[+]] and [[--] ].
199 cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/P.var
203 cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/Punit.var
207 cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/op_pres_P.var
211 cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/inv_pres_P.var
214 inline procedural "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/subcrr.con" "CGroup_basics__SubCGroups__" as definition.
216 inline procedural "cic:/CoRN/algebra/CGroups/CGroup_basics/SubCGroups/subinv.con" "CGroup_basics__SubCGroups__" as definition.
218 inline procedural "cic:/CoRN/algebra/CGroups/isgrp_scrr.con" as lemma.
220 inline procedural "cic:/CoRN/algebra/CGroups/Build_SubCGroup.con" as definition.
231 Hint Resolve cg_rht_inv_unfolded cg_lft_inv_unfolded: algebra.
235 Hint Resolve cg_inv_inv cg_minus_correct cg_zero_inv cg_inv_zero: algebra.
239 Hint Resolve cg_minus_unfolded grp_inv_assoc cg_inv_op: algebra.
243 Hint Resolve cg_minus_wd: algebra_c.
247 ** Associative properties of groups
248 %\begin{convention}% Let [G] be a group.
253 Section Assoc_properties
257 cic:/CoRN/algebra/CGroups/Assoc_properties/G.var
260 inline procedural "cic:/CoRN/algebra/CGroups/assoc_2.con" as lemma.
262 inline procedural "cic:/CoRN/algebra/CGroups/zero_minus.con" as lemma.
264 inline procedural "cic:/CoRN/algebra/CGroups/cg_cancel_mixed.con" as lemma.
266 inline procedural "cic:/CoRN/algebra/CGroups/plus_resp_eq.con" as lemma.
273 Hint Resolve assoc_2 minus_plus zero_minus cg_cancel_mixed plus_resp_eq:
278 ** Apartness in Constructive Groups
279 Specific properties of apartness.
280 %\begin{convention}% Let [G] be a group.
285 Section cgroups_apartness
289 cic:/CoRN/algebra/CGroups/cgroups_apartness/G.var
292 inline procedural "cic:/CoRN/algebra/CGroups/cg_add_ap_zero.con" as lemma.
294 inline procedural "cic:/CoRN/algebra/CGroups/op_rht_resp_ap.con" as lemma.
296 inline procedural "cic:/CoRN/algebra/CGroups/cg_ap_cancel_rht.con" as lemma.
298 inline procedural "cic:/CoRN/algebra/CGroups/plus_cancel_ap_rht.con" as lemma.
300 inline procedural "cic:/CoRN/algebra/CGroups/minus_ap_zero.con" as lemma.
302 inline procedural "cic:/CoRN/algebra/CGroups/zero_minus_apart.con" as lemma.
304 inline procedural "cic:/CoRN/algebra/CGroups/inv_resp_ap_zero.con" as lemma.
306 inline procedural "cic:/CoRN/algebra/CGroups/inv_resp_ap.con" as lemma.
308 inline procedural "cic:/CoRN/algebra/CGroups/minus_resp_ap_rht.con" as lemma.
310 inline procedural "cic:/CoRN/algebra/CGroups/minus_resp_ap_lft.con" as lemma.
312 inline procedural "cic:/CoRN/algebra/CGroups/minus_cancel_ap_rht.con" as lemma.
315 End cgroups_apartness
319 Hint Resolve op_rht_resp_ap: algebra.
323 Hint Resolve minus_ap_zero zero_minus_apart inv_resp_ap_zero: algebra.
331 ** Functional operations
333 As before, we lift our group operations to the function space of the group.
336 Let [G] be a group and [F,F':(PartFunct G)] with domains given respectively
342 cic:/CoRN/algebra/CGroups/CGroup_Ops/G.var
346 cic:/CoRN/algebra/CGroups/CGroup_Ops/F.var
350 cic:/CoRN/algebra/CGroups/CGroup_Ops/F'.var
355 inline procedural "cic:/CoRN/algebra/CGroups/CGroup_Ops/P.con" "CGroup_Ops__" as definition.
357 inline procedural "cic:/CoRN/algebra/CGroups/CGroup_Ops/Q.con" "CGroup_Ops__" as definition.
362 Section Part_Function_Inv
365 inline procedural "cic:/CoRN/algebra/CGroups/part_function_inv_strext.con" as lemma.
367 inline procedural "cic:/CoRN/algebra/CGroups/Finv.con" as definition.
370 End Part_Function_Inv
374 Section Part_Function_Minus
377 inline procedural "cic:/CoRN/algebra/CGroups/part_function_minus_strext.con" as lemma.
379 inline procedural "cic:/CoRN/algebra/CGroups/Fminus.con" as definition.
382 End Part_Function_Minus
386 %\begin{convention}% Let [R:G->CProp].
391 cic:/CoRN/algebra/CGroups/CGroup_Ops/R.var
394 inline procedural "cic:/CoRN/algebra/CGroups/included_FInv.con" as lemma.
396 inline procedural "cic:/CoRN/algebra/CGroups/included_FInv'.con" as lemma.
398 inline procedural "cic:/CoRN/algebra/CGroups/included_FMinus.con" as lemma.
400 inline procedural "cic:/CoRN/algebra/CGroups/included_FMinus'.con" as lemma.
402 inline procedural "cic:/CoRN/algebra/CGroups/included_FMinus''.con" as lemma.
409 Implicit Arguments Finv [G].
413 Notation "{--} x" := (Finv x) (at level 2, right associativity).
417 Implicit Arguments Fminus [G].
421 Infix "{-}" := Fminus (at level 50, left associativity).
425 Hint Resolve included_FInv included_FMinus : included.
429 Hint Immediate included_FInv' included_FMinus' included_FMinus'' : included.