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.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/lists/listb.ma".
14 (****** DeqSet: a set with a decidbale equality ******)
16 record FinSet : Type[1] ≝
19 enum_complete: ∀x.memb carr x enum = true;
20 enum_unique: uniqueb carr enum = true
24 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
26 unification hint 0 ≔ ;
27 X ≟ mk_DeqSet bool beqb beqb_true
28 (* ---------------------------------------- *) ⊢
31 unification hint 0 ≔ b1,b2:bool;
32 X ≟ mk_DeqSet bool beqb beqb_true
33 (* ---------------------------------------- *) ⊢
34 beqb b1 b2 ≡ eqb X b1 b2.
36 example exhint: ∀b:bool. (b == false) = true → b = false.
42 λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
44 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
45 eq_pairs A B p1 p2 = true ↔ p1 = p2.
46 #A #B * #a1 #b1 * #a2 #b2 %
47 [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
48 |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
52 definition DeqProd ≝ λA,B:DeqSet.
53 mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
55 unification hint 0 ≔ C1,C2;
59 (* ---------------------------------------- *) ⊢
62 unification hint 0 ≔ T1,T2,p1,p2;
64 (* ---------------------------------------- *) ⊢
65 eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
67 example hint2: ∀b1,b2.
68 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.