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] ≝ { carr :> Type[0];
  18    eqb: carr → carr → bool;
  19    eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
  20 }.
  21
  22 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
  23 interpretation "eqb" 'eqb a b = (eqb ? a b).
  24
  25 notation "\P H" non associative with precedence 90
  26   for @{(proj1 … (eqb_true ???) $H)}.
  27
  28 notation "\b H" non associative with precedence 90
  29   for @{(proj2 … (eqb_true ???) $H)}.
  30
  31 lemma eqb_false: ∀S:DeqSet.∀a,b:S.
  32   (eqb ? a b) = false ↔ a ≠ b.
  33 #S #a #b % #H
  34   [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
  35   |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
  36   ]
  37 qed.
  38
  39 notation "\Pf H" non associative with precedence 90
  40   for @{(proj1 … (eqb_false ???) $H)}.
  41
  42 notation "\bf H" non associative with precedence 90
  43   for @{(proj2 … (eqb_false ???) $H)}.
  44
  45 lemma dec_eq: ∀S:DeqSet.∀a,b:S. a = b ∨ a ≠ b.
  46 #S #a #b cases (true_or_false (eqb ? a b)) #H
  47   [%1 @(\P H) | %2 @(\Pf H)]
  48 qed.
  49
  50 definition beqb ≝ λb1,b2.
  51   match b1 with [ true ⇒ b2 | false ⇒ notb b2].
  52
  53 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
  54 lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
  55 #b1 #b2 cases b1 cases b2 normalize /2/
  56 qed.
  57
  58 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
  59
  60 unification hint  0 ≔ ;
  61     X ≟ mk_DeqSet bool beqb beqb_true
  62 (* ---------------------------------------- *) ⊢
  63     bool ≡ carr X.
  64
  65 unification hint  0 ≔ b1,b2:bool;
  66     X ≟ mk_DeqSet bool beqb beqb_true
  67 (* ---------------------------------------- *) ⊢
  68     beqb b1 b2 ≡ eqb X b1 b2.
  69
  70 example exhint: ∀b:bool. (b == false) = true → b = false.
  71 #b #H @(\P H).
  72 qed.
  73
  74 (* pairs *)
  75 definition eq_pairs ≝
  76   λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
  77
  78 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
  79   eq_pairs A B p1 p2 = true ↔ p1 = p2.
  80 #A #B * #a1 #b1 * #a2 #b2 %
  81   [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
  82   |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
  83   ]
  84 qed.
  85
  86 definition DeqProd ≝ λA,B:DeqSet.
  87   mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
  88
  89 unification hint  0 ≔ C1,C2;
  90     T1 ≟ carr C1,
  91     T2 ≟ carr C2,
  92     X ≟ DeqProd C1 C2
  93 (* ---------------------------------------- *) ⊢
  94     T1×T2 ≡ carr X.
  95
  96 unification hint  0 ≔ T1,T2,p1,p2;
  97     X ≟ DeqProd T1 T2
  98 (* ---------------------------------------- *) ⊢
  99     eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
 100
 101 example hint2: ∀b1,b2.
 102   〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
 103 #b1 #b2 #H @(\P H)
 104 qed.
 105
 106 (* sum *)
 107 definition eq_sum ≝
 108   λA,B:DeqSet.λp1,p2:A+B.
 109   match p1 with
 110   [ inl a1 ⇒ match p2 with
 111     [ inl a2 ⇒ a1 == a2 | inr b2 ⇒ false ]
 112   | inr b1 ⇒ match p2 with
 113     [ inl a2 ⇒ false | inr b2 ⇒ b1 == b2 ]
 114   ].
 115
 116 lemma eq_sum_true: ∀A,B:DeqSet.∀p1,p2:A+B.
 117   eq_sum A B p1 p2 = true ↔ p1 = p2.
 118 #A #B *
 119   [#a1 *
 120     [#a2 normalize %
 121       [#eqa >(\P eqa) // | #H destruct @(\b ?) //]
 122     |#b2 normalize % #H destruct
 123     ]
 124   |#b1 *
 125     [#a2 normalize % #H destruct
 126     |#b2 normalize %
 127       [#eqb >(\P eqb) // | #H destruct @(\b ?) //]
 128     ]
 129   ]
 130 qed.
 131
 132 definition DeqSum ≝ λA,B:DeqSet.
 133   mk_DeqSet (A+B) (eq_sum A B) (eq_sum_true A B).
 134
 135 unification hint  0 ≔ C1,C2;
 136     T1 ≟ carr C1,
 137     T2 ≟ carr C2,
 138     X ≟ DeqSum C1 C2
 139 (* ---------------------------------------- *) ⊢
 140     T1+T2 ≡ carr X.
 141
 142 unification hint  0 ≔ T1,T2,p1,p2;
 143     X ≟ DeqSum T1 T2
 144 (* ---------------------------------------- *) ⊢
 145     eq_sum T1 T2 p1 p2 ≡ eqb X p1 p2.
 146