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