]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/CoRN/algebra/CoRN/SemiGroups.ma
commit in delayed_updating
[helm.git] / matita / matita / contribs / CoRN / algebra / CoRN / SemiGroups.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* $Id: CSemiGroups.v,v 1.10 2004/09/24 15:30:34 loeb Exp $ *)
16 (* printing [+] %\ensuremath+% #+# *)
17 (* printing {+} %\ensuremath+% #+# *)
18
19 (* Require Export CSetoidInc. *)
20
21 (* Begin_SpecReals *)
22
23 set "baseuri" "cic:/matita/algebra/CoRN/CSemiGroups".
24 include "algebra/CoRN/SetoidInc.ma".
25
26 (*------------------------------------------------------------------*)
27 (* Semigroups - Definition of the notion of Constructive Semigroup  *)
28 (*------------------------------------------------------------------*)
29
30 definition is_CSemiGroup : \forall A : CSetoid. \forall op: CSetoid_bin_op A. Prop \def 
31 \lambda A : CSetoid. \lambda op: CSetoid_bin_op A. CSassociative A (csbf_fun A A A op).
32
33 record CSemiGroup : Type \def 
34   {csg_crr   :> CSetoid;
35    csg_op    :  CSetoid_bin_op csg_crr;
36    csg_proof :  is_CSemiGroup csg_crr csg_op}.
37
38 (*
39 Implicit Arguments csg_op [c].
40 Infix "[+]" := csg_op (at level 50, left associativity).
41 End_SpecReals *)
42
43
44
45 (*--------------------------------------------------------------*) 
46 (*  Semigroup axioms - The axiomatic properties of a semi group *)
47 (*--------------------------------------------------------------*)
48 (* Variable G : CSemiGroup. *)
49
50 lemma CSemiGroup_is_CSemiGroup : \forall G : CSemiGroup. is_CSemiGroup (csg_crr G) (csg_op G).
51 intro.
52 elim G. simplify. exact H.
53 qed.
54 (* CoRN 
55 Lemma CSemiGroup_is_CSemiGroup : is_CSemiGroup G csg_op.*)
56
57 lemma plus_assoc : \forall G : CSemiGroup. 
58 CSassociative G (csbf_fun G G G (csg_op G)).
59 exact CSemiGroup_is_CSemiGroup.
60 qed.
61
62 (*--------------------------------------------------------------*) 
63 (*                          Semigroup basics                    *)
64 (*--------------------------------------------------------------*)
65
66 lemma plus_assoc_unfolded : \forall G : CSemiGroup. \forall x,y,z : ?.
67  (csbf_fun G G G (csg_op G) x (csbf_fun G G G (csg_op G) y z)) = 
68     (csbf_fun G G G (csg_op G) (csbf_fun G G G  (csg_op G) x y) z).
69   intros.
70   apply plus_assoc.
71 qed.
72
73 (* Section p71R1. *)
74
75 (* Morphism
76 %\begin{convention}%
77 Let [S1 S2:CSemiGroup].
78 %\end{convention}%
79 *)
80
81 (* Variable S1:CSemiGroup.
82 Variable S2:CSemiGroup. *)
83
84 definition morphism_of_CSemiGroups: \forall S1,S2: CSemiGroup. \forall f: CSetoid_fun S1 S2. 
85   Prop \def
86   \lambda S1,S2: CSemiGroup. \lambda f: CSetoid_fun S1 S2. 
87   (\forall a,b:S1. (csf_fun S1 S2 f (csbf_fun ? ? ? (csg_op ?) a b)) =
88     (csbf_fun ? ? ? (csg_op ?) (csf_fun S1 S2 f a) (csf_fun S1 S2  f b))).
89
90 (* End p71R1. *)
91
92 (* About the unit *)
93
94 (* Zero ?????  *)
95
96 definition is_rht_unit: \forall S: CSemiGroup. \forall op : CSetoid_bin_op S. \forall  Zero: ?. Prop  
97   \def 
98   \lambda S: CSemiGroup. \lambda op : CSetoid_bin_op S. \lambda  Zero: ?.
99   \forall x:?. (csbf_fun ? ? ? op x Zero) = x.
100
101 (* Definition is_rht_unit S (op : CSetoid_bin_op S) Zero : Prop := forall x, op x Zero [=] x. *)
102
103 (* End_SpecReals *)
104
105 definition is_lft_unit: \forall S: CSemiGroup. \forall op : CSetoid_bin_op S. \forall  Zero: ?. Prop 
106   \def 
107   \lambda S: CSemiGroup. \lambda op : CSetoid_bin_op S. \lambda  Zero: ?.
108    \forall x:?. (csbf_fun ? ? ? op Zero x) = x.
109
110
111 (* Implicit Arguments is_lft_unit [S]. *)
112
113 (* Begin_SpecReals *)
114
115 (* Implicit Arguments is_rht_unit [S]. *)
116
117 (* An alternative definition:
118 *)
119
120 definition is_unit: \forall S:CSemiGroup.  S \to Prop \def
121 \lambda S:CSemiGroup.
122 \lambda e. (\forall (a:S). (csbf_fun ? ? ? (csg_op ?) e a) = a \and (csbf_fun ? ? ? (csg_op ?) a e) 
123  = a).
124
125 lemma cs_unique_unit : \forall S:CSemiGroup. \forall e,f:S. 
126 (is_unit S e) \and (is_unit S f) \to e = f.
127 intros 3 (S e f).
128 unfold is_unit.
129 intro H.
130 elim H 0.
131 clear H.
132 intros (H0 H1).
133 elim (H0 f) 0.
134 clear H0.
135 intros (H2 H3).
136 elim (H1 e) 0.
137 clear H1.
138 intros (H4 H5).
139 autobatch.
140 qed.
141 (*
142 astepr (e[+]f). 
143 astepl (e[+]f).
144 apply eq_reflexive.
145 Qed.
146 *)
147
148 (* End_SpecReals *)
149
150 (* Hint Resolve plus_assoc_unfolded: algebra. *)
151
152 (* Functional operations
153 We can also define a similar addition operator, which will be denoted by [{+}], on partial functions.
154
155 %\begin{convention}% Whenever possible, we will denote the functional construction corresponding to an algebraic operation by the same symbol enclosed in curly braces.
156 %\end{convention}%
157
158 At this stage, we will always consider autobatchmorphisms; we %{\em %could%}% treat this in a more general setting, but we feel that it wouldn't really be a useful effort.
159
160 %\begin{convention}% Let [G:CSemiGroup] and [F,F':(PartFunct G)] and denote by [P] and [Q], respectively, the predicates characterizing their domains.
161 %\end{convention}%
162 *)
163
164 (* Section Part_Function_Plus. *)
165
166 (* Variable G : CSemiGroup.
167 Variables F F' : PartFunct G. *)
168
169 (* begin hide *)
170 (*Let P := Dom F.
171 Let Q := Dom F'.*)
172 (* end hide *)
173 definition NP : \forall G:CSemiGroup. \forall F,F': PartFunct G. ? \def
174    \lambda G:CSemiGroup. \lambda F,F': PartFunct G.
175    pfdom ? F.
176 definition NQ : \forall G:CSemiGroup. \forall F,F': PartFunct G. ? \def
177    \lambda G:CSemiGroup. \lambda F,F': PartFunct G.
178    pfdom ? F'.
179    
180 lemma part_function_plus_strext :  \forall G:CSemiGroup. \forall F,F': PartFunct G. 
181 \forall x, y:G. \forall Hx : conjP G (pfdom G F) (pfdom G F') x. 
182 \forall Hy : conjP G (pfdom G F) (pfdom G F') y.
183 (csbf_fun ? ? ? (csg_op G) (pfpfun ? F x (prj1 G (pfdom G F) (pfdom G F') x Hx)) 
184   (pfpfun ? F' x (prj2 G (pfdom G F) (pfdom G F') x Hx))) 
185   \neq (csbf_fun ? ? ? (csg_op G) (pfpfun ? F y (prj1 G (pfdom G F) (pfdom G F') y Hy)) 
186     (pfpfun ? F' y (prj2 G (pfdom G F) (pfdom G F') y Hy))) 
187   \to x \neq y.
188 intros (G F F' x y Hx Hy H).
189 elim (bin_op_strext_unfolded ? ? ? ? ? ? H)[
190 apply pfstrx[apply F|elim Hx.apply a|elim Hy.apply a|exact H1]|
191 apply pfstrx[apply F'|elim Hx.apply b|elim Hy.apply b|exact H1]]
192 qed.
193
194 definition Fplus : \forall G:CSemiGroup. \forall F,F': PartFunct G. ? \def 
195   \lambda G:CSemiGroup. \lambda F,F': PartFunct G.
196 mk_PartFunct G ? (conj_wd ? ? ? (dom_wd ? F) (dom_wd ? F'))
197   (\lambda x,Hx. (csbf_fun ? ? ? (csg_op ?) 
198             (pfpfun ? F x (prj1 ? ? ? ? Hx))  (pfpfun ? F' x (prj2 ? ? ? ? Hx)))) 
199   (part_function_plus_strext G F F').
200
201 (*
202 %\begin{convention}% Let [R:G->CProp].
203 %\end{convention}%
204 *)
205
206 (* Variable R : G -> CProp. *)
207
208 lemma included_FPlus :  \forall G:CSemiGroup.  \forall R : G \to Type. \forall F,F': PartFunct G. 
209 included ? R (NP G F F' ) -> included ? R (NQ G F F') \to included ? R (pfdom ? (Fplus G F F')).
210 intros; unfold Fplus;simplify. apply included_conj; assumption.
211 qed.
212
213 lemma included_FPlus' : \forall G:CSemiGroup.  \forall R : G \to Type. \forall F,F': PartFunct G. 
214   included ? R (pfdom ? (Fplus G F F')) \to included ? R (NP G F F').
215 intros. unfold Fplus in i. simplify in i; unfold NP.
216   apply (included_conj_lft ? ? ? ? i); apply H.
217 qed.
218
219 lemma included_FPlus'' : \forall G:CSemiGroup.  \forall R : G \to Type. \forall F,F': PartFunct G.
220    included ? R (pfdom ? (Fplus G F F')) -> included ? R (NQ G F F').
221 intros (G R F F'H); unfold Fplus in H. simplify in H;
222 unfold NQ. apply (included_conj_rht ? (pfdom G F)); apply H.
223 qed.
224
225 (* End Part_Function_Plus. *)
226
227 (* Implicit Arguments Fplus [G].
228 Infix "{+}" := Fplus (at level 50, left associativity).
229
230 Hint Resolve included_FPlus : included.
231
232 Hint Immediate included_FPlus' included_FPlus'' : included.
233 *) 
234
235 (* Subsemigroups
236 %\begin{convention}%
237 Let [csg] a semi-group and [P] a non-empty
238 predicate on the semi-group which is preserved by [[+]].
239 %\end{convention}%
240 *)
241
242 (* Section SubCSemiGroups. *)
243
244 (* Variable csg : CSemiGroup.
245    Variable P : csg -> CProp.
246    Variable op_pres_P : bin_op_pres_pred _ P csg_op. *) 
247
248 definition subcrr : \forall csg: CSemiGroup. \forall P : csg -> Prop. CSetoid \def 
249   \lambda csg: CSemiGroup. \lambda P : csg -> Prop.
250   mk_SubCSetoid ? P.
251 definition mk_SubCSemiGroup :\forall csg: CSemiGroup. \forall P : csg -> Prop.
252     \forall op_pres_P : bin_op_pres_pred csg P (csg_op csg). CSemiGroup \def
253   \lambda csg: CSemiGroup. \lambda P : csg -> Prop. 
254     \lambda op_pres_P : bin_op_pres_pred csg P (csg_op csg).
255    mk_CSemiGroup (subcrr csg P) (mk_SubCSetoid_bin_op ? ? ? op_pres_P )
256  (restr_f_assoc csg P ? op_pres_P  (plus_assoc csg)).
257 (* Section D9S. *)
258
259 (* Direct Product
260 %\begin{convention}%
261 Let [M1 M2:CSemiGroup]
262 %\end{convention}%
263 *)
264
265 (* Variable M1 M2: CSemiGroup. *)
266
267 definition dprod: \forall M1,M2:CSemiGroup. \forall x:ProdCSetoid (csg_crr M1) (csg_crr M2).
268   \forall y:ProdCSetoid (csg_crr M1) (csg_crr M2). (ProdCSetoid (csg_crr M1) (csg_crr M2)) \def
269   \lambda M1,M2:CSemiGroup. \lambda x:ProdCSetoid (csg_crr M1) (csg_crr M2).
270   \lambda y:ProdCSetoid (csg_crr M1) (csg_crr M2).
271   match x with 
272     [pair (x1: (cs_crr (csg_crr M1))) (x2: (cs_crr (csg_crr M2))) \Rightarrow 
273      match y with 
274        [pair (y1: (cs_crr (csg_crr M1))) (y2: (cs_crr (csg_crr M2))) \Rightarrow 
275           pair (cs_crr (csg_crr M1)) (cs_crr (csg_crr M2))
276 (csbf_fun ? ? ? (csg_op M1) x1 y1) (csbf_fun ? ? ? (csg_op M2) x2 y2)]].
277
278 lemma dprod_strext: \forall M1,M2:CSemiGroup.
279 (bin_fun_strext (ProdCSetoid M1 M2)(ProdCSetoid M1 M2)
280   (ProdCSetoid M1 M2) (dprod M1 M2)).
281 unfold bin_fun_strext.
282 intros 6 (M1 M2 x1 x2 y1 y2).
283 unfold dprod.
284 elim x1 0.
285 intros 2 (a1 a2).
286 elim x2 0.
287 intros 2 (b1 b2).
288 elim y1 0.
289 intros 2 (c1 c2).
290 elim y2 0.
291 intros 2 (d1 d2).
292 simplify.
293 intro H.
294 elim H 0[simplify.
295 clear H.
296 intro H.
297 cut (a1 \neq b1 \lor c1 \neq d1).
298 elim Hcut[left.left.assumption|right.left.assumption]
299 |intros.simplify in H1.
300 clear H.
301 cut (a2 \neq b2 \lor c2 \neq d2).
302 elim Hcut [left.right.assumption|right.right.assumption]
303 ][
304 letin H0 \def (csg_op M1).
305 unfold csg_op in H0.
306 unfold CSetoid_bin_op in H0.
307 letin H1 \def (csbf_strext M1 M1 M1 H0).
308 unfold csbf_strext in H1.
309 unfold bin_fun_strext in H1.
310 apply H1.
311 exact H|
312 letin H0 \def (csg_op M2).
313 unfold csg_op in H0.
314 unfold CSetoid_bin_op in H0.
315 letin H2 \def (csbf_strext M2 M2 M2 H0).
316 unfold csbf_strext in H2.
317 unfold bin_fun_strext in H2.
318 apply H2.
319 exact H1]
320 qed.
321
322 definition dprod_as_csb_fun: \forall M1,M2:CSemiGroup. 
323   CSetoid_bin_fun (ProdCSetoid M1 M2) (ProdCSetoid M1 M2)(ProdCSetoid M1 M2)\def
324   \lambda M1,M2:CSemiGroup.
325   mk_CSetoid_bin_fun (ProdCSetoid M1 M2)(ProdCSetoid M1 M2)
326   (ProdCSetoid M1 M2) (dprod M1 M2) (dprod_strext M1 M2).
327
328 lemma direct_product_is_CSemiGroup: \forall M1,M2:CSemiGroup. 
329   (is_CSemiGroup (ProdCSetoid M1 M2) (dprod_as_csb_fun M1 M2)).
330   intros.
331 unfold is_CSemiGroup.
332 unfold CSassociative.
333 intros (x y z).
334 elim x 0.
335 intros (x1 x2).
336 elim y 0.
337 intros (y1 y2).
338 elim z 0.
339 intros (z1 z2).
340 split[unfold dprod_as_csb_fun. simplify.apply CSemiGroup_is_CSemiGroup|
341       unfold dprod_as_csb_fun. simplify.apply CSemiGroup_is_CSemiGroup].
342 qed.
343
344 definition direct_product_as_CSemiGroup : \forall M1,M2:CSemiGroup. ? \def
345   \lambda M1,M2: CSemiGroup.
346   mk_CSemiGroup (ProdCSetoid M1 M2) (dprod_as_csb_fun M1 M2) 
347   (direct_product_is_CSemiGroup M1 M2).
348
349 (* End D9S. *)
350
351 (* The SemiGroup of Setoid functions *)
352
353 lemma FS_is_CSemiGroup:\forall X:CSetoid.
354   is_CSemiGroup (FS_as_CSetoid X X) (comp_as_bin_op  X ).
355   intro.
356 unfold is_CSemiGroup.
357 apply assoc_comp.
358 qed.
359
360 definition FS_as_CSemiGroup : \forall A : CSetoid. ? \def \lambda A:CSetoid.
361   mk_CSemiGroup (FS_as_CSetoid A A) (comp_as_bin_op A) (assoc_comp A).
362
363 (* Section p66E2b4. *)
364
365 (* The Free SemiGroup
366 %\begin{convention}% Let [A:CSetoid].
367 %\end{convention}%
368 *)
369
370 (* Variable A:CSetoid. *)
371
372 lemma Astar_is_CSemiGroup: \forall A:CSetoid. 
373   (is_CSemiGroup (free_csetoid_as_csetoid A) (app_as_csb_fun A)).
374   intro.
375 unfold is_CSemiGroup.
376 unfold CSassociative.
377 intro x.
378 unfold app_as_csb_fun.
379 simplify.
380 elim x 0.
381 simplify.
382 intros (x y).
383 elim x.
384 simplify.
385 apply eq_reflexive_unfolded.
386 simplify. left. apply eq_reflexive_unfolded.assumption.
387
388 simplify.
389 intros.unfold appA in H.
390 generalize in match (H y z).intros.unfold appA in H1.left. 
391 apply eq_reflexive_unfolded.
392 assumption.
393 qed.
394
395 definition Astar_as_CSemiGroup: \forall A:CSetoid. ? \def
396   \lambda A:CSetoid. 
397   mk_CSemiGroup (free_csetoid_as_csetoid A) (app_as_csb_fun A) 
398    (Astar_is_CSemiGroup A).
399
400 (* End p66E2b4. *)