X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Flibrary%2Falgebra%2FCoRN%2FSemiGroups.ma;fp=matita%2Flibrary%2Falgebra%2FCoRN%2FSemiGroups.ma;h=b57d3b2fde5f22d2a735e277df8be2f35090d085;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/library/algebra/CoRN/SemiGroups.ma b/matita/library/algebra/CoRN/SemiGroups.ma
new file mode 100644
index 000000000..b57d3b2fd
--- /dev/null
+++ b/matita/library/algebra/CoRN/SemiGroups.ma
@@ -0,0 +1,400 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* $Id: CSemiGroups.v,v 1.10 2004/09/24 15:30:34 loeb Exp $ *)
+(* printing [+] %\ensuremath+% #+# *)
+(* printing {+} %\ensuremath+% #+# *)
+
+(* Require Export CSetoidInc. *)
+
+(* Begin_SpecReals *)
+
+set "baseuri" "cic:/matita/algebra/CoRN/CSemiGroups".
+include "algebra/CoRN/SetoidInc.ma".
+
+(*------------------------------------------------------------------*)
+(* Semigroups - Definition of the notion of Constructive Semigroup  *)
+(*------------------------------------------------------------------*)
+
+definition is_CSemiGroup : \forall A : CSetoid. \forall op: CSetoid_bin_op A. Prop \def 
+\lambda A : CSetoid. \lambda op: CSetoid_bin_op A. CSassociative A (csbf_fun A A A op).
+
+record CSemiGroup : Type \def 
+  {csg_crr   :> CSetoid;
+   csg_op    :  CSetoid_bin_op csg_crr;
+   csg_proof :  is_CSemiGroup csg_crr csg_op}.
+
+(*
+Implicit Arguments csg_op [c].
+Infix "[+]" := csg_op (at level 50, left associativity).
+End_SpecReals *)
+
+
+
+(*--------------------------------------------------------------*) 
+(*  Semigroup axioms - The axiomatic properties of a semi group *)
+(*--------------------------------------------------------------*)
+(* Variable G : CSemiGroup. *)
+
+lemma CSemiGroup_is_CSemiGroup : \forall G : CSemiGroup. is_CSemiGroup (csg_crr G) (csg_op G).
+intro.
+elim G. simplify. exact H.
+qed.
+(* CoRN 
+Lemma CSemiGroup_is_CSemiGroup : is_CSemiGroup G csg_op.*)
+
+lemma plus_assoc : \forall G : CSemiGroup. 
+CSassociative G (csbf_fun G G G (csg_op G)).
+exact CSemiGroup_is_CSemiGroup.
+qed.
+
+(*--------------------------------------------------------------*) 
+(*                          Semigroup basics                    *)
+(*--------------------------------------------------------------*)
+
+lemma plus_assoc_unfolded : \forall G : CSemiGroup. \forall x,y,z : ?.
+ (csbf_fun G G G (csg_op G) x (csbf_fun G G G (csg_op G) y z)) = 
+    (csbf_fun G G G (csg_op G) (csbf_fun G G G  (csg_op G) x y) z).
+  intros.
+  apply plus_assoc.
+qed.
+
+(* Section p71R1. *)
+
+(* Morphism
+%\begin{convention}%
+Let [S1 S2:CSemiGroup].
+%\end{convention}%
+*)
+
+(* Variable S1:CSemiGroup.
+Variable S2:CSemiGroup. *)
+
+definition morphism_of_CSemiGroups: \forall S1,S2: CSemiGroup. \forall f: CSetoid_fun S1 S2. 
+  Prop \def
+  \lambda S1,S2: CSemiGroup. \lambda f: CSetoid_fun S1 S2. 
+  (\forall a,b:S1. (csf_fun S1 S2 f (csbf_fun ? ? ? (csg_op ?) a b)) =
+    (csbf_fun ? ? ? (csg_op ?) (csf_fun S1 S2 f a) (csf_fun S1 S2  f b))).
+
+(* End p71R1. *)
+
+(* About the unit *)
+
+(* Zero ?????  *)
+
+definition is_rht_unit: \forall S: CSemiGroup. \forall op : CSetoid_bin_op S. \forall  Zero: ?. Prop  
+  \def 
+  \lambda S: CSemiGroup. \lambda op : CSetoid_bin_op S. \lambda  Zero: ?.
+  \forall x:?. (csbf_fun ? ? ? op x Zero) = x.
+
+(* Definition is_rht_unit S (op : CSetoid_bin_op S) Zero : Prop := forall x, op x Zero [=] x. *)
+
+(* End_SpecReals *)
+
+definition is_lft_unit: \forall S: CSemiGroup. \forall op : CSetoid_bin_op S. \forall  Zero: ?. Prop 
+  \def 
+  \lambda S: CSemiGroup. \lambda op : CSetoid_bin_op S. \lambda  Zero: ?.
+   \forall x:?. (csbf_fun ? ? ? op Zero x) = x.
+
+
+(* Implicit Arguments is_lft_unit [S]. *)
+
+(* Begin_SpecReals *)
+
+(* Implicit Arguments is_rht_unit [S]. *)
+
+(* An alternative definition:
+*)
+
+definition is_unit: \forall S:CSemiGroup.  S \to Prop \def
+\lambda S:CSemiGroup.
+\lambda e. (\forall (a:S). (csbf_fun ? ? ? (csg_op ?) e a) = a \and (csbf_fun ? ? ? (csg_op ?) a e) 
+ = a).
+
+lemma cs_unique_unit : \forall S:CSemiGroup. \forall e,f:S. 
+(is_unit S e) \and (is_unit S f) \to e = f.
+intros 3 (S e f).
+unfold is_unit.
+intro H.
+elim H 0.
+clear H.
+intros (H0 H1).
+elim (H0 f) 0.
+clear H0.
+intros (H2 H3).
+elim (H1 e) 0.
+clear H1.
+intros (H4 H5).
+autobatch new.
+qed.
+(*
+astepr (e[+]f). 
+astepl (e[+]f).
+apply eq_reflexive.
+Qed.
+*)
+
+(* End_SpecReals *)
+
+(* Hint Resolve plus_assoc_unfolded: algebra. *)
+
+(* Functional operations
+We can also define a similar addition operator, which will be denoted by [{+}], on partial functions.
+
+%\begin{convention}% Whenever possible, we will denote the functional construction corresponding to an algebraic operation by the same symbol enclosed in curly braces.
+%\end{convention}%
+
+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.
+
+%\begin{convention}% Let [G:CSemiGroup] and [F,F':(PartFunct G)] and denote by [P] and [Q], respectively, the predicates characterizing their domains.
+%\end{convention}%
+*)
+
+(* Section Part_Function_Plus. *)
+
+(* Variable G : CSemiGroup.
+Variables F F' : PartFunct G. *)
+
+(* begin hide *)
+(*Let P := Dom F.
+Let Q := Dom F'.*)
+(* end hide *)
+definition NP : \forall G:CSemiGroup. \forall F,F': PartFunct G. ? \def
+   \lambda G:CSemiGroup. \lambda F,F': PartFunct G.
+   pfdom ? F.
+definition NQ : \forall G:CSemiGroup. \forall F,F': PartFunct G. ? \def
+   \lambda G:CSemiGroup. \lambda F,F': PartFunct G.
+   pfdom ? F'.
+   
+lemma part_function_plus_strext :  \forall G:CSemiGroup. \forall F,F': PartFunct G. 
+\forall x, y:G. \forall Hx : conjP G (pfdom G F) (pfdom G F') x. 
+\forall Hy : conjP G (pfdom G F) (pfdom G F') y.
+(csbf_fun ? ? ? (csg_op G) (pfpfun ? F x (prj1 G (pfdom G F) (pfdom G F') x Hx)) 
+  (pfpfun ? F' x (prj2 G (pfdom G F) (pfdom G F') x Hx))) 
+  \neq (csbf_fun ? ? ? (csg_op G) (pfpfun ? F y (prj1 G (pfdom G F) (pfdom G F') y Hy)) 
+    (pfpfun ? F' y (prj2 G (pfdom G F) (pfdom G F') y Hy))) 
+  \to x \neq y.
+intros (G F F' x y Hx Hy H).
+elim (bin_op_strext_unfolded ? ? ? ? ? ? H)[
+apply pfstrx[apply F|elim Hx.apply t|elim Hy.apply t|exact H1]|
+apply pfstrx[apply F'|elim Hx.apply t1|elim Hy.apply t1|exact H1]]
+qed.
+
+definition Fplus : \forall G:CSemiGroup. \forall F,F': PartFunct G. ? \def 
+  \lambda G:CSemiGroup. \lambda F,F': PartFunct G.
+mk_PartFunct G ? (conj_wd ? ? ? (dom_wd ? F) (dom_wd ? F'))
+  (\lambda x,Hx. (csbf_fun ? ? ? (csg_op ?) 
+            (pfpfun ? F x (prj1 ? ? ? ? Hx))  (pfpfun ? F' x (prj2 ? ? ? ? Hx)))) 
+  (part_function_plus_strext G F F').
+
+(*
+%\begin{convention}% Let [R:G->CProp].
+%\end{convention}%
+*)
+
+(* Variable R : G -> CProp. *)
+
+lemma included_FPlus :  \forall G:CSemiGroup.  \forall R : G \to Type. \forall F,F': PartFunct G. 
+included ? R (NP G F F' ) -> included ? R (NQ G F F') \to included ? R (pfdom ? (Fplus G F F')).
+intros; unfold Fplus;simplify. apply included_conj; assumption.
+qed.
+
+lemma included_FPlus' : \forall G:CSemiGroup.  \forall R : G \to Type. \forall F,F': PartFunct G. 
+  included ? R (pfdom ? (Fplus G F F')) \to included ? R (NP G F F').
+intros. unfold Fplus in i. simplify in i; unfold NP.
+  apply (included_conj_lft ? ? ? ? i); apply H.
+qed.
+
+lemma included_FPlus'' : \forall G:CSemiGroup.  \forall R : G \to Type. \forall F,F': PartFunct G.
+   included ? R (pfdom ? (Fplus G F F')) -> included ? R (NQ G F F').
+intros (G R F F'H); unfold Fplus in H. simplify in H;
+unfold NQ. apply (included_conj_rht ? (pfdom G F)); apply H.
+qed.
+
+(* End Part_Function_Plus. *)
+
+(* Implicit Arguments Fplus [G].
+Infix "{+}" := Fplus (at level 50, left associativity).
+
+Hint Resolve included_FPlus : included.
+
+Hint Immediate included_FPlus' included_FPlus'' : included.
+*) 
+
+(* Subsemigroups
+%\begin{convention}%
+Let [csg] a semi-group and [P] a non-empty
+predicate on the semi-group which is preserved by [[+]].
+%\end{convention}%
+*)
+
+(* Section SubCSemiGroups. *)
+
+(* Variable csg : CSemiGroup.
+   Variable P : csg -> CProp.
+   Variable op_pres_P : bin_op_pres_pred _ P csg_op. *) 
+
+definition subcrr : \forall csg: CSemiGroup. \forall P : csg -> Prop. CSetoid \def 
+  \lambda csg: CSemiGroup. \lambda P : csg -> Prop.
+  mk_SubCSetoid ? P.
+definition mk_SubCSemiGroup :\forall csg: CSemiGroup. \forall P : csg -> Prop.
+    \forall op_pres_P : bin_op_pres_pred csg P (csg_op csg). CSemiGroup \def
+  \lambda csg: CSemiGroup. \lambda P : csg -> Prop. 
+    \lambda op_pres_P : bin_op_pres_pred csg P (csg_op csg).
+   mk_CSemiGroup (subcrr csg P) (mk_SubCSetoid_bin_op ? ? ? op_pres_P )
+ (restr_f_assoc csg P ? op_pres_P  (plus_assoc csg)).
+(* Section D9S. *)
+
+(* Direct Product
+%\begin{convention}%
+Let [M1 M2:CSemiGroup]
+%\end{convention}%
+*)
+
+(* Variable M1 M2: CSemiGroup. *)
+
+definition dprod: \forall M1,M2:CSemiGroup. \forall x:ProdCSetoid (csg_crr M1) (csg_crr M2).
+  \forall y:ProdCSetoid (csg_crr M1) (csg_crr M2). (ProdCSetoid (csg_crr M1) (csg_crr M2)) \def
+  \lambda M1,M2:CSemiGroup. \lambda x:ProdCSetoid (csg_crr M1) (csg_crr M2).
+  \lambda y:ProdCSetoid (csg_crr M1) (csg_crr M2).
+  match x with 
+    [pair (x1: (cs_crr (csg_crr M1))) (x2: (cs_crr (csg_crr M2))) \Rightarrow 
+     match y with 
+       [pair (y1: (cs_crr (csg_crr M1))) (y2: (cs_crr (csg_crr M2))) \Rightarrow 
+          pair (cs_crr (csg_crr M1)) (cs_crr (csg_crr M2))
+(csbf_fun ? ? ? (csg_op M1) x1 y1) (csbf_fun ? ? ? (csg_op M2) x2 y2)]].
+
+lemma dprod_strext: \forall M1,M2:CSemiGroup.
+(bin_fun_strext (ProdCSetoid M1 M2)(ProdCSetoid M1 M2)
+  (ProdCSetoid M1 M2) (dprod M1 M2)).
+unfold bin_fun_strext.
+intros 6 (M1 M2 x1 x2 y1 y2).
+unfold dprod.
+elim x1 0.
+intros 2 (a1 a2).
+elim x2 0.
+intros 2 (b1 b2).
+elim y1 0.
+intros 2 (c1 c2).
+elim y2 0.
+intros 2 (d1 d2).
+simplify.
+intro H.
+elim H 0[simplify.
+clear H.
+intro H.
+cut (a1 \neq b1 \lor c1 \neq d1).
+elim Hcut[left.left.assumption|right.left.assumption]
+|intros.simplify in H1.
+clear H.
+cut (a2 \neq b2 \lor c2 \neq d2).
+elim Hcut [left.right.assumption|right.right.assumption]
+][
+letin H0 \def (csg_op M1).
+unfold csg_op in H0.
+unfold CSetoid_bin_op in H0.
+letin H1 \def (csbf_strext M1 M1 M1 H0).
+unfold csbf_strext in H1.
+unfold bin_fun_strext in H1.
+apply H1.
+exact H|
+letin H0 \def (csg_op M2).
+unfold csg_op in H0.
+unfold CSetoid_bin_op in H0.
+letin H2 \def (csbf_strext M2 M2 M2 H0).
+unfold csbf_strext in H2.
+unfold bin_fun_strext in H2.
+apply H2.
+exact H1]
+qed.
+
+definition dprod_as_csb_fun: \forall M1,M2:CSemiGroup. 
+  CSetoid_bin_fun (ProdCSetoid M1 M2) (ProdCSetoid M1 M2)(ProdCSetoid M1 M2)\def
+  \lambda M1,M2:CSemiGroup.
+  mk_CSetoid_bin_fun (ProdCSetoid M1 M2)(ProdCSetoid M1 M2)
+  (ProdCSetoid M1 M2) (dprod M1 M2) (dprod_strext M1 M2).
+
+lemma direct_product_is_CSemiGroup: \forall M1,M2:CSemiGroup. 
+  (is_CSemiGroup (ProdCSetoid M1 M2) (dprod_as_csb_fun M1 M2)).
+  intros.
+unfold is_CSemiGroup.
+unfold CSassociative.
+intros (x y z).
+elim x 0.
+intros (x1 x2).
+elim y 0.
+intros (y1 y2).
+elim z 0.
+intros (z1 z2).
+split[unfold dprod_as_csb_fun. simplify.apply CSemiGroup_is_CSemiGroup|
+      unfold dprod_as_csb_fun. simplify.apply CSemiGroup_is_CSemiGroup].
+qed.
+
+definition direct_product_as_CSemiGroup : \forall M1,M2:CSemiGroup. ? \def
+  \lambda M1,M2: CSemiGroup.
+  mk_CSemiGroup (ProdCSetoid M1 M2) (dprod_as_csb_fun M1 M2) 
+  (direct_product_is_CSemiGroup M1 M2).
+
+(* End D9S. *)
+
+(* The SemiGroup of Setoid functions *)
+
+lemma FS_is_CSemiGroup:\forall X:CSetoid.
+  is_CSemiGroup (FS_as_CSetoid X X) (comp_as_bin_op  X ).
+  intro.
+unfold is_CSemiGroup.
+apply assoc_comp.
+qed.
+
+definition FS_as_CSemiGroup : \forall A : CSetoid. ? \def \lambda A:CSetoid.
+  mk_CSemiGroup (FS_as_CSetoid A A) (comp_as_bin_op A) (assoc_comp A).
+
+(* Section p66E2b4. *)
+
+(* The Free SemiGroup
+%\begin{convention}% Let [A:CSetoid].
+%\end{convention}%
+*)
+
+(* Variable A:CSetoid. *)
+
+lemma Astar_is_CSemiGroup: \forall A:CSetoid. 
+  (is_CSemiGroup (free_csetoid_as_csetoid A) (app_as_csb_fun A)).
+  intro.
+unfold is_CSemiGroup.
+unfold CSassociative.
+intro x.
+unfold app_as_csb_fun.
+simplify.
+elim x 0.
+simplify.
+intros (x y).
+elim x.
+simplify.
+apply eq_reflexive_unfolded.
+simplify. left. apply eq_reflexive_unfolded.assumption.
+
+simplify.
+intros.unfold appA in H.
+generalize in match (H y z).intros.unfold appA in H1.left. 
+apply eq_reflexive_unfolded.
+assumption.
+qed.
+
+definition Astar_as_CSemiGroup: \forall A:CSetoid. ? \def
+  \lambda A:CSetoid. 
+  mk_CSemiGroup (free_csetoid_as_csetoid A) (app_as_csb_fun A) 
+   (Astar_is_CSemiGroup A).
+
+(* End p66E2b4. *)