From b715c8a42bd126e4b11b8b72451d6497ce1f7f73 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 7 Feb 2008 18:08:50 +0000 Subject: [PATCH] ProdT was a perfect copy of Prod. Removed. Sum is now in Type. --- .../matita/library/algebra/CoRN/SemiGroups.ma | 6 ++--- .../matita/library/algebra/CoRN/Setoids.ma | 22 +++++++++---------- .../matita/library/datatypes/constructors.ma | 20 +++++------------ 3 files changed, 20 insertions(+), 28 deletions(-) diff --git a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma index f57e7c41a..b57d3b2fd 100644 --- a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma +++ b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma @@ -269,10 +269,10 @@ definition dprod: \forall M1,M2:CSemiGroup. \forall x:ProdCSetoid (csg_crr M1) ( \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 - [pairT (x1: (cs_crr (csg_crr M1))) (x2: (cs_crr (csg_crr M2))) \Rightarrow + [pair (x1: (cs_crr (csg_crr M1))) (x2: (cs_crr (csg_crr M2))) \Rightarrow match y with - [pairT (y1: (cs_crr (csg_crr M1))) (y2: (cs_crr (csg_crr M2))) \Rightarrow - pairT (cs_crr (csg_crr M1)) (cs_crr (csg_crr M2)) + [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. diff --git a/helm/software/matita/library/algebra/CoRN/Setoids.ma b/helm/software/matita/library/algebra/CoRN/Setoids.ma index 982d61caf..30c8c8bd5 100644 --- a/helm/software/matita/library/algebra/CoRN/Setoids.ma +++ b/helm/software/matita/library/algebra/CoRN/Setoids.ma @@ -215,19 +215,19 @@ qed. (* -----------------The product of setoids----------------------- *) -definition prod_ap: \forall A,B : CSetoid.\forall c,d: ProdT A B. Prop \def -\lambda A,B : CSetoid.\lambda c,d: ProdT A B. - ((cs_ap A (fstT A B c) (fstT A B d)) \or - (cs_ap B (sndT A B c) (sndT A B d))). - -definition prod_eq: \forall A,B : CSetoid.\forall c,d: ProdT A B. Prop \def -\lambda A,B : CSetoid.\lambda c,d: ProdT A B. - ((cs_eq A (fstT A B c) (fstT A B d)) \and - (cs_eq B (sndT A B c) (sndT A B d))). +definition prod_ap: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def +\lambda A,B : CSetoid.\lambda c,d: Prod A B. + ((cs_ap A (fst A B c) (fst A B d)) \or + (cs_ap B (snd A B c) (snd A B d))). + +definition prod_eq: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def +\lambda A,B : CSetoid.\lambda c,d: Prod A B. + ((cs_eq A (fst A B c) (fst A B d)) \and + (cs_eq B (snd A B c) (snd A B d))). lemma prodcsetoid_is_CSetoid: \forall A,B: CSetoid. - is_CSetoid (ProdT A B) (prod_eq A B) (prod_ap A B). + is_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B). intros. apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B)) [unfold. @@ -301,7 +301,7 @@ qed. definition ProdCSetoid : \forall A,B: CSetoid. CSetoid \def \lambda A,B: CSetoid. - mk_CSetoid (ProdT A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B). + mk_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B). diff --git a/helm/software/matita/library/datatypes/constructors.ma b/helm/software/matita/library/datatypes/constructors.ma index 6d0a68503..dd2a1760b 100644 --- a/helm/software/matita/library/datatypes/constructors.ma +++ b/helm/software/matita/library/datatypes/constructors.ma @@ -34,11 +34,11 @@ interpretation "Product" 'product x y = notation "hvbox(x break \times y)" with precedence 89 for @{ 'product $x $y}. -definition fst \def \lambda A,B:Set.\lambda p: Prod A B. +definition fst \def \lambda A,B:Type.\lambda p: Prod A B. match p with [(pair a b) \Rightarrow a]. -definition snd \def \lambda A,B:Set.\lambda p: Prod A B. +definition snd \def \lambda A,B:Type.\lambda p: Prod A B. match p with [(pair a b) \Rightarrow b]. @@ -54,25 +54,17 @@ interpretation "Second projection" 'snd x = notation "\snd x" with precedence 89 for @{ 'snd $x}. -theorem eq_pair_fst_snd: \forall A,B:Set.\forall p:Prod A B. +theorem eq_pair_fst_snd: \forall A,B:Type.\forall p:Prod A B. p = 〈 (\fst p), (\snd p) 〉. intros.elim p.simplify.reflexivity. qed. -inductive Sum (A,B:Set) : Set \def +inductive Sum (A,B:Type) : Type \def inl : A \to Sum A B | inr : B \to Sum A B. -inductive ProdT (A,B:Type) : Type \def -pairT : A \to B \to ProdT A B. - -definition fstT \def \lambda A,B:Type.\lambda p: ProdT A B. -match p with -[(pairT a b) \Rightarrow a]. - -definition sndT \def \lambda A,B:Type.\lambda p: ProdT A B. -match p with -[(pairT a b) \Rightarrow b]. +interpretation "Disjoint union" 'plus A B = + (cic:/matita/datatypes/constructors/Sum.ind#xpointer(1/1) A B). inductive option (A:Type) : Type ≝ None : option A -- 2.39.2