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