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/deqsets.ma".
13 include "basics/lists/listb.ma".
17 record DeqSet : Type[1] ≝ {
19 eqb: carr → carr → bool;
20 eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
26 let rec eq_list (A:DeqSet) (l1,l2:list A) on l1 ≝
28 [ nil ⇒ match l2 with [nil ⇒ true | _ ⇒ false]
30 match l2 with [nil ⇒ false | cons a2 tl2 ⇒ a1 ==a2 ∧ eq_list A tl1 tl2]].
32 lemma eq_list_true: ∀A:DeqSet.∀l1,l2:list A.
33 eq_list A l1 l2 = true ↔ l1 = l2.
35 [* [% // |#a #tl % normalize #H destruct ]
37 [normalize % #H destruct
39 [cases (true_or_false (a1==a2)) #Heq >Heq normalize
40 [#Htl >(\P Heq) >(proj1 … (Hind tl2) Htl) // | #H destruct ]
41 |#H destruct >(\b (refl … )) >(proj2 … (Hind tl2) (refl …)) //
47 definition DeqList ≝ λA:DeqSet.
48 mk_DeqSet (list A) (eq_list A) (eq_list_true A).
50 unification hint 0 ≔ C;
53 (* ---------------------------------------- *) ⊢
56 alias id "eqb" = "cic:/matita/basics/deqsets/eqb#fix:0:0:3".
57 alias symbol "hint_decl" (instance 1) = "hint_decl_Type0".
58 unification hint 0 ≔ T,a1,a2;
60 (* ---------------------------------------- *) ⊢
61 eq_list T a1 a2 ≡ eqb X a1 a2.