matita/matita/lib/basics/deqsets.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||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_______________________________________________________________ *)
  11
  12 include "basics/types.ma".
  13 include "basics/bool.ma".
  14
  15 (****** DeqSet: a set with a decidbale equality ******)
  16
  17 record DeqSet : Type[1] ≝ {
  18    carr :> Type[0];
  19    eqb: carr → carr → bool;
  20    eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
  21 }.
  22
  23 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
  24 interpretation "eqb" 'eqb a b = (eqb ? a b).
  25
  26 notation "\P H" non associative with precedence 90
  27   for @{(proj1 … (eqb_true ???) $H)}.
  28
  29 notation "\b H" non associative with precedence 90
  30   for @{(proj2 … (eqb_true ???) $H)}.
  31
  32 notation < "𝐃" non associative with precedence 90
  33  for @{'bigD}.
  34 interpretation "DeqSet" 'bigD = (mk_DeqSet ???).
  35
  36 lemma eqb_false: ∀S:DeqSet.∀a,b:S.
  37   (eqb ? a b) = false ↔ a ≠ b.
  38 #S #a #b % #H
  39   [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
  40   |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
  41   ]
  42 qed.
  43
  44 notation "\Pf H" non associative with precedence 90
  45   for @{(proj1 … (eqb_false ???) $H)}.
  46
  47 notation "\bf H" non associative with precedence 90
  48   for @{(proj2 … (eqb_false ???) $H)}.
  49
  50 lemma dec_eq: ∀S:DeqSet.∀a,b:S. a = b ∨ a ≠ b.
  51 #S #a #b cases (true_or_false (eqb ? a b)) #H
  52   [%1 @(\P H) | %2 @(\Pf H)]
  53 qed.
  54
  55 definition beqb ≝ λb1,b2.
  56   match b1 with [ true ⇒ b2 | false ⇒ notb b2].
  57
  58 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
  59 lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
  60 #b1 #b2 cases b1 cases b2 normalize /2/
  61 qed.
  62
  63 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
  64
  65 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
  66 unification hint  0 ≔ ;
  67     X ≟ mk_DeqSet bool beqb beqb_true
  68 (* ---------------------------------------- *) ⊢
  69     bool ≡ carr X.
  70
  71 unification hint  0 ≔ b1,b2:bool;
  72     X ≟ mk_DeqSet bool beqb beqb_true
  73 (* ---------------------------------------- *) ⊢
  74     beqb b1 b2 ≡ eqb X b1 b2.
  75
  76 example exhint: ∀b:bool. (b == false) = true → b = false.
  77 #b #H @(\P H).
  78 qed.
  79
  80 (* option *)
  81
  82 definition eq_option ≝
  83   λA:DeqSet.λa1,a2:option A.
  84     match a1 with
  85     [ None ⇒ match a2 with [None ⇒ true | _ ⇒ false]
  86     | Some a1' ⇒ match a2 with [None ⇒ false | Some a2' ⇒ a1'==a2']].
  87
  88 lemma eq_option_true: ∀A:DeqSet.∀a1,a2:option A.
  89   eq_option A a1 a2 = true ↔ a1 = a2.
  90 #A *
  91   [*
  92     [% //
  93     |#a1 % normalize #H destruct
  94     ]
  95   |#a1 *
  96     [normalize % #H destruct
  97     |#a2 normalize %
  98       [#Heq >(\P Heq) //
  99       |#H destruct @(\b ?) //
 100       ]
 101   ]
 102 qed.
 103
 104 definition DeqOption ≝ λA:DeqSet.
 105   mk_DeqSet (option A) (eq_option A) (eq_option_true A).
 106
 107 unification hint  0 ≔ C;
 108     T ≟ carr C,
 109     X ≟ DeqOption C
 110 (* ---------------------------------------- *) ⊢
 111     option T ≡ carr X.
 112
 113 unification hint  0 ≔ T,a1,a2;
 114     X ≟ DeqOption T
 115 (* ---------------------------------------- *) ⊢
 116     eq_option T a1 a2 ≡ eqb X a1 a2.
 117
 118
 119 (* pairs *)
 120 definition eq_pairs ≝
 121   λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
 122
 123 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
 124   eq_pairs A B p1 p2 = true ↔ p1 = p2.
 125 #A #B * #a1 #b1 * #a2 #b2 %
 126   [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
 127   |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
 128   ]
 129 qed.
 130
 131 definition DeqProd ≝ λA,B:DeqSet.
 132   mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
 133
 134 unification hint  0 ≔ C1,C2;
 135     T1 ≟ carr C1,
 136     T2 ≟ carr C2,
 137     X ≟ DeqProd C1 C2
 138 (* ---------------------------------------- *) ⊢
 139     T1×T2 ≡ carr X.
 140
 141 unification hint  0 ≔ T1,T2,p1,p2;
 142     X ≟ DeqProd T1 T2
 143 (* ---------------------------------------- *) ⊢
 144     eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
 145
 146 example hint2: ∀b1,b2.
 147   〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
 148 #b1 #b2 #H @(\P H)
 149 qed.
 150
 151 (* sum *)
 152 definition eq_sum ≝
 153   λA,B:DeqSet.λp1,p2:A+B.
 154   match p1 with
 155   [ inl a1 ⇒ match p2 with
 156     [ inl a2 ⇒ a1 == a2 | inr b2 ⇒ false ]
 157   | inr b1 ⇒ match p2 with
 158     [ inl a2 ⇒ false | inr b2 ⇒ b1 == b2 ]
 159   ].
 160
 161 lemma eq_sum_true: ∀A,B:DeqSet.∀p1,p2:A+B.
 162   eq_sum A B p1 p2 = true ↔ p1 = p2.
 163 #A #B *
 164   [#a1 *
 165     [#a2 normalize %
 166       [#eqa >(\P eqa) // | #H destruct @(\b ?) //]
 167     |#b2 normalize % #H destruct
 168     ]
 169   |#b1 *
 170     [#a2 normalize % #H destruct
 171     |#b2 normalize %
 172       [#eqb >(\P eqb) // | #H destruct @(\b ?) //]
 173     ]
 174   ]
 175 qed.
 176
 177 definition DeqSum ≝ λA,B:DeqSet.
 178   mk_DeqSet (A+B) (eq_sum A B) (eq_sum_true A B).
 179
 180 unification hint  0 ≔ C1,C2;
 181     T1 ≟ carr C1,
 182     T2 ≟ carr C2,
 183     X ≟ DeqSum C1 C2
 184 (* ---------------------------------------- *) ⊢
 185     T1+T2 ≡ carr X.
 186
 187 unification hint  0 ≔ T1,T2,p1,p2;
 188     X ≟ DeqSum T1 T2
 189 (* ---------------------------------------- *) ⊢
 190     eq_sum T1 T2 p1 p2 ≡ eqb X p1 p2.
 191
 192 (* sigma *)
 193 definition eq_sigma ≝
 194   λA:DeqSet.λP:A→Prop.λp1,p2:Σx:A.P x.
 195   match p1 with
 196   [mk_Sig a1 h1 ⇒
 197     match p2 with
 198     [mk_Sig a2 h2 ⇒ a1==a2]].
 199
 200 (* uses proof irrelevance *)
 201 lemma eq_sigma_true: ∀A:DeqSet.∀P.∀p1,p2:Σx.P x.
 202   eq_sigma A P p1 p2 = true ↔ p1 = p2.
 203 #A #P * #a1 #Ha1 * #a2 #Ha2 %
 204   [normalize #eqa generalize in match Ha1; >(\P eqa) //
 205   |#H >H @(\b ?) //
 206   ]
 207 qed.
 208
 209 definition DeqSig ≝ λA:DeqSet.λP:A→Prop.
 210   mk_DeqSet (Σx:A.P x) (eq_sigma A P) (eq_sigma_true A P).
 211
 212 (*
 213 unification hint  0 ≔ C,P;
 214     T ≟ carr C,
 215     X ≟ DeqSig C P
 216 (* ---------------------------------------- *) ⊢
 217     Σx:T.P x ≡ carr X.
 218
 219 unification hint  0 ≔ T,P,p1,p2;
 220     X ≟ DeqSig T P
 221 (* ---------------------------------------- *) ⊢
 222     eq_sigma T P p1 p2 ≡ eqb X p1 p2.
 223 *)