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=f94c94d9cba79e2c7ad10d8a25753a3e408ade0a;hpb=a0c0e92cee3ed99995e12b02f18e30f018d946ea;p=helm.git diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index f94c94d9c..4e7418fd9 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -28,213 +28,231 @@ 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.λT:Type[0].λf:T → Ω \sup A.{ x | ∃i. x ∈ f i }. +ndefinition big_union ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∃i. i ∈ T ∧ x ∈ f i }. -ndefinition big_intersection ≝ λA.λT:Type[0].λf:T → Ω \sup A.{ x | ∀i. 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 }. -(* bug dichiarazione coercion qui *) -(* 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. -unification hint 0 (∀A. (λx,y.True) (carr1 (powerclass_setoid A)) (Ω \sup A)). +include "hints_declaration.ma". + +alias symbol "hint_decl" = "hint_decl_Type2". +unification hint 0 ≔ A ⊢ carr1 (powerclass_setoid A) ≡ Ω^A. (************ SETS OVER SETOIDS ********************) include "logic/cprop.ma". nrecord qpowerclass (A: setoid) : Type[1] ≝ - { pc:> Ω \sup 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 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. eq_rel1 ? (eq1 (powerclass_setoid 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. (λx,y.True) (carr1 (qpowerclass_setoid A)) (qpowerclass A)). -ncoercion qpowerclass_hint: ∀A: setoid. ∀S: qpowerclass_setoid A. Ω \sup A ≝ λA.λS.S - on _S: (carr1 (qpowerclass_setoid ?)) to (Ω \sup ?). +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 - [ napply (λx.λS: qpowerclass_setoid A. x ∈ S) (* CSC: ??? *) - | #a; #a'; #b; #b'; #Ha; #Hb; (* CSC: qui *; non funziona *) - nwhd; nwhd in ⊢ (? (? % ??) (? % ??)); napply mk_iff; #H - [ ncases Hb; #Hb1; #_; napply Hb1; napply (. (mem_ok' …)) - [ nassumption | napply Ha^-1 | ##skip ] - ##| ncases Hb; #_; #Hb2; napply Hb2; napply (. (mem_ok' …)) - [ nassumption | napply Ha | ##skip ]##] -nqed. - -unification hint 0 (∀A,x,S. (λx,y.True) (fun21 ??? (mem_ok A) x S) (mem A S x)). - + #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; + 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 - [ napply (subseteq_trans … a' a) (* anche qui, perche' serve a'? *) - [ nassumption | napply (subseteq_trans … a b); nassumption ] - ##| napply (subseteq_trans … a a') (* anche qui, perche' serve a'? *) - [ nassumption | napply (subseteq_trans … a' b'); nassumption ] ##] + #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 |##1,4: nassumption |##*: ##skip] - ##|##3,4: napply (. (mem_ok' …)) [##2,5: nassumption |##1,4: 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. -unification hint 0 (∀A.∀U,V.(λx,y.True) (fun21 ??? (intersect_ok A) U V) (intersect A U V)). +(* unfold if intersect, exposing fun21 *) +alias symbol "hint_decl" = "hint_decl_Type1". +unification hint 0 ≔ + 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. -ndefinition surjective ≝ λA,B.λf:unary_morphism A B. ∀y.∃x. f x = y. +ndefinition surjective ≝ + λA,B.λS: qpowerclass A.λT: qpowerclass B.λf:unary_morphism A B. + ∀y. y ∈ T → ∃x. x ∈ S ∧ f x = y. -ndefinition injective ≝ λA,B.λf:unary_morphism A B. ∀x,x'. f x = f x' → x = x'. +ndefinition injective ≝ + λA,B.λS: qpowerclass A.λf:unary_morphism A B. + ∀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 ?? (canonical_proj ? (eqrel_of_morphism ?? f)). - #A; #B; #f; nwhd; #y; napply (ex_intro … y); 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 ?? (quotiented_mor ?? f). - #A; #B; #f; nwhd; #x; #x'; #H; nassumption. + ∀A,B.∀f: unary_morphism A B. + injective … (Full_set ?) (quotiented_mor … f). + #A; #B; #f; nwhd; #x; #x'; #Hx; #Hx'; #K; nassumption. nqed. -(************************** partitions ****************************) - -nrecord partition (A: Type[0]) : Type[1] ≝ - { index_set: setoid; - class: index_set → Ω \sup A; - disjoint: ∀i,j. ¬ (i = j) → ¬(class i ≬ class j); - covers: big_union ?? class = full_set A +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 }. (* -nrecord has_card (A: Type[0]) (S: Ω \sup A) (n: nat) : Prop ≝ - { f: ∀m:nat. m < n → S; - f_inj: injective ?? f; - f_sur: surjective ?? 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 ] ). + + ; }. - -nlemma subset_of_finite: - ∀A. ∃n. has_card ? (full_subset A) n → ∀S. ∃m. has_card ? S m. -nqed. - -nlemma partition_splits_card: - ∀A. ∀P: partition A. ∀s: index_set P → nat. - (∀i. has_card ? (class i) = s i) → - has_card ? (full_subset A) (big_plus ? (λi. s i)). -nqed. -*) \ No newline at end of file +*)