weblib/tutorial/chapter4.ma

   1 (* In this Chapter we shall develop a naif theory of sets represented as characteristic
   2 predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type A→Prop *)
   3
   4 include "basics/logic.ma".
   5
   6 (**** For instance the empty set is defined by the always function predicate *)
   7
   8 definition empty_set ≝ λA:Type[0].λa:A.\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
   9 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
  10 interpretation "empty set" 'empty_set = (empty_set ?).
  11
  12 (* Similarly, a singleton set contaning containing an element a, is defined
  13 by by the characteristic function asserting equality with a *)
  14
  15 definition singleton ≝ λA.λx,a:A.x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6a.
  16 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
  17 interpretation "singleton" 'singl x = (singleton ? x).
  18
  19 (* The operations of union, intersection, complement and substraction
  20 are easily defined in terms of the propositional connectives of dijunction,
  21 conjunction and negation *)
  22
  23 definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 Q a.
  24 interpretation "union" 'union a b = (union ? a b).
  25
  26 definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 Q a.
  27 interpretation "intersection" 'intersects a b = (intersection ? a b).
  28
  29 definition complement ≝ λU:Type[0].λA:U → Prop.λw.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 A w.
  30 interpretation "complement" 'not a = (complement ? a).
  31
  32 definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 B w.
  33 interpretation "substraction" 'minus a b = (substraction ? a b).
  34
  35 (* Finally, we use implication to define the inclusion relation between
  36 sets *)
  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 (* Two sets are equals if and only if they have the same elements, that is,
  42 if the two characteristic functions are extensionally equivalent: *)
  43
  44 definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 Q a.
  45 notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
  46 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
  47
  48 (* This notion of equality is different from the intensional equality of
  49 fucntions, hence we have to prove the usual properties: *)
  50
  51 lemma eqP_sym: ∀U.∀A,B:U →Prop.
  52   A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B → B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
  53 #U #A #B #eqAB #a @iff_sym @eqAB qed.
  54
  55 lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
  56   A =1 B → B =1 C → A =1 C.
  57 #U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
  58
  59 (* For the same reason, we must also prove that all the operations we have
  60  lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
  61   A =1 C  → A ∪ B =1 C ∪ B.
  62 #U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
  63
  64 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
  65   B =1 C  → A ∪ B =1 A ∪ C.
  66 #U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
  67
  68 lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
  69   A =1 C  → A ∩ B =1 C ∩ B.
  70 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
  71
  72 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
  73   B =1 C  → A ∩ B =1 A ∩ C.
  74 #U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
  75
  76 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
  77   A =1 C  → A - B =1 C - B.
  78 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
  79
  80 lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
  81   B =1 C  → A - B =1 A - C.
  82 #U #A #B #C #eqBC #a @iff_and_l /2/ qed.
  83
  84 (* set equalities *)
  85 lemma union_empty_r: ∀U.∀A:U→Prop.
  86   A ∪ ∅ =1 A.
  87 #U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
  88 qed.
  89
  90 lemma union_comm : ∀U.∀A,B:U →Prop.
  91   A ∪ B =1 B ∪ A.
  92 #U #A #B #a % * /2/ qed.
  93
  94 lemma union_assoc: ∀U.∀A,B,C:U → Prop.
  95   A ∪ B ∪ C =1 A ∪ (B ∪ C).
  96 #S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
  97 qed.
  98
  99 lemma cap_comm : ∀U.∀A,B:U →Prop.
 100   A ∩ B =1 B ∩ A.
 101 #U #A #B #a % * /2/ qed.
 102
 103 lemma union_idemp: ∀U.∀A:U →Prop.
 104   A ∪ A =1 A.
 105 #U #A #a % [* // | /2/] qed.
 106
 107 lemma cap_idemp: ∀U.∀A:U →Prop.
 108   A ∩ A =1 A.
 109 #U #A #a % [* // | /2/] qed.
 110
 111 (*distributivities *)
 112
 113 lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
 114   (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C).
 115 #U #A #B #C #w % [* * /3/ | * * /3/]
 116 qed.
 117
 118 lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
 119   (A ∪ B) - C =1 (A - C) ∪ (B - C).
 120 #U #A #B #C #w % [* * /3/ | * * /3/]
 121 qed.
 122
 123 (* substraction *)
 124 lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
 125 #U #A #B #w normalize /2/
 126 qed.
 127
 128 include "basics/types.ma".
 129 include "basics/bool.ma".
 130
 131 (****** DeqSet: a set with a decidbale equality ******)
 132
 133 record DeqSet : Type[1] ≝ { carr :> Type[0];
 134    eqb: carr → carr → bool;
 135    eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
 136 }.
 137
 138 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
 139 interpretation "eqb" 'eqb a b = (eqb ? a b).
 140
 141 notation "\P H" non associative with precedence 90
 142   for @{(proj1 … (eqb_true ???) $H)}.
 143
 144 notation "\b H" non associative with precedence 90
 145   for @{(proj2 … (eqb_true ???) $H)}.
 146
 147 lemma eqb_false: ∀S:DeqSet.∀a,b:S.
 148   (eqb ? a b) = false ↔ a ≠ b.
 149 #S #a #b % #H
 150   [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
 151   |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
 152   ]
 153 qed.
 154
 155 notation "\Pf H" non associative with precedence 90
 156   for @{(proj1 … (eqb_false ???) $H)}.
 157
 158 notation "\bf H" non associative with precedence 90
 159   for @{(proj2 … (eqb_false ???) $H)}.
 160
 161 lemma dec_eq: ∀S:DeqSet.∀a,b:S. a = b ∨ a ≠ b.
 162 #S #a #b cases (true_or_false (eqb ? a b)) #H
 163   [%1 @(\P H) | %2 @(\Pf H)]
 164 qed.
 165
 166 definition beqb ≝ λb1,b2.
 167   match b1 with [ true ⇒ b2 | false ⇒ notb b2].
 168
 169 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
 170 lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
 171 #b1 #b2 cases b1 cases b2 normalize /2/
 172 qed.
 173
 174 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
 175
 176 unification hint  0 ≔ ;
 177     X ≟ mk_DeqSet bool beqb beqb_true
 178 (* ---------------------------------------- *) ⊢
 179     bool ≡ carr X.
 180
 181 unification hint  0 ≔ b1,b2:bool;
 182     X ≟ mk_DeqSet bool beqb beqb_true
 183 (* ---------------------------------------- *) ⊢
 184     beqb b1 b2 ≡ eqb X b1 b2.
 185
 186 example exhint: ∀b:bool. (b == false) = true → b = false.
 187 #b #H @(\P H).
 188 qed.
 189
 190 (* pairs *)
 191 definition eq_pairs ≝
 192   λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
 193
 194 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
 195   eq_pairs A B p1 p2 = true ↔ p1 = p2.
 196 #A #B * #a1 #b1 * #a2 #b2 %
 197   [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
 198   |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
 199   ]
 200 qed.
 201
 202 definition DeqProd ≝ λA,B:DeqSet.
 203   mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
 204
 205 unification hint  0 ≔ C1,C2;
 206     T1 ≟ carr C1,
 207     T2 ≟ carr C2,
 208     X ≟ DeqProd C1 C2
 209 (* ---------------------------------------- *) ⊢
 210     T1×T2 ≡ carr X.
 211
 212 unification hint  0 ≔ T1,T2,p1,p2;
 213     X ≟ DeqProd T1 T2
 214 (* ---------------------------------------- *) ⊢
 215     eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
 216
 217 example hint2: ∀b1,b2.
 218   〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
 219 #b1 #b2 #H @(\P H).