1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/decidable_kit/fintype/".
17 include "decidable_kit/eqtype.ma".
18 include "decidable_kit/list_aux.ma".
20 record finType : Type ≝ {
23 enum_uniq : ∀x:fsort. count fsort (cmp fsort x) enum = (S O)
26 definition segment : nat → eqType ≝
27 λn.sub_eqType nat_eqType (λx:nat_eqType.ltb x n).
29 definition is_some : ∀d:eqType. option d → bool ≝
30 λd:eqType.λo:option d.notb (cmp (option_eqType d) (None ?) o).
33 λA,B:Type.λp:A→option B.λl:list A.
35 (λx,acc. match (p x) with [None ⇒ acc | (Some y) ⇒ cons B y acc]) (nil B) l.
37 definition segment_enum ≝
38 λbound.filter ? ? (if_p nat_eqType (λx.ltb x bound)) (iota O bound).
40 lemma iota_ltb : ∀x,p:nat. mem nat_eqType x (iota O p) = ltb x p.
41 intros (x p); elim p; simplify;[reflexivity]
42 generalize in match (refl_eq ? (cmp ? x n));
43 generalize in match (cmp ? x n) in ⊢ (? ? ? % → %); intros 1 (b);
44 cases b; simplify; intros (H1); rewrite > H; clear H;
45 rewrite < (leb_eqb x n); rewrite > H1; reflexivity;
49 ∀d1,d2:eqType.∀x:d2.∀l:list d1.∀p:d1 → option d2.
50 (∀y.mem d1 y l = true →
51 match (p y) with [None ⇒ false | (Some q) ⇒ cmp d2 x q] = false) →
52 mem d2 x (filter d1 d2 p l) = false.
53 intros 5 (d1 d2 x l p);
54 elim l; simplify; [reflexivity]
55 generalize in match (refl_eq ? (p t));
56 generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; intros (Hpt);
57 [1: apply H; intros (y Hyl);
59 rewrite > Hyl; rewrite > orbC; reflexivity;
60 |2: generalize in match (refl_eq ? (cmp ? x s));
61 generalize in match (cmp ? x s) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
62 [1: simplify; intros (Exs);
63 rewrite > orbC; rewrite > H;
64 [2: intros; apply H1; simplify; rewrite > H2; rewrite > orbC; reflexivity
65 |1: lapply (H1 t) as H2; [2: simplify; rewrite > cmp_refl; reflexivity]
66 rewrite > Hpt in H2; simplify in H2; rewrite > H2 in Exs;
68 |2: intros (Dxs); simplify; rewrite > H;
69 [2: intros; apply (H1 y); simplify; rewrite > H2; rewrite > orbC; reflexivity
70 |1: rewrite > Dxs; reflexivity]]]
74 ∀d:eqType.∀p:d→bool.∀l:list d.
75 (∀x:d.mem d x l = true → notb (p x) = true) → count d p l = O.
76 intros 3 (d p l); elim l; simplify; [1: reflexivity]
77 generalize in match (refl_eq ? (p t));
78 generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b);
80 [2:intros (Hpt); apply H; intros; apply H1; simplify;
81 generalize in match (refl_eq ? (cmp d x t));
82 generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b1);
83 cases b1; simplify; intros; [2:rewrite > H2] autobatch.
84 |1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; autobatch]
85 rewrite > H2 in Hletin; simplify in Hletin; destruct Hletin]
88 lemma segment_finType : nat → finType.
90 letin fsort ≝ (segment bound);
91 letin enum ≝ (segment_enum bound);
92 cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O));
93 [ apply (mk_finType fsort enum Hcut)
94 | intros (x); cases x (n Hn); simplify in Hn; clear x;
95 generalize in match Hn; generalize in match Hn; clear Hn;
97 generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?);
98 intros 1 (m); elim m (Hm Hn p IH Hm Hn); [ destruct Hm ]
99 simplify; cases (eqP bool_eqType (ltb p bound) true); simplify;
100 [1:unfold segment in ⊢ (? ? match ? % ? ? with [true⇒ ?|false⇒ ?] ?);
101 unfold nat_eqType in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?);
103 generalize in match (refl_eq ? (eqb n p));
104 generalize in match (eqb n p) in ⊢ (? ? ? % → %); intros 1(b); cases b; clear b;
105 intros (Enp); simplify;
106 [2:rewrite > IH; [1,3: autobatch]
107 rewrite < ltb_n_Sm in Hm; rewrite > Enp in Hm;
108 generalize in match Hm; cases (ltb n p); intros; [reflexivity]
109 simplify in H1; destruct H1;
110 |1:clear IH; rewrite > (count_O fsort); [reflexivity]
111 intros 1 (x); rewrite < (b2pT ? ? (eqP ? n ?) Enp);
112 cases x (y Hy); intros (ABS); clear x;
113 unfold segment; unfold notb; simplify;
114 generalize in match (refl_eq ? (cmp ? n y));
115 generalize in match (cmp ? n y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
116 intros (Eny); simplify; [2:reflexivity]
117 rewrite < ABS; symmetry; clear ABS;
118 generalize in match Hy; clear Hy;
119 rewrite < (b2pT ? ? (eqP nat_eqType ? ?) Eny);
120 simplify; intros (Hn); apply (mem_filter nat_eqType fsort); intros (w Hw);
121 fold simplify (sort nat_eqType); (* CANONICAL?! *)
122 cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w);
123 simplify; [2: reflexivity]
124 generalize in match H1; clear H1; cases s; clear s; intros (H1);
125 unfold segment; simplify; simplify in H1; rewrite > H1;
126 rewrite > iota_ltb in Hw; apply (p2bF ? ? (eqP nat_eqType ? ?));
127 unfold Not; intros (Enw); rewrite > Enw in Hw;
128 rewrite > ltb_refl in Hw; destruct Hw]
129 |2:rewrite > IH; [1:reflexivity|3:assumption]
130 rewrite < ltb_n_Sm in Hm;
131 cases (b2pT ? ?(orbP ? ?) Hm);[1: assumption]
132 rewrite > (b2pT ? ? (eqbP ? ?) H1) in Hn;
133 rewrite > Hn in H; cases (H ?); reflexivity]]
136 let rec uniq (d:eqType) (l:list d) on l : bool ≝
139 | (cons x tl) ⇒ andb (notb (mem d x tl)) (uniq d tl)].
141 lemma uniq_mem : ∀d:eqType.∀x:d.∀l:list d.uniq d (x::l) = true → mem d x l = false.
142 intros (d x l H); simplify in H; lapply (b2pT ? ? (andbP ? ?) H) as H1; clear H;
143 cases H1 (H2 H3); lapply (b2pT ? ?(negbP ?) H2); assumption;
146 lemma andbA : ∀a,b,c.andb a (andb b c) = andb (andb a b) c.
147 intros; cases a; cases b; cases c; reflexivity; qed.
149 lemma andbC : ∀a,b. andb a b = andb b a.
150 intros; cases a; cases b; reflexivity; qed.
153 ∀d:eqType.∀x:d.∀l:list d. uniq d (x::l) = andb (negb (mem d x l)) (uniq d l).
154 intros (d x l); elim l; simplify; [reflexivity]
155 generalize in match (refl_eq ? (cmp d x t));
156 generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
157 intros (E); simplify ; rewrite > E; [reflexivity]
158 rewrite > andbA; rewrite > andbC in ⊢ (? ? (? % ?) ?); rewrite < andbA;
159 rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA; reflexivity;
162 lemma count_O_mem : ∀d:eqType.∀x:d.∀l:list d.ltb O (count d (cmp d x) l) = mem d x l.
163 intros 3 (d x l); elim l [reflexivity] simplify; rewrite < H; cases (cmp d x t);
166 lemma uniqP : ∀d:eqType.∀l:list d.
167 reflect (∀x:d.mem d x l = true → count d (cmp d x) l = (S O)) (uniq d l).
168 intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: destruct H]
169 [1: generalize in match H2; simplify in H2;
170 lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2;
171 cases H3; clear H3; intros;
172 [2: lapply (uniq_mem ? ? ? H1) as H4;
173 generalize in match (refl_eq ? (cmp d x t));
174 generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
176 [1: simplify; rewrite > H5; simplify; rewrite > count_O; [reflexivity]
177 intros (y Hy); rewrite > (b2pT ? ? (eqP d ? ?) H5) in H2 H3 H4 ⊢ %;
178 clear H5; clear x; rewrite > H2 in H4; destruct H4;
179 |2: simplify; rewrite > H5; simplify; apply H;
180 rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1);
182 |1: simplify; rewrite > H2; simplify; rewrite > count_O; [reflexivity]
183 intros (y Hy); rewrite > (b2pT ? ? (eqP d ? ?) H2) in H3 ⊢ %;
184 clear H2; clear x; lapply (uniq_mem ? ? ? H1) as H4;
185 generalize in match (refl_eq ? (cmp d t y));
186 generalize in match (cmp d t y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; intros (E);
187 [1: rewrite > (b2pT ? ? (eqP d ? ?) E) in H4;
188 rewrite > H4 in Hy; destruct Hy;
189 |2:intros; reflexivity]]
190 |2: rewrite > uniq_tail in H1;
191 generalize in match (refl_eq ? (uniq d l1));
192 generalize in match (uniq d l1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
193 [1: intros (E); rewrite > E in H1; rewrite > andbC in H1; simplify in H1;
194 unfold Not; intros (A); lapply (A t) as A';
195 [1: simplify in A'; rewrite > cmp_refl in A'; simplify in A';
196 destruct A'; clear A'; rewrite < count_O_mem in H1;
197 rewrite > Hcut in H1; destruct H1;
198 |2: simplify; rewrite > cmp_refl; reflexivity;]
199 |2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin;
200 intros (r Mrl1); lapply (A r);
201 [2: simplify; rewrite > Mrl1; cases (cmp d r t); reflexivity]
202 generalize in match (refl_eq ? (cmp d r t));
203 generalize in match (cmp d r t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
204 [1: intros (E); simplify in Hletin1; rewrite > E in Hletin1;
205 destruct Hletin1; rewrite < count_O_mem in Mrl1;
206 rewrite > Hcut in Mrl1; destruct Mrl1;
207 |2: intros; simplify in Hletin1; rewrite > H2 in Hletin1;
208 simplify in Hletin1; apply (Hletin1);]]]
211 lemma mem_finType : ∀d:finType.∀x:d. mem d x (enum d) = true.
212 intros 1 (d); cases d; simplify; intros; rewrite < count_O_mem;
213 rewrite > H; reflexivity;
216 lemma uniq_fintype_enum : ∀d:finType. uniq d (enum d) = true.
217 intros; cases d; simplify; apply (p2bT ? ? (uniqP ? ?)); intros; apply H;
220 lemma sub_enumP : ∀d:finType.∀p:d→bool.∀x:sub_eqType d p.
221 count (sub_eqType d p) (cmp ? x) (filter ? ? (if_p ? p) (enum d)) = (S O).
222 intros (d p x); cases x (t Ht); clear x;
223 generalize in match (mem_finType d t);
224 generalize in match (uniq_fintype_enum d);
225 elim (enum d); [destruct H1] simplify;
226 cases (in_sub_eq d p t1); simplify;
227 [1:generalize in match H3; clear H3; cases s (r Hr); clear s;
228 simplify; intros (Ert1); generalize in match Hr; clear Hr;
229 rewrite > Ert1; clear Ert1; clear r; intros (Ht1);
230 unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?);
231 simplify; generalize in match (refl_eq ? (cmp d t t1));
232 generalize in match (cmp d t t1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
233 intros (Ett1); simplify;
234 [1: cut (count (sub_eqType d p) (cmp (sub_eqType d p) {t,Ht})
235 (filter d (sigma d p) (if_p d p) l) = O); [1:rewrite > Hcut; reflexivity]
236 lapply (uniq_mem ? ? ? H1);
237 generalize in match Ht;
238 rewrite > (b2pT ? ? (eqP d ? ?) Ett1); intros (Ht1'); clear Ht1;
239 generalize in match Hletin; elim l; [ reflexivity]
240 simplify; cases (in_sub_eq d p t2); simplify;
241 [1: generalize in match H5; cases s; simplify; intros; clear H5;
242 unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?);
243 simplify; rewrite > H7; simplify in H4;
244 generalize in match H4; clear H4;
245 generalize in match (refl_eq ? (cmp d t1 t2));
246 generalize in match (cmp d t1 t2) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
247 simplify; intros; [1: destruct H5] apply H3; assumption;
249 generalize in match H4; clear H4; simplify;
250 generalize in match (refl_eq ? (cmp d t1 t2));
251 generalize in match (cmp d t1 t2) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
252 simplify; intros; [1: destruct H6] assumption;]
253 |2: apply H; [ rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]
254 simplify in H2; rewrite > Ett1 in H2; simplify in H2; assumption]
255 |2:rewrite > H; [1:reflexivity|2: rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]
256 simplify in H2; generalize in match H2; generalize in match (refl_eq ? (cmp d t t1));
257 generalize in match (cmp d t t1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
258 intros (E); [2:assumption]
259 lapply (b2pT ? ? (eqP d ? ?) E); clear H; rewrite > Hletin in Ht;
260 rewrite > Ht in H3; destruct H3;]
263 definition sub_finType : ∀d:finType.∀p:d→bool.finType ≝
264 λd:finType.λp:d→bool. mk_finType (sub_eqType d p) (filter ? ? (if_p ? p) (enum d)) (sub_enumP d p).