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] ≝ { carr :> Type[0];
18 eqb: carr → carr → bool;
19 eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
22 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
23 interpretation "eqb" 'eqb a b = (eqb ? a b).
25 notation "\P H" non associative with precedence 90
26 for @{(proj1 … (eqb_true ???) $H)}.
28 notation "\b H" non associative with precedence 90
29 for @{(proj2 … (eqb_true ???) $H)}.
31 notation < "𝐃" non associative with precedence 90
33 interpretation "DeqSet" 'bigD = (mk_DeqSet ???).
35 lemma eqb_false: ∀S:DeqSet.∀a,b:S.
36 (eqb ? a b) = false ↔ a ≠ b.
38 [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
39 |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
43 notation "\Pf H" non associative with precedence 90
44 for @{(proj1 … (eqb_false ???) $H)}.
46 notation "\bf H" non associative with precedence 90
47 for @{(proj2 … (eqb_false ???) $H)}.
49 lemma dec_eq: ∀S:DeqSet.∀a,b:S. a = b ∨ a ≠ b.
50 #S #a #b cases (true_or_false (eqb ? a b)) #H
51 [%1 @(\P H) | %2 @(\Pf H)]
54 definition beqb ≝ λb1,b2.
55 match b1 with [ true ⇒ b2 | false ⇒ notb b2].
57 notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
58 lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
59 #b1 #b2 cases b1 cases b2 normalize /2/
62 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
64 alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
65 unification hint 0 ≔ ;
66 X ≟ mk_DeqSet bool beqb beqb_true
67 (* ---------------------------------------- *) ⊢
70 unification hint 0 ≔ b1,b2:bool;
71 X ≟ mk_DeqSet bool beqb beqb_true
72 (* ---------------------------------------- *) ⊢
73 beqb b1 b2 ≡ eqb X b1 b2.
75 example exhint: ∀b:bool. (b == false) = true → b = false.
81 λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
83 lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
84 eq_pairs A B p1 p2 = true ↔ p1 = p2.
85 #A #B * #a1 #b1 * #a2 #b2 %
86 [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
87 |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
91 definition DeqProd ≝ λA,B:DeqSet.
92 mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
94 unification hint 0 ≔ C1,C2;
98 (* ---------------------------------------- *) ⊢
101 unification hint 0 ≔ T1,T2,p1,p2;
103 (* ---------------------------------------- *) ⊢
104 eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
106 example hint2: ∀b1,b2.
107 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
113 λA,B:DeqSet.λp1,p2:A+B.
115 [ inl a1 ⇒ match p2 with
116 [ inl a2 ⇒ a1 == a2 | inr b2 ⇒ false ]
117 | inr b1 ⇒ match p2 with
118 [ inl a2 ⇒ false | inr b2 ⇒ b1 == b2 ]
121 lemma eq_sum_true: ∀A,B:DeqSet.∀p1,p2:A+B.
122 eq_sum A B p1 p2 = true ↔ p1 = p2.
126 [#eqa >(\P eqa) // | #H destruct @(\b ?) //]
127 |#b2 normalize % #H destruct
130 [#a2 normalize % #H destruct
132 [#eqb >(\P eqb) // | #H destruct @(\b ?) //]
137 definition DeqSum ≝ λA,B:DeqSet.
138 mk_DeqSet (A+B) (eq_sum A B) (eq_sum_true A B).
140 unification hint 0 ≔ C1,C2;
144 (* ---------------------------------------- *) ⊢
147 unification hint 0 ≔ T1,T2,p1,p2;
149 (* ---------------------------------------- *) ⊢
150 eq_sum T1 T2 p1 p2 ≡ eqb X p1 p2.