matita/library/decidable_kit/fintype.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/decidable_kit/fintype/".
  16
  17 include "decidable_kit/eqtype.ma".
  18 include "decidable_kit/list_aux.ma".
  19
  20 record finType : Type ≝ {
  21   fsort :> eqType;
  22   enum : list fsort;
  23   enum_uniq : ∀x:fsort. count fsort (cmp fsort x) enum = (S O)
  24 }.
  25
  26 definition segment : nat → eqType ≝
  27   λn.sub_eqType nat_eqType (λx:nat_eqType.ltb x n).
  28
  29 definition is_some : ∀d:eqType. option d → bool ≝
  30   λd:eqType.λo:option d.notb (cmp (option_eqType d) (None ?) o).
  31
  32 definition filter ≝
  33   λA,B:Type.λp:A→option B.λl:list A.
  34   foldr A ?
  35     (λx,acc. match (p x) with [None ⇒ acc | (Some y) ⇒ cons B y acc]) (nil B) l.
  36
  37 definition segment_enum  ≝
  38   λbound.filter ? ? (if_p nat_eqType (λx.ltb x bound)) (iota O bound).
  39
  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]
  42 rewrite < leb_eqb;
  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;
  47 qed.
  48
  49 lemma mem_filter :
  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;]]
  71 qed.
  72
  73 lemma count_O :
  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);
  80 cases b; simplify;
  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]
  87 qed.
  88
  89 lemma segment_finType : nat → finType.
  90 intros (bound);
  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;
  97    unfold segment_enum;
  98    generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?);
  99    intros 1 (m); elim m  (Hm Hn p IH Hm Hn);
 100    [ destruct Hm;
 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);
 110         cases b; simplify;
 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]
 120            intros 1 (x);
 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);
 131            intros (w Hw);
 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;
 146      ]]]
 147 qed.
 148
 149 let rec uniq (d:eqType) (l:list d) on l : bool ≝
 150   match l with
 151   [ nil⇒ true
 152   | (cons x tl) ⇒ andb (notb (mem d x tl)) (uniq d tl)].
 153
 154 lemma uniq_tail_OLD : ∀d:eqType.∀x:d.∀l:list d.uniq d (x::l) = true → uniq d l = true.
 155 intros (d x l Uxl); simplify in Uxl; cases (b2pT ? ? (andbP ? ?) Uxl); assumption;
 156 qed.
 157
 158 lemma uniq_mem : ∀d:eqType.∀x:d.∀l:list d.uniq d (x::l) = true → mem d x l = false.
 159 intros (d x l H); simplify in H; lapply (b2pT ? ? (andbP ? ?) H) as H1; clear H;
 160 cases H1 (H2 H3); lapply (b2pT ? ?(negbP ?) H2); assumption;
 161 qed.
 162
 163 lemma andbA : ∀a,b,c.andb a (andb b c) = andb (andb a b) c.
 164 intros; cases a; cases b; cases c; reflexivity; qed.
 165
 166 lemma andbC : ∀a,b. andb a b = andb b a.
 167 intros; cases a; cases b; reflexivity; qed.
 168
 169 lemma uniq_tail :
 170   ∀d:eqType.∀x:d.∀l:list d. uniq d (x::l) = andb (negb (mem d x l)) (uniq d l).
 171 intros (d x l);
 172 elim l; [1: simplify; reflexivity]
 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;
 175 intros (E); simplify ; rewrite > E; simplify; [1: reflexivity;]
 176 rewrite > andbA; rewrite > andbC in ⊢ (? ? (? % ?) ?); rewrite < andbA;
 177 rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA;
 178 reflexivity;
 179 qed.
 180
 181 lemma count_O_mem : ∀d:eqType.∀x:d.∀l:list d.ltb O (count d (cmp d x) l) = mem d x l.
 182 intros 3 (d x l); elim l [reflexivity]
 183 simplify; fold simplify (mem d x l1); fold simplify (count d (cmp d x) l1);
 184 rewrite < H; cases (cmp d x t); simplify; reflexivity;
 185 qed.
 186
 187 lemma uniqP : ∀d:eqType.∀l:list d.
 188   reflect (∀x:d.mem d x l = true → count d (cmp d x) l = (S O)) (uniq d l).
 189 intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: destruct H]
 190 [1: generalize in match H2; simplify in H2; fold simplify (orb (cmp d x t) (mem d x l1)) in H2;
 191     (* lapply (uniq_tail ? ? ? H1) as Ul1; *)
 192     lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2;
 193     cases H3; clear H3; intros;
 194     [2: lapply (uniq_mem ? ? ? H1) as H4;
 195         generalize in match (refl_eq ? (cmp d x t));
 196         generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
 197         intros (H5);
 198         [1: simplify; rewrite > H5; simplify; fold simplify (count d (cmp d x) l1);
 199             rewrite > count_O; [1:reflexivity]
 200             intros (y Hy); rewrite > (b2pT ? ? (eqP d ? ?) H5) in H2 H3 H4 ⊢ %;
 201             clear H5; clear x; rewrite > H2 in H4; destruct H4;
 202          |2: simplify; rewrite > H5; simplify;
 203              fold simplify (count d (cmp d x) (l1));
 204              apply H; rewrite > uniq_tail in H1;
 205              cases (b2pT ? ? (andbP ? ?) H1);
 206              assumption;]
 207     |1: simplify; rewrite > H2; simplify;
 208         fold simplify (count d (cmp d x) l1);
 209         rewrite > count_O; [1:reflexivity]
 210         intros (y Hy); rewrite > (b2pT ? ? (eqP d ? ?) H2) in H3 ⊢ %;
 211         clear H2; clear x;
 212         lapply (uniq_mem ? ? ? H1) as H4;
 213         generalize in match (refl_eq ? (cmp d t y));
 214         generalize in match (cmp d t y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
 215         [1: intros (E); rewrite > (b2pT ? ? (eqP d ? ?) E) in H4;
 216             rewrite > H4 in Hy; destruct Hy;
 217         |2:intros; reflexivity]]
 218 |2: rewrite > uniq_tail in H1;
 219     generalize in match (refl_eq ? (uniq d l1));
 220     generalize in match (uniq d l1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
 221     [1: intros (E); rewrite > E in H1; rewrite > andbC in H1; simplify in H1;
 222       unfold Not; intros (A); lapply (A t) as A';
 223       [1: simplify in A';
 224           rewrite > cmp_refl in A'; simplify in A';
 225           destruct A'; clear A'; fold simplify (count d (cmp d t) l1) in Hcut;
 226           rewrite < count_O_mem in H1;
 227           rewrite > Hcut in H1; destruct H1;
 228       |2: simplify; rewrite > cmp_refl; reflexivity;]
 229     |2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin;
 230         intros (r Mrl1); lapply (A r); [2: simplify; rewrite > Mrl1; cases (cmp d r t); reflexivity]
 231         generalize in match (refl_eq ? (cmp d r t));
 232         generalize in match (cmp d r t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
 233         [1: intros (E); simplify in Hletin1; rewrite > E in Hletin1;
 234             simplify in Hletin1; fold simplify (count d (cmp d r) l1) in Hletin1;
 235             destruct Hletin1;
 236             rewrite < count_O_mem in Mrl1;
 237             rewrite > Hcut in Mrl1;
 238             destruct Mrl1;
 239         |2: intros; simplify in Hletin1; rewrite > H2 in Hletin1;
 240             simplify in Hletin1; apply (Hletin1);]]]
 241 qed.
 242
 243 lemma mem_finType : ∀d:finType.∀x:d. mem d x (enum d) = true.
 244 intros 1 (d); cases d; simplify; intros; rewrite < count_O_mem;
 245 rewrite > H; reflexivity;
 246 qed.
 247
 248 lemma uniq_fintype_enum :  ∀d:finType. uniq d (enum d) = true.
 249 intros; cases d; simplify; apply (p2bT ? ? (uniqP ? ?)); intros; apply H;
 250 qed.
 251
 252 lemma sub_enumP : ∀d:finType.∀p:d→bool.∀x:sub_eqType d p.
 253   count (sub_eqType d p) (cmp ? x) (filter ? ? (if_p ? p) (enum d)) = (S O).
 254 intros (d p x); cases x (t Ht); clear x;
 255 generalize in match (mem_finType d t);
 256 generalize in match (uniq_fintype_enum d);
 257 elim (enum d); [1:destruct H1]
 258 simplify; fold simplify (filter d (sigma d p) (if_p d p) l);
 259 cases (in_sub_eq d p t1); simplify in ⊢ (? ? (? ? ? %) ?);
 260  [simplify; fold simplify (count (sub_eqType d p) (cmp (sub_eqType d p) {t,Ht})
 261                         (filter d (sigma d p) (if_p d p) l));
 262   generalize in match H3; clear H3; cases s (r Hr); clear s;
 263   simplify; intros (Ert1); generalize in match Hr; clear Hr;
 264   rewrite > Ert1; clear Ert1; clear r; intros (Ht1);
 265   unfold  sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?);
 266   simplify; generalize in match (refl_eq ? (cmp d t t1));
 267   generalize in match (cmp d t t1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
 268   intros (Ett1); simplify;
 269     [1: cut (count (sub_eqType d p) (cmp (sub_eqType d p) {t,Ht})
 270             (filter d (sigma d p) (if_p d p) l) = O); [1:rewrite > Hcut; reflexivity]
 271         lapply (uniq_mem ? ? ? H1);
 272         generalize in match Ht;
 273         rewrite > (b2pT ? ? (eqP d ? ?) Ett1); intros (Ht1'); clear Ht1;
 274         generalize in match Hletin; elim l; [1: reflexivity]
 275         simplify; cases (in_sub_eq d p t2); simplify;
 276           [1: generalize in match H5; cases s; simplify; intros; clear H5;
 277               unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?);
 278               simplify; rewrite > H7; simplify in H4;
 279               generalize in match H4; clear H4;
 280               generalize in match (refl_eq ? (cmp d t1 t2));
 281               generalize in match (cmp d t1 t2) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
 282               simplify; intros; [1: destruct H5] apply H3; assumption
 283           |2:apply H3;
 284               generalize in match H4; clear H4; simplify;
 285               generalize in match (refl_eq ? (cmp d t1 t2));
 286               generalize in match (cmp d t1 t2) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
 287               simplify; intros; [1: destruct H6] assumption;]
 288     |2: apply H; [ rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]
 289         simplify in H2; rewrite > Ett1 in H2; simplify in H2; assumption]
 290  | rewrite > H; [1:reflexivity|2: rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]
 291    simplify in H2; generalize in match H2; generalize in match (refl_eq ? (cmp d t t1));
 292    generalize in match (cmp d t t1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
 293    intros (E);
 294      [lapply (b2pT ? ? (eqP d ? ?) E); clear H; rewrite > Hletin in Ht;
 295       rewrite > Ht in H3; destruct H3;
 296      |assumption]]
 297 qed.
 298
 299 definition sub_finType : ∀d:finType.∀p:d→bool.finType ≝
 300   λd:finType.λp:d→bool. mk_finType (sub_eqType d p) (filter ? ? (if_p ? p) (enum d)) (sub_enumP d p).
 301