matitaB/matita/nlibrary/sets/sets.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (******************* SETS OVER TYPES *****************)
  16
  17 include "logic/connectives.ma".
  18
  19 record powerclass (A: Type[0]) : Type[1] ≝ { mem: A → CProp[0] }.
  20
  21 interpretation "mem" 'mem a S = (mem ? S a).
  22 interpretation "powerclass" 'powerset A = (powerclass A).
  23 interpretation "subset construction" 'subset \eta.x = (mk_powerclass ? x).
  24
  25 definition subseteq ≝ λA.λU,V.∀a:A. a ∈ U → a ∈ V.
  26 interpretation "subseteq" 'subseteq U V = (subseteq ? U V).
  27
  28 definition overlaps ≝ λA.λU,V.∃x:A.x ∈ U ∧ x ∈ V.
  29 interpretation "overlaps" 'overlaps U V = (overlaps ? U V).
  30
  31 definition intersect ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ x ∈ V }.
  32 interpretation "intersect" 'intersects U V = (intersect ? U V).
  33
  34 definition union ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∨ x ∈ V }.
  35 interpretation "union" 'union U V = (union ? U V).
  36
  37 definition substract ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ ¬ x ∈ V }.
  38 interpretation "substract" 'minus U V = (substract ? U V).
  39
  40
  41 definition big_union ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∃i. i ∈ T ∧ x ∈ f i }.
  42
  43 definition big_intersection ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∀i. i ∈ T → x ∈ f i }.
  44
  45 definition full_set: ∀A. Ω^A ≝ λA.{ x | True }.
  46
  47 lemma subseteq_refl: ∀A.∀S: Ω^A. S ⊆ S.
  48 //.qed.
  49
  50 lemma subseteq_trans: ∀A.∀S,T,U: Ω^A. S ⊆ T → T ⊆ U → S ⊆ U.
  51 /3/.qed.
  52
  53 include "properties/relations1.ma".
  54
  55 definition seteq: ∀A. equivalence_relation1 (Ω^A).
  56 #A % [@(λS,S'. S ⊆ S' ∧ S' ⊆ S)]
  57 /2/[ #A #B * /3/]
  58 #S #T #U * #H1 #H2 * /4/
  59 qed.
  60
  61 include "sets/setoids1.ma".
  62
  63 ndefinition singleton ≝ λA:setoid.λa:A.{ x | a = x }.
  64 interpretation "singl" 'singl a = (singleton ? a).
  65
  66 (* this has to be declared here, so that it is combined with carr *)
  67 ncoercion full_set : ∀A:Type[0]. Ω^A ≝ full_set on A: Type[0] to (Ω^?).
  68
  69 ndefinition powerclass_setoid: Type[0] → setoid1.
  70  #A; @(Ω^A);//.
  71 nqed.
  72
  73 alias symbol "hint_decl" = "hint_decl_Type2".
  74 unification hint 0 ≔ A;
  75   R ≟ (mk_setoid1 (Ω^A) (eq1 (powerclass_setoid A)))
  76 (*--------------------------------------------------*)⊢
  77      carr1 R ≡ Ω^A.
  78
  79 (************ SETS OVER SETOIDS ********************)
  80
  81 include "logic/cprop.ma".
  82
  83 nrecord ext_powerclass (A: setoid) : Type[1] ≝ {
  84    ext_carr:> Ω^A; (* qui pc viene dichiarato con un target preciso...
  85                       forse lo si vorrebbe dichiarato con un target più lasco
  86                       ma la sintassi :> non lo supporta *)
  87    ext_prop: ∀x,x':A. x=x' → (x ∈ ext_carr) = (x' ∈ ext_carr)
  88 }.
  89
  90 notation > "𝛀 ^ term 90 A" non associative with precedence 70
  91 for @{ 'ext_powerclass $A }.
  92
  93 notation < "Ω term 90 A \atop ≈" non associative with precedence 90
  94 for @{ 'ext_powerclass $A }.
  95
  96 interpretation "extensional powerclass" 'ext_powerclass a = (ext_powerclass a).
  97
  98 ndefinition Full_set: ∀A. 𝛀^A.
  99  #A; @[ napply A | #x; #x'; #H; napply refl1]
 100 nqed.
 101 ncoercion Full_set: ∀A. ext_powerclass A ≝ Full_set on A: setoid to ext_powerclass ?.
 102
 103 ndefinition ext_seteq: ∀A. equivalence_relation1 (𝛀^A).
 104  #A; @ [ napply (λS,S'. S = S') ] /2/.
 105 nqed.
 106
 107 ndefinition ext_powerclass_setoid: setoid → setoid1.
 108  #A; @ (ext_seteq A).
 109 nqed.
 110
 111 unification hint 0 ≔ A;
 112       R ≟ (mk_setoid1 (𝛀^A) (eq1 (ext_powerclass_setoid A)))
 113   (* ----------------------------------------------------- *) ⊢
 114                  carr1 R ≡ ext_powerclass A.
 115
 116 nlemma mem_ext_powerclass_setoid_is_morph:
 117  ∀A. (setoid1_of_setoid A) ⇒_1 ((𝛀^A) ⇒_1 CPROP).
 118 #A; napply (mk_binary_morphism1 … (λx:setoid1_of_setoid A.λS: 𝛀^A. x ∈ S));
 119 #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; @; #H
 120 [ napply (. (ext_prop … Ha^-1)) | napply (. (ext_prop … Ha)) ] /2/.
 121 nqed.
 122
 123 unification hint 0 ≔  AA : setoid, S : 𝛀^AA, x : carr AA;
 124      A ≟ carr AA,
 125      SS ≟ (ext_carr ? S),
 126      TT ≟ (mk_unary_morphism1 ??
 127              (λx:carr1 (setoid1_of_setoid ?).
 128                mk_unary_morphism1 ??
 129                  (λS:carr1 (ext_powerclass_setoid ?). x ∈ (ext_carr ? S))
 130                  (prop11 ?? (fun11 ?? (mem_ext_powerclass_setoid_is_morph AA) x)))
 131              (prop11 ?? (mem_ext_powerclass_setoid_is_morph AA))),
 132      T2 ≟ (ext_powerclass_setoid AA)
 133 (*---------------------------------------------------------------------------*) ⊢
 134     fun11 T2 CPROP (fun11 (setoid1_of_setoid AA) (unary_morphism1_setoid1 T2 CPROP) TT x) S ≡ mem A SS x.
 135
 136 nlemma set_ext : ∀S.∀A,B:Ω^S.A =_1 B → ∀x:S.(x ∈ A) =_1 (x ∈ B).
 137 #S A B; *; #H1 H2 x; @; ##[ napply H1 | napply H2] nqed.
 138
 139 nlemma ext_set : ∀S.∀A,B:Ω^S.(∀x:S. (x ∈ A) = (x ∈ B)) → A = B.
 140 #S A B H; @; #x; ncases (H x); #H1 H2; ##[ napply H1 | napply H2] nqed.
 141
 142 nlemma subseteq_is_morph: ∀A.  𝛀^A ⇒_1 𝛀^A ⇒_1 CPROP.
 143  #A; napply (mk_binary_morphism1 … (λS,S':𝛀^A. S ⊆ S'));
 144  #a; #a'; #b; #b'; *; #H1; #H2; *; /5/ by mk_iff, sym1, subseteq_trans;
 145 nqed.
 146
 147 (* hints for ∩ *)
 148 nlemma intersect_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
 149 #S A B; @ (A ∩ B); #x y Exy; @; *; #H1 H2; @;
 150 ##[##1,2: napply (. Exy^-1╪_1#); nassumption;
 151 ##|##3,4: napply (. Exy‡#); nassumption]
 152 nqed.
 153
 154 alias symbol "hint_decl" = "hint_decl_Type1".
 155 unification hint 0 ≔ A : setoid, B,C : 𝛀^A;
 156   AA ≟ carr A,
 157   BB ≟ ext_carr ? B,
 158   CC ≟ ext_carr ? C,
 159   R ≟ (mk_ext_powerclass ?
 160         (ext_carr ? B ∩ ext_carr ? C)
 161         (ext_prop ? (intersect_is_ext ? B C)))
 162   (* ------------------------------------------*)  ⊢
 163     ext_carr A R ≡ intersect AA BB CC.
 164
 165 nlemma intersect_is_morph: ∀A. Ω^A ⇒_1 Ω^A ⇒_1 Ω^A.
 166 #A; napply (mk_binary_morphism1 … (λS,S'. S ∩ S'));
 167 #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #x; nnormalize; *;/3/.
 168 nqed.
 169
 170 alias symbol "hint_decl" = "hint_decl_Type1".
 171 unification hint 0 ≔ A : Type[0], B,C : Ω^A;
 172   T ≟ powerclass_setoid A,
 173   R ≟ mk_unary_morphism1 ??
 174        (λX. mk_unary_morphism1 ??
 175          (λY.X ∩ Y) (prop11 ?? (fun11 ?? (intersect_is_morph A) X)))
 176        (prop11 ?? (intersect_is_morph A))
 177 (*------------------------------------------------------------------------*) ⊢
 178     fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C  ≡ intersect A B C.
 179
 180 interpretation "prop21 ext" 'prop2 l r =
 181  (prop11 (ext_powerclass_setoid ?)
 182   (unary_morphism1_setoid1 (ext_powerclass_setoid ?) ?) ? ?? l ?? r).
 183
 184 nlemma intersect_is_ext_morph: ∀A. 𝛀^A ⇒_1 𝛀^A ⇒_1 𝛀^A.
 185  #A; napply (mk_binary_morphism1 … (intersect_is_ext …));
 186  #a; #a'; #b; #b'; #Ha; #Hb; napply (prop11 … (intersect_is_morph A)); nassumption.
 187 nqed.
 188
 189 unification hint 1 ≔
 190       AA : setoid, B,C : 𝛀^AA;
 191       A ≟ carr AA,
 192       T ≟ ext_powerclass_setoid AA,
 193       R ≟ (mk_unary_morphism1 ?? (λX:𝛀^AA.
 194                mk_unary_morphism1 ?? (λY:𝛀^AA.
 195                   mk_ext_powerclass AA
 196                     (ext_carr ? X ∩ ext_carr ? Y)
 197                     (ext_prop AA (intersect_is_ext ? X Y)))
 198                 (prop11 ?? (fun11 ?? (intersect_is_ext_morph AA) X)))
 199               (prop11 ?? (intersect_is_ext_morph AA))) ,
 200        BB ≟ (ext_carr ? B),
 201        CC ≟ (ext_carr ? C)
 202    (* ---------------------------------------------------------------------------------------*) ⊢
 203       ext_carr AA (fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C) ≡ intersect A BB CC.
 204
 205
 206 (* hints for ∪ *)
 207 nlemma union_is_morph : ∀A. Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A).
 208 #X; napply (mk_binary_morphism1 … (λA,B.A ∪ B));
 209 #A1 A2 B1 B2 EA EB; napply ext_set; #x;
 210 nchange in match (x ∈ (A1 ∪ B1)) with (?∨?);
 211 napply (.= (set_ext ??? EA x)‡#);
 212 napply (.= #‡(set_ext ??? EB x)); //;
 213 nqed.
 214
 215 nlemma union_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
 216  #S A B; @ (A ∪ B); #x y Exy; @; *; #H1;
 217 ##[##1,3: @; ##|##*: @2 ]
 218 ##[##1,3: napply (. (Exy^-1)╪_1#)
 219 ##|##2,4: napply (. Exy╪_1#)]
 220 nassumption;
 221 nqed.
 222
 223 alias symbol "hint_decl" = "hint_decl_Type1".
 224 unification hint 0 ≔ A : setoid, B,C :  𝛀^A;
 225    AA ≟ carr A,
 226    BB ≟ ext_carr ? B,
 227    CC ≟ ext_carr ? C,
 228    R ≟ mk_ext_powerclass ?
 229          (ext_carr ? B ∪ ext_carr ? C) (ext_prop ? (union_is_ext ? B C))
 230 (*-------------------------------------------------------------------------*)  ⊢
 231     ext_carr A R ≡ union AA BB CC.
 232
 233 unification hint 0 ≔ S:Type[0], A,B:Ω^S;
 234   T ≟ powerclass_setoid S,
 235   MM ≟ mk_unary_morphism1 ??
 236         (λA.mk_unary_morphism1 ??
 237           (λB.A ∪ B) (prop11 ?? (fun11 ?? (union_is_morph S) A)))
 238         (prop11 ?? (union_is_morph S))
 239 (*--------------------------------------------------------------------------*) ⊢
 240    fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ A ∪ B.
 241
 242 nlemma union_is_ext_morph:∀A.𝛀^A ⇒_1 𝛀^A ⇒_1 𝛀^A.
 243 #A; napply (mk_binary_morphism1 …  (union_is_ext …));
 244 #x1 x2 y1 y2 Ex Ey; napply (prop11 … (union_is_morph A)); nassumption.
 245 nqed.
 246
 247 unification hint 1 ≔
 248   AA : setoid, B,C : 𝛀^AA;
 249   A ≟ carr AA,
 250   T ≟ ext_powerclass_setoid AA,
 251   R ≟ mk_unary_morphism1 ?? (λX:𝛀^AA.
 252            mk_unary_morphism1 ?? (λY:𝛀^AA.
 253               mk_ext_powerclass AA
 254                (ext_carr ? X ∪ ext_carr ? Y) (ext_prop AA (union_is_ext ? X Y)))
 255             (prop11 ?? (fun11 ?? (union_is_ext_morph AA) X)))
 256           (prop11 ?? (union_is_ext_morph AA)),
 257    BB ≟ (ext_carr ? B),
 258    CC ≟ (ext_carr ? C)
 259 (*------------------------------------------------------*) ⊢
 260    ext_carr AA (fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C) ≡ union A BB CC.
 261
 262
 263 (* hints for - *)
 264 nlemma substract_is_morph : ∀A. Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A).
 265 #X; napply (mk_binary_morphism1 … (λA,B.A - B));
 266 #A1 A2 B1 B2 EA EB; napply ext_set; #x;
 267 nchange in match (x ∈ (A1 - B1)) with (?∧?);
 268 napply (.= (set_ext ??? EA x)‡#); @; *; #H H1; @; //; #H2; napply H1;
 269 ##[ napply (. (set_ext ??? EB x)); ##| napply (. (set_ext ??? EB^-1 x)); ##] //;
 270 nqed.
 271
 272 nlemma substract_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
 273  #S A B; @ (A - B); #x y Exy; @; *; #H1 H2; @; ##[##2,4: #H3; napply H2]
 274 ##[##1,4: napply (. Exy╪_1#); // ##|##2,3: napply (. Exy^-1╪_1#); //]
 275 nqed.
 276
 277 alias symbol "hint_decl" = "hint_decl_Type1".
 278 unification hint 0 ≔ A : setoid, B,C :  𝛀^A;
 279    AA ≟ carr A,
 280    BB ≟ ext_carr ? B,
 281    CC ≟ ext_carr ? C,
 282    R ≟ mk_ext_powerclass ?
 283          (ext_carr ? B - ext_carr ? C)
 284          (ext_prop ? (substract_is_ext ? B C))
 285 (*---------------------------------------------------*)  ⊢
 286     ext_carr A R ≡ substract AA BB CC.
 287
 288 unification hint 0 ≔ S:Type[0], A,B:Ω^S;
 289   T ≟ powerclass_setoid S,
 290   MM ≟ mk_unary_morphism1 ??
 291         (λA.mk_unary_morphism1 ??
 292           (λB.A - B) (prop11 ?? (fun11 ?? (substract_is_morph S) A)))
 293         (prop11 ?? (substract_is_morph S))
 294 (*--------------------------------------------------------------------------*) ⊢
 295    fun11 T T (fun11 T (unary_morphism1_setoid1 T T) MM A) B ≡ A - B.
 296
 297 nlemma substract_is_ext_morph:∀A.𝛀^A ⇒_1 𝛀^A ⇒_1 𝛀^A.
 298 #A; napply (mk_binary_morphism1 …  (substract_is_ext …));
 299 #x1 x2 y1 y2 Ex Ey; napply (prop11 … (substract_is_morph A)); nassumption.
 300 nqed.
 301
 302 unification hint 1 ≔
 303   AA : setoid, B,C : 𝛀^AA;
 304   A ≟ carr AA,
 305   T ≟ ext_powerclass_setoid AA,
 306   R ≟ mk_unary_morphism1 ?? (λX:𝛀^AA.
 307            mk_unary_morphism1 ?? (λY:𝛀^AA.
 308               mk_ext_powerclass AA
 309                 (ext_carr ? X - ext_carr ? Y)
 310                 (ext_prop AA (substract_is_ext ? X Y)))
 311             (prop11 ?? (fun11 ?? (substract_is_ext_morph AA) X)))
 312           (prop11 ?? (substract_is_ext_morph AA)),
 313    BB ≟ (ext_carr ? B),
 314    CC ≟ (ext_carr ? C)
 315 (*------------------------------------------------------*) ⊢
 316    ext_carr AA (fun11 T T (fun11 T (unary_morphism1_setoid1 T T) R B) C) ≡ substract A BB CC.
 317
 318 (* hints for {x} *)
 319 nlemma single_is_morph : ∀A:setoid. (setoid1_of_setoid A) ⇒_1 Ω^A.
 320 #X; @; ##[ napply (λx.{(x)}); ##]
 321 #a b E; napply ext_set; #x; @; #H; /3/; nqed.
 322
 323 nlemma single_is_ext: ∀A:setoid. A → 𝛀^A.
 324 #X a; @; ##[ napply ({(a)}); ##] #x y E; @; #H; /3/; nqed.
 325
 326 alias symbol "hint_decl" = "hint_decl_Type1".
 327 unification hint 0 ≔ A : setoid, a : carr A;
 328    R ≟ (mk_ext_powerclass ? {(a)} (ext_prop ? (single_is_ext ? a)))
 329 (*-------------------------------------------------------------------------*)  ⊢
 330     ext_carr A R ≡ singleton A a.
 331
 332 unification hint 0 ≔ A:setoid, a : carr A;
 333   T ≟ setoid1_of_setoid A,
 334   AA ≟ carr A,
 335   MM ≟ mk_unary_morphism1 ??
 336          (λa:carr1 (setoid1_of_setoid A).{(a)}) (prop11 ?? (single_is_morph A))
 337 (*--------------------------------------------------------------------------*) ⊢
 338    fun11 T (powerclass_setoid AA) MM a ≡ {(a)}.
 339
 340 nlemma single_is_ext_morph:∀A:setoid.(setoid1_of_setoid A) ⇒_1 𝛀^A.
 341 #A; @; ##[ #a; napply (single_is_ext ? a); ##] #a b E; @; #x; /3/; nqed.
 342
 343 unification hint 1 ≔ AA : setoid, a: carr AA;
 344   T ≟ ext_powerclass_setoid AA,
 345   R ≟ mk_unary_morphism1 ??
 346        (λa:carr1 (setoid1_of_setoid AA).
 347          mk_ext_powerclass AA {(a)} (ext_prop ? (single_is_ext AA a)))
 348             (prop11 ?? (single_is_ext_morph AA))
 349 (*------------------------------------------------------*) ⊢
 350    ext_carr AA (fun11 (setoid1_of_setoid AA) T R a) ≡ singleton AA a.
 351
 352
 353 (*
 354 alias symbol "hint_decl" = "hint_decl_Type2".
 355 unification hint 0 ≔
 356   A : setoid, B,C : 𝛀^A ;
 357   CC ≟ (ext_carr ? C),
 358   BB ≟ (ext_carr ? B),
 359   C1 ≟ (carr1 (powerclass_setoid (carr A))),
 360   C2 ≟ (carr1 (ext_powerclass_setoid A))
 361   ⊢
 362      eq_rel1 C1 (eq1 (powerclass_setoid (carr A))) BB CC ≡
 363           eq_rel1 C2 (eq1 (ext_powerclass_setoid A)) B C.
 364
 365 unification hint 0 ≔
 366   A, B : CPROP ⊢ iff A B ≡ eq_rel1 ? (eq1 CPROP) A B.
 367
 368 nlemma test: ∀U.∀A,B:𝛀^U. A ∩ B = A →
 369  ∀x,y. x=y → x ∈ A → y ∈ A ∩ B.
 370  #U; #A; #B; #H; #x; #y; #K; #K2;
 371   alias symbol "prop2" = "prop21 mem".
 372   alias symbol "invert" = "setoid1 symmetry".
 373   napply (. K^-1‡H);
 374   nassumption;
 375 nqed.
 376
 377
 378 nlemma intersect_ok: ∀A. binary_morphism1 (ext_powerclass_setoid A) (ext_powerclass_setoid A) (ext_powerclass_setoid A).
 379  #A; @
 380   [ #S; #S'; @
 381      [ napply (S ∩ S')
 382      | #a; #a'; #Ha;
 383         nwhd in ⊢ (? ? ? % %); @; *; #H1; #H2; @
 384         [##1,2: napply (. Ha^-1‡#); nassumption;
 385       ##|##3,4: napply (. Ha‡#); nassumption]##]
 386  ##| #a; #a'; #b; #b'; #Ha; #Hb; nwhd; @; #x; nwhd in ⊢ (% → %); #H
 387       [ alias symbol "invert" = "setoid1 symmetry".
 388         alias symbol "refl" = "refl".
 389 alias symbol "prop2" = "prop21".
 390 napply (. ((#‡Ha^-1)‡(#‡Hb^-1))); nassumption
 391       | napply (. ((#‡Ha)‡(#‡Hb))); nassumption ]##]
 392 nqed.
 393
 394 (* unfold if intersect, exposing fun21 *)
 395 alias symbol "hint_decl" = "hint_decl_Type1".
 396 unification hint 0 ≔
 397   A : setoid, B,C : ext_powerclass A ⊢
 398     pc A (fun21 …
 399             (mk_binary_morphism1 …
 400               (λS,S':qpowerclass_setoid A.mk_qpowerclass ? (S ∩ S') (mem_ok' ? (intersect_ok ? S S')))
 401               (prop21 … (intersect_ok A)))
 402             B
 403             C)
 404     ≡ intersect ? (pc ? B) (pc ? C).
 405
 406 nlemma test: ∀A:setoid. ∀U,V:qpowerclass A. ∀x,x':setoid1_of_setoid A. x=x' → x ∈ U ∩ V → x' ∈ U ∩ V.
 407  #A; #U; #V; #x; #x'; #H; #p; napply (. (H^-1‡#)); nassumption.
 408 nqed.
 409 *)
 410
 411 ndefinition image: ∀A,B. (carr A → carr B) → Ω^A → Ω^B ≝
 412  λA,B:setoid.λf:carr A → carr B.λSa:Ω^A.
 413   {y | ∃x. x ∈ Sa ∧ eq_rel (carr B) (eq0 B) (f x) y}.
 414
 415 ndefinition counter_image: ∀A,B. (carr A → carr B) → Ω^B → Ω^A ≝
 416  λA,B,f,Sb. {x | ∃y. y ∈ Sb ∧ f x = y}.
 417
 418 (******************* compatible equivalence relations **********************)
 419
 420 nrecord compatible_equivalence_relation (A: setoid) : Type[1] ≝
 421  { rel:> equivalence_relation A;
 422    compatibility: ∀x,x':A. x=x' → rel x x'
 423  }.
 424
 425 ndefinition quotient: ∀A. compatible_equivalence_relation A → setoid.
 426  #A; #R; @ A R;
 427 nqed.
 428
 429 (******************* first omomorphism theorem for sets **********************)
 430
 431 ndefinition eqrel_of_morphism:
 432  ∀A,B. A ⇒_0 B → compatible_equivalence_relation A.
 433  #A; #B; #f; @
 434   [ @ [ napply (λx,y. f x = f y) ] /2/;
 435 ##| #x; #x'; #H; nwhd; alias symbol "prop1" = "prop1".
 436 napply (.= (†H)); // ]
 437 nqed.
 438
 439 ndefinition canonical_proj: ∀A,R. A ⇒_0 (quotient A R).
 440  #A; #R; @
 441   [ napply (λx.x) |  #a; #a'; #H; napply (compatibility … R … H) ]
 442 nqed.
 443
 444 ndefinition quotiented_mor:
 445  ∀A,B.∀f:A ⇒_0 B.(quotient … (eqrel_of_morphism … f)) ⇒_0 B.
 446  #A; #B; #f; @ [ napply f ] //.
 447 nqed.
 448
 449 nlemma first_omomorphism_theorem_functions1:
 450  ∀A,B.∀f: unary_morphism A B.
 451   ∀x. f x = quotiented_mor … (canonical_proj … (eqrel_of_morphism … f) x).
 452 //. nqed.
 453
 454 alias symbol "eq" = "setoid eq".
 455 ndefinition surjective ≝
 456  λA,B.λS: ext_powerclass A.λT: ext_powerclass B.λf:A ⇒_0 B.
 457   ∀y. y ∈ T → ∃x. x ∈ S ∧ f x = y.
 458
 459 ndefinition injective ≝
 460  λA,B.λS: ext_powerclass A.λf:A ⇒_0 B.
 461   ∀x,x'. x ∈ S → x' ∈ S → f x = f x' → x = x'.
 462
 463 nlemma first_omomorphism_theorem_functions2:
 464  ∀A,B.∀f:A ⇒_0 B.
 465    surjective … (Full_set ?) (Full_set ?) (canonical_proj ? (eqrel_of_morphism … f)).
 466 /3/. nqed.
 467
 468 nlemma first_omomorphism_theorem_functions3:
 469  ∀A,B.∀f:A ⇒_0 B.
 470    injective … (Full_set ?) (quotiented_mor … f).
 471  #A; #B; #f; nwhd; #x; #x'; #Hx; #Hx'; #K; nassumption.
 472 nqed.
 473
 474 nrecord isomorphism (A, B : setoid) (S: ext_powerclass A) (T: ext_powerclass B) : Type[0] ≝
 475  { iso_f:> A ⇒_0 B;
 476    f_closed: ∀x. x ∈ S → iso_f x ∈ T;
 477    f_sur: surjective … S T iso_f;
 478    f_inj: injective … S iso_f
 479  }.
 480
 481
 482 (*
 483 nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝
 484  { iso_f:> unary_morphism A B;
 485    f_closed: ∀x. x ∈ pc A S → fun1 ?? iso_f x ∈ pc B T}.
 486
 487
 488 ncheck (λA:?.
 489    λB:?.
 490     λS:?.
 491      λT:?.
 492       λxxx:isomorphism A B S T.
 493        match xxx
 494        return λxxx:isomorphism A B S T.
 495                ∀x: carr A.
 496                 ∀x_72: mem (carr A) (pc A S) x.
 497                  mem (carr B) (pc B T) (fun1 A B ((λ_.?) A B S T xxx) x)
 498         with [ mk_isomorphism _ yyy ⇒ yyy ] ).
 499
 500    ;
 501  }.
 502 *)
 503
 504 (* Set theory *)
 505
 506 nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
 507 #A; #U; #V; #W; *; #H; #x; *; /2/.
 508 nqed.
 509
 510 nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
 511 #A; #U; #V; #W; #H; #H1; #x; *; /2/.
 512 nqed.
 513
 514 nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
 515 /3/. nqed.
 516
 517 nlemma cupC : ∀S. ∀a,b:Ω^S.a ∪ b = b ∪ a.
 518 #S a b; @; #w; *; nnormalize; /2/; nqed.
 519
 520 nlemma cupID : ∀S. ∀a:Ω^S.a ∪ a = a.
 521 #S a; @; #w; ##[*; //] /2/; nqed.
 522
 523 (* XXX Bug notazione \cup, niente parentesi *)
 524 nlemma cupA : ∀S.∀a,b,c:Ω^S.a ∪ b ∪ c = a ∪ (b ∪ c).
 525 #S a b c; @; #w; *; /3/; *; /3/; nqed.
 526
 527 ndefinition Empty_set : ∀A.Ω^A ≝ λA.{ x | False }.
 528
 529 notation "∅" non associative with precedence 90 for @{ 'empty }.
 530 interpretation "empty set" 'empty = (Empty_set ?).
 531
 532 nlemma cup0 :∀S.∀A:Ω^S.A ∪ ∅ = A.
 533 #S p; @; #w; ##[*; //| #; @1; //] *; nqed.
 534