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 decidable equality ******)
16 record FinSet : Type[1] ≝
17 { FinSetcarr:> DeqSet;
18 enum: list FinSetcarr;
19 enum_unique: uniqueb FinSetcarr enum = true
23 lemma bool_enum_unique: uniqueb ? [true;false] = true.
26 definition FinBool ≝ mk_FinSet DeqBool [true;false] bool_enum_unique.
28 unification hint 0 ≔ ;
30 (* ---------------------------------------- *) ⊢
35 lemma eqbnat_true : ∀n,m. eqb n m = true ↔ n = m.
36 #n #m % [@eqb_true_to_eq | @eq_to_eqb_true]
39 definition DeqNat ≝ mk_DeqSet nat eqb eqbnat_true.
42 match n with [ O ⇒ [ ] | S p ⇒ p::enumn p ].
44 lemma memb_enumn: ∀m,n. n ≤ m → (¬ (memb DeqNat m (enumn n))) = true.
45 #m #n elim n // #n1 #Hind #ltm @sym_eq @noteq_to_eqnot @sym_not_eq
46 % #H cases (orb_true_l … H)
47 [#H1 @(absurd … (\P H1)) @sym_not_eq /2/
48 |<(notb_notb (memb …)) >Hind normalize /2/
52 lemma enumn_unique: ∀n. uniqueb DeqNat (enumn n) = true.
53 #n elim n // #m #Hind @true_to_andb_true /2/
56 definition initN ≝ λn.mk_FinSet DeqNat (enumn n) (enumn_unique n).
58 example tipa: ∀n.∃x: initN (S n). x = n.
59 #n @(ex_intro … n) // qed.
61 example inject : ∃f: initN 2 → initN 4. injective ?? f.
66 definition enum_sum ≝ λA,B:DeqSet.λl1.λl2.
67 (map ?? (inl A B) l1) @ (map ?? (inr A B) l2).
69 lemma enumAB_def : ∀A,B:FinSet.∀l1,l2. enum_sum A B l1 l2 =
70 (map ?? (inl A B) l1) @ (map ?? (inr A B) l2).
73 lemma enumAB_unique: ∀A,B:DeqSet.∀l1,l2.
74 uniqueb A l1 = true → uniqueb B l2 = true →
75 uniqueb ? (enum_sum A B l1 l2) = true.
77 [#_ #ul2 @unique_map_inj // #b1 #b2 #Hinr destruct //
78 |#a #tl #Hind #uA #uB @true_to_andb_true
79 [@sym_eq @noteq_to_eqnot % #H
80 cases (memb_append … (sym_eq … H))
81 [#H1 @(absurd (memb ? a tl = true))
82 [@(memb_map_inj …H1) #a1 #a2 #Hinl destruct //
83 |<(andb_true_l … uA) @eqnot_to_noteq //
86 [normalize #H destruct
87 |#b #tlB #Hind #membH cases (orb_true_l … membH)
88 [#H lapply (\P H) #H1 destruct |@Hind]
91 |@Hind // @(andb_true_r … uA)
96 definition FinSum ≝ λA,B:FinSet.
97 mk_FinSet (DeqSum A B)
98 (enum_sum A B (enum A) (enum B))
99 (enumAB_unique … (enum_unique A) (enum_unique B)).
101 unification hint 0 ≔ C1,C2;
105 (* ---------------------------------------- *) ⊢
106 T1+T2 ≡ FinSetcarr X.
110 definition enum_prod ≝ λA,B:DeqSet.λl1.λl2.
111 compose ??? (mk_Prod A B) l1 l2.
113 axiom enum_prod_unique: ∀A,B,l1,l2.
114 uniqueb A l1 = true → uniqueb B l2 = true →
115 uniqueb ? (enum_prod A B l1 l2) = true.
118 λA,B:FinSet.mk_FinSet (DeqProd A B)
119 (enum_prod A B (enum A) (enum B))
120 (enum_prod_unique A B (enum A) (enum B) (enum_unique A) (enum_unique B) ).
122 unification hint 0 ≔ C1,C2;
126 (* ---------------------------------------- *) ⊢
127 T1×T2 ≡ FinSetcarr X.