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