src/General.v

   1 (*********************************************************************************************************************************)
   2 (* General: general data structures                                                                                              *)
   3 (*********************************************************************************************************************************)
   4
   5 Require Import Coq.Unicode.Utf8.
   6 Require Import Coq.Classes.RelationClasses.
   7 Require Import Coq.Classes.Morphisms.
   8 Require Import Coq.Setoids.Setoid.
   9 Require Import Coq.Strings.String.
  10 Require Setoid.
  11 Require Import Coq.Lists.List.
  12 Require Import Preamble.
  13 Generalizable All Variables.
  14 Require Import Omega.
  15
  16 Definition EqDecider T := forall (n1 n2:T),  sumbool (n1=n2) (not (n1=n2)).
  17 Class EqDecidable (T:Type) :=
  18 { eqd_type           := T
  19 ; eqd_dec            :  forall v1 v2:T, sumbool (v1=v2) (not (v1=v2))
  20 }.
  21 Coercion eqd_type : EqDecidable >-> Sortclass.
  22
  23
  24 Class ToString (T:Type) := { toString : T -> string }.
  25 Instance StringToString : ToString string := { toString := fun x => x }.
  26 Notation "a +++ b" := (append (toString a) (toString b)) (at level 100).
  27
  28 (*******************************************************************************)
  29 (* Trees                                                                       *)
  30
  31 Inductive Tree (a:Type) : Type :=
  32   | T_Leaf   : a -> Tree a
  33   | T_Branch : Tree a -> Tree a -> Tree a.
  34 Implicit Arguments T_Leaf   [ a ].
  35 Implicit Arguments T_Branch [ a ].
  36
  37 Notation "a ,, b"   := (@T_Branch _ a b)                        : tree_scope.
  38
  39 (* tree-of-option-of-X comes up a lot, so we give it special notations *)
  40 Notation "[ q ]"    := (@T_Leaf (option _) (Some q))            : tree_scope.
  41 Notation "[ ]"      := (@T_Leaf (option _) None)                : tree_scope.
  42 Notation "[]"       := (@T_Leaf (option _) None)                : tree_scope.
  43
  44 Open Scope tree_scope.
  45
  46 Fixpoint mapTree {a b:Type}(f:a->b)(t:@Tree a) : @Tree b :=
  47   match t with
  48     | T_Leaf x     => T_Leaf (f x)
  49     | T_Branch l r => T_Branch (mapTree f l) (mapTree f r)
  50   end.
  51 Fixpoint mapOptionTree {a b:Type}(f:a->b)(t:@Tree ??a) : @Tree ??b :=
  52   match t with
  53     | T_Leaf None     => T_Leaf None
  54     | T_Leaf (Some x) => T_Leaf (Some (f x))
  55     | T_Branch l r    => T_Branch (mapOptionTree f l) (mapOptionTree f r)
  56   end.
  57 Fixpoint mapTreeAndFlatten {a b:Type}(f:a->@Tree b)(t:@Tree a) : @Tree b :=
  58   match t with
  59     | T_Leaf x        => f x
  60     | T_Branch l r    => T_Branch (mapTreeAndFlatten f l) (mapTreeAndFlatten f r)
  61   end.
  62 Fixpoint mapOptionTreeAndFlatten {a b:Type}(f:a->@Tree ??b)(t:@Tree ??a) : @Tree ??b :=
  63   match t with
  64     | T_Leaf None     => []
  65     | T_Leaf (Some x) => f x
  66     | T_Branch l r    => T_Branch (mapOptionTreeAndFlatten f l) (mapOptionTreeAndFlatten f r)
  67   end.
  68 Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tree T) :=
  69   match t with
  70   | T_Leaf x => mapLeaf x
  71   | T_Branch y z => mergeBranches (treeReduce mapLeaf mergeBranches y) (treeReduce mapLeaf mergeBranches z)
  72   end.
  73 Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
  74   forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.
  75
  76 Lemma tree_dec_eq :
  77    forall {Q}(t1 t2:Tree ??Q),
  78      (forall q1 q2:Q, sumbool (q1=q2) (not (q1=q2))) ->
  79      sumbool (t1=t2) (not (t1=t2)).
  80   intro Q.
  81   intro t1.
  82   induction t1; intros.
  83
  84   destruct a; destruct t2.
  85   destruct o.
  86   set (X q q0) as X'.
  87   inversion X'; subst.
  88   left; auto.
  89   right; unfold not; intro; apply H. inversion H0; subst. auto.
  90   right. unfold not; intro; inversion H.
  91   right. unfold not; intro; inversion H.
  92   destruct o.
  93   right. unfold not; intro; inversion H.
  94   left; auto.
  95   right. unfold not; intro; inversion H.
  96
  97   destruct t2.
  98   right. unfold not; intro; inversion H.
  99   set (IHt1_1 t2_1 X) as X1.
 100   set (IHt1_2 t2_2 X) as X2.
 101   destruct X1; destruct X2; subst.
 102   left; auto.
 103
 104   right.
 105   unfold not; intro H.
 106   apply n.
 107   inversion H; auto.
 108
 109   right.
 110   unfold not; intro H.
 111   apply n.
 112   inversion H; auto.
 113
 114   right.
 115   unfold not; intro H.
 116   apply n.
 117   inversion H; auto.
 118   Defined.
 119
 120 Lemma mapOptionTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree ??A),
 121   (mapOptionTree (g ○ f) l) = (mapOptionTree g (mapOptionTree f l)).
 122   induction l.
 123     destruct a.
 124     reflexivity.
 125     reflexivity.
 126     simpl.
 127     rewrite IHl1.
 128     rewrite IHl2.
 129     reflexivity.
 130     Qed.
 131
 132 Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (forall t, mapOptionTree f t = mapOptionTree g t).
 133   intros.
 134   induction t.
 135   destruct a; auto.
 136   simpl; rewrite H; auto.
 137   simpl; rewrite IHt1; rewrite IHt2; auto.
 138   Qed.
 139
 140 Open Scope string_scope.
 141 Fixpoint treeToString {T}{TT:ToString T}(t:Tree ??T) : string :=
 142 match t with
 143   | T_Leaf None => "[]"
 144   | T_Leaf (Some s) => "["+++s+++"]"
 145   | T_Branch b1 b2 => treeToString b1 +++ ",," +++ treeToString b2
 146 end.
 147 Instance TreeToString {T}{TT:ToString T} : ToString (Tree ??T) := { toString := treeToString }.
 148
 149 (*******************************************************************************)
 150 (* Lists                                                                       *)
 151
 152 Notation "a :: b"         := (cons a b)                               : list_scope.
 153 Open Scope list_scope.
 154 Fixpoint leaves {a:Type}(t:Tree (option a)) : list a :=
 155   match t with
 156     | (T_Leaf l)     => match l with
 157                           | None   => nil
 158                           | Some x => x::nil
 159                         end
 160     | (T_Branch l r) => app (leaves l) (leaves r)
 161   end.
 162 (* weak inverse of "leaves" *)
 163 Fixpoint unleaves {A:Type}(l:list A) : Tree (option A) :=
 164   match l with
 165     | nil    => []
 166     | (a::b) => [a],,(unleaves b)
 167   end.
 168
 169 (* a map over a list and the conjunction of the results *)
 170 Fixpoint mapProp {A:Type} (f:A->Prop) (l:list A) : Prop :=
 171   match l with
 172     | nil => True
 173     | (a::al) => f a /\ mapProp f al
 174   end.
 175
 176 Lemma map_id : forall A (l:list A), (map (fun x:A => x) l) = l.
 177   induction l.
 178   auto.
 179   simpl.
 180   rewrite IHl.
 181   auto.
 182   Defined.
 183 Lemma map_app : forall `(f:A->B) l l', map f (app l l') = app (map f l) (map f l').
 184   intros.
 185   induction l; auto.
 186   simpl.
 187   rewrite IHl.
 188   auto.
 189   Defined.
 190 Lemma map_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
 191   (map (g ○ f) l) = (map g (map f l)).
 192   intros.
 193   induction l.
 194   simpl; auto.
 195   simpl.
 196   rewrite IHl.
 197   auto.
 198   Defined.
 199 Lemma list_cannot_be_longer_than_itself : forall `(a:A)(b:list A), b = (a::b) -> False.
 200   intros.
 201   induction b.
 202   inversion H.
 203   inversion H. apply IHb in H2.
 204   auto.
 205   Defined.
 206 Lemma list_cannot_be_longer_than_itself' : forall A (b:list A) (a c:A), b = (a::c::b) -> False.
 207   induction b.
 208   intros; inversion H.
 209   intros.
 210   inversion H.
 211   apply IHb in H2.
 212   auto.
 213   Defined.
 214
 215 Lemma mapOptionTree_on_nil : forall `(f:A->B) h, [] = mapOptionTree f h -> h=[].
 216   intros.
 217   destruct h.
 218   destruct o. inversion H.
 219   auto.
 220   inversion H.
 221   Defined.
 222
 223 Lemma mapOptionTree_comp a b c (f:a->b) (g:b->c) q : (mapOptionTree g (mapOptionTree f q)) = mapOptionTree (g ○ f) q.
 224   induction q.
 225     destruct a0; simpl.
 226     reflexivity.
 227     reflexivity.
 228     simpl.
 229     rewrite IHq1.
 230     rewrite IHq2.
 231     reflexivity.
 232   Qed.
 233
 234 Lemma leaves_unleaves {T}(t:list T) : leaves (unleaves t) = t.
 235   induction t; auto.
 236   simpl.
 237   rewrite IHt; auto.
 238   Qed.
 239
 240 Lemma mapleaves' {T:Type}(t:list T){Q}{f:T->Q} : unleaves (map f t) = mapOptionTree f (unleaves t).
 241   induction t; simpl in *; auto.
 242   rewrite IHt; auto.
 243   Qed.
 244
 245 (* handy facts: map preserves the length of a list *)
 246 Lemma map_on_nil : forall A B (s1:list A) (f:A->B), nil = map f s1 -> s1=nil.
 247   intros.
 248   induction s1.
 249   auto.
 250   assert False.
 251   simpl in H.
 252   inversion H.
 253   inversion H0.
 254   Defined.
 255 Lemma map_on_singleton : forall A B (f:A->B) x (s1:list A), (cons x nil) = map f s1 -> { y : A & s1=(cons y nil) & (f y)=x }.
 256   induction s1.
 257   intros.
 258   simpl in H; assert False. inversion H. inversion H0.
 259   clear IHs1.
 260   intros.
 261   exists a.
 262   simpl in H.
 263   assert (s1=nil).
 264     inversion H. apply map_on_nil in H2. auto.
 265   subst.
 266   auto.
 267   assert (s1=nil).
 268     inversion H. apply map_on_nil in H2. auto.
 269   subst.
 270   simpl in H.
 271   inversion H. auto.
 272   Defined.
 273
 274 Lemma map_on_doubleton : forall A B (f:A->B) x y (s1:list A), ((x::y::nil) = map f s1) ->
 275   { z : A*A & s1=((fst z)::(snd z)::nil) & (f (fst z))=x /\ (f (snd z))=y }.
 276   intros.
 277   destruct s1.
 278   inversion H.
 279   destruct s1.
 280   inversion H.
 281   destruct s1.
 282   inversion H.
 283   exists (a,a0); auto.
 284   simpl in H.
 285   inversion H.
 286   Defined.
 287
 288
 289 Lemma mapTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree A),
 290   (mapTree (g ○ f) l) = (mapTree g (mapTree f l)).
 291   induction l.
 292     reflexivity.
 293     simpl.
 294     rewrite IHl1.
 295     rewrite IHl2.
 296     reflexivity.
 297     Defined.
 298
 299 Lemma lmap_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
 300   (map (g ○ f) l) = (map g (map f l)).
 301   intros.
 302   induction l.
 303   simpl; auto.
 304   simpl.
 305   rewrite IHl.
 306   auto.
 307   Defined.
 308
 309 (* sends a::b::c::nil to [[[[],,c],,b],,a] *)
 310 Fixpoint unleaves' {A:Type}(l:list A) : Tree (option A) :=
 311   match l with
 312     | nil    => []
 313     | (a::b) => (unleaves' b),,[a]
 314   end.
 315
 316 (* sends a::b::c::nil to [[[[],,c],,b],,a] *)
 317 Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A :=
 318   match l with
 319     | nil    => []
 320     | (a::b) => (unleaves'' b),,(T_Leaf a)
 321   end.
 322
 323 Lemma mapleaves {T:Type}(t:Tree ??T){Q}{f:T->Q} : leaves (mapOptionTree f t) = map f (leaves t).
 324   induction t.
 325   destruct a; auto.
 326   simpl.
 327   rewrite IHt1.
 328   rewrite IHt2.
 329   rewrite map_app.
 330   auto.
 331   Qed.
 332
 333 Fixpoint filter {T:Type}(l:list ??T) : list T :=
 334   match l with
 335     | nil => nil
 336     | (None::b) => filter b
 337     | ((Some x)::b) => x::(filter b)
 338   end.
 339
 340 Inductive distinct {T:Type} : list T -> Prop :=
 341 | distinct_nil  : distinct nil
 342 | distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax).
 343
 344 Lemma in_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (v:VV)(lv:list VV), sumbool (In v lv) (not (In v lv)).
 345   intros.
 346   induction lv.
 347   right.
 348   unfold not.
 349   intros.
 350   inversion H.
 351   destruct IHlv.
 352   left.
 353   simpl.
 354   auto.
 355   set (eqd_dec v a) as dec.
 356   destruct dec.
 357   subst.
 358   left; simpl; auto.
 359   right.
 360   unfold not; intros.
 361   destruct H.
 362   subst.
 363   apply n0; auto.
 364   apply n.
 365   apply H.
 366   Defined.
 367
 368 Lemma distinct_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (lv:list VV), sumbool (distinct lv) (not (distinct lv)).
 369   intros.
 370   induction lv.
 371   left; apply distinct_nil.
 372   destruct IHlv.
 373   set (in_decidable a lv) as dec.
 374   destruct dec.
 375   right; unfold not; intros.
 376   inversion H.
 377   subst.
 378   apply H2; auto.
 379   left.
 380   apply distinct_cons; auto.
 381   right.
 382   unfold not; intros.
 383   inversion H.
 384   subst.
 385   apply n; auto.
 386   Defined.
 387
 388 Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
 389   induction l; auto.
 390   simpl.
 391   omega.
 392   Qed.
 393
 394 (* decidable quality on a list of elements which have decidable equality *)
 395 Definition list_eq_dec : forall {T:Type}(l1 l2:list T)(dec:forall t1 t2:T, sumbool (eq t1 t2) (not (eq t1 t2))),
 396   sumbool (eq l1 l2) (not (eq l1 l2)).
 397   intro T.
 398   intro l1.
 399   induction l1; intros.
 400     destruct l2.
 401     left; reflexivity.
 402     right; intro H; inversion H.
 403   destruct l2 as [| b l2].
 404     right; intro H; inversion H.
 405   set (IHl1 l2 dec) as eqx.
 406     destruct eqx.
 407     subst.
 408     set (dec a b) as eqy.
 409     destruct eqy.
 410       subst.
 411       left; reflexivity.
 412       right. intro. inversion H. subst. apply n. auto.
 413     right.
 414       intro.
 415       inversion H.
 416       apply n.
 417       auto.
 418       Defined.
 419
 420 Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
 421   apply Build_EqDecidable.
 422   intros.
 423   apply list_eq_dec.
 424   apply eqd_dec.
 425   Defined.
 426
 427 (*******************************************************************************)
 428 (* Length-Indexed Lists                                                        *)
 429
 430 Inductive vec (A:Type) : nat -> Type :=
 431 | vec_nil  : vec A 0
 432 | vec_cons : forall n, A -> vec A n -> vec A (S n).
 433
 434 Fixpoint vec2list {n:nat}{t:Type}(v:vec t n) : list t :=
 435   match v with
 436     | vec_nil => nil
 437     | vec_cons n a va => a::(vec2list va)
 438   end.
 439
 440 Require Import Omega.
 441 Definition vec_get : forall {T:Type}{l:nat}(v:vec T l)(n:nat)(pf:lt n l), T.
 442   intro T.
 443   intro len.
 444   intro v.
 445   induction v; intros.
 446     assert False.
 447     inversion pf.
 448     inversion H.
 449   rename n into len.
 450     destruct n0 as [|n].
 451     exact a.
 452     apply (IHv n).
 453     omega.
 454     Defined.
 455
 456 Definition vec_zip {n:nat}{A B:Type}(va:vec A n)(vb:vec B n) : vec (A*B) n.
 457   induction n.
 458   apply vec_nil.
 459   inversion va; subst.
 460   inversion vb; subst.
 461   apply vec_cons; auto.
 462   Defined.
 463
 464 Definition vec_map {n:nat}{A B:Type}(f:A->B)(v:vec A n) : vec B n.
 465   induction n.
 466   apply vec_nil.
 467   inversion v; subst.
 468   apply vec_cons; auto.
 469   Defined.
 470
 471 Fixpoint vec_In {A:Type} {n:nat} (a:A) (l:vec A n) : Prop :=
 472   match l with
 473     | vec_nil         => False
 474     | vec_cons _ n m  => (n = a) \/ vec_In a m
 475   end.
 476 Implicit Arguments vec_nil  [ A   ].
 477 Implicit Arguments vec_cons [ A n ].
 478
 479 Definition append_vec {n:nat}{T:Type}(v:vec T n)(t:T) : vec T (S n).
 480   induction n.
 481   apply (vec_cons t vec_nil).
 482   apply vec_cons; auto.
 483   Defined.
 484
 485 Definition list2vec {T:Type}(l:list T) : vec T (length l).
 486   induction l.
 487   apply vec_nil.
 488   apply vec_cons; auto.
 489   Defined.
 490
 491 Definition vec_head {n:nat}{T}(v:vec T (S n)) : T.
 492   inversion v;  auto.
 493   Defined.
 494 Definition vec_tail {n:nat}{T}(v:vec T (S n)) : vec T n.
 495   inversion v;  auto.
 496   Defined.
 497
 498 Lemma vec_chop {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l1).
 499   induction l1.
 500   apply vec_nil.
 501   apply vec_cons.
 502   simpl in *.
 503   inversion v; subst; auto.
 504   apply IHl1.
 505   inversion v; subst; auto.
 506   Defined.
 507
 508 Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l2).
 509   induction l1.
 510   apply v.
 511   simpl in *.
 512   apply IHl1; clear IHl1.
 513   inversion v; subst; auto.
 514   Defined.
 515
 516 Lemma vec2list_len {T}{n}(v:vec T n) : length (vec2list v) = n.
 517   induction v; auto.
 518   simpl.
 519   omega.
 520   Qed.
 521
 522 Lemma vec2list_map_list2vec {A B}{n}(f:A->B)(v:vec A n) : map f (vec2list v) = vec2list (vec_map f v).
 523   induction v; auto.
 524   simpl. rewrite IHv.
 525   reflexivity.
 526   Qed.
 527
 528 Lemma vec2list_list2vec {A}(v:list A) : vec2list (list2vec v) = v.
 529   induction v; auto.
 530   set (vec2list (list2vec (a :: v))) as q.
 531   rewrite <- IHv.
 532   unfold q.
 533   clear q.
 534   simpl.
 535   reflexivity.
 536   Qed.
 537
 538 Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20).
 539
 540
 541
 542 (*******************************************************************************)
 543 (* Shaped Trees                                                                *)
 544
 545 (* a ShapedTree is a tree indexed by the shape (but not the leaf values) of another tree; isomorphic to (ITree (fun _ => Q)) *)
 546 Inductive ShapedTree {T:Type}(Q:Type) : Tree ??T -> Type :=
 547 | st_nil    : @ShapedTree T Q []
 548 | st_leaf   : forall {t}, Q -> @ShapedTree T Q [t]
 549 | st_branch : forall {t1}{t2}, @ShapedTree T Q t1 -> @ShapedTree T Q t2 -> @ShapedTree T Q (t1,,t2).
 550
 551 Fixpoint unshape {T:Type}{Q:Type}{idx:Tree ??T}(st:@ShapedTree T Q idx) : Tree ??Q :=
 552 match st with
 553 | st_nil => []
 554 | st_leaf _ q => [q]
 555 | st_branch _ _ b1 b2 => (unshape b1),,(unshape b2)
 556 end.
 557
 558 Definition mapShapedTree {T}{idx:Tree ??T}{V}{Q}(f:V->Q)(st:ShapedTree V idx) : ShapedTree Q idx.
 559   induction st.
 560   apply st_nil.
 561   apply st_leaf. apply f. apply q.
 562   apply st_branch; auto.
 563   Defined.
 564
 565 Definition zip_shapedTrees {T:Type}{Q1 Q2:Type}{idx:Tree ??T}
 566    (st1:ShapedTree Q1 idx)(st2:ShapedTree Q2 idx) : ShapedTree (Q1*Q2) idx.
 567   induction idx.
 568     destruct a.
 569     apply st_leaf; auto.
 570     inversion st1.
 571     inversion st2.
 572     auto.
 573     apply st_nil.
 574     apply st_branch; auto.
 575     inversion st1; subst; apply IHidx1; auto.
 576     inversion st2; subst; auto.
 577     inversion st2; subst; apply IHidx2; auto.
 578     inversion st1; subst; auto.
 579   Defined.
 580
 581 Definition build_shapedTree {T:Type}(idx:Tree ??T){Q:Type}(f:T->Q) : ShapedTree Q idx.
 582   induction idx.
 583   destruct a.
 584   apply st_leaf; auto.
 585   apply st_nil.
 586   apply st_branch; auto.
 587   Defined.
 588
 589 Lemma unshape_map : forall {Q}{b}(f:Q->b){T}{idx:Tree ??T}(t:ShapedTree Q idx),
 590    mapOptionTree f (unshape t) = unshape (mapShapedTree f t).
 591   intros.
 592   induction t; auto.
 593   simpl.
 594   rewrite IHt1.
 595   rewrite IHt2.
 596   reflexivity.
 597   Qed.
 598
 599
 600
 601
 602 (*******************************************************************************)
 603 (* Type-Indexed Lists                                                          *)
 604
 605 (* an indexed list *)
 606 Inductive IList (I:Type)(F:I->Type) : list I -> Type :=
 607 | INil      :                                       IList I F nil
 608 | ICons     :   forall i is, F i -> IList I F is -> IList I F (i::is).
 609 Implicit Arguments INil [ I F ].
 610 Implicit Arguments ICons [ I F ].
 611
 612 Notation "a :::: b" := (@ICons _ _ _ _ a b) (at level 20).
 613
 614 Definition ilist_head {T}{F}{x}{y} : IList T F (x::y) -> F x.
 615   intro il.
 616   inversion il.
 617   subst.
 618   apply X.
 619   Defined.
 620
 621 Definition ilist_tail {T}{F}{x}{y} : IList T F (x::y) -> IList T F y.
 622   intro il.
 623   inversion il.
 624   subst.
 625   apply X0.
 626   Defined.
 627
 628 Definition ilmap {I}{F}{G}{il:list I}(f:forall i:I, F i -> G i) : IList I F il -> IList I G il.
 629   induction il; intros; auto.
 630   apply INil.
 631   inversion X; subst.
 632   apply ICons; auto.
 633   Defined.
 634
 635 Lemma ilist_chop {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l1.
 636   induction l1; auto.
 637   apply INil.
 638   apply ICons.
 639   inversion v; auto.
 640   apply IHl1.
 641   inversion v; auto.
 642   Defined.
 643
 644 Lemma ilist_chop' {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l2.
 645   induction l1; auto.
 646   apply IHl1.
 647   inversion v; subst; auto.
 648   Defined.
 649
 650 Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
 651   match il with
 652   | INil   => nil
 653   | a::::b => a::(ilist_to_list b)
 654   end.
 655
 656 (* a tree indexed by a (Tree (option X)) *)
 657 Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type :=
 658 | INone      :                                ITree I F []
 659 | ILeaf      :  forall       i:     I, F i -> ITree I F [i]
 660 | IBranch    :  forall it1 it2:Tree ??I, ITree I F it1 -> ITree I F it2 -> ITree I F (it1,,it2).
 661 Implicit Arguments INil    [ I F ].
 662 Implicit Arguments ILeaf   [ I F ].
 663 Implicit Arguments IBranch [ I F ].
 664
 665 Definition itmap {I}{F}{G}{il:Tree ??I}(f:forall i:I, F i -> G i) : ITree I F il -> ITree I G il.
 666   induction il; intros; auto.
 667   destruct a.
 668   apply ILeaf.
 669   apply f.
 670   inversion X; auto.
 671   apply INone.
 672   apply IBranch; inversion X; auto.
 673   Defined.
 674
 675 Fixpoint itree_to_tree {T}{Z}{l:Tree ??T}(il:ITree T (fun _ => Z) l) : Tree ??Z :=
 676   match il with
 677   | INone     => []
 678   | ILeaf _ a => [a]
 679   | IBranch _ _ b1 b2 => (itree_to_tree b1),,(itree_to_tree b2)
 680   end.
 681
 682
 683 (*******************************************************************************)
 684 (* Extensional equality on functions                                           *)
 685
 686 Definition extensionality := fun (t1 t2:Type) => (fun (f:t1->t2) g => forall x:t1, (f x)=(g x)).
 687 Hint Transparent extensionality.
 688 Instance extensionality_Equivalence : forall t1 t2, Equivalence (extensionality t1 t2).
 689   intros; apply Build_Equivalence;
 690     intros; compute; intros; auto.
 691     rewrite H; rewrite H0; auto.
 692   Defined.
 693   Add Parametric Morphism (A B C:Type) : (fun f g => g ○ f)
 694   with signature (extensionality A B ==> extensionality B C ==> extensionality A C) as parametric_morphism_extensionality.
 695   unfold extensionality; intros; rewrite (H x1); rewrite (H0 (y x1)); auto.
 696   Defined.
 697 Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
 698   (extensionality _ _ f f') ->
 699   (extensionality _ _ g g') ->
 700   (extensionality _ _ (g ○ f) (g' ○ f')).
 701   intros.
 702   unfold extensionality.
 703   unfold extensionality in H.
 704   unfold extensionality in H0.
 705   intros.
 706   rewrite H.
 707   rewrite H0.
 708   auto.
 709   Qed.
 710
 711
 712
 713
 714
 715 CoInductive Fresh A T :=
 716 { next  : forall a:A, (T a * Fresh A T)
 717 ; split : Fresh A T * Fresh A T
 718 }.
 719
 720
 721
 722
 723
 724 Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
 725
 726
 727 (* string stuff *)
 728 Variable eol : string.
 729 Extract Constant eol  => "'\n':[]".
 730
 731 Class Monad {T:Type->Type} :=
 732 { returnM : forall {a},     a -> T a
 733 ; bindM   : forall {a}{b},  T a -> (a -> T b) -> T b
 734 }.
 735 Implicit Arguments Monad [ ].
 736 Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).
 737
 738 (* the Error monad *)
 739 Inductive OrError (T:Type) :=
 740 | Error : forall error_message:string, OrError T
 741 | OK    : T      -> OrError T.
 742 Notation "??? T" := (OrError T) (at level 10).
 743 Implicit Arguments Error [T].
 744 Implicit Arguments OK [T].
 745
 746 Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
 747   match oe with
 748     | Error s => Error s
 749     | OK    t => f t
 750   end.
 751 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
 752
 753 Open Scope string_scope.
 754 Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg :=
 755   match oe with
 756     | Error s => Error (err_msg +++ eol +++ "  " +++ s)
 757     | OK    t => f t
 758   end.
 759
 760 Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
 761
 762 Definition addErrorMessage s {T} (x:OrError T) :=
 763   x >>=[ s ] (fun y => OK y).
 764
 765 Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
 766 | Indexed_Error : forall error_message:string, Indexed f (Error error_message)
 767 | Indexed_OK    : forall t, f t -> Indexed f (OK t)
 768 .
 769
 770
 771 Require Import Coq.Arith.EqNat.
 772 Instance EqDecidableNat : EqDecidable nat.
 773   apply Build_EqDecidable.
 774   intros.
 775   apply eq_nat_dec.
 776   Defined.
 777
 778 (* for a type with decidable equality, we can maintain lists of distinct elements *)
 779 Section DistinctList.
 780   Context `{V:EqDecidable}.
 781
 782   Fixpoint addToDistinctList (cv:V)(cvl:list V) :=
 783   match cvl with
 784   | nil       => cv::nil
 785   | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl')
 786   end.
 787
 788   Fixpoint removeFromDistinctList (cv:V)(cvl:list V) :=
 789   match cvl with
 790   | nil => nil
 791   | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl')
 792   end.
 793
 794   Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) :=
 795   match cvrem with
 796   | nil         => cvl
 797   | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl)
 798   end.
 799
 800   Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) :=
 801   match cvl1 with
 802   | nil       => cvl2
 803   | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
 804   end.
 805 End DistinctList.
 806
 807 Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(vec T n).
 808   set (list2vec l) as v.
 809   destruct (eqd_dec (length l) n).
 810     rewrite e in v; apply OK; apply v.
 811     apply (Error (error_message (length l) n)).
 812     Defined.
 813
 814 (* Uniques *)
 815 Variable UniqSupply      : Type.                   Extract Inlined Constant UniqSupply     => "UniqSupply.UniqSupply".
 816 Variable Unique          : Type.                   Extract Inlined Constant Unique         => "Unique.Unique".
 817 Variable uniqFromSupply  : UniqSupply -> Unique.   Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply".
 818 Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply.
 819     Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply".
 820 Variable unique_eq       : forall u1 u2:Unique, sumbool (u1=u2) (u1≠u2).
 821     Extract Inlined Constant unique_eq => "(==)".
 822 Variable unique_toString : Unique -> string.
 823     Extract Inlined Constant unique_toString => "show".
 824 Instance EqDecidableUnique : EqDecidable Unique :=
 825   { eqd_dec := unique_eq }.
 826 Instance EqDecidableToString : ToString Unique :=
 827   { toString := unique_toString }.
 828
 829 Inductive UniqM {T:Type} : Type :=
 830  | uniqM    : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
 831  Implicit Arguments UniqM [ ].
 832
 833 Instance UniqMonad : Monad UniqM :=
 834 { returnM := fun T (x:T) => uniqM (fun u => OK (u,x))
 835 ; bindM   := fun a b (x:UniqM a) (f:a->UniqM b) =>
 836   uniqM (fun u =>
 837     match x with
 838       | uniqM fa =>
 839         match fa u with
 840           | Error s   => Error s
 841           | OK (u',va) => match f va with
 842                            | uniqM fb => fb u'
 843                          end
 844         end
 845     end)
 846 }.
 847
 848 Definition getU : UniqM Unique :=
 849   uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
 850
 851 Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity).
 852 Notation "'return' x" := (returnM x) (at level 100).
 853 Notation "'failM'  x" := (uniqM (fun _ => Error x)) (at level 100).
 854
 855
 856
 857
 858
 859
 860 Record FreshMonad {T:Type} :=
 861 { FMT       :  Type -> Type
 862 ; FMT_Monad :> Monad FMT
 863 ; FMT_fresh :  forall tl:list T, FMT { t:T & @In _ t tl -> False }
 864 }.
 865 Implicit Arguments FreshMonad [ ].
 866 Coercion FMT       : FreshMonad >-> Funclass.
 867
 868
 869
 870 Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
 871
 872
 873
 874
 875 Ltac eqd_dec_refl X :=
 876   destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
 877     [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].
 878
 879 Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 -> t1 = t2.
 880   intros T.
 881   induction t1; intros.
 882   destruct t2.
 883   auto.
 884   inversion H.
 885   destruct t2.
 886   inversion H.
 887   simpl in H.
 888   inversion H.
 889   set (IHt1 _ H2) as q.
 890   rewrite q.
 891   reflexivity.
 892   Qed.
 893
 894 Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
 895   admit.
 896   Qed.
 897
 898 Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
 899   admit.
 900   Defined.