From a8285ad2e16e571100a666bc9178347d9e61dbe5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Dec 2009 17:31:56 +0000 Subject: [PATCH] Porting of Sambin's stuff started. --- .../matita/nlibrary/properties/relations2.ma | 26 +++++ .../matita/nlibrary/sets/categories.ma | 98 +++++++++++++++++ .../matita/nlibrary/sets/categories2.ma | 104 ++++++++++++++++++ .../software/matita/nlibrary/sets/setoids2.ma | 69 ++++++++++++ .../matita/nlibrary/topology/igft-setoid.ma | 3 +- 5 files changed, 299 insertions(+), 1 deletion(-) create mode 100644 helm/software/matita/nlibrary/properties/relations2.ma create mode 100644 helm/software/matita/nlibrary/sets/categories.ma create mode 100644 helm/software/matita/nlibrary/sets/categories2.ma create mode 100644 helm/software/matita/nlibrary/sets/setoids2.ma diff --git a/helm/software/matita/nlibrary/properties/relations2.ma b/helm/software/matita/nlibrary/properties/relations2.ma new file mode 100644 index 000000000..67d09e938 --- /dev/null +++ b/helm/software/matita/nlibrary/properties/relations2.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "logic/pts.ma". + +ndefinition reflexive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x.P x x. +ndefinition symmetric2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀x,y.P x y → P y x. +ndefinition transitive2 ≝ λT:Type[2].λP:T → T → CProp[2]. ∀z,x,y. P x z → P z y → P x y. + +nrecord equivalence_relation2 (A:Type[2]) : Type[3] ≝ + { eq_rel2:2> A → A → CProp[2]; + refl2: reflexive2 ? eq_rel2; + sym2: symmetric2 ? eq_rel2; + trans2: transitive2 ? eq_rel2 + }. diff --git a/helm/software/matita/nlibrary/sets/categories.ma b/helm/software/matita/nlibrary/sets/categories.ma new file mode 100644 index 000000000..80f3b4cf6 --- /dev/null +++ b/helm/software/matita/nlibrary/sets/categories.ma @@ -0,0 +1,98 @@ + +include "sets/sets.ma". + +ndefinition binary_morph_setoid : setoid → setoid → setoid → setoid. +#S1; #S2; #T; @ (binary_morphism S1 S2 T); @; +##[ #f; #g; napply (∀x,y. f x y = g x y); +##| #f; #x; #y; napply #; +##| #f; #g; #H; #x; #y; napply ((H x y)^-1); +##| #f; #g; #h; #H1; #H2; #x; #y; napply (trans … (H1 …) (H2 …)); ##] +nqed. + +ndefinition unary_morph_setoid : setoid → setoid → setoid. +#S1; #S2; @ (unary_morphism S1 S2); @; +##[ #f; #g; napply (∀x. f x = g x); +##| #f; #x; napply #; +##| #f; #g; #H; #x; napply ((H x)^-1); +##| #f; #g; #h; #H1; #H2; #x; napply (trans … (H1 …) (H2 …)); ##] +nqed. + +nrecord category : Type[2] ≝ + { objs:> Type[1]; + arrows: objs → objs → setoid; + id: ∀o:objs. arrows o o; + comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3); + comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34. + comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34); + id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a; + id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a + }. + +notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }. +interpretation "arrows1" 'arrows A B = (unary_morphism1 A B). +interpretation "arrows" 'arrows A B = (unary_morphism A B). + +notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }. +notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }. + +interpretation "id" 'id A = (id ? A). + +ndefinition SETOID : category. +@; +##[ napply setoid; +##| napply unary_morph_setoid; +##| #o; @ (λx.x); #a; #b; #H; napply H; +##| #o1; #o2; #o3; @; + ##[ #f; #g; @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #; + ##| #f; #g; #f'; #g'; #H1; #H2; nwhd; #x; napply (.= (H2 (f x))); + napply (.= (†(H1 x))); napply #; ##] +##| #o1; #o2; #o3; #o4; #f; #g; #h; nwhd; #x; napply #; +##|##6,7: #o1; #o2; #f; nwhd; #x; napply #; ##] +nqed. + +unification hint 0 ≔ ; + R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID) + (comp_assoc SETOID) (id_neutral_left SETOID) + (id_neutral_right SETOID)) + (* -------------------------------------------------------------------- *) ⊢ + objs R ≡ setoid. + + unification hint 0 ≔ x,y ; + R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID) + (comp_assoc SETOID) (id_neutral_left SETOID) + (id_neutral_right SETOID)) + (* -------------------------------------------------------------------- *) ⊢ + arrows R x y ≡ unary_morph_setoid x y. + +unification hint 0 ≔ A,B ; + T ≟ (unary_morph_setoid A B) + (* ----------------------------------- *) ⊢ + unary_morphism A B ≡ carr T. + + +ndefinition TYPE : setoid1. +@ setoid; @; +##[ #T1; #T2; + alias symbol "eq" = "setoid eq". + napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y)); +##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #; +##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption; +##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg'; + @; ##[ @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #; + ##| @; ##[ @(λx.f'(g' x)); #a; #b; #H; napply (.= (††H)); napply #; ##] + @; #x; + ##[ napply (.= (†(Hf …))); napply Hg; + ##| napply (.= (†(Hg' …))); napply Hf'; ##] ##] +nqed. + +unification hint 0 ≔ ; + R ≟ (mk_setoid1 setoid (eq1 TYPE)) + (* -------------------------------------------- *) ⊢ + carr1 R ≡ setoid. + +nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝ + { fun01:1> A → B; + prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a') + }. + +interpretation "prop01" 'prop1 c = (prop01 ????? c). diff --git a/helm/software/matita/nlibrary/sets/categories2.ma b/helm/software/matita/nlibrary/sets/categories2.ma new file mode 100644 index 000000000..17d621431 --- /dev/null +++ b/helm/software/matita/nlibrary/sets/categories2.ma @@ -0,0 +1,104 @@ + +include "sets/sets.ma". +include "sets/setoids2.ma". +include "sets/categories.ma". + +(* +ndefinition binary_morph_setoid : setoid → setoid → setoid → setoid. +#S1; #S2; #T; @ (binary_morphism S1 S2 T); @; +##[ #f; #g; napply (∀x,y. f x y = g x y); +##| #f; #x; #y; napply #; +##| #f; #g; #H; #x; #y; napply ((H x y)^-1); +##| #f; #g; #h; #H1; #H2; #x; #y; napply (trans … (H1 …) (H2 …)); ##] +nqed. + +ndefinition unary_morph_setoid : setoid → setoid → setoid. +#S1; #S2; @ (unary_morphism S1 S2); @; +##[ #f; #g; napply (∀x. f x = g x); +##| #f; #x; napply #; +##| #f; #g; #H; #x; napply ((H x)^-1); +##| #f; #g; #h; #H1; #H2; #x; napply (trans … (H1 …) (H2 …)); ##] +nqed. + +nrecord category : Type[2] ≝ + { objs:> Type[1]; + arrows: objs → objs → setoid; + id: ∀o:objs. arrows o o; + comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3); + comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34. + comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34); + id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a; + id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a + }. +*) + +notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }. +interpretation "arrows1" 'arrows A B = (unary_morphism1 A B). +interpretation "arrows" 'arrows A B = (unary_morphism A B). + +(* +notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }. +notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }. + +interpretation "id" 'id A = (id ? A). + +ndefinition SETOID : category. +@; +##[ napply setoid; +##| napply unary_morph_setoid; +##| #o; @ (λx.x); #a; #b; #H; napply H; +##| #o1; #o2; #o3; @; + ##[ #f; #g; @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #; + ##| #f; #g; #f'; #g'; #H1; #H2; nwhd; #x; napply (.= (H2 (f x))); + napply (.= (†(H1 x))); napply #; ##] +##| #o1; #o2; #o3; #o4; #f; #g; #h; nwhd; #x; napply #; +##|##6,7: #o1; #o2; #f; nwhd; #x; napply #; ##] +nqed. + +unification hint 0 ≔ ; + R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID) + (comp_assoc SETOID) (id_neutral_left SETOID) + (id_neutral_right SETOID)) + (* -------------------------------------------------------------------- *) ⊢ + objs R ≡ setoid. + + unification hint 0 ≔ x,y ; + R ≟ (mk_category setoid unary_morph_setoid (id SETOID) (comp SETOID) + (comp_assoc SETOID) (id_neutral_left SETOID) + (id_neutral_right SETOID)) + (* -------------------------------------------------------------------- *) ⊢ + arrows R x y ≡ unary_morph_setoid x y. + +unification hint 0 ≔ A,B ; + T ≟ (unary_morph_setoid A B) + (* ----------------------------------- *) ⊢ + unary_morphism A B ≡ carr T. + + +ndefinition TYPE : setoid1. +@ setoid; @; +##[ #T1; #T2; + alias symbol "eq" = "setoid eq". + napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y)); +##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #; +##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption; +##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg'; + @; ##[ @(λx.g (f x)); #a; #b; #H; napply (.= (††H)); napply #; + ##| @; ##[ @(λx.f'(g' x)); #a; #b; #H; napply (.= (††H)); napply #; ##] + @; #x; + ##[ napply (.= (†(Hf …))); napply Hg; + ##| napply (.= (†(Hg' …))); napply Hf'; ##] ##] +nqed. + +unification hint 0 ≔ ; + R ≟ (mk_setoid1 setoid (eq1 TYPE)) + (* -------------------------------------------- *) ⊢ + carr1 R ≡ setoid. + +nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝ + { fun01:1> A → B; + prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a') + }. + +interpretation "prop01" 'prop1 c = (prop01 ????? c). +*) diff --git a/helm/software/matita/nlibrary/sets/setoids2.ma b/helm/software/matita/nlibrary/sets/setoids2.ma new file mode 100644 index 000000000..578503f6c --- /dev/null +++ b/helm/software/matita/nlibrary/sets/setoids2.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "properties/relations2.ma". +include "sets/setoids1.ma". + +nrecord setoid2: Type[3] ≝ + { carr2:> Type[2]; + eq2: equivalence_relation2 carr2 + }. + +ndefinition setoid2_of_setoid1: setoid1 → setoid2. + #s; @ (carr1 s); @ (carr1 s) (eq1 ?) + [ napply refl1 + | napply sym1 + | napply trans1] +nqed. + +(*ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid + on _s: setoid to setoid1.*) +(*prefer coercion Type_OF_setoid.*) + +interpretation "setoid2 eq" 'eq t x y = (eq_rel2 ? (eq2 t) x y). +interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y). +interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y). + +(* +notation > "hvbox(a break =_12 b)" non associative with precedence 45 +for @{ eq_rel2 (carr2 (setoid2_of_setoid1 ?)) (eq2 (setoid2_of_setoid1 ?)) $a $b }. +*) +notation > "hvbox(a break =_0 b)" non associative with precedence 45 +for @{ eq_rel ? (eq ?) $a $b }. +notation > "hvbox(a break =_1 b)" non associative with precedence 45 +for @{ eq_rel1 ? (eq1 ?) $a $b }. +notation > "hvbox(a break =_2 b)" non associative with precedence 45 +for @{ eq_rel2 ? (eq2 ?) $a $b }. + +interpretation "setoid2 symmetry" 'invert r = (sym2 ???? r). +interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r). +interpretation "setoid symmetry" 'invert r = (sym ???? r). +notation ".= r" with precedence 50 for @{'trans $r}. +interpretation "trans2" 'trans r = (trans2 ????? r). +interpretation "trans1" 'trans r = (trans1 ????? r). +interpretation "trans" 'trans r = (trans ????? r). + +nrecord unary_morphism2 (A,B: setoid2) : Type[2] ≝ + { fun12:1> A → B; + prop12: ∀a,a'. eq2 ? a a' → eq2 ? (fun12 a) (fun12 a') + }. + +nrecord binary_morphism2 (A,B,C:setoid2) : Type[2] ≝ + { fun22:2> A → B → C; + prop22: ∀a,a',b,b'. eq2 ? a a' → eq2 ? b b' → eq2 ? (fun22 a b) (fun22 a' b') + }. + +interpretation "prop12" 'prop1 c = (prop12 ????? c). +interpretation "prop22" 'prop2 l r = (prop22 ???????? l r). +interpretation "refl2" 'refl = (refl2 ???). diff --git a/helm/software/matita/nlibrary/topology/igft-setoid.ma b/helm/software/matita/nlibrary/topology/igft-setoid.ma index 30f2d161e..7235b4ba0 100644 --- a/helm/software/matita/nlibrary/topology/igft-setoid.ma +++ b/helm/software/matita/nlibrary/topology/igft-setoid.ma @@ -200,7 +200,7 @@ nlet rec famU (A : nAx) (U : 𝛀^A) (x : Ord A) on x : 𝛀^A ≝ @; #w; #Hw; nwhd; ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]); - +(* notation < "term 90 U \sub (term 90 x)" non associative with precedence 50 for @{ 'famU $U $x }. notation > "U ⎽ term 90 x" non associative with precedence 50 for @{ 'famU $U $x }. @@ -574,3 +574,4 @@ D*) [1]: http://upsilon.cc/~zack/research/publications/notation.pdf D*) +*) \ No newline at end of file -- 2.39.2