helm/software/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 include "logic/connectives.ma".
  16
  17 nrecord powerset (A: Type) : Type[1] ≝ { mem: A → CProp }.
  18 (* This is a projection! *)
  19 ndefinition mem ≝ λA.λr:powerset A.match r with [mk_powerset f ⇒ f].
  20
  21 interpretation "powerset" 'powerset A = (powerset A).
  22
  23 interpretation "subset construction" 'subset \eta.x = (mk_powerset ? x).
  24
  25 interpretation "mem" 'mem a S = (mem ? S a).
  26
  27 ndefinition subseteq ≝ λA.λU,V.∀a:A. a ∈ U → a ∈ V.
  28
  29 interpretation "subseteq" 'subseteq U V = (subseteq ? U V).
  30
  31 ntheorem subseteq_refl: ∀A.∀S:Ω \sup A.S ⊆ S.
  32  #A; #S; #x; #H; nassumption;
  33 nqed.
  34
  35 ntheorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3.
  36  #A; #S1; #S2; #S3; #H12; #H23; #x; #H;
  37  napply (H23 ??); napply (H12 ??); nassumption;
  38 nqed.
  39
  40 ndefinition overlaps ≝ λA.λU,V:Ω \sup A.∃x:A.x ∈ U ∧ x ∈ V.
  41
  42 interpretation "overlaps" 'overlaps U V = (fun1 ??? (overlaps ?) U V).
  43
  44 definition intersects:
  45  ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
  46  intros;
  47  constructor 1;
  48   [ apply (λU,V. {x | x ∈ U ∧ x ∈ V });
  49     intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1;
  50   | intros;
  51     split; intros 2; simplify in f ⊢ %;
  52     [ apply (. (#‡H)‡(#‡H1)); assumption
  53     | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
  54 qed.
  55
  56 interpretation "intersects" 'intersects U V = (fun1 ??? (intersects ?) U V).
  57
  58 definition union:
  59  ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
  60  intros;
  61  constructor 1;
  62   [ apply (λU,V. {x | x ∈ U ∨ x ∈ V });
  63     intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1
  64   | intros;
  65     split; intros 2; simplify in f ⊢ %;
  66     [ apply (. (#‡H)‡(#‡H1)); assumption
  67     | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
  68 qed.
  69
  70 interpretation "union" 'union U V = (fun1 ??? (union ?) U V).
  71
  72 definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A).
  73  intros; constructor 1;
  74   [ apply (λA:setoid.λa:A.{b | a=b});
  75     intros; simplify;
  76     split; intro;
  77     apply (.= H1);
  78      [ apply H | apply (H \sup -1) ]
  79   | intros; split; intros 2; simplify in f ⊢ %; apply trans;
  80      [ apply a |4: apply a'] try assumption; apply sym; assumption]
  81 qed.
  82
  83 interpretation "singleton" 'singl a = (fun_1 ?? (singleton ?) a).