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/types.ma".
13 include "basics/bool.ma".
15 (****** DeqSet: a set with a decidbale equality ******)
17 record DeqSet : Type[1] ≝ {
19 eqb: carr → carr → bool;
20 eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
23 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
24 interpretation "eqb" 'eqb a b = (eqb ? a b).
26 notation "\P H" non associative with precedence 90
27 for @{(proj1 … (eqb_true ???) $H)}.
29 notation "\b H" non associative with precedence 90
30 for @{(proj2 … (eqb_true ???) $H)}.
32 notation < "𝐃" non associative with precedence 90
34 interpretation "DeqSet" 'bigD = (mk_DeqSet ???).
36 lemma eqb_false: ∀S:DeqSet.∀a,b:S.
37 (eqb ? a b) = false ↔ a ≠ b.
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)
44 notation "\Pf H" non associative with precedence 90
45 for @{(proj1 … (eqb_false ???) $H)}.
47 notation "\bf H" non associative with precedence 90
48 for @{(proj2 … (eqb_false ???) $H)}.
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)]
55 definition beqb ≝ λb1,b2.
56 match b1 with [ true ⇒ b2 | false ⇒ notb b2].
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/
63 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
65 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
66 unification hint 0 ≔ ;
67 X ≟ mk_DeqSet bool beqb beqb_true
68 (* ---------------------------------------- *) ⊢
71 unification hint 0 ≔ b1,b2:bool;
72 X ≟ mk_DeqSet bool beqb beqb_true
73 (* ---------------------------------------- *) ⊢
74 beqb b1 b2 ≡ eqb X b1 b2.
76 example exhint: ∀b:bool. (b == false) = true → b = false.
82 definition eq_option ≝
83 λA:DeqSet.λa1,a2:option A.
85 [ None ⇒ match a2 with [None ⇒ true | _ ⇒ false]
86 | Some a1' ⇒ match a2 with [None ⇒ false | Some a2' ⇒ a1'==a2']].
88 lemma eq_option_true: ∀A:DeqSet.∀a1,a2:option A.
89 eq_option A a1 a2 = true ↔ a1 = a2.
93 |#a1 % normalize #H destruct
96 [normalize % #H destruct
99 |#H destruct @(\b ?) //
104 definition DeqOption ≝ λA:DeqSet.
105 mk_DeqSet (option A) (eq_option A) (eq_option_true A).
107 unification hint 0 ≔ C;
110 (* ---------------------------------------- *) ⊢
113 unification hint 0 ≔ T,a1,a2;
115 (* ---------------------------------------- *) ⊢
116 eq_option T a1 a2 ≡ eqb X a1 a2.
120 definition eq_pairs ≝
121 λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
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)) //
131 definition DeqProd ≝ λA,B:DeqSet.
132 mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
134 unification hint 0 ≔ C1,C2;
138 (* ---------------------------------------- *) ⊢
141 unification hint 0 ≔ T1,T2,p1,p2;
143 (* ---------------------------------------- *) ⊢
144 eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
146 example hint2: ∀b1,b2.
147 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
153 λA,B:DeqSet.λp1,p2:A+B.
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 ]
161 lemma eq_sum_true: ∀A,B:DeqSet.∀p1,p2:A+B.
162 eq_sum A B p1 p2 = true ↔ p1 = p2.
166 [#eqa >(\P eqa) // | #H destruct @(\b ?) //]
167 |#b2 normalize % #H destruct
170 [#a2 normalize % #H destruct
172 [#eqb >(\P eqb) // | #H destruct @(\b ?) //]
177 definition DeqSum ≝ λA,B:DeqSet.
178 mk_DeqSet (A+B) (eq_sum A B) (eq_sum_true A B).
180 unification hint 0 ≔ C1,C2;
184 (* ---------------------------------------- *) ⊢
187 unification hint 0 ≔ T1,T2,p1,p2;
189 (* ---------------------------------------- *) ⊢
190 eq_sum T1 T2 p1 p2 ≡ eqb X p1 p2.
193 definition eq_sigma ≝
194 λA:DeqSet.λP:A→Prop.λp1,p2:Σx:A.P x.
198 [mk_Sig a2 h2 ⇒ a1==a2]].
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) //
209 definition DeqSig ≝ λA:DeqSet.λP:A→Prop.
210 mk_DeqSet (Σx:A.P x) (eq_sigma A P) (eq_sigma_true A P).
213 unification hint 0 ≔ C,P;
216 (* ---------------------------------------- *) ⊢
219 unification hint 0 ≔ T,P,p1,p2;
221 (* ---------------------------------------- *) ⊢
222 eq_sigma T P p1 p2 ≡ eqb X p1 p2.