From: Enrico Tassi Date: Fri, 2 Oct 2009 17:58:31 +0000 (+0000) Subject: hints fixed X-Git-Tag: make_still_working~3392 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d446c5ce6678ab367e26b76a7be522241fb17fc2;p=helm.git hints fixed --- diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index b09c206ab..f230957a7 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -77,27 +77,27 @@ unification hint 0 ≔ A ⊢ carr1 (mk_setoid1 (Ω^A) (eq1 (powerclass_setoid A) include "logic/cprop.ma". -nrecord qpowerclass (A: setoid) : Type[1] ≝ - { pc:> Ω^A; (* qui pc viene dichiarato con un target preciso... +nrecord ext_powerclass (A: setoid) : Type[1] ≝ + { ext_carr:> Ω^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) + ext_prop: ∀x,x':A. x=x' → (x ∈ ext_carr) = (x' ∈ ext_carr) }. notation > "𝛀 ^ term 90 A" non associative with precedence 70 -for @{ 'qpowerclass $A }. +for @{ 'ext_powerclass $A }. notation "Ω term 90 A \atop ≈" non associative with precedence 70 -for @{ 'qpowerclass $A }. +for @{ 'ext_powerclass $A }. -interpretation "qpowerclass" 'qpowerclass a = (qpowerclass a). +interpretation "extensional powerclass" 'ext_powerclass a = (ext_powerclass 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 ?. +ncoercion Full_set: ∀A. ext_powerclass A ≝ Full_set on A: setoid to ext_powerclass ?. -ndefinition qseteq: ∀A. equivalence_relation1 (𝛀^A). +ndefinition ext_seteq: ∀A. equivalence_relation1 (𝛀^A). #A; @ [ napply (λS,S'. S = S') | #S; napply (refl1 ? (seteq A)) @@ -105,40 +105,46 @@ ndefinition qseteq: ∀A. equivalence_relation1 (𝛀^A). | #S; #T; #U; napply (trans1 ? (seteq A))] nqed. -ndefinition qpowerclass_setoid: setoid → setoid1. +ndefinition ext_powerclass_setoid: setoid → setoid1. #A; @ - [ napply (qpowerclass A) - | napply (qseteq A) ] + [ napply (ext_powerclass A) + | napply (ext_seteq A) ] nqed. -unification hint 0 ≔ A ⊢ - carr1 (mk_setoid1 (𝛀^A) (eq1 (qpowerclass_setoid A))) -≡ qpowerclass A. +unification hint 0 ≔ A; + R ≟ (mk_setoid1 (𝛀^A) (eq1 (ext_powerclass_setoid A))) + (* ----------------------------------------------------- *) ⊢ + carr1 R ≡ ext_powerclass A. -ncoercion pc' : ∀A.∀x:qpowerclass_setoid A. Ω^A ≝ pc -on _x : (carr1 (qpowerclass_setoid ?)) to (Ω^?). + +(* +ncoercion ext_carr' : ∀A.∀x:ext_powerclass_setoid A. Ω^A ≝ ext_carr +on _x : (carr1 (ext_powerclass_setoid ?)) to (Ω^?). +*) -nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP. +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 (. (mem_ok' …)); ##[##3: napply H| napply Ha^-1;##] - ##| napply Hb2; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha;##] + ##[ napply Hb1; napply (. (ext_prop … Ha^-1)); nassumption; + ##| napply Hb2; napply (. (ext_prop … Ha)); nassumption; ##] ##] nqed. unification hint 0 ≔ A:setoid, x, S; - SS ≟ (pc ? S), - TT ≟ (mk_binary_morphism1 ??? - (λx:setoid1_of_setoid ?.λS:qpowerclass_setoid ?. x ∈ S) - (prop21 ??? (mem_ok A))) - + 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))), + M1 ≟ ?, + M2 ≟ ?, + M3 ≟ ? (*-------------------------------------*) ⊢ - fun21 ? ? ? TT x S - ≡ mem A SS x. + fun21 M1 M2 M3 TT x S ≡ mem A SS x. -nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP. +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; *; #Hb1; #Hb2; @; #H @@ -152,7 +158,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. 𝛀^A → 𝛀^A → 𝛀^A. +nlemma intersect_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A. #A; #S; #S'; @ (S ∩ S'); #a; #a'; #Ha; @; *; #H1; #H2; @ [##1,2: napply (. Ha^-1‡#); nassumption; @@ -160,19 +166,15 @@ nlemma intersect_ok: ∀A. 𝛀^A → 𝛀^A → 𝛀^A. nqed. alias symbol "hint_decl" = "hint_decl_Type1". -unification hint 1 ≔ - A : setoid, B,C : qpowerclass A ⊢ - pc A (mk_qpowerclass ? (B ∩ C) (mem_ok' ? (intersect_ok ? B C))) - ≡ intersect ? (pc ? B) (pc ? C). - -unification hint 1 ≔ - A : setoid, B,C : qpowerclass A; - DX ≟ (intersect ? (pc ? B) (pc ? C)), - SX ≟ (mk_qpowerclass ? (B ∩ C) (mem_ok' ? (intersect_ok ? B C))) - (*-----------------------------------------------------------------*) ⊢ - pc A SX ≡ DX. - -nlemma intersect_ok': ∀A. binary_morphism1 (powerclass_setoid A) (powerclass_setoid A) (powerclass_setoid A). +unification hint 0 ≔ + A : setoid, B,C : ext_powerclass A; + R ≟ (mk_ext_powerclass ? (B ∩ C) (ext_prop ? (intersect_is_ext ? B C))) + + (* ------------------------------------------*) ⊢ + 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'); #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #x; nnormalize; *; #Ka; #Kb; @ [ napply Ha1; nassumption @@ -183,37 +185,46 @@ nqed. alias symbol "hint_decl" = "hint_decl_Type1". unification hint 0 ≔ - A : Type[0], B,C : powerclass A ⊢ - fun21 … - (mk_binary_morphism1 … + A : Type[0], B,C : Ω^A; + R ≟ (mk_binary_morphism1 … (λS,S'.S ∩ S') - (prop21 … (intersect_ok' A))) B C - ≡ intersect ? B C. + (prop21 … (intersect_is_morph A))) + ⊢ + fun21 (powerclass_setoid A) (powerclass_setoid A) (powerclass_setoid A) R B C + ≡ intersect ? B C. ndefinition prop21_mem : - ∀A,C.∀f:binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) C. + ∀A,C.∀f:binary_morphism1 (setoid1_of_setoid A) (ext_powerclass_setoid A) C. ∀a,a':setoid1_of_setoid A. - ∀b,b':qpowerclass_setoid A.a = a' → b = b' → f a b = f a' b'. + ∀b,b':ext_powerclass_setoid A.a = a' → b = b' → f a b = f a' b'. #A; #C; #f; #a; #a'; #b; #b'; #H1; #H2; napply prop21; nassumption; 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; +nlemma intersect_is_ext_morph: + ∀A. binary_morphism1 (ext_powerclass_setoid A) (ext_powerclass_setoid A) (ext_powerclass_setoid A). + #A; @ (intersect_is_ext …); nlapply (prop21 … (intersect_is_morph 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. - + A:setoid, B,C : 𝛀^A; + R ≟ (mk_binary_morphism1 (ext_powerclass_setoid A) (ext_powerclass_setoid A) (ext_powerclass_setoid A) + (λS,S':carr1 (ext_powerclass_setoid A). + mk_ext_powerclass A (S∩S') (ext_prop A (intersect_is_ext ? S S'))) + (prop21 … (intersect_is_ext_morph A))) , + BB ≟ (ext_carr ? B), + CC ≟ (ext_carr ? C) + (* ------------------------------------------------------*) ⊢ + ext_carr A + (fun21 + (ext_powerclass_setoid A) + (ext_powerclass_setoid A) + (ext_powerclass_setoid A) R B C) ≡ + intersect (carr A) BB CC. +(* nlemma test: ∀U.∀A,B:qpowerclass U. A ∩ B = A → @@ -354,3 +365,4 @@ ncheck (λA:?. ; }. *) +*) \ No newline at end of file