From e8fbe5898b3214a5b0c4d48e8c9d1ee55f3415cc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 12 Sep 2010 11:06:39 +0000 Subject: [PATCH] non uniform coercions landed in hints_declaration.ma, setoids and sets library updated accordingly --- .../matita/nlibrary/hints_declaration.ma | 40 +++++++-- .../software/matita/nlibrary/re/re-setoids.ma | 87 ++++++------------- .../matita/nlibrary/sets/categories.ma | 8 +- helm/software/matita/nlibrary/sets/setoids.ma | 19 ++-- .../software/matita/nlibrary/sets/setoids1.ma | 12 ++- helm/software/matita/nlibrary/sets/sets.ma | 81 +++++++++-------- 6 files changed, 129 insertions(+), 118 deletions(-) diff --git a/helm/software/matita/nlibrary/hints_declaration.ma b/helm/software/matita/nlibrary/hints_declaration.ma index 27330da46..3df2db001 100644 --- a/helm/software/matita/nlibrary/hints_declaration.ma +++ b/helm/software/matita/nlibrary/hints_declaration.ma @@ -69,11 +69,35 @@ interpretation "hint_decl_CProp1" 'hint_decl a b = (hint_declaration_CProp1 ? a interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b). interpretation "hint_decl_Type0" 'hint_decl a b = (hint_declaration_Type0 ? a b). -(* little test -naxiom A : Type[0]. -naxiom C : A → A → Type[0]. -ndefinition D ≝ C. -alias symbol "hint_decl" = "hint_decl_Type1". -unification hint 0 ≔ - X, R : A, Y ; Z ≟ X, W ≟ Y ⊢ C X Y ≡ D Z W. -*) +(* Non uniform coercions support *) +nrecord lock2 (S : Type[2]) (s : S) : Type[3] ≝ { + force2 : Type[2]; + lift2 : force2 +}. + +nrecord lock1 (S : Type[1]) (s : S) : Type[2] ≝ { + force1 : Type[1]; + lift1 : force1 +}. + +ncoercion lift1 : ∀S:Type[1].∀s:S.∀l:lock1 S s. force1 S s l ≝ lift1 + on s : ? to force1 ???. + +ncoercion lift2 : ∀S:Type[2].∀s:S.∀l:lock2 S s. force2 S s l ≝ lift2 + on s : ? to force2 ???. + +(* Example of a non uniform coercion declaration + + Type[0] setoid + >---> + MR R + + provided MR = carr R + +unification hint 0 ≔ R : setoid; + MR ≟ carr R, + lock ≟ mk_lock1 Type[0] MR setoid R +(* ---------------------------------------- *) ⊢ + setoid ≡ force1 ? MR lock. + +*) \ No newline at end of file diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma index e69294c96..a340fadf7 100644 --- a/helm/software/matita/nlibrary/re/re-setoids.ma +++ b/helm/software/matita/nlibrary/re/re-setoids.ma @@ -41,6 +41,12 @@ unification hint 0 ≔ S : setoid; (*-----------------------------------------------------------------------*) ⊢ carr X ≡ list T. +unification hint 0 ≔ S,a,b; + R ≟ LIST S, + L ≟ (list S) +(* -------------------------------------------- *) ⊢ + eq_list S a b ≡ eq_rel L (eq0 R) a b. + notation "hvbox(hd break :: tl)" right associative with precedence 47 for @{'cons $hd $tl}. @@ -68,33 +74,9 @@ ntheorem append_nil: ∀A:setoid.∀l:list A.l @ [] = l. ndefinition associative ≝ λA:setoid.λf:A → A → A.∀x,y,z.f x (f y z) = f (f x y) z. -ninductive one : Type[0] ≝ unit : one. - -ndefinition force ≝ - λS:Type[2].λs:S.λT:Type[2].λt:T.λlock:one. - match lock return λ_.Type[2] with [ unit ⇒ T]. - -nlet rec lift (S:Type[2]) (s:S) (T:Type[2]) (t:T) (lock:one) on lock : force S s T t lock ≝ - match lock return λlock.force S s T t lock with [ unit ⇒ t ]. - -ncoercion lift1 : ∀S:Type[1].∀s:S.∀T:Type[1].∀t:T.∀lock:one. force S s T t lock ≝ lift - on s : ? to force ?????. - -ncoercion lift2 : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock ≝ lift - on s : ? to force ?????. - -unification hint 0 ≔ R : setoid; - TR ≟ setoid, MR ≟ (carr R), lock ≟ unit -(* ---------------------------------------- *) ⊢ - setoid ≡ force ?(*Type[0]*) MR TR R lock. - -unification hint 0 ≔ R : setoid1; - TR ≟ setoid1, MR ≟ (carr1 R), lock ≟ unit -(* ---------------------------------------- *) ⊢ - setoid1 ≡ force ? MR TR R lock. ntheorem associative_append: ∀A:setoid.associative (list A) (append A). -#A;#x;#y;#z;nelim x[//|#a;#x1;#H;nnormalize;/2/]nqed. +#A;#x;#y;#z;nelim x[ napply # |#a;#x1;#H;nnormalize;/2/]nqed. interpretation "iff" 'iff a b = (iff a b). @@ -136,6 +118,12 @@ unification hint 0 ≔ ; (*-----------------------------------------------------------------------*) ⊢ carr X ≡ bool. +unification hint 0 ≔ a,b; + R ≟ BOOL, + L ≟ bool +(* -------------------------------------------- *) ⊢ + eq bool a b ≡ eq_rel L (eq0 R) a b. + nrecord Alpha : Type[1] ≝ { acarr :> setoid; eqb: acarr → acarr → bool; @@ -168,6 +156,12 @@ unification hint 0 ≔ A : Alpha; (*-----------------------------------------------------------------------*) ⊢ carr X ≡ (re T). +unification hint 0 ≔ A,a,b; + R ≟ RE A, + L ≟ re A +(* -------------------------------------------- *) ⊢ + eq_re A a b ≡ eq_rel L (eq0 R) a b. + notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}. notation > "a ^ *" non associative with precedence 75 for @{ 'pk $a}. interpretation "star" 'pk a = (k ? a). @@ -186,8 +180,8 @@ interpretation "atom" 'ps a = (s ? a). notation "ϵ" non associative with precedence 90 for @{ 'epsilon }. interpretation "epsilon" 'epsilon = (e ?). -notation "0" non associative with precedence 90 for @{ 'empty }. -interpretation "empty" 'empty = (z ?). +notation "0" non associative with precedence 90 for @{ 'empty_r }. +interpretation "empty" 'empty_r = (z ?). notation > "'lang' S" non associative with precedence 90 for @{ Ω^(list $S) }. notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(list $S) }. @@ -198,16 +192,6 @@ match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ]. nlet rec conjunct S (l : list (list S)) (L : lang S) on l: CProp[0] ≝ match l with [ nil ⇒ True | cons w tl ⇒ w ∈ L ∧ conjunct ? tl L ]. - -ndefinition empty_set : ∀A.Ω^A ≝ λA.{ w | False }. -notation "∅" non associative with precedence 90 for @{'emptyset}. -interpretation "empty set" 'emptyset = (empty_set ?). - -(* -notation "{}" non associative with precedence 90 for @{'empty_lang}. -interpretation "empty lang" 'empty_lang = (empty_lang ?). -*) - ndefinition sing_lang : ∀A:setoid.∀x:A.Ω^A ≝ λS.λx.{ w | x = w }. interpretation "sing lang" 'singl x = (sing_lang ? x). @@ -264,7 +248,7 @@ interpretation "ppatom" 'pp a = (pp ? a). ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S ≝ pc on _p : pitem ? to ∀_:?.?. interpretation "patom" 'ps a = (ps ? a). interpretation "pepsilon" 'epsilon = (pe ?). -interpretation "pempty" 'empty = (pz ?). +interpretation "pempty" 'empty_r = (pz ?). notation > "|term 19 e|" non associative with precedence 70 for @{forget ? $e}. nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝ @@ -293,12 +277,7 @@ notation > "𝐋\p term 70 E" non associative with precedence 75 for @{'L_pi $E} notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'L_pi $E}. interpretation "in_pl" 'L_pi E = (L_pi ? E). -unification hint 0 ≔ S,a,b; - R ≟ LIST S, - L ≟ (list S) -(* -------------------------------------------- *) ⊢ - eq_list S a b ≡ eq_rel L (eq0 R) a b. - +(* The caml, as some patches for it *) ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1. alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2". @@ -314,7 +293,7 @@ unification hint 0 ≔ SS : setoid; (*-----------------------------------------------------------------*) ⊢ list S ≡ carr1 TT. - +(* Ex setoid support *) nlemma Sig: ∀S,T:setoid.∀P: S → (T → CPROP). ∀y,z:T.y = z → (∀x.y=z → P x y = P x z) → (Ex S (λx.P x y)) =_1 (Ex S (λx.P x z)). #S T P y z Q E; @; *; #x Px; @x; nlapply (E x Q); *; /2/; nqed. @@ -351,6 +330,7 @@ nlemma test3 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP. napply (.=_1 (∑ E (λw,H.(H ╪_1 #) ╪_1 #)) ╪_1 #). napply #. nqed. +(* Ex setoid support end *) ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S. #S r; @(𝐋\p r); #w1 w2 E; nelim r; @@ -470,15 +450,6 @@ notation > "• x" non associative with precedence 60 for @{'eclose $x}. ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉. interpretation "reclose" 'eclose x = (reclose ? x). -nlemma cup0 :∀S.∀p:lang S.p ∪ ∅ = p. -#S p; @; #w; ##[*; //| #; @1; //] *; nqed. - -nlemma cupC : ∀S. ∀a,b:lang S.a ∪ b = b ∪ a. -#S a b; @; #w; *; nnormalize; /2/; nqed. - -nlemma cupID : ∀S. ∀a:lang S.a ∪ a = a. -#S a; @; #w; ##[*; //] /2/; nqed. - nlemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) = ϵ b1 ∪ ϵ b2. ##[##2: napply S] #S b1 b2; ncases b1; ncases b2; nchange in match (true || true) with true; @@ -486,13 +457,11 @@ nchange in match (true || false) with true; nchange in match (ϵ true) with {[]}; nchange in match (ϵ false) with ∅; ##[##1,4: napply ((cupID…)^-1); -##| napply ((cup0 S {[]})^-1); -##| napply (.= (cup0 S {[]})^-1); napply cupC; ##] +##| napply ((cup0 ? {[]})^-1); +##| napply (.= (cup0 ? {[]})^-1); napply cupC; ##] nqed. -nlemma cupA : ∀S.∀a,b,c:lang S.a ∪ b ∪ c = a ∪ (b ∪ c). -#S a b c; @; #w; *; /3/; *; /3/; nqed. - +(* XXX move somewere else *) ndefinition if': ∀A,B:CPROP. A = B → A → B. #A B; *; /2/. nqed. diff --git a/helm/software/matita/nlibrary/sets/categories.ma b/helm/software/matita/nlibrary/sets/categories.ma index 38c8129fa..6d57deddb 100644 --- a/helm/software/matita/nlibrary/sets/categories.ma +++ b/helm/software/matita/nlibrary/sets/categories.ma @@ -26,10 +26,6 @@ nrecord category : Type[2] ≝ id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o1) = a }. -notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }. -interpretation "arrows1" 'arrows A B = (unary_morphism1 A B). -interpretation "arrows" 'arrows A B = (unary_morphism A B). - notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }. notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }. @@ -69,7 +65,7 @@ ndefinition TYPE : setoid1. @ setoid; @; ##[ #T1; #T2; alias symbol "eq" = "setoid eq". - napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y)); + napply (∃f:T1 ⇒_0 T2.∃g:T2 ⇒_0 T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y)); ##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #; ##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption; ##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg'; @@ -87,7 +83,7 @@ unification hint 0 ≔ ; nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝ { fun01:1> A → B; - prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a') + prop01: ∀a,a'. eq0 ? a a' → eq1 ? (fun01 a) (fun01 a') }. interpretation "prop01" 'prop1 c = (prop01 ????? c). diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma index f633470ed..e593ea7d5 100644 --- a/helm/software/matita/nlibrary/sets/setoids.ma +++ b/helm/software/matita/nlibrary/sets/setoids.ma @@ -21,6 +21,13 @@ nrecord setoid : Type[1] ≝ { eq0: equivalence_relation carr }. +(* activate non uniform coercions on: Type → setoid *) +unification hint 0 ≔ R : setoid; + MR ≟ carr R, + lock ≟ mk_lock1 Type[0] MR setoid R +(* ---------------------------------------- *) ⊢ + setoid ≡ force1 ? MR lock. + interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y). notation > "hvbox(a break =_0 b)" non associative with precedence 45 @@ -94,11 +101,13 @@ unification hint 0 ≔ o1,o2,o3:setoid,f:o2 ⇒_0 o3,g:o1 ⇒_0 o2; (* -------------------------------------------------------------------- *) ⊢ fun1 ?? R ≡ (composition … f g). -ndefinition comp_binary_morphisms: - ∀o1,o2,o3. - (unary_morph_setoid o2 o3) ⇒_0 - (unary_morph_setoid (unary_morph_setoid o1 o2) (unary_morph_setoid o1 o3)). +ndefinition comp_binary_morphisms: + ∀o1,o2,o3.(o2 ⇒_0 o3) ⇒_0 ((o1 ⇒_0 o2) ⇒_0 (o1 ⇒_0 o3)). #o1; #o2; #o3; napply mk_binary_morphism - [ #f; #g; napply (comp_unary_morphisms … f g) (*CSC: why not ∘?*) + [ #f; #g; napply (comp_unary_morphisms ??? f g) + (* CSC: why not ∘? + GARES: because the coercion to FunClass is not triggered if there + are no "extra" arguments. We could fix that in the refiner + *) | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ] nqed. diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma index 622c9401d..4ab57d568 100644 --- a/helm/software/matita/nlibrary/sets/setoids1.ma +++ b/helm/software/matita/nlibrary/sets/setoids1.ma @@ -21,6 +21,12 @@ nrecord setoid1: Type[2] ≝ { eq1: equivalence_relation1 carr1 }. +unification hint 0 ≔ R : setoid1; + MR ≟ (carr1 R), + lock ≟ mk_lock2 Type[1] MR setoid1 R +(* ---------------------------------------- *) ⊢ + setoid1 ≡ force2 ? MR lock. + ndefinition setoid1_of_setoid: setoid → setoid1. #s; @ (carr s); @ (eq0…) (refl…) (sym…) (trans…); nqed. @@ -102,10 +108,8 @@ unification hint 0 ≔ o1,o2,o3:setoid1,f:o2 ⇒_1 o3,g:o1 ⇒_1 o2; fun11 ?? R ≡ (composition1 … f g). ndefinition comp1_binary_morphisms: - ∀o1,o2,o3. - (unary_morphism1_setoid1 o2 o3) ⇒_1 - (unary_morphism1_setoid1 (unary_morphism1_setoid1 o1 o2) (unary_morphism1_setoid1 o1 o3)). + ∀o1,o2,o3. (o2 ⇒_1 o3) ⇒_1 ((o1 ⇒_1 o2) ⇒_1 (o1 ⇒_1 o3)). #o1; #o2; #o3; napply mk_binary_morphism1 - [ #f; #g; napply (comp1_unary_morphisms … f g) (*CSC: why not ∘?*) + [ #f; #g; napply (comp1_unary_morphisms … f g) | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ] nqed. diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index 544db6a56..dcb740921 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -62,8 +62,6 @@ ndefinition powerclass_setoid: Type[0] → setoid1. #A; @(Ω^A);//. nqed. -include "hints_declaration.ma". - alias symbol "hint_decl" = "hint_decl_Type2". unification hint 0 ≔ A; R ≟ (mk_setoid1 (Ω^A) (eq1 (powerclass_setoid A))) @@ -108,10 +106,10 @@ unification hint 0 ≔ A; carr1 R ≡ ext_powerclass A. nlemma mem_ext_powerclass_setoid_is_morph: - ∀A. (setoid1_of_setoid A) ⇒_1 (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/. + ∀A. (setoid1_of_setoid A) ⇒_1 ((𝛀^A) ⇒_1 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 ≔ AA, x, S; @@ -135,9 +133,7 @@ nlemma set_ext : ∀S.∀A,B:Ω^S.A =_1 B → ∀x:S.(x ∈ A) =_1 (x ∈ B). nlemma ext_set : ∀S.∀A,B:Ω^S.(∀x:S. (x ∈ A) = (x ∈ B)) → A = B. #S A B H; @; #x; ncases (H x); #H1 H2; ##[ napply H1 | napply H2] nqed. -nlemma subseteq_is_morph: ∀A. - (ext_powerclass_setoid A) ⇒_1 - (unary_morphism1_setoid1 (ext_powerclass_setoid A) CPROP). +nlemma subseteq_is_morph: ∀A. 𝛀^A ⇒_1 𝛀^A ⇒_1 CPROP. #A; napply (mk_binary_morphism1 … (λS,S':𝛀^A. S ⊆ S')); #a; #a'; #b; #b'; *; #H1; #H2; *; /5/ by mk_iff, sym1, subseteq_trans; nqed. @@ -161,11 +157,10 @@ unification hint 0 ≔ 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. (powerclass_setoid A) ⇒_1 (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/. + +nlemma intersect_is_morph: ∀A. Ω^A ⇒_1 Ω^A ⇒_1 Ω^A. +#A; napply (mk_binary_morphism1 … (λS,S'. S ∩ S')); +#a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #x; nnormalize; *;/3/. nqed. alias symbol "hint_decl" = "hint_decl_Type1". @@ -180,10 +175,7 @@ interpretation "prop21 ext" 'prop2 l r = (prop11 (ext_powerclass_setoid ?) (unary_morphism1_setoid1 (ext_powerclass_setoid ?) ?) ? ?? l ?? r). -nlemma intersect_is_ext_morph: - ∀A. - (ext_powerclass_setoid A) ⇒_1 - (unary_morphism1_setoid1 (ext_powerclass_setoid A) (ext_powerclass_setoid A)). +nlemma intersect_is_ext_morph: ∀A. 𝛀^A ⇒_1 𝛀^A ⇒_1 𝛀^A. #A; napply (mk_binary_morphism1 … (intersect_is_ext …)); #a; #a'; #b; #b'; #Ha; #Hb; napply (prop11 … (intersect_is_morph A)); nassumption. nqed. @@ -203,9 +195,7 @@ unification hint 1 ≔ (* ------------------------------------------------------*) ⊢ ext_carr AA (R B C) ≡ intersect A BB CC. -nlemma union_is_morph : - ∀A. (powerclass_setoid A) ⇒_1 (unary_morphism1_setoid1 (powerclass_setoid A) (powerclass_setoid A)). -(*XXX ∀A.Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A). avec non-unif-coerc*) +nlemma union_is_morph : ∀A. Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A). #X; napply (mk_binary_morphism1 … (λA,B.A ∪ B)); #A1 A2 B1 B2 EA EB; napply ext_set; #x; nchange in match (x ∈ (A1 ∪ B1)) with (?∨?); @@ -235,10 +225,7 @@ unification hint 0 ≔ S:Type[0], A,B:Ω^S; (*--------------------------------------------------------------------------*) ⊢ fun11 ?? (fun11 ?? MM A) B ≡ A ∪ B. -nlemma union_is_ext_morph:∀A. - (ext_powerclass_setoid A) ⇒_1 - (unary_morphism1_setoid1 (ext_powerclass_setoid A) (ext_powerclass_setoid A)). -(*XXX ∀A:setoid.𝛀^A ⇒_1 (𝛀^A ⇒_1 𝛀^A). with coercion non uniformi *) +nlemma union_is_ext_morph:∀A.𝛀^A ⇒_1 𝛀^A ⇒_1 𝛀^A. #A; napply (mk_binary_morphism1 … (union_is_ext …)); #x1 x2 y1 y2 Ex Ey; napply (prop11 … (union_is_morph A)); nassumption. nqed. @@ -386,16 +373,6 @@ nrecord isomorphism (A, B : setoid) (S: ext_powerclass A) (T: ext_powerclass B) f_inj: injective … S iso_f }. -nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W. -#A; #U; #V; #W; *; #H; #x; *; /2/. -nqed. - -nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W. -#A; #U; #V; #W; #H; #H1; #x; *; /2/. -nqed. - -nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V. -/3/. nqed. (* nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝ @@ -417,4 +394,36 @@ ncheck (λA:?. ; }. -*) \ No newline at end of file +*) + +(* Set theory *) + +nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W. +#A; #U; #V; #W; *; #H; #x; *; /2/. +nqed. + +nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W. +#A; #U; #V; #W; #H; #H1; #x; *; /2/. +nqed. + +nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V. +/3/. nqed. + +nlemma cupC : ∀S. ∀a,b:Ω^S.a ∪ b = b ∪ a. +#S a b; @; #w; *; nnormalize; /2/; nqed. + +nlemma cupID : ∀S. ∀a:Ω^S.a ∪ a = a. +#S a; @; #w; ##[*; //] /2/; nqed. + +(* XXX Bug notazione \cup, niente parentesi *) +nlemma cupA : ∀S.∀a,b,c:Ω^S.a ∪ b ∪ c = a ∪ (b ∪ c). +#S a b c; @; #w; *; /3/; *; /3/; nqed. + +ndefinition Empty_set : ∀A.Ω^A ≝ λA.{ x | False }. + +notation "∅" non associative with precedence 90 for @{ 'empty }. +interpretation "empty set" 'empty = (Empty_set ?). + +nlemma cup0 :∀S.∀A:Ω^S.A ∪ ∅ = A. +#S p; @; #w; ##[*; //| #; @1; //] *; nqed. + -- 2.39.2