From aaa04b3cfa6fc3410c953f21c53796f82bb22411 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 3 Feb 2010 22:46:21 +0000 Subject: [PATCH] Curryfication of binary setoids. --- .../matita/nlibrary/algebra/magmas.ma | 2 +- .../matita/nlibrary/sets/categories.ma | 20 ++++++-- .../matita/nlibrary/sets/partitions.ma | 6 +-- helm/software/matita/nlibrary/sets/setoids.ma | 13 ++--- .../software/matita/nlibrary/sets/setoids1.ma | 15 +++--- .../matita/nlibrary/topology/cantor.ma | 14 +++++- .../matita/nlibrary/topology/igft-setoid.ma | 50 ++++++++----------- 7 files changed, 66 insertions(+), 54 deletions(-) diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma index 8ca0254b4..685d62480 100644 --- a/helm/software/matita/nlibrary/algebra/magmas.ma +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -16,7 +16,7 @@ include "sets/sets.ma". nrecord magma_type : Type[1] ≝ { mtcarr:> setoid; - op: binary_morphism mtcarr mtcarr mtcarr + op: unary_morphism mtcarr (unary_morph_setoid mtcarr mtcarr) }. nrecord magma (A: magma_type) : Type[1] ≝ diff --git a/helm/software/matita/nlibrary/sets/categories.ma b/helm/software/matita/nlibrary/sets/categories.ma index 310aa709e..38c8129fa 100644 --- a/helm/software/matita/nlibrary/sets/categories.ma +++ b/helm/software/matita/nlibrary/sets/categories.ma @@ -1,3 +1,17 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "sets/sets.ma". @@ -5,7 +19,7 @@ nrecord category : Type[2] ≝ { objs:> Type[1]; arrows: objs → objs → setoid; id: ∀o:objs. arrows o o; - comp: ∀o1,o2,o3. binary_morphism (arrows o2 o3) (arrows o1 o2) (arrows o1 o3); + comp: ∀o1,o2,o3. unary_morphism (arrows o2 o3) (unary_morph_setoid (arrows o1 o2) (arrows o1 o3)); comp_assoc: ∀o1,o2,o3,o4. ∀a34,a23,a12. comp o1 o3 o4 a34 (comp o1 o2 o3 a23 a12) = comp o1 o2 o4 (comp o2 o3 o4 a34 a23) a12; id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o2) a = a; @@ -27,8 +41,8 @@ ndefinition SETOID : category. ##| napply unary_morph_setoid; ##| #o; @ (λx.x); #a; #b; #H; napply H; ##| napply comp_binary_morphisms; (*CSC: why not ∘?*) -##| #o1; #o2; #o3; #o4; #f; #g; #h; nwhd; #x; napply #; -##|##6,7: #o1; #o2; #f; nwhd; #x; napply #; ##] +##| #o1; #o2; #o3; #o4; #f; #g; #h; #x; #x'; #Hx; nnormalize; napply (†(†(†Hx))) +##|##6,7: #o1; #o2; #f; #x; #x'; #Hx; nnormalize; napply (†Hx) ] nqed. unification hint 0 ≔ ; diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index 84d320e7f..b92fe9ab3 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -128,9 +128,9 @@ nlemma partition_splits_card: nlapply (Hc y I); *; #index; *; #Hi1; #Hi2; nlapply (f_sur ???? f ? Hi1); *; #nindex; *; #Hni1; #Hni2; nlapply (f_sur ???? (fi nindex) y ?) - [ alias symbol "refl" = "refl". -alias symbol "prop1" = "prop11". -alias symbol "prop2" = "prop21 mem". + [ alias symbol "refl" (instance 3) = "refl". +alias symbol "prop2" (instance 2) = "prop21". +alias symbol "prop1" (instance 4) = "prop11". napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##] *; #nindex2; *; #Hni21; #Hni22; nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2); diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma index f9fcfd020..58fe21844 100644 --- a/helm/software/matita/nlibrary/sets/setoids.ma +++ b/helm/software/matita/nlibrary/sets/setoids.ma @@ -93,14 +93,11 @@ unification hint 0 ≔ o1,o2,o3:setoid,f:unary_morphism o2 o3,g:unary_morphism o (* -------------------------------------------------------------------- *) ⊢ fun1 ?? R ≡ (composition … f g). -(* ndefinition comp_binary_morphisms: ∀o1,o2,o3. - binary_morphism (unary_morph_setoid o2 o3) (unary_morph_setoid o1 o2) - (unary_morph_setoid o1 o3). -#o1; #o2; #o3; @ + unary_morphism (unary_morph_setoid o2 o3) + (unary_morph_setoid (unary_morph_setoid o1 o2) (unary_morph_setoid o1 o3)). +#o1; #o2; #o3; napply mk_binary_morphism [ #f; #g; napply (comp_unary_morphisms … f g) (*CSC: why not ∘?*) - | #a; #a'; #b; #b'; #ea; #eb; #x; nnormalize; - napply (.= †(eb x)); napply ea. -nqed. -*) + | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ] +nqed. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma index fa615c8e4..69e095874 100644 --- a/helm/software/matita/nlibrary/sets/setoids1.ma +++ b/helm/software/matita/nlibrary/sets/setoids1.ma @@ -104,14 +104,11 @@ unification hint 0 ≔ o1,o2,o3:setoid1,f:unary_morphism1 o2 o3,g:unary_morphism (* -------------------------------------------------------------------- *) ⊢ fun11 ?? R ≡ (composition1 … f g). -(* -ndefinition comp_binary_morphisms: +ndefinition comp1_binary_morphisms: ∀o1,o2,o3. - binary_morphism1 (unary_morphism1_setoid1 o2 o3) (unary_morphism1_setoid1 o1 o2) - (unary_morphism1_setoid1 o1 o3). -#o1; #o2; #o3; @ + unary_morphism1 (unary_morphism1_setoid1 o2 o3) + (unary_morphism1_setoid1 (unary_morphism1_setoid1 o1 o2) (unary_morphism1_setoid1 o1 o3)). +#o1; #o2; #o3; napply mk_binary_morphism1 [ #f; #g; napply (comp1_unary_morphisms … f g) (*CSC: why not ∘?*) - | #a; #a'; #b; #b'; #ea; #eb; #x; nnormalize; - napply (.= †(eb x)); napply ea. -nqed. -*) + | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ] +nqed. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/topology/cantor.ma b/helm/software/matita/nlibrary/topology/cantor.ma index e7f9a5a15..3e9214f37 100644 --- a/helm/software/matita/nlibrary/topology/cantor.ma +++ b/helm/software/matita/nlibrary/topology/cantor.ma @@ -1,4 +1,16 @@ - +(**************************************************************************) +(* ___ *) +(* ||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 "topology/igft.ma". diff --git a/helm/software/matita/nlibrary/topology/igft-setoid.ma b/helm/software/matita/nlibrary/topology/igft-setoid.ma index 7235b4ba0..a4d833cae 100644 --- a/helm/software/matita/nlibrary/topology/igft-setoid.ma +++ b/helm/software/matita/nlibrary/topology/igft-setoid.ma @@ -1,27 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "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: ∀o1,o2,o3. unary_morphism (arrows o1 o2) (unary_morph_setoid (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; @@ -40,13 +37,11 @@ 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 #; ##] +##| #o; @ (λx.x); // +##| #o1; #o2; #o3; napply mk_binary_morphism [ #f; #g; @(λx.g (f x)) ] + nnormalize; /3/ +##| nnormalize; /4/ +##|##6,7: nnormalize; /2/ ] nqed. unification hint 0 ≔ ; @@ -192,10 +187,7 @@ nlet rec famU (A : nAx) (U : 𝛀^A) (x : Ord A) on x : 𝛀^A ≝ @ (f i); #a; #Ha; napply H1; ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]); - ##[##2: #E; alias symbol "refl" = "refl". - alias symbol "prop2" = "prop21 mem". - alias symbol "invert" = "setoid1 symmetry". - napply (. (#‡E^-1)); napply Ha; ##] + ##[##2: #E; napply (. (#‡E^-1)); napply Ha; ##] @; #w; #Hw; nwhd; ncut (𝐈𝐦[𝐝 y (f i)] = 𝐈𝐦[𝐝 x i]); @@ -574,4 +566,4 @@ D*) [1]: http://upsilon.cc/~zack/research/publications/notation.pdf D*) -*) \ No newline at end of file +*) -- 2.39.2