matita/matita/lib/basics/sets.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "basics/logic.ma".
  13 include "basics/core_notation/singl_1.ma".
  14 include "basics/core_notation/subseteq_2.ma".
  15
  16 (**** a subset of A is just an object of type A→Prop ****)
  17
  18 definition empty_set ≝ λA:Type[0].λa:A.False.
  19 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
  20 interpretation "empty set" 'empty_set = (empty_set ?).
  21
  22 definition singleton ≝ λA.λx,a:A.x=a.
  23 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
  24 interpretation "singleton" 'singl x = (singleton ? x).
  25
  26 definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a.
  27 interpretation "union" 'union a b = (union ? a b).
  28
  29 definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a.
  30 interpretation "intersection" 'intersects a b = (intersection ? a b).
  31
  32 definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
  33 interpretation "complement" 'not a = (complement ? a).
  34
  35 definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
  36 interpretation "substraction" 'minus a b = (substraction ? a b).
  37
  38 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
  39 interpretation "subset" 'subseteq a b = (subset ? a b).
  40
  41 (* extensional equality *)
  42 definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
  43 (* ≐ is typed as \doteq *)
  44 notation "A ≐ B" non associative with precedence 45 for @{'eqP $A $B}.
  45 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
  46
  47 lemma eqP_sym: ∀U.∀A,B:U →Prop.
  48   A ≐ B → B ≐ A.
  49 #U #A #B #eqAB #a @iff_sym @eqAB qed.
  50
  51 lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
  52   A ≐ B → B ≐ C → A ≐ C.
  53 #U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
  54
  55 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
  56   A ≐ C  → A ∪ B ≐ C ∪ B.
  57 #U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
  58
  59 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
  60   B ≐ C  → A ∪ B ≐ A ∪ C.
  61 #U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
  62
  63 lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
  64   A ≐ C  → A ∩ B ≐ C ∩ B.
  65 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
  66
  67 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
  68   B ≐ C  → A ∩ B ≐ A ∩ C.
  69 #U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
  70
  71 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
  72   A ≐ C  → A - B ≐ C - B.
  73 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
  74
  75 lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
  76   B ≐ C  → A - B ≐ A - C.
  77 #U #A #B #C #eqBC #a @iff_and_l /2/ qed.
  78
  79 (* set equalities *)
  80 lemma union_empty_r: ∀U.∀A:U→Prop.
  81   A ∪ ∅ ≐ A.
  82 #U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
  83 qed.
  84
  85 lemma union_comm : ∀U.∀A,B:U →Prop.
  86   A ∪ B ≐ B ∪ A.
  87 #U #A #B #a % * /2/ qed.
  88
  89 lemma union_assoc: ∀U.∀A,B,C:U → Prop.
  90   A ∪ B ∪ C ≐ A ∪ (B ∪ C).
  91 #S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
  92 qed.
  93
  94 lemma cap_comm : ∀U.∀A,B:U →Prop.
  95   A ∩ B ≐ B ∩ A.
  96 #U #A #B #a % * /2/ qed.
  97
  98 lemma union_idemp: ∀U.∀A:U →Prop.
  99   A ∪ A ≐ A.
 100 #U #A #a % [* // | /2/] qed.
 101
 102 lemma cap_idemp: ∀U.∀A:U →Prop.
 103   A ∩ A ≐ A.
 104 #U #A #a % [* // | /2/] qed.
 105
 106 (*distributivities *)
 107
 108 lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
 109   (A ∪ B) ∩ C ≐ (A ∩ C) ∪ (B ∩ C).
 110 #U #A #B #C #w % [* * /3/ | * * /3/]
 111 qed.
 112
 113 lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
 114   (A ∪ B) - C ≐ (A - C) ∪ (B - C).
 115 #U #A #B #C #w % [* * /3/ | * * /3/]
 116 qed.
 117
 118 (* substraction *)
 119 lemma substract_def:∀U.∀A,B:U→Prop. A-B ≐ A ∩ ¬B.
 120 #U #A #B #w normalize /2/
 121 qed.