weblib/tutorial/chapter4.ma

   1 include "basics/logic.ma".
   2
   3 (**** a subset of A is just an object of type A→Prop ****)
   4
   5 definition empty_set ≝ λA:Type[0].λa:A.False.
   6 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
   7 interpretation "empty set" 'empty_set = (empty_set ?).
   8
   9 definition singleton ≝ λA.λx,a:A.x=a.
  10 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
  11 interpretation "singleton" 'singl x = (singleton ? x).
  12
  13 definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a.
  14 interpretation "union" 'union a b = (union ? a b).
  15
  16 definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a.
  17 interpretation "intersection" 'intersects a b = (intersection ? a b).
  18
  19 definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
  20 interpretation "complement" 'not a = (complement ? a).
  21
  22 definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
  23 interpretation "substraction" 'minus a b = (substraction ? a b).
  24
  25 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
  26 interpretation "subset" 'subseteq a b = (subset ? a b).
  27
  28 (* extensional equality *)
  29 definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
  30 notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
  31 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
  32
  33 lemma eqP_sym: ∀U.∀A,B:U →Prop.
  34   A =1 B → B =1 A.
  35 #U #A #B #eqAB #a @iff_sym @eqAB qed.
  36
  37 lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
  38   A =1 B → B =1 C → A =1 C.
  39 #U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
  40
  41 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
  42   A =1 C  → A ∪ B =1 C ∪ B.
  43 #U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
  44
  45 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
  46   B =1 C  → A ∪ B =1 A ∪ C.
  47 #U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
  48
  49 lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
  50   A =1 C  → A ∩ B =1 C ∩ B.
  51 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
  52
  53 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
  54   B =1 C  → A ∩ B =1 A ∩ C.
  55 #U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
  56
  57 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
  58   A =1 C  → A - B =1 C - B.
  59 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
  60
  61 lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
  62   B =1 C  → A - B =1 A - C.
  63 #U #A #B #C #eqBC #a @iff_and_l /2/ qed.
  64
  65 (* set equalities *)
  66 lemma union_empty_r: ∀U.∀A:U→Prop.
  67   A ∪ ∅ =1 A.
  68 #U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
  69 qed.
  70
  71 lemma union_comm : ∀U.∀A,B:U →Prop.
  72   A ∪ B =1 B ∪ A.
  73 #U #A #B #a % * /2/ qed.
  74
  75 lemma union_assoc: ∀U.∀A,B,C:U → Prop.
  76   A ∪ B ∪ C =1 A ∪ (B ∪ C).
  77 #S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
  78 qed.
  79
  80 lemma cap_comm : ∀U.∀A,B:U →Prop.
  81   A ∩ B =1 B ∩ A.
  82 #U #A #B #a % * /2/ qed.
  83
  84 lemma union_idemp: ∀U.∀A:U →Prop.
  85   A ∪ A =1 A.
  86 #U #A #a % [* // | /2/] qed.
  87
  88 lemma cap_idemp: ∀U.∀A:U →Prop.
  89   A ∩ A =1 A.
  90 #U #A #a % [* // | /2/] qed.
  91
  92 (*distributivities *)
  93
  94 lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
  95   (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C).
  96 #U #A #B #C #w % [* * /3/ | * * /3/]
  97 qed.
  98
  99 lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
 100   (A ∪ B) - C =1 (A - C) ∪ (B - C).
 101 #U #A #B #C #w % [* * /3/ | * * /3/]
 102 qed.
 103
 104 (* substraction *)
 105 lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
 106 #U #A #B #w normalize /2/
 107 qed.
 108
 109 include "basics/types.ma".
 110 include "basics/bool.ma".
 111
 112 (****** DeqSet: a set with a decidbale equality ******)
 113
 114 record DeqSet : Type[1] ≝ { carr :> Type[0];
 115    eqb: carr → carr → bool;
 116    eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
 117 }.
 118
 119 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
 120 interpretation "eqb" 'eqb a b = (eqb ? a b).
 121
 122 notation "\P H" non associative with precedence 90
 123   for @{(proj1 … (eqb_true ???) $H)}.
 124
 125 notation "\b H" non associative with precedence 90
 126   for @{(proj2 … (eqb_true ???) $H)}.
 127
 128 lemma eqb_false: ∀S:DeqSet.∀a,b:S.
 129   (eqb ? a b) = false ↔ a ≠ b.
 130 #S #a #b % #H
 131   [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
 132   |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
 133   ]
 134 qed.
 135
 136 notation "\Pf H" non associative with precedence 90
 137   for @{(proj1 … (eqb_false ???) $H)}.
 138
 139 notation "\bf H" non associative with precedence 90
 140   for @{(proj2 … (eqb_false ???) $H)}.
 141
 142 lemma dec_eq: ∀S:DeqSet.∀a,b:S. a = b ∨ a ≠ b.
 143 #S #a #b cases (true_or_false (eqb ? a b)) #H
 144   [%1 @(\P H) | %2 @(\Pf H)]
 145 qed.
 146
 147 definition beqb ≝ λb1,b2.
 148   match b1 with [ true ⇒ b2 | false ⇒ notb b2].
 149
 150 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
 151 lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
 152 #b1 #b2 cases b1 cases b2 normalize /2/
 153 qed.
 154
 155 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
 156
 157 unification hint  0 ≔ ;
 158     X ≟ mk_DeqSet bool beqb beqb_true
 159 (* ---------------------------------------- *) ⊢
 160     bool ≡ carr X.
 161
 162 unification hint  0 ≔ b1,b2:bool;
 163     X ≟ mk_DeqSet bool beqb beqb_true
 164 (* ---------------------------------------- *) ⊢
 165     beqb b1 b2 ≡ eqb X b1 b2.
 166
 167 example exhint: ∀b:bool. (b == false) = true → b = false.
 168 #b #H @(\P H).
 169 qed.
 170
 171 (* pairs *)
 172 definition eq_pairs ≝
 173   λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
 174
 175 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
 176   eq_pairs A B p1 p2 = true ↔ p1 = p2.
 177 #A #B * #a1 #b1 * #a2 #b2 %
 178   [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
 179   |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
 180   ]
 181 qed.
 182
 183 definition DeqProd ≝ λA,B:DeqSet.
 184   mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
 185
 186 unification hint  0 ≔ C1,C2;
 187     T1 ≟ carr C1,
 188     T2 ≟ carr C2,
 189     X ≟ DeqProd C1 C2
 190 (* ---------------------------------------- *) ⊢
 191     T1×T2 ≡ carr X.
 192
 193 unification hint  0 ≔ T1,T2,p1,p2;
 194     X ≟ DeqProd T1 T2
 195 (* ---------------------------------------- *) ⊢
 196     eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
 197
 198 example hint2: ∀b1,b2.
 199   〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
 200 #b1 #b2 #H @(\P H).