matita/matita/re_complete/basics/deqsets.ma

   1 include "basics/types.ma".
   2 include "basics/bool.ma".
   3
   4 (****** DeqSet: a set with a decidbale equality ******)
   5
   6 record DeqSet : Type[1] ≝ { carr :> Type[0];
   7    eqb: carr → carr → bool;
   8    eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
   9 }.
  10
  11 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
  12 interpretation "eqb" 'eqb a b = (eqb ? a b).
  13
  14 notation "\P H" non associative with precedence 90
  15   for @{(proj1 … (eqb_true ???) $H)}.
  16
  17 notation "\b H" non associative with precedence 90
  18   for @{(proj2 … (eqb_true ???) $H)}.
  19
  20 lemma eqb_false: ∀S:DeqSet.∀a,b:S.
  21   (eqb ? a b) = false ↔ a ≠ b.
  22 #S #a #b % #H
  23   [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
  24   |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
  25   ]
  26 qed.
  27
  28 notation "\Pf H" non associative with precedence 90
  29   for @{(proj1 … (eqb_false ???) $H)}.
  30
  31 notation "\bf H" non associative with precedence 90
  32   for @{(proj2 … (eqb_false ???) $H)}.
  33
  34 lemma dec_eq: ∀S:DeqSet.∀a,b:S. a = b ∨ a ≠ b.
  35 #S #a #b cases (true_or_false (eqb ? a b)) #H
  36   [%1 @(\P H) | %2 @(\Pf H)]
  37 qed.
  38
  39 definition beqb ≝ λb1,b2.
  40   match b1 with [ true ⇒ b2 | false ⇒ notb b2].
  41
  42 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
  43 lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
  44 #b1 #b2 cases b1 cases b2 normalize /2/
  45 qed.
  46
  47 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
  48
  49 unification hint  0 ≔ ;
  50     X ≟ mk_DeqSet bool beqb beqb_true
  51 (* ---------------------------------------- *) ⊢
  52     bool ≡ carr X.
  53
  54 unification hint  0 ≔ b1,b2:bool;
  55     X ≟ mk_DeqSet bool beqb beqb_true
  56 (* ---------------------------------------- *) ⊢
  57     beqb b1 b2 ≡ eqb X b1 b2.
  58
  59 example exhint: ∀b:bool. (b == false) = true → b = false.
  60 #b #H @(\P H).
  61 qed.
  62
  63 (* pairs *)
  64 definition eq_pairs ≝
  65   λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
  66
  67 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
  68   eq_pairs A B p1 p2 = true ↔ p1 = p2.
  69 #A #B * #a1 #b1 * #a2 #b2 %
  70   [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
  71   |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
  72   ]
  73 qed.
  74
  75 definition DeqProd ≝ λA,B:DeqSet.
  76   mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
  77
  78 unification hint  0 ≔ C1,C2;
  79     T1 ≟ carr C1,
  80     T2 ≟ carr C2,
  81     X ≟ DeqProd C1 C2
  82 (* ---------------------------------------- *) ⊢
  83     T1×T2 ≡ carr X.
  84
  85 unification hint  0 ≔ T1,T2,p1,p2;
  86     X ≟ DeqProd T1 T2
  87 (* ---------------------------------------- *) ⊢
  88     eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
  89
  90 example hint2: ∀b1,b2.
  91   〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
  92 #b1 #b2 #H @(\P H).