From fd52068e75c3ea1e67b2066ac9f7e2a862148a18 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 3 Feb 2010 20:03:57 +0000 Subject: [PATCH] Work in Progress: Who needs binary_morphisms? Curryfication is your friend. But... 1) the hints are uglier 2) you really need to apply mk_binary_morphism to prove a curryfied binary morphism if you want to remain sane... Note: with non uniform coercions everywhere we should be able to finally get a beautiful script. Yet to be done. --- helm/software/matita/nlibrary/logic/cprop.ma | 72 +++++++++++-------- helm/software/matita/nlibrary/sets/setoids.ma | 40 +++++------ .../software/matita/nlibrary/sets/setoids1.ma | 28 +++++--- helm/software/matita/nlibrary/sets/sets.ma | 42 +++++------ 4 files changed, 100 insertions(+), 82 deletions(-) diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma index 0302264c6..47ccef5d0 100644 --- a/helm/software/matita/nlibrary/logic/cprop.ma +++ b/helm/software/matita/nlibrary/logic/cprop.ma @@ -42,40 +42,50 @@ nqed. notation ". r" with precedence 50 for @{'fi $r}. interpretation "fi" 'fi r = (fi' ?? r). -ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP. - napply mk_binary_morphism1 - [ napply And - | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #K1; #K2; napply conj - [ napply (H1 K1) - | napply (H3 K2) - | napply (H2 K1) - | napply (H4 K2)]##] +ndefinition and_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP). + napply (mk_binary_morphism1 … And); + #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x; #y; @ + [ napply (. Ha^-1) | napply (. Hb^-1) | napply (. Ha) | napply (. Hb)] //. nqed. -unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … And (prop21 … and_morphism)) A B ≡ And A B. - -(*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B. - #A; #A'; #B; #H1; #H2; - napply (. ((#‡H1)‡H2^-1)); nnormalize; -nqed.*) - -ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP. - napply mk_binary_morphism1 - [ napply Or - | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #H; - ##[##1,3: napply or_introl |##*: napply or_intror ] - ##[ napply (H1 H) - | napply (H2 H) - | napply (H3 H) - | napply (H4 H)]##] +unification hint 0 ≔ A,B ⊢ + mk_unary_morphism1 … + (λX.mk_unary_morphism1 … (And X) (prop11 … (and_morphism X))) + (prop11 … and_morphism) + A B ≡ And A B. + +(* +naxiom daemon: False. + +nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B. + #A; #A'; #B; #H1; #H2; napply (. (#‡H1)‡H2^-1); nelim daemon. +nqed. + +CSC: ugly proof term +ncheck test. +*) + +ndefinition or_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP). + napply (mk_binary_morphism1 … Or); + #a; #a'; #b; #b'; #Ha; #Hb; @; *; #x + [ @1; napply (. Ha^-1) | @2; napply (. Hb^-1) | @1; napply (. Ha) | @2; napply (. Hb)] //. nqed. -unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … Or (prop21 … or_morphism)) A B ≡ Or A B. +unification hint 0 ≔ A,B ⊢ + mk_unary_morphism1 … + (λX.mk_unary_morphism1 … (Or X) (prop11 … (or_morphism X))) + (prop11 … or_morphism) + A B ≡ Or A B. -ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP. - napply mk_binary_morphism1 - [ napply (λA,B. A → B) - | #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w - [ napply (if … H2); napply H; napply (fi … H1); nassumption - | napply (fi … H2); napply H; napply (if … H1); nassumption]##] +ndefinition if_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP). + napply (mk_binary_morphism1 … (λA,B:CProp[0]. A → B)); + #a; #a'; #b; #b'; #Ha; #Hb; @; #H; #x + [ napply (. Hb^-1); napply H; napply (. Ha) | napply (. Hb); napply H; napply (. Ha^-1)] + //. nqed. + +unification hint 0 ≔ A,B ⊢ + mk_unary_morphism1 … + (λX:CProp[0].mk_unary_morphism1 … (λY:CProp[0]. X → Y) (prop11 … (if_morphism X))) + (prop11 … if_morphism) + A B ≡ A → B. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma index dac7b1375..f9fcfd020 100644 --- a/helm/software/matita/nlibrary/sets/setoids.ma +++ b/helm/software/matita/nlibrary/sets/setoids.ma @@ -45,38 +45,34 @@ nrecord unary_morphism (A,B: setoid) : Type[0] ≝ prop1: ∀a,a'. eq ? a a' → eq ? (fun1 a) (fun1 a') }. -nrecord binary_morphism (A,B,C:setoid) : Type[0] ≝ - { fun2:2> A → B → C; - prop2: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun2 a b) (fun2 a' b') - }. - notation "† c" with precedence 90 for @{'prop1 $c }. notation "l ‡ r" with precedence 90 for @{'prop2 $l $r }. notation "#" with precedence 90 for @{'refl}. interpretation "prop1" 'prop1 c = (prop1 ????? c). -interpretation "prop2" 'prop2 l r = (prop2 ???????? l r). interpretation "refl" 'refl = (refl ???). -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 …)); ##] +##[ #f; #g; napply (∀x,x'. x=x' → f x = g x'); +##| #f; #x; #x'; #Hx; napply (.= †Hx); napply #; +##| #f; #g; #H; #x; #x'; #Hx; napply ((H … Hx^-1)^-1); +##| #f; #g; #h; #H1; #H2; #x; #x'; #Hx; napply (trans … (H1 …) (H2 …)); //; ##] nqed. -(* unification hint 0 (∀o1,o2. (λx,y:Type[0].True) (carr (unary_morph_setoid o1 o2)) (unary_morphism o1 o2)). -*) + +interpretation "prop2" 'prop2 l r = (prop1 ? (unary_morph_setoid ??) ? ?? l ?? r). + +nlemma unary_morph_eq: ∀A,B.∀f,g: unary_morphism A B. (∀x. f x = g x) → f=g. +/3/. nqed. + +nlemma mk_binary_morphism: + ∀A,B,C: setoid. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') → + unary_morphism A (unary_morph_setoid B C). + #A; #B; #C; #f; #H; @ [ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph_eq; #y] + /2/. +nqed. ndefinition composition ≝ λo1,o2,o3:Type[0].λf:o2 → o3.λg: o1 → o2.λx.f (g x). @@ -96,7 +92,8 @@ unification hint 0 ≔ o1,o2,o3:setoid,f:unary_morphism o2 o3,g:unary_morphism o (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g))) (* -------------------------------------------------------------------- *) ⊢ fun1 ?? R ≡ (composition … f g). - + +(* ndefinition comp_binary_morphisms: ∀o1,o2,o3. binary_morphism (unary_morph_setoid o2 o3) (unary_morph_setoid o1 o2) @@ -106,3 +103,4 @@ ndefinition comp_binary_morphisms: | #a; #a'; #b; #b'; #ea; #eb; #x; nnormalize; napply (.= †(eb x)); napply ea. nqed. +*) diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma index 49d259d5d..fa615c8e4 100644 --- a/helm/software/matita/nlibrary/sets/setoids1.ma +++ b/helm/software/matita/nlibrary/sets/setoids1.ma @@ -56,21 +56,15 @@ nrecord unary_morphism1 (A,B: setoid1) : Type[1] ≝ prop11: ∀a,a'. eq1 ? a a' → eq1 ? (fun11 a) (fun11 a') }. -nrecord binary_morphism1 (A,B,C:setoid1) : Type[1] ≝ - { fun21:2> A → B → C; - prop21: ∀a,a',b,b'. eq1 ? a a' → eq1 ? b b' → eq1 ? (fun21 a b) (fun21 a' b') - }. - interpretation "prop11" 'prop1 c = (prop11 ????? c). -interpretation "prop21" 'prop2 l r = (prop21 ???????? l r). interpretation "refl1" 'refl = (refl1 ???). ndefinition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1. #s; #s1; @ (unary_morphism1 s s1); @ - [ #f; #g; napply (∀a:s. f a = g a) - | #x; #a; napply refl1 - | #x; #y; #H; #a; napply sym1; // - | #x; #y; #z; #H1; #H2; #a; napply trans1; ##[##2: napply H1 | ##skip | napply H2]##] + [ #f; #g; napply (∀a,a':s. a=a' → f a = g a') + | #x; #a; #a'; #Ha; napply (.= †Ha); napply refl1 + | #x; #y; #H; #a; #a'; #Ha; napply (.= †Ha); napply sym1; /2/ + | #x; #y; #z; #H1; #H2; #a; #a'; #Ha; napply (.= †Ha); napply trans1; ##[##2: napply H1 | ##skip | napply H2]//;##] nqed. unification hint 0 ≔ S, T ; @@ -78,6 +72,18 @@ unification hint 0 ≔ S, T ; (* --------------------------------- *) ⊢ carr1 R ≡ unary_morphism1 S T. +interpretation "prop21" 'prop2 l r = (prop11 ? (unary_morphism1_setoid1 ??) ? ?? l ?? r). + +nlemma unary_morph1_eq1: ∀A,B.∀f,g: unary_morphism1 A B. (∀x. f x = g x) → f=g. +/3/. nqed. + +nlemma mk_binary_morphism1: + ∀A,B,C: setoid1. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') → + unary_morphism1 A (unary_morphism1_setoid1 B C). + #A; #B; #C; #f; #H; @ [ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph1_eq1; #y] + /2/. +nqed. + ndefinition composition1 ≝ λo1,o2,o3:Type[1].λf:o2 → o3.λg: o1 → o2.λx.f (g x). @@ -98,6 +104,7 @@ unification hint 0 ≔ o1,o2,o3:setoid1,f:unary_morphism1 o2 o3,g:unary_morphism (* -------------------------------------------------------------------- *) ⊢ fun11 ?? R ≡ (composition1 … f g). +(* ndefinition comp_binary_morphisms: ∀o1,o2,o3. binary_morphism1 (unary_morphism1_setoid1 o2 o3) (unary_morphism1_setoid1 o1 o2) @@ -107,3 +114,4 @@ ndefinition comp_binary_morphisms: | #a; #a'; #b; #b'; #ea; #eb; #x; nnormalize; napply (.= †(eb x)); napply ea. nqed. +*) diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index 241282c1a..c66b51e2d 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -107,38 +107,40 @@ unification hint 0 ≔ A; (* ----------------------------------------------------- *) ⊢ carr1 R ≡ ext_powerclass A. +(* interpretation "prop21 mem" 'prop2 l r = (prop21 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ???? l r). - +*) + (* ncoercion ext_carr' : ∀A.∀x:ext_powerclass_setoid A. Ω^A ≝ ext_carr on _x : (carr1 (ext_powerclass_setoid ?)) to (Ω^?). *) nlemma mem_ext_powerclass_setoid_is_morph: - ∀A. binary_morphism1 (setoid1_of_setoid A) (ext_powerclass_setoid A) CPROP. - #A; @ - [ napply (λx,S. x ∈ S) - | #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; @; #H; - ##[ napply Hb1; napply (. (ext_prop … Ha^-1)); nassumption; - ##| napply Hb2; napply (. (ext_prop … Ha)); nassumption; - ##] - ##] + ∀A. unary_morphism1 (setoid1_of_setoid A) (unary_morphism1_setoid1 (ext_powerclass_setoid A) CPROP). + #A; napply (mk_binary_morphism1 … (λx:setoid1_of_setoid A.λS: 𝛀^A. x ∈ S)); + #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; @; #H + [ napply (. (ext_prop … Ha^-1)) | napply (. (ext_prop … Ha)) ] /2/. nqed. unification hint 0 ≔ A:setoid, x, S; SS ≟ (ext_carr ? S), - TT ≟ (mk_binary_morphism1 ??? - (λx:setoid1_of_setoid ?.λS:ext_powerclass_setoid ?. x ∈ S) - (prop21 ??? (mem_ext_powerclass_setoid_is_morph A))), + TT ≟ (mk_unary_morphism1 … + (λx:setoid1_of_setoid ?. + mk_unary_morphism1 … + (λS:ext_powerclass_setoid ?. x ∈ S) + (prop11 … (mem_ext_powerclass_setoid_is_morph A x))) + (prop11 … (mem_ext_powerclass_setoid_is_morph A))), XX ≟ (ext_powerclass_setoid A) (*-------------------------------------*) ⊢ - fun21 (setoid1_of_setoid A) XX CPROP TT x S + fun11 (setoid1_of_setoid A) + (unary_morphism1_setoid1 XX CPROP) TT x S ≡ mem A SS x. -nlemma subseteq_is_morph: ∀A. binary_morphism1 (ext_powerclass_setoid A) (ext_powerclass_setoid A) CPROP. - #A; @ - [ napply (λS,S'. S ⊆ S') - | #a; #a'; #b; #b'; *; #Ha1; #Ha2; *;/4/] +nlemma subseteq_is_morph: ∀A. unary_morphism1 (ext_powerclass_setoid A) + (unary_morphism1_setoid1 (ext_powerclass_setoid A) CPROP). + #A; napply (mk_binary_morphism1 … (λS,S':𝛀^A. S ⊆ S')); + #a; #a'; #b; #b'; *; #H1; #H2; *; /4/. nqed. unification hint 0 ≔ A,a,a' @@ -160,9 +162,9 @@ unification hint 0 ≔ (* ------------------------------------------*) ⊢ ext_carr A R ≡ intersect ? (ext_carr ? B) (ext_carr ? C). -nlemma intersect_is_morph: - ∀A. binary_morphism1 (powerclass_setoid A) (powerclass_setoid A) (powerclass_setoid A). - #A; @ (λS,S'. S ∩ S'); +nlemma intersect_is_morph: + ∀A. unary_morphism1 (powerclass_setoid A) (unary_morphism1_setoid1 (powerclass_setoid A) (powerclass_setoid A)). + #A; napply (mk_binary_morphism1 … (λS,S'. S ∩ S')); #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #x; nnormalize; *;/3/. nqed. -- 2.39.2