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; [1:reflexivity]
43 generalize in match (refl_eq ? (cmp ? x n));
44 generalize in match (cmp ? x n) in ⊢ (? ? % ? → %); intros 1 (b);
45 cases b; simplify; intros (H1); [1: reflexivity]
46 rewrite > H; fold simplify (ltb x n); rewrite > H1; reflexivity;
50 ∀d1,d2:eqType.(*∀y:d1.*)∀x:d2.∀l:list d1.∀p:d1 → option d2.
51 (∀y.mem d1 y l = true →
52 match (p y) with [None ⇒ false | (Some q) ⇒ cmp d2 x q] = false) →
53 mem d2 x (filter d1 d2 p l) = false.
54 intros 5 (d1 d2 x l p);
55 elim l; [1: simplify; auto]
56 simplify; fold simplify (filter d1 d2 p l1);
57 generalize in match (refl_eq ? (p t));
58 generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
59 [1: simplify; intros (Hpt); apply H; intros (y Hyl);
60 apply H1; simplify; fold simplify (orb (cmp ? y t) (mem ? y l1));
61 rewrite > Hyl; rewrite > orbC; reflexivity;
62 |2:simplify; intros (Hpt);
63 generalize in match (refl_eq ? (cmp ? x s));
64 generalize in match (cmp ? x s) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
65 [1: simplify; intros (Exs);
66 rewrite < (H1 t); [2: simplify; rewrite > cmp_refl; reflexivity;]
67 rewrite > Hpt; simplify; symmetry; assumption;
68 |2: intros (Dxs); simplify; apply H; intros;
69 apply H1; simplify; fold simplify (orb (cmp ? y t) (mem ? y l1));
70 rewrite > H2; rewrite > orbC; 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 fold simplify (count d p l1); (* XXX simplify troppo *)
78 generalize in match (refl_eq ? (p t));
79 generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b);
81 [2:intros (Hpt); apply H; intros; apply H1; simplify;
82 generalize in match (refl_eq ? (cmp d x t));
83 generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b1);
84 cases b1; simplify; intros; [2:rewrite > H2] auto.
85 |1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; auto]
86 rewrite > H2 in Hletin; simplify in Hletin; destruct Hletin]
89 lemma segment_finType : nat → finType.
91 letin fsort ≝ (segment bound);
92 letin enum ≝ (segment_enum bound);
93 cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O));
94 [ apply (mk_finType fsort enum Hcut)
95 | intros (x); cases x (n Hn); simplify in Hn; clear x;
96 generalize in match Hn; generalize in match Hn; clear Hn;
98 generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?);
99 intros 1 (m); elim m (Hm Hn p IH Hm Hn);
101 | simplify; cases (eqP bool_eqType (ltb p bound) true); simplify;
102 (* XXX simplify che spacca troppo *)
103 fold simplify (filter nat_eqType (sigma nat_eqType (λx.ltb x bound))
104 (if_p nat_eqType (λx.ltb x bound)) (iota O p));
105 [1:unfold segment in ⊢ (? ? match ? % ? ? with [true⇒ ?|false⇒ ?] ?);
106 unfold nat_eqType in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?);
107 simplify in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?);
108 generalize in match (refl_eq ? (eqb n p));
109 generalize in match (eqb n p) in ⊢ (? ? ? % → %); intros 1(b);
111 [2:intros (Enp); rewrite > IH; [1,3: auto]
112 rewrite < ltb_n_Sm in Hm; rewrite > Enp in Hm;
113 generalize in match Hm; cases (ltb n p); intros; [1:reflexivity]
114 simplify in H1; destruct H1;
115 |1:clear IH; intros (Enp);
116 fold simplify (count fsort (cmp fsort {n, Hn})
117 (filter ? (sigma nat_eqType (λx.ltb x bound))
118 (if_p nat_eqType (λx.ltb x bound)) (iota O p)));
119 rewrite > (count_O fsort); [1: reflexivity]
121 rewrite < (b2pT ? ? (eqP ? n ?) Enp);
122 cases x (y Hy); intros (ABS); clear x;
123 unfold segment; unfold notb; simplify;
124 generalize in match (refl_eq ? (cmp ? n y));
125 generalize in match (cmp ? n y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
126 intros (Eny); simplify; [2: auto]
127 rewrite < ABS; symmetry; clear ABS;
128 generalize in match Hy; clear Hy; rewrite < (b2pT ? ? (eqP nat_eqType ? ?) Eny);
129 simplify; intros (Hn); fold simplify (iota O n);
130 apply (mem_filter nat_eqType fsort);
132 fold simplify (sort nat_eqType);
133 cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w);
134 simplify; [2: reflexivity]
135 generalize in match H1; clear H1; cases s; clear s; intros (H1);
136 unfold segment; simplify; simplify in H1; rewrite > H1;
137 rewrite > iota_ltb in Hw;
138 apply (p2bF ? ? (eqP nat_eqType ? ?));
139 unfold Not; intros (Enw);
140 rewrite > Enw in Hw; rewrite > ltb_refl in Hw; destruct Hw]
141 |2:rewrite > IH; [1:reflexivity|3:assumption]
142 rewrite < ltb_n_Sm in Hm;
143 cases (b2pT ? ?(orbP ? ?) Hm);[1: assumption]
144 rewrite > (b2pT ? ? (eqbP ? ?) H1) in Hn;
145 rewrite > Hn in H; cases (H ?); reflexivity;