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;[reflexivity]
  42 apply (cmpP nat_eqType x n); intros (E); rewrite > H; clear H; simplify;
  43 [1: symmetry; apply (p2bT ? ? (lebP ? ?)); rewrite > E; apply le_n;
  44 |2: rewrite < (leb_eqb x n); rewrite > E; reflexivity;]
  45 qed.
  46
  47 lemma mem_filter :
  48   ∀d1,d2:eqType.∀x:d2.∀l:list d1.∀p:d1 → option d2.
  49   (∀y.mem d1 y l = true →
  50     match (p y) with [None ⇒ false | (Some q) ⇒ cmp d2 x q] = false) →
  51   mem d2 x (filter d1 d2 p l) = false.
  52 intros 5 (d1 d2 x l p);
  53 elim l; simplify; [reflexivity]
  54 generalize in match (refl_eq ? (p t));
  55 generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; intros (Hpt);
  56 [1: apply H; intros (y Hyl);
  57     apply H1; simplify;
  58     rewrite > Hyl; rewrite > orbC; reflexivity;
  59 |2: simplify; apply (cmpP d2 x s); simplify; intros (E);
  60     [1: rewrite < (H1 t); simplify; [rewrite > Hpt; rewrite > E]
  61         simplify; rewrite > cmp_refl; reflexivity
  62     |2: apply H; intros; apply H1; simplify; rewrite > H2;
  63         rewrite > orbC; reflexivity]]
  64 qed.
  65
  66 lemma count_O :
  67   ∀d:eqType.∀p:d→bool.∀l:list d.
  68     (∀x:d.mem d x l = true → notb (p x) = true) → count d p l = O.
  69 intros 3 (d p l); elim l; simplify; [1: reflexivity]
  70 generalize in match (refl_eq ? (p t));
  71 generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b);
  72 cases b; simplify;
  73 [2:intros (Hpt); apply H; intros; apply H1; simplify;
  74    apply (cmpP d x t); [2: rewrite > H2;]; intros; reflexivity;
  75 |1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; autobatch]
  76    rewrite > H2 in Hletin; simplify in Hletin; destruct Hletin]
  77 qed.
  78
  79 lemma segment_finType : nat → finType.
  80 intros (bound);
  81 letin fsort ≝ (segment bound);
  82 letin enum ≝ (segment_enum bound);
  83 cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O));
  84  [ apply (mk_finType fsort enum Hcut)
  85  | intros (x); cases x (n Hn); simplify in Hn; clear x;
  86    generalize in match Hn; generalize in match Hn; clear Hn;
  87    unfold enum;
  88    unfold segment_enum;
  89    generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?);
  90    intros 1 (m); elim m  (Hm Hn p IH Hm Hn); [ simplify in Hm; destruct Hm ]
  91    simplify; cases (eqP bool_eqType (ltb p bound) true); simplify;
  92    [1:unfold fsort;
  93       unfold segment in ⊢ (? ? match ? % ? ? with [_ ⇒ ?|_ ⇒ ?] ?);
  94       unfold nat_eqType in ⊢ (? ? match % with [_ ⇒ ?|_ ⇒ ?] ?);
  95       simplify; apply (cmpP nat_eqType n p); intros (Enp); simplify;
  96       [2:rewrite > IH; [1,3: autobatch]
  97          rewrite <  ltb_n_Sm in Hm; rewrite > Enp in Hm;
  98          rewrite > orbC in Hm; assumption;
  99       |1:clear IH; rewrite > (count_O fsort); [reflexivity]
 100          intros 1 (x); rewrite < Enp; cases x (y Hy);
 101          intros (ABS); clear x; unfold segment; unfold notb; simplify;
 102          apply (cmpP ? n y); intros (Eny); simplify; [2:reflexivity]
 103          rewrite < ABS; symmetry; clear ABS;
 104          generalize in match Hy; clear Hy;rewrite < Eny;
 105          simplify; intros (Hn); apply (mem_filter nat_eqType fsort); intros (w Hw);
 106          fold simplify (sort nat_eqType); (* CANONICAL?! *)
 107          cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w);
 108          simplify; [2: reflexivity]
 109          generalize in match H1; clear H1; cases s (r Pr); clear s; intros (H1);
 110          unfold fsort; unfold segment; simplify; simplify in H1; rewrite > H1;
 111          rewrite > iota_ltb in Hw; apply (p2bF ? ? (eqP nat_eqType ? ?));
 112          unfold Not; intros (Enw); rewrite > Enw in Hw;
 113          rewrite > ltb_refl in Hw; destruct Hw]
 114    |2:rewrite > IH; [1:reflexivity|3:assumption]
 115       rewrite <  ltb_n_Sm in Hm;
 116       cases (b2pT ? ?(orbP ? ?) Hm);[1: assumption]
 117       rewrite > (b2pT ? ? (eqbP ? ?) H1) in Hn;
 118       rewrite > Hn in H; cases (H ?); reflexivity]]
 119 qed.
 120
 121 let rec uniq (d:eqType) (l:list d) on l : bool ≝
 122   match l with
 123   [ nil ⇒ true
 124   | (cons x tl) ⇒ andb (notb (mem d x tl)) (uniq d tl)].
 125
 126 lemma uniq_mem : ∀d:eqType.∀x:d.∀l:list d.uniq d (x::l) = true → mem d x l = false.
 127 intros (d x l H); simplify in H; lapply (b2pT ? ? (andbP ? ?) H) as H1; clear H;
 128 cases H1 (H2 H3); lapply (b2pT ? ?(negbP ?) H2); assumption;
 129 qed.
 130
 131 lemma andbA : ∀a,b,c.andb a (andb b c) = andb (andb a b) c.
 132 intros; cases a; cases b; cases c; reflexivity; qed.
 133
 134 lemma andbC : ∀a,b. andb a b = andb b a.
 135 intros; cases a; cases b; reflexivity; qed.
 136
 137 lemma uniq_tail :
 138   ∀d:eqType.∀x:d.∀l:list d. uniq d (x::l) = andb (negb (mem d x l)) (uniq d l).
 139 intros (d x l); elim l; simplify; [reflexivity]
 140 apply (cmpP d x t); intros (E); simplify ; try rewrite > E; [reflexivity]
 141 rewrite > andbA; rewrite > andbC in ⊢ (? ? (? % ?) ?); rewrite < andbA;
 142 rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA; reflexivity;
 143 qed.
 144
 145 lemma count_O_mem : ∀d:eqType.∀x:d.∀l:list d.ltb O (count d (cmp d x) l) = mem d x l.
 146 intros 3 (d x l); elim l [reflexivity] simplify; rewrite < H; cases (cmp d x t);
 147 reflexivity; qed.
 148
 149 lemma uniqP : ∀d:eqType.∀l:list d.
 150   reflect (∀x:d.mem d x l = true → count d (cmp d x) l = (S O)) (uniq d l).
 151 intros (d l); apply prove_reflect; elim l; [1: simplify in H1; destruct H1 | 3: simplify in H; destruct H]
 152 [1: generalize in match H2; simplify in H2;
 153     lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2;
 154     cases H3; clear H3; intros;
 155     [2: lapply (uniq_mem ? ? ? H1) as H4; simplify; apply (cmpP d x t);
 156         intros (H5); simplify;
 157         [1: rewrite > count_O; [reflexivity]
 158             intros (y Hy); rewrite > H5 in H2 H3 ⊢ %; clear H5; clear x;
 159             rewrite > H2 in H4; destruct H4;
 160          |2: simplify; apply H;
 161              rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1);
 162              assumption;]
 163     |1: simplify; rewrite > H2; simplify; rewrite > count_O; [reflexivity]
 164         intros (y Hy); rewrite > (b2pT ? ? (eqP d ? ?) H2) in H3 ⊢ %;
 165         clear H2; clear x; lapply (uniq_mem ? ? ? H1) as H4;
 166         apply (cmpP d t y); intros (E); [2: reflexivity].
 167         rewrite > E in H4; rewrite > H4 in Hy; destruct Hy;]
 168 |2: rewrite > uniq_tail in H1;
 169     generalize in match (refl_eq ? (uniq d l1));
 170     generalize in match (uniq d l1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
 171     [1: intros (E); rewrite > E in H1; rewrite > andbC in H1; simplify in H1;
 172         unfold Not; intros (A); lapply (A t) as A';
 173         [1: simplify in A'; rewrite > cmp_refl in A'; simplify in A';
 174             destruct A'; rewrite < count_O_mem in H1;
 175             rewrite > Hcut in H1; simplify in H1; destruct H1;
 176         |2: simplify; rewrite > cmp_refl; reflexivity;]
 177     |2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin;
 178         intros (r Mrl1); lapply (A r);
 179           [2: simplify; rewrite > Mrl1; cases (cmp d r t); reflexivity]
 180         generalize in match Hletin1; simplify; apply (cmpP d r t);
 181         simplify; intros (E Hc); [2: assumption]
 182         destruct Hc; rewrite < count_O_mem in Mrl1;
 183         rewrite > Hcut in Mrl1; simplify in Mrl1; destruct Mrl1;]]
 184 qed.
 185
 186 lemma mem_finType : ∀d:finType.∀x:d. mem d x (enum d) = true.
 187 intros 1 (d); cases d; simplify; intros; rewrite < count_O_mem;
 188 rewrite > H; reflexivity;
 189 qed.
 190
 191 lemma uniq_fintype_enum :  ∀d:finType. uniq d (enum d) = true.
 192 intros; cases d; simplify; apply (p2bT ? ? (uniqP ? ?)); intros; apply H;
 193 qed.
 194
 195 lemma sub_enumP : ∀d:finType.∀p:d→bool.∀x:sub_eqType d p.
 196   count (sub_eqType d p) (cmp ? x) (filter ? ? (if_p ? p) (enum d)) = (S O).
 197 intros (d p x); cases x (t Ht); clear x;
 198 generalize in match (mem_finType d t);
 199 generalize in match (uniq_fintype_enum d);
 200 elim (enum d); [simplify in H1; destruct H1] simplify;
 201 cases (in_sub_eq d p t1); simplify;
 202 [1:generalize in match H3; clear H3; cases s (r Hr); clear s;
 203    simplify; intros (Ert1); generalize in match Hr; clear Hr;
 204    rewrite > Ert1; clear Ert1; clear r; intros (Ht1);
 205    unfold  sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [_ ⇒ ?|_ ⇒ ?] ?);
 206    simplify; apply (cmpP ? t t1); simplify; intros (Ett1);
 207    [1: cut (count (sub_eqType d p) (cmp (sub_eqType d p) {t,Ht})
 208             (filter d (sigma d p) (if_p d p) l) = O); [1:rewrite > Hcut; reflexivity]
 209        lapply (uniq_mem ? ? ? H1);
 210        generalize in match Ht;
 211        rewrite > Ett1; intros (Ht1'); clear Ht1;
 212        generalize in match Hletin; elim l; [ reflexivity]
 213        simplify; cases (in_sub_eq d p t2); simplify;
 214        [1: generalize in match H5; cases s; simplify; intros; clear H5;
 215            unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [_ ⇒ ?|_ ⇒ ?] ?);
 216            simplify; rewrite > H7; simplify in H4;
 217            generalize in match H4; clear H4; apply (cmpP ? t1 t2);
 218            simplify; intros; [destruct H5] apply H3; assumption;
 219        |2: apply H3;
 220            generalize in match H4; clear H4; simplify; apply (cmpP ? t1 t2);
 221            simplify; intros; [destruct H6] assumption;]
 222    |2: apply H; [ rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]
 223        simplify in H2; rewrite > Ett1 in H2; simplify in H2; assumption]
 224 |2:rewrite > H; [1:reflexivity|2: rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]
 225    simplify in H2; generalize in match H2; apply (cmpP ? t t1);
 226    intros (E) [2:assumption] clear H; rewrite > E in Ht; rewrite > H3 in Ht;
 227    destruct Ht;]
 228 qed.
 229
 230 definition sub_finType : ∀d:finType.∀p:d→bool.finType ≝
 231   λd:finType.λp:d→bool. mk_finType (sub_eqType d p) (filter ? ? (if_p ? p) (enum d)) (sub_enumP d p).
 232