helm/software/matita/library/decidable_kit/fgraph.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 include "decidable_kit/fintype.ma".
  16
  17 definition setA : ∀T:eqType.T → bool := λT,x.true.
  18
  19 inductive fgraphType (d1 : finType) (d2 : eqType) : Type :=
  20   | Fgraph : ∀val:list d2. (length ? val) = (count ? (setA d1) (enum d1)) -> fgraphType d1 d2.
  21
  22 definition fval : ∀d1: finType. ∀d2 : eqType. fgraphType d1 d2 → list d2 :=
  23   λd1,d2,x. match x with [ (Fgraph val _) ⇒ val].
  24
  25 definition fproof : ∀d1:finType.∀d2:eqType.∀u. length ? (fval d1 d2 u) = (count ? (setA d1) ?) :=
  26   λd1:finType.λd2,u. match u return (λx. length ? (fval d1 d2 x) = (count ? (setA d1) (enum d1))) with [
  27     (Fgraph _ proof) ⇒ proof].
  28
  29 lemma fgraph_eqP : ∀d1:finType.∀d2:eqType.∀f1,f2:fgraphType d1 d2.
  30   eq_compatible ? f1 f2 (cmp (list_eqType d2) (fval d1 d2 f1) (fval d1 d2 f2)).
  31 intros (d1 d2 f1 f2); cases f1; cases f2; simplify; clear f1 f2;
  32 apply prove_reflect; intros;
  33  [1: generalize in match H; rewrite > (b2pT ? ? (eqP (list_eqType d2) ? ?) H2);
  34      intros; clear H H2; rewrite < (pirrel ? ? ? H1 H3 (eqType_decidable nat_eqType));
  35      reflexivity
  36  |2: unfold Not; intros (H3); destruct H3;
  37      rewrite > (cmp_refl (list_eqType d2)) in H2; destruct H2;]
  38 qed.
  39
  40 definition fgraph_eqType : finType → eqType → eqType ≝
  41   λd1,d2. mk_eqType ? ? (fgraph_eqP d1 d2).
  42
  43 lemma fval_eqE :
  44   ∀d1:finType.∀d2:eqType.∀u,v:fgraph_eqType d1 d2. cmp (list_eqType d2) (fval ? ? u) (fval ? ? v) = cmp ? u v.
  45 intros; reflexivity; qed.
  46
  47 (*
  48 lemma fval_inj : injective fval.
  49 Proof. by move => u v; move/eqP; move/fgraph_eqP. Qed.
  50 *)
  51
  52  (* if the domain is not empty the default is the first elem of the graph *)
  53 lemma fgraph_default : ∀d1:finType.∀d2:eqType. d1 -> fgraph_eqType d1 d2 -> d2.
  54 intros 4 (d1 d2 x f); cases f; fold unfold sort (sort d2);
  55 generalize in match H; clear H; cases val; clear val;
  56  [2: intros; assumption
  57  |1: simplify; generalize in match (enum_uniq d1); cases (enum d1);
  58      unfold setA; simplify; intros (H H1); [1: destruct (H x) | destruct H1]]
  59 qed.
  60
  61 definition infgraph : ∀d1,d2:finType.∀s : list_eqType d2. option (fgraph_eqType d1 d2) :=
  62   λd1,d2:finType.λs:list d2.
  63   match eqbP (length ? s) (count ? (setA d1) (enum d1))
  64   with
  65   [ (reflect_true p) ⇒ Some ? (Fgraph ? ? ? p)
  66   | (reflect_false p) ⇒ None ?].
  67
  68 inductive infgraph_spec (d1, d2 : finType) (s : list_eqType d2) : option (fgraph_eqType d1 d2) -> Type :=
  69   | Some_tup : ∀u : fgraphType d1 d2. length ? s = (count ? (setA d1) (enum d1)) -> fval ? ? u = s -> infgraph_spec ? ? s (Some ? u)
  70   | None_tup: notb (eqb (length ? s) (count ? (setA d1) (enum d1))) = true -> infgraph_spec ? ? s (None ?).
  71
  72 lemma infgraphP : ∀d1,d2:finType.∀s:list_eqType d2. infgraph_spec d1 d2 s (infgraph ? ? s).
  73 unfold infgraph; intros; cases (eqbP (length d2 s) (count d1 (setA d1) (enum d1)));
  74 simplify;
  75  [1: apply (Some_tup d1 d2 s ? H); reflexivity;
  76  |2: apply None_tup; rewrite > (p2bF ? ? (eqbP ? ?) H). reflexivity]
  77 qed.
  78
  79 definition infgraphseq :
  80   ∀d1,d2:finType.list_eqType (list_eqType d2) -> list_eqType (fgraph_eqType d1 d2) :=
  81   λd1,d2:finType.
  82     (foldr ? ?
  83       (λs: list d2.λts:list (fgraphType d1 d2).
  84          match infgraph d1 d2 s with
  85          [ None ⇒ ts
  86          | (Some u) ⇒ u::ts]) (nil ?)).
  87
  88 lemma count_setA : ∀d:eqType.∀l. count ? (setA d) l = length ? l.
  89 intros; elim l; [reflexivity] simplify; rewrite > H; clear H; reflexivity; qed.
  90
  91 lemma mem_infgraphseq :
  92   ∀d1,d2:finType.∀a:list_eqType (list_eqType d2).∀x:fgraph_eqType d1 d2.
  93     mem ? x (infgraphseq d1 d2 a) = mem (list_eqType d2) (fval d1 d2 x) a.
  94 intros 3 (d1 d2 l); elim l (x hd tl IH x); [1: reflexivity]
  95 simplify; cases (infgraphP d1 d2 hd); simplify;
  96 rewrite > IH; clear IH; [1: rewrite < H1; reflexivity;]
  97 lapply (b2pT ? ? (negbP ?) H) as H1; clear H;
  98 lapply (b2pF ? ? (eqbP ? ?) H1) as H2; clear H1;
  99 cases (mem (list_eqType d2) (fval d1 d2 x) tl); rewrite > orbC; simplify; [reflexivity]
 100 symmetry; apply (p2bF ? ? (eqP ? ? ?)); unfold Not; intros (Exhd);
 101 apply H2; rewrite < Exhd; clear Exhd H2 tl hd l;
 102 generalize in match x; clear x; cases d1 0; simplify; intros; cases s;
 103 simplify; clear s;  rewrite > H1; simplify; reflexivity;
 104 qed.
 105
 106 lemma uniq_infgraphseq : ∀d1,d2,s. uniq ? s = true -> uniq ? (infgraphseq d1 d2 s) = true.
 107 intros 3 (d1 d2 l); elim l (H hd tl IH H); [reflexivity] simplify;
 108 rewrite > (uniq_tail) in H; lapply (b2pT ? ? (andbP ? ?) H); clear H; decompose;
 109 cases (infgraphP d1 d2 hd); simplify;
 110   [1: rewrite > IH; [2:assumption] rewrite > andbC; simplify;
 111       rewrite < H3 in H; rewrite > mem_infgraphseq; assumption
 112   |2: apply IH; assumption]
 113 qed.
 114
 115 definition multes :
 116   ∀d:finType.∀e:d.list_eqType (list_eqType d) -> list_eqType (list_eqType d)
 117  :=
 118   λd:finType.λe:d.λl:list (list d). map ? ? (λl. e :: l) l.
 119
 120 definition multss :
 121   ∀d:finType.∀e:list_eqType d.list_eqType (list_eqType d) -> list_eqType (list_eqType d)
 122 :=
 123   λd:finType.λe:list d.λl:list (list d).
 124     foldr ? ? (λx,acc. (multes ? x l) @ acc) [] e.
 125
 126 (*
 127 Eval compute in multss (Seq x1 x2) (Seq (Seq x3 x4) (Seq x5 x6)).
 128 -> Seq (Seq x1 x3 x4) (Seq x1 x5 x6) (Seq x2 x3 x4) (Seq x2 x5 x6)
 129 *)
 130
 131 definition iter :=
 132   λB:eqType.λn:nat.λf:nat→B→B.λacc:B.foldr ? B f acc (iota O n).
 133
 134 (* the sequence of all the strings of length m on the d alphabet *)
 135 definition mkpermr :=
 136   λd:finType.λm:nat. iter ? m (λx,acc.multss d (enum d) acc) [[]].
 137
 138 lemma mem_multes :
 139   ∀d:finType.∀e:d.∀l:list_eqType (list_eqType d).∀s:list_eqType d.
 140   mem ? s (multes ? e l) =
 141   match s in list with [ nil ⇒ false | (cons e1 tl) ⇒ andb (cmp ? e e1) (mem ? tl l)].
 142 intros (d e l s); elim l (hd tl IH); [cases s;simplify;[2: rewrite > andbC] reflexivity]
 143 simplify; rewrite > IH; cases s; simplify; [reflexivity]
 144 unfold list_eqType; simplify;
 145 apply (cmpP ? e s1); cases (lcmp d l1 hd); intros (E);
 146 [1,2: rewrite > E; simplify; rewrite > cmp_refl; reflexivity
 147 |3,4: rewrite > cmpC; rewrite > E; simplify; reflexivity;]
 148 qed.
 149
 150 lemma mem_concat:
 151   ∀d:eqType. ∀x.∀l1,l2:list d.
 152     mem d x (l1 @ l2) = orb (mem d x l1) (mem d x l2).
 153 intros; elim l1; [reflexivity] simplify; cases (cmp d x a); simplify; [reflexivity|assumption]
 154 qed.
 155
 156 lemma orb_refl : ∀x.orb x x = x. intros (x); cases x; reflexivity; qed.
 157
 158 lemma mem_multss :
 159   ∀d:finType.∀s:list_eqType d.∀l:list_eqType (list_eqType d).∀x:list_eqType d.
 160   mem ? x (multss ? s l) =
 161   match x in list with [ nil ⇒ false | (cons he tl) ⇒ andb (mem ? he s) (mem ? tl l)].
 162 intros (d s l x); elim s; [cases x] simplify; try reflexivity; rewrite > mem_concat;
 163 rewrite > H; clear H; rewrite > mem_multes; cases x; simplify; [reflexivity]
 164 unfold list_eqType; simplify; apply (cmpP ? a s1); intros (E);
 165 cases (mem d s1 l1);
 166 [1,2: rewrite > E; rewrite > cmp_refl; simplify;
 167       [rewrite > orb_refl | rewrite > orbC ] reflexivity
 168 |3,4: simplify; rewrite > orbC; simplify; [reflexivity] symmetry;
 169       apply (p2bF ? ? (andbP ? ?)); unfold Not; intros (H); decompose;
 170       rewrite > cmpC in H1; rewrite > E in H1; destruct H1;]
 171 qed.
 172
 173 lemma mem_mkpermr_size :
 174   ∀d:finType.∀m,x. mem (list_eqType d) x (mkpermr d m) = (eqb (length ? x) m).
 175 intros 2 (d m); elim m 0; simplify; [intros (x); cases x; reflexivity]
 176 intros (n IH x); elim x; rewrite > mem_multss; simplify; [reflexivity]
 177 rewrite > mem_finType; simplify; rewrite > IH; reflexivity;
 178 qed.
 179 (*
 180 axiom uniq_concat : ∀d:eqType.∀l1,l2. uniq d (l1@l1) = (andb (uniq ? l1) (andb (uniq ? l2) ())).
 181
 182 lemma uniq_mkpermr : ∀d:finType.∀m. uniq ? (mkpermr d m) = true.
 183 intros; elim m; [reflexivity] simplify; fold simplify (mkpermr d n);
 184 generalize in match (enum_uniq d); elim (enum d); [reflexivity];
 185 simplify; rewrite
 186
 187 unfold multss;
 188 lapply (b2pT ? ? (uniqP (list_eqType d) (mkpermr d n)) H) as H1; clear H;
 189
 190 Proof.
 191 elim=> //= i IHi; elim: enum (uniq_enum d) => //= x e IHe.
 192 move/andP=> [Hx He]; rewrite uniq_cat {}IHe {He}// andbT.
 193 rewrite {1}/multes uniq_maps ?{}IHi; last move=> _ _ [] //.
 194 apply/hasP; case=> s Hs.
 195 by move/mapsP => [s' _ Ds]; rewrite mem_multss -Ds (negbET Hx) in Hs.
 196 Qed.
 197
 198
 199 definition finfgraph_enum :=
 200   λd1,d2:finType.infgraphseq (mkpermr d2 (count ? (setA d1) (enum d1))).
 201
 202 Lemma maps_tval_fintuple_enum:
 203   maps (@fval d1 d2) finfgraph_enum = mkpermr d2 (card (setA d1)).
 204 Proof.
 205 rewrite /finfgraph_enum.
 206 have: all (fun s => size s == (card (setA d1))) (mkpermr d2 (card (setA d1))).
 207   by apply/allP => s; rewrite mem_mkpermr_size.
 208 elim: (mkpermr d2 (card (setA d1))) => //= s s2 IHs; move/andP => [Hs Hs2].
 209 by case: infgraphP => [_ _ /= ->|]; [rewrite (IHs Hs2)|rewrite Hs].
 210 Qed.
 211
 212   (* good enumeration *)
 213 Lemma finfgraph_enumP : forall u, count (set1 u) finfgraph_enum = 1.
 214 Proof.
 215 move => [s ps].
 216 rewrite /finfgraph_enum count_set1_uniq; last exact (uniq_infgraphseq (uniq_mkpermr d2 (card (setA d1)))).
 217 by rewrite mem_infgraphseq /= mem_mkpermr_size ps set11.
 218 Qed.
 219
 220 Canonical Structure fgraph_finType := FinType finfgraph_enumP.
 221
 222 End FinGraph.
 223
 224 Definition fgraph_of_fun :=
 225   locked (fun (d1 :finType) (d2 :eqType) (f : d1 -> d2) => Fgraph (size_maps f _)).
 226
 227 Definition fun_of_fgraph :=
 228   locked
 229    (fun d1 (d2:eqType) g x =>
 230       sub (@fgraph_default d1 d2 x g) (fval g) (index x (enum d1))).
 231
 232 Coercion fun_of_fgraph : fgraphType >-> Funclass.
 233 Lemma fgraphP : forall (d1 : finType) (d2 :eqType) (f g : fgraphType d1 d2), f =1 g <-> f = g.
 234 Proof.
 235 move=> d1 d2 f g; split; last by move=>->.
 236 move=> Efg; rewrite -(can_fun_of_fgraph f) -(can_fun_of_fgraph g).
 237 by apply: fval_inj; unlock fgraph_of_fun => /=; apply: eq_maps.
 238 Qed.
 239
 240 CoInductive setType : Type := Sett : fgraphType G bool_finType -> setType.
 241
 242 Definition sval (s : setType) := match s with Sett g => g end.
 243
 244 Lemma can_sval : cancel sval Sett.
 245 Proof. by rewrite /cancel; case => /=. Qed.
 246
 247 Lemma sval_inj : injective sval.
 248 Proof. exact: can_inj can_sval. Qed.
 249
 250 Canonical Structure set_eqType := EqType (can_eq can_sval).
 251
 252 Canonical Structure set_finType := FinType (can_uniq can_sval).
 253
 254 Definition iset_of_fun (f : G -> bool_finType) : setType :=
 255   locked Sett (fgraph_of_fun f).
 256
 257 *)