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. *)