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
22 notation < "𝐅" non associative with precedence 90
24 interpretation "FinSet" 'bigF = (mk_FinSet ???).
27 lemma bool_enum_unique: uniqueb ? [true;false] = true.
30 definition FinBool ≝ mk_FinSet DeqBool [true;false] bool_enum_unique.
32 unification hint 0 ≔ ;
34 (* ---------------------------------------- *) ⊢
39 lemma eqbnat_true : ∀n,m. eqb n m = true ↔ n = m.
40 #n #m % [@eqb_true_to_eq | @eq_to_eqb_true]
43 definition DeqNat ≝ mk_DeqSet nat eqb eqbnat_true.
46 match n with [ O ⇒ [ ] | S p ⇒ p::enumn p ].
48 lemma memb_enumn: ∀m,n. n ≤ m → (¬ (memb DeqNat m (enumn n))) = true.
49 #m #n elim n // #n1 #Hind #ltm @sym_eq @noteq_to_eqnot @sym_not_eq
50 % #H cases (orb_true_l … H)
51 [#H1 @(absurd … (\P H1)) @sym_not_eq /2/
52 |<(notb_notb (memb …)) >Hind normalize /2/
56 lemma enumn_unique: ∀n. uniqueb DeqNat (enumn n) = true.
57 #n elim n // #m #Hind @true_to_andb_true /2/
60 definition initN ≝ λn.mk_FinSet DeqNat (enumn n) (enumn_unique n).
62 example tipa: ∀n.∃x: initN (S n). x = n.
63 #n @(ex_intro … n) // qed.
65 example inject : ∃f: initN 2 → initN 4. injective ?? f.
70 definition enum_sum ≝ λA,B:DeqSet.λl1.λl2.
71 (map ?? (inl A B) l1) @ (map ?? (inr A B) l2).
73 lemma enumAB_def : ∀A,B:FinSet.∀l1,l2. enum_sum A B l1 l2 =
74 (map ?? (inl A B) l1) @ (map ?? (inr A B) l2).
77 lemma enumAB_unique: ∀A,B:DeqSet.∀l1,l2.
78 uniqueb A l1 = true → uniqueb B l2 = true →
79 uniqueb ? (enum_sum A B l1 l2) = true.
81 [#_ #ul2 @unique_map_inj // #b1 #b2 #Hinr destruct //
82 |#a #tl #Hind #uA #uB @true_to_andb_true
83 [@sym_eq @noteq_to_eqnot % #H
84 cases (memb_append … (sym_eq … H))
85 [#H1 @(absurd (memb ? a tl = true))
86 [@(memb_map_inj …H1) #a1 #a2 #Hinl destruct //
87 |<(andb_true_l … uA) @eqnot_to_noteq //
90 [normalize #H destruct
91 |#b #tlB #Hind #membH cases (orb_true_l … membH)
92 [#H lapply (\P H) #H1 destruct |@Hind]
95 |@Hind // @(andb_true_r … uA)
100 definition FinSum ≝ λA,B:FinSet.
101 mk_FinSet (DeqSum A B)
102 (enum_sum A B (enum A) (enum B))
103 (enumAB_unique … (enum_unique A) (enum_unique B)).
105 include alias "basics/types.ma".
107 unification hint 0 ≔ C1,C2;
111 (* ---------------------------------------- *) ⊢
112 T1+T2 ≡ FinSetcarr X.
116 definition enum_prod ≝ λA,B:DeqSet.λl1.λl2.
117 compose ??? (mk_Prod A B) l1 l2.
119 axiom enum_prod_unique: ∀A,B,l1,l2.
120 uniqueb A l1 = true → uniqueb B l2 = true →
121 uniqueb ? (enum_prod A B l1 l2) = true.
124 λA,B:FinSet.mk_FinSet (DeqProd A B)
125 (enum_prod A B (enum A) (enum B))
126 (enum_prod_unique A B (enum A) (enum B) (enum_unique A) (enum_unique B) ).
128 unification hint 0 ≔ C1,C2;
132 (* ---------------------------------------- *) ⊢
133 T1×T2 ≡ FinSetcarr X.