X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsets.ma;h=4e7418fd93bcc17f4777d3bb30a293d674bc43c3;hb=8b1a49bbee9eea86eb74c040defe701370ca5893;hp=2f0725d851284586220445d860c03a72d15163e6;hpb=f5f35ef830b1335dad2fcc3c1aae2b57815f73b1;p=helm.git diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index 2f0725d85..4e7418fd9 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -1,4 +1,3 @@ - (**************************************************************************) (* ___ *) (* ||M|| *) @@ -29,182 +28,182 @@ interpretation "subseteq" 'subseteq U V = (subseteq ? U V). ndefinition overlaps ≝ λA.λU,V.∃x:A.x ∈ U ∧ x ∈ V. interpretation "overlaps" 'overlaps U V = (overlaps ? U V). -ndefinition intersect ≝ λA.λU,V:Ω \sup A.{ x | x ∈ U ∧ x ∈ V }. +ndefinition intersect ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ x ∈ V }. interpretation "intersect" 'intersects U V = (intersect ? U V). -ndefinition union ≝ λA.λU,V:Ω \sup A.{ x | x ∈ U ∨ x ∈ V }. +ndefinition union ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∨ x ∈ V }. interpretation "union" 'union U V = (union ? U V). -ndefinition big_union ≝ λA,B.λT:Ω \sup A.λf:A → Ω \sup B.{ x | ∃i. i ∈ T ∧ x ∈ f i }. +ndefinition big_union ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∃i. i ∈ T ∧ x ∈ f i }. -ndefinition big_intersection ≝ λA,B.λT:Ω \sup A.λf:A → Ω \sup B.{ x | ∀i. i ∈ T → x ∈ f i }. +ndefinition big_intersection ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∀i. i ∈ T → x ∈ f i }. -ndefinition full_set: ∀A. Ω \sup A ≝ λA.{ x | True }. -ncoercion full_set : ∀A:Type[0]. Ω \sup A ≝ full_set on A: Type[0] to (Ω \sup ?). +ndefinition full_set: ∀A. Ω^A ≝ λA.{ x | True }. -nlemma subseteq_refl: ∀A.∀S: Ω \sup A. S ⊆ S. +nlemma subseteq_refl: ∀A.∀S: Ω^A. S ⊆ S. #A; #S; #x; #H; nassumption. nqed. -nlemma subseteq_trans: ∀A.∀S,T,U: Ω \sup A. S ⊆ T → T ⊆ U → S ⊆ U. +nlemma subseteq_trans: ∀A.∀S,T,U: Ω^A. S ⊆ T → T ⊆ U → S ⊆ U. #A; #S; #T; #U; #H1; #H2; #x; #P; napply H2; napply H1; nassumption. nqed. include "properties/relations1.ma". -ndefinition seteq: ∀A. equivalence_relation1 (Ω \sup A). - #A; napply mk_equivalence_relation1 +ndefinition seteq: ∀A. equivalence_relation1 (Ω^A). + #A; @ [ napply (λS,S'. S ⊆ S' ∧ S' ⊆ S) - | #S; napply conj; napply subseteq_refl - | #S; #S'; *; #H1; #H2; napply conj; nassumption - | #S; #T; #U; *; #H1; #H2; *; #H3; #H4; napply conj; napply subseteq_trans; + | #S; @; napply subseteq_refl + | #S; #S'; *; #H1; #H2; @; nassumption + | #S; #T; #U; *; #H1; #H2; *; #H3; #H4; @; napply subseteq_trans; ##[##2,5: nassumption |##1,4: ##skip |##*: nassumption]##] -nqed. +nqed. include "sets/setoids1.ma". +(* this has to be declared here, so that it is combined with carr *) +ncoercion full_set : ∀A:Type[0]. Ω^A ≝ full_set on A: Type[0] to (Ω^?). + ndefinition powerclass_setoid: Type[0] → setoid1. - #A; napply mk_setoid1 - [ napply (Ω \sup A) - | napply seteq ] + #A; @[ napply (Ω^A)| napply seteq ] nqed. include "hints_declaration.ma". alias symbol "hint_decl" = "hint_decl_Type2". -unification hint 0 ≔ A : ? ⊢ carr1 (powerclass_setoid A) ≡ Ω^A. +unification hint 0 ≔ A ⊢ carr1 (powerclass_setoid A) ≡ Ω^A. (************ SETS OVER SETOIDS ********************) include "logic/cprop.ma". nrecord qpowerclass (A: setoid) : Type[1] ≝ - { pc:> Ω^A; + { pc:> Ω^A; (* qui pc viene dichiarato con un target preciso... + forse lo si vorrebbe dichiarato con un target più lasco + ma la sintassi :> non lo supporta *) mem_ok': ∀x,x':A. x=x' → (x ∈ pc) = (x' ∈ pc) }. ndefinition Full_set: ∀A. qpowerclass A. - #A; napply mk_qpowerclass - [ napply (full_set A) - | #x; #x'; #H; napply refl1; ##] + #A; @[ napply A | #x; #x'; #H; napply refl1] nqed. +ncoercion Full_set: ∀A. qpowerclass A ≝ Full_set on A: setoid to qpowerclass ?. ndefinition qseteq: ∀A. equivalence_relation1 (qpowerclass A). - #A; napply mk_equivalence_relation1 - [ napply (λS,S':qpowerclass A. S = S') + #A; @ + [ napply (λS,S'. S = S') | #S; napply (refl1 ? (seteq A)) | #S; #S'; napply (sym1 ? (seteq A)) | #S; #T; #U; napply (trans1 ? (seteq A))] nqed. ndefinition qpowerclass_setoid: setoid → setoid1. - #A; napply mk_setoid1 + #A; @ [ napply (qpowerclass A) | napply (qseteq A) ] nqed. -unification hint 0 ≔ A : ? ⊢ carr1 (qpowerclass_setoid A) ≡ qpowerclass A. +unification hint 0 ≔ A ⊢ + carr1 (qpowerclass_setoid A) ≡ qpowerclass A. nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP. - #A; napply mk_binary_morphism1 - [ #x; napply (λS: qpowerclass_setoid ?. x ∈ S) (* ERROR CSC: ??? *) - | #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; napply mk_iff; #H; + #A; @ + [ napply (λx,S. x ∈ S) + | #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; @; #H; ##[ napply Hb1; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha^-1;##] ##| napply Hb2; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha;##] ##] ##] nqed. -unification hint 0 ≔ - A : setoid, x : ?, S : ? ⊢ (mem_ok A) x S ≡ mem A S x. - +unification hint 0 ≔ A:setoid, x, S; + SS ≟ (pc ? S) + (*-------------------------------------*) ⊢ + fun21 ??? (mem_ok A) x S ≡ mem A SS x. + nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP. - #A; napply mk_binary_morphism1 - [ napply (λS,S': qpowerclass_setoid ?. S ⊆ S') - | #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; napply mk_iff; #H + #A; @ + [ napply (λS,S'. S ⊆ S') + | #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #H [ napply (subseteq_trans … a) [ nassumption | napply (subseteq_trans … b); nassumption ] ##| napply (subseteq_trans … a') [ nassumption | napply (subseteq_trans … b'); nassumption ] ##] nqed. +unification hint 0 ≔ A,a,a' + (*-----------------------------------------------------------------*) ⊢ + eq_rel ? (eq A) a a' ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) a a'. + nlemma intersect_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) (qpowerclass_setoid A). - #A; napply mk_binary_morphism1 - [ #S; #S'; napply mk_qpowerclass + #A; @ + [ #S; #S'; @ [ napply (S ∩ S') - | #a; #a'; #Ha; nwhd in ⊢ (? ? ? % %); napply mk_iff; *; #H1; #H2; napply conj - [##1,2: napply (. (mem_ok' …)^-1) [##3,6: nassumption |##2,5: nassumption |##*: ##skip] - ##|##3,4: napply (. (mem_ok' …)) [##1,3,4,6: nassumption |##*: ##skip]##]##] - ##| #a; #a'; #b; #b'; #Ha; #Hb; nwhd; napply conj; #x; nwhd in ⊢ (% → %); #H - [ napply (. ((#‡Ha^-1)‡(#‡Hb^-1))); nassumption + | #a; #a'; #Ha; + nwhd in ⊢ (? ? ? % %); @; *; #H1; #H2; @ + [##1,2: napply (. Ha^-1‡#); nassumption; + ##|##3,4: napply (. Ha‡#); nassumption]##] + ##| #a; #a'; #b; #b'; #Ha; #Hb; nwhd; @; #x; nwhd in ⊢ (% → %); #H + [ alias symbol "invert" = "setoid1 symmetry". + napply (. ((#‡Ha^-1)‡(#‡Hb^-1))); nassumption | napply (. ((#‡Ha)‡(#‡Hb))); nassumption ]##] nqed. -(* +(* unfold if intersect, exposing fun21 *) +alias symbol "hint_decl" = "hint_decl_Type1". unification hint 0 ≔ - A : setoid, U : qpowerclass_setoid A, V : ? ⊢ (intersect_ok A) U V ≡ U ∩ V. - *) + A : setoid, B,C : qpowerclass A ⊢ + pc A (intersect_ok A B C) ≡ intersect ? (pc ? B) (pc ? C). nlemma test: ∀A:setoid. ∀U,V:qpowerclass A. ∀x,x':setoid1_of_setoid A. x=x' → x ∈ U ∩ V → x' ∈ U ∩ V. - #A; #U; #V; #x; #x'; #H; #p; - (* CSC: senza la change non funziona! *) - nchange with (x' ∈ (fun21 ??? (intersect_ok A) U V)); - napply (. (H^-1‡#)); nassumption. + #A; #U; #V; #x; #x'; #H; #p; napply (. (H^-1‡#)); nassumption. nqed. -(* -(* qui non funziona una cippa *) -ndefinition image: ∀A,B. (carr A → carr B) → Ω \sup A → Ω \sup B ≝ - λA,B:setoid.λf:carr A → carr B.λSa:Ω \sup A. - {y | ∃x. x ∈ Sa ∧ eq_rel (carr B) (eq B) ? ?(*(f x) y*)}. - ##[##2: napply (f x); ##|##3: napply y] - #a; #a'; #H; nwhd; nnormalize; (* per togliere setoid1_of_setoid *) napply (mk_iff ????); - *; #x; #Hx; napply (ex_intro … x) - [ napply (. (#‡(#‡#))); - -ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝ +ndefinition image: ∀A,B. (carr A → carr B) → Ω^A → Ω^B ≝ + λA,B:setoid.λf:carr A → carr B.λSa:Ω^A. + {y | ∃x. x ∈ Sa ∧ eq_rel (carr B) (eq B) (f x) y}. + +ndefinition counter_image: ∀A,B. (carr A → carr B) → Ω^B → Ω^A ≝ λA,B,f,Sb. {x | ∃y. y ∈ Sb ∧ f x = y}. -*) (******************* compatible equivalence relations **********************) nrecord compatible_equivalence_relation (A: setoid) : Type[1] ≝ { rel:> equivalence_relation A; - compatibility: ∀x,x':A. x=x' → eq_rel ? rel x x' (* coercion qui non va *) + compatibility: ∀x,x':A. x=x' → rel x x' }. ndefinition quotient: ∀A. compatible_equivalence_relation A → setoid. - #A; #R; napply mk_setoid - [ napply A - | napply R] + #A; #R; @ A R; nqed. (******************* first omomorphism theorem for sets **********************) ndefinition eqrel_of_morphism: ∀A,B. unary_morphism A B → compatible_equivalence_relation A. - #A; #B; #f; napply mk_compatible_equivalence_relation - [ napply mk_equivalence_relation + #A; #B; #f; @ + [ @ [ napply (λx,y. f x = f y) | #x; napply refl | #x; #y; napply sym | #x; #y; #z; napply trans] -##| #x; #x'; #H; nwhd; napply (.= (†H)); napply refl ] +##| #x; #x'; #H; nwhd; alias symbol "prop1" = "prop1". +napply (.= (†H)); napply refl ] nqed. ndefinition canonical_proj: ∀A,R. unary_morphism A (quotient A R). - #A; #R; napply mk_unary_morphism - [ napply (λx.x) | #a; #a'; #H; napply (compatibility ? R … H) ] + #A; #R; @ + [ napply (λx.x) | #a; #a'; #H; napply (compatibility … R … H) ] nqed. ndefinition quotiented_mor: ∀A,B.∀f:unary_morphism A B. - unary_morphism (quotient ? (eqrel_of_morphism ?? f)) B. - #A; #B; #f; napply mk_unary_morphism + unary_morphism (quotient … (eqrel_of_morphism … f)) B. + #A; #B; #f; @ [ napply f | #a; #a'; #H; nassumption] nqed. nlemma first_omomorphism_theorem_functions1: ∀A,B.∀f: unary_morphism A B. - ∀x. f x = quotiented_mor ??? (canonical_proj ? (eqrel_of_morphism ?? f) x). + ∀x. f x = quotiented_mor … (canonical_proj … (eqrel_of_morphism … f) x). #A; #B; #f; #x; napply refl; nqed. @@ -217,19 +216,43 @@ ndefinition injective ≝ ∀x,x'. x ∈ S → x' ∈ S → f x = f x' → x = x'. nlemma first_omomorphism_theorem_functions2: - ∀A,B.∀f: unary_morphism A B. surjective ?? (Full_set ?) (Full_set ?) (canonical_proj ? (eqrel_of_morphism ?? f)). - #A; #B; #f; nwhd; #y; #Hy; napply (ex_intro … y); napply conj - [ napply I | napply refl] + ∀A,B.∀f: unary_morphism A B. + surjective … (Full_set ?) (Full_set ?) (canonical_proj ? (eqrel_of_morphism … f)). + #A; #B; #f; nwhd; #y; #Hy; @ y; @ I ; napply refl; + (* bug, prova @ I refl *) nqed. nlemma first_omomorphism_theorem_functions3: - ∀A,B.∀f: unary_morphism A B. injective ?? (Full_set ?) (quotiented_mor ?? f). + ∀A,B.∀f: unary_morphism A B. + injective … (Full_set ?) (quotiented_mor … f). #A; #B; #f; nwhd; #x; #x'; #Hx; #Hx'; #K; nassumption. nqed. -nrecord isomorphism (A) (B) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝ +nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : Type[0] ≝ { iso_f:> unary_morphism A B; f_closed: ∀x. x ∈ S → iso_f x ∈ T; - f_sur: surjective ?? S T iso_f; - f_inj: injective ?? S iso_f + f_sur: surjective … S T iso_f; + f_inj: injective … S iso_f }. + +(* +nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝ + { iso_f:> unary_morphism A B; + f_closed: ∀x. x ∈ pc A S → fun1 ?? iso_f x ∈ pc B T}. + + +ncheck (λA:?. + λB:?. + λS:?. + λT:?. + λxxx:isomorphism A B S T. + match xxx + return λxxx:isomorphism A B S T. + ∀x: carr A. + ∀x_72: mem (carr A) (pc A S) x. + mem (carr B) (pc B T) (fun1 A B ((λ_.?) A B S T xxx) x) + with [ mk_isomorphism _ yyy ⇒ yyy ] ). + + ; + }. +*)