From: Enrico Tassi Date: Tue, 29 Sep 2009 14:03:50 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~3420 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a5a3d944e528c6006f0ea901dded7c79367adb75;p=helm.git ... --- diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index c21751c21..b644c4f42 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -83,13 +83,21 @@ nrecord qpowerclass (A: setoid) : Type[1] ≝ ma la sintassi :> non lo supporta *) mem_ok': ∀x,x':A. x=x' → (x ∈ pc) = (x' ∈ pc) }. + +notation > "𝛀 ^ term 90 A" non associative with precedence 70 +for @{ 'qpowerclass $A }. -ndefinition Full_set: ∀A. qpowerclass A. +notation "Ω term 90 A \atop ≈" non associative with precedence 70 +for @{ 'qpowerclass $A }. + +interpretation "qpowerclass" 'qpowerclass a = (qpowerclass a). + +ndefinition Full_set: ∀A. 𝛀^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). +ndefinition qseteq: ∀A. equivalence_relation1 (𝛀^A). #A; @ [ napply (λS,S'. S = S') | #S; napply (refl1 ? (seteq A)) @@ -104,7 +112,7 @@ ndefinition qpowerclass_setoid: setoid → setoid1. nqed. unification hint 0 ≔ A ⊢ - carr1 (mk_setoid1 (qpowerclass A) (eq1 (qpowerclass_setoid A))) + carr1 (mk_setoid1 (𝛀^A) (eq1 (qpowerclass_setoid A))) ≡ qpowerclass A. ncoercion pc' : ∀A.∀x:qpowerclass_setoid A. Ω^A ≝ pc @@ -144,7 +152,7 @@ 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. qpowerclass A → qpowerclass A → qpowerclass A. +nlemma intersect_ok: ∀A. 𝛀^A → 𝛀^A → 𝛀^A. #A; #S; #S'; @ (S ∩ S'); #a; #a'; #Ha; @; *; #H1; #H2; @ [##1,2: napply (. Ha^-1‡#); nassumption; @@ -183,11 +191,32 @@ ndefinition prop21_mem : nqed. interpretation "prop21 mem" 'prop2 l r = (prop21_mem ??????? l r). + +nlemma intersect_ok'': + ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) (qpowerclass_setoid A). + #A; @ (intersect_ok A); nlapply (prop21 … (intersect_ok' A)); #H; + #a; #a'; #b; #b'; #H1; #H2; napply H; nassumption; +nqed. + +unification hint 1 ≔ + A:?, B,C : 𝛀^A ⊢ + fun21 … + (mk_binary_morphism1 … + (λS,S':qpowerclass_setoid A.S ∩ S') + (prop21 … (intersect_ok'' A))) B C + ≡ intersect ? B C. + + nlemma test: ∀U.∀A,B:qpowerclass U. A ∩ B = A → ∀x,y. x=y → x ∈ A → y ∈ A ∩ B. - #U; #A; #B; #H; #x; #y; #K; #K2; napply (. K^-1‡(H^-1‡#)); nassumption; + #U; #A; #B; #H; #x; #y; #K; #K2; + alias symbol "prop2" = "prop21". +alias symbol "invert" = "setoid1 symmetry". +napply (. (K^-1 ‡ (prop21 ??? (intersect_ok'' U) ???? H^-1 #))); STOP + + napply (. K^-1‡(H^-1‡#)); nassumption; nqed. (*