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 Fixpoint filter {T:Type}(l:list ??T) : list T :=
 305   match l with
 306     | nil => nil
 307     | (None::b) => filter b
 308     | ((Some x)::b) => x::(filter b)
 309   end.
 310
 311 Inductive distinct {T:Type} : list T -> Prop :=
 312 | distinct_nil  : distinct nil
 313 | distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax).
 314
 315 Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
 316   induction l; auto.
 317   simpl.
 318   omega.
 319   Qed.
 320
 321 (* decidable quality on a list of elements which have decidable equality *)
 322 Definition list_eq_dec : forall {T:Type}(l1 l2:list T)(dec:forall t1 t2:T, sumbool (eq t1 t2) (not (eq t1 t2))),
 323   sumbool (eq l1 l2) (not (eq l1 l2)).
 324   intro T.
 325   intro l1.
 326   induction l1; intros.
 327     destruct l2.
 328     left; reflexivity.
 329     right; intro H; inversion H.
 330   destruct l2 as [| b l2].
 331     right; intro H; inversion H.
 332   set (IHl1 l2 dec) as eqx.
 333     destruct eqx.
 334     subst.
 335     set (dec a b) as eqy.
 336     destruct eqy.
 337       subst.
 338       left; reflexivity.
 339       right. intro. inversion H. subst. apply n. auto.
 340     right.
 341       intro.
 342       inversion H.
 343       apply n.
 344       auto.
 345       Defined.
 346
 347 Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
 348   apply Build_EqDecidable.
 349   intros.
 350   apply list_eq_dec.
 351   apply eqd_dec.
 352   Defined.
 353
 354 (*******************************************************************************)
 355 (* Length-Indexed Lists                                                        *)
 356
 357 Inductive vec (A:Type) : nat -> Type :=
 358 | vec_nil  : vec A 0
 359 | vec_cons : forall n, A -> vec A n -> vec A (S n).
 360
 361 Fixpoint vec2list {n:nat}{t:Type}(v:vec t n) : list t :=
 362   match v with
 363     | vec_nil => nil
 364     | vec_cons n a va => a::(vec2list va)
 365   end.
 366
 367 Require Import Omega.
 368 Definition vec_get : forall {T:Type}{l:nat}(v:vec T l)(n:nat)(pf:lt n l), T.
 369   intro T.
 370   intro len.
 371   intro v.
 372   induction v; intros.
 373     assert False.
 374     inversion pf.
 375     inversion H.
 376   rename n into len.
 377     destruct n0 as [|n].
 378     exact a.
 379     apply (IHv n).
 380     omega.
 381     Defined.
 382
 383 Definition vec_zip {n:nat}{A B:Type}(va:vec A n)(vb:vec B n) : vec (A*B) n.
 384   induction n.
 385   apply vec_nil.
 386   inversion va; subst.
 387   inversion vb; subst.
 388   apply vec_cons; auto.
 389   Defined.
 390
 391 Definition vec_map {n:nat}{A B:Type}(f:A->B)(v:vec A n) : vec B n.
 392   induction n.
 393   apply vec_nil.
 394   inversion v; subst.
 395   apply vec_cons; auto.
 396   Defined.
 397
 398 Fixpoint vec_In {A:Type} {n:nat} (a:A) (l:vec A n) : Prop :=
 399   match l with
 400     | vec_nil         => False
 401     | vec_cons _ n m  => (n = a) \/ vec_In a m
 402   end.
 403 Implicit Arguments vec_nil  [ A   ].
 404 Implicit Arguments vec_cons [ A n ].
 405
 406 Definition append_vec {n:nat}{T:Type}(v:vec T n)(t:T) : vec T (S n).
 407   induction n.
 408   apply (vec_cons t vec_nil).
 409   apply vec_cons; auto.
 410   Defined.
 411
 412 Definition list2vec {T:Type}(l:list T) : vec T (length l).
 413   induction l.
 414   apply vec_nil.
 415   apply vec_cons; auto.
 416   Defined.
 417
 418 Definition vec_head {n:nat}{T}(v:vec T (S n)) : T.
 419   inversion v;  auto.
 420   Defined.
 421 Definition vec_tail {n:nat}{T}(v:vec T (S n)) : vec T n.
 422   inversion v;  auto.
 423   Defined.
 424
 425 Lemma vec_chop {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l1).
 426   induction l1.
 427   apply vec_nil.
 428   apply vec_cons.
 429   simpl in *.
 430   inversion v; subst; auto.
 431   apply IHl1.
 432   inversion v; subst; auto.
 433   Defined.
 434
 435 Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l2).
 436   induction l1.
 437   apply v.
 438   simpl in *.
 439   apply IHl1; clear IHl1.
 440   inversion v; subst; auto.
 441   Defined.
 442
 443 Lemma vec2list_len {T}{n}(v:vec T n) : length (vec2list v) = n.
 444   induction v; auto.
 445   simpl.
 446   omega.
 447   Qed.
 448
 449 Lemma vec2list_map_list2vec {A B}{n}(f:A->B)(v:vec A n) : map f (vec2list v) = vec2list (vec_map f v).
 450   induction v; auto.
 451   simpl. rewrite IHv.
 452   reflexivity.
 453   Qed.
 454
 455 Lemma vec2list_list2vec {A}(v:list A) : vec2list (list2vec v) = v.
 456   induction v; auto.
 457   set (vec2list (list2vec (a :: v))) as q.
 458   rewrite <- IHv.
 459   unfold q.
 460   clear q.
 461   simpl.
 462   reflexivity.
 463   Qed.
 464
 465 Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20).
 466
 467
 468
 469 (*******************************************************************************)
 470 (* Shaped Trees                                                                *)
 471
 472 (* a ShapedTree is a tree indexed by the shape (but not the leaf values) of another tree; isomorphic to (ITree (fun _ => Q)) *)
 473 Inductive ShapedTree {T:Type}(Q:Type) : Tree ??T -> Type :=
 474 | st_nil    : @ShapedTree T Q []
 475 | st_leaf   : forall {t}, Q -> @ShapedTree T Q [t]
 476 | st_branch : forall {t1}{t2}, @ShapedTree T Q t1 -> @ShapedTree T Q t2 -> @ShapedTree T Q (t1,,t2).
 477
 478 Fixpoint unshape {T:Type}{Q:Type}{idx:Tree ??T}(st:@ShapedTree T Q idx) : Tree ??Q :=
 479 match st with
 480 | st_nil => []
 481 | st_leaf _ q => [q]
 482 | st_branch _ _ b1 b2 => (unshape b1),,(unshape b2)
 483 end.
 484
 485 Definition mapShapedTree {T}{idx:Tree ??T}{V}{Q}(f:V->Q)(st:ShapedTree V idx) : ShapedTree Q idx.
 486   induction st.
 487   apply st_nil.
 488   apply st_leaf. apply f. apply q.
 489   apply st_branch; auto.
 490   Defined.
 491
 492 Definition zip_shapedTrees {T:Type}{Q1 Q2:Type}{idx:Tree ??T}
 493    (st1:ShapedTree Q1 idx)(st2:ShapedTree Q2 idx) : ShapedTree (Q1*Q2) idx.
 494   induction idx.
 495     destruct a.
 496     apply st_leaf; auto.
 497     inversion st1.
 498     inversion st2.
 499     auto.
 500     apply st_nil.
 501     apply st_branch; auto.
 502     inversion st1; subst; apply IHidx1; auto.
 503     inversion st2; subst; auto.
 504     inversion st2; subst; apply IHidx2; auto.
 505     inversion st1; subst; auto.
 506   Defined.
 507
 508 Definition build_shapedTree {T:Type}(idx:Tree ??T){Q:Type}(f:T->Q) : ShapedTree Q idx.
 509   induction idx.
 510   destruct a.
 511   apply st_leaf; auto.
 512   apply st_nil.
 513   apply st_branch; auto.
 514   Defined.
 515
 516 Lemma unshape_map : forall {Q}{b}(f:Q->b){T}{idx:Tree ??T}(t:ShapedTree Q idx),
 517    mapOptionTree f (unshape t) = unshape (mapShapedTree f t).
 518   intros.
 519   induction t; auto.
 520   simpl.
 521   rewrite IHt1.
 522   rewrite IHt2.
 523   reflexivity.
 524   Qed.
 525
 526
 527
 528
 529 (*******************************************************************************)
 530 (* Type-Indexed Lists                                                          *)
 531
 532 (* an indexed list *)
 533 Inductive IList (I:Type)(F:I->Type) : list I -> Type :=
 534 | INil      :                                       IList I F nil
 535 | ICons     :   forall i is, F i -> IList I F is -> IList I F (i::is).
 536 Implicit Arguments INil [ I F ].
 537 Implicit Arguments ICons [ I F ].
 538
 539 Notation "a :::: b" := (@ICons _ _ _ _ a b) (at level 20).
 540
 541 Definition ilist_head {T}{F}{x}{y} : IList T F (x::y) -> F x.
 542   intro il.
 543   inversion il.
 544   subst.
 545   apply X.
 546   Defined.
 547
 548 Definition ilist_tail {T}{F}{x}{y} : IList T F (x::y) -> IList T F y.
 549   intro il.
 550   inversion il.
 551   subst.
 552   apply X0.
 553   Defined.
 554
 555 Definition ilmap {I}{F}{G}{il:list I}(f:forall i:I, F i -> G i) : IList I F il -> IList I G il.
 556   induction il; intros; auto.
 557   apply INil.
 558   inversion X; subst.
 559   apply ICons; auto.
 560   Defined.
 561
 562 Lemma ilist_chop {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l1.
 563   induction l1; auto.
 564   apply INil.
 565   apply ICons.
 566   inversion v; auto.
 567   apply IHl1.
 568   inversion v; auto.
 569   Defined.
 570
 571 Lemma ilist_chop' {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l2.
 572   induction l1; auto.
 573   apply IHl1.
 574   inversion v; subst; auto.
 575   Defined.
 576
 577 Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
 578   match il with
 579   | INil   => nil
 580   | a::::b => a::(ilist_to_list b)
 581   end.
 582
 583 (* a tree indexed by a (Tree (option X)) *)
 584 Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type :=
 585 | INone      :                                ITree I F []
 586 | ILeaf      :  forall       i:     I, F i -> ITree I F [i]
 587 | IBranch    :  forall it1 it2:Tree ??I, ITree I F it1 -> ITree I F it2 -> ITree I F (it1,,it2).
 588 Implicit Arguments INil    [ I F ].
 589 Implicit Arguments ILeaf   [ I F ].
 590 Implicit Arguments IBranch [ I F ].
 591
 592 Definition itmap {I}{F}{G}{il:Tree ??I}(f:forall i:I, F i -> G i) : ITree I F il -> ITree I G il.
 593   induction il; intros; auto.
 594   destruct a.
 595   apply ILeaf.
 596   apply f.
 597   inversion X; auto.
 598   apply INone.
 599   apply IBranch; inversion X; auto.
 600   Defined.
 601
 602 Fixpoint itree_to_tree {T}{Z}{l:Tree ??T}(il:ITree T (fun _ => Z) l) : Tree ??Z :=
 603   match il with
 604   | INone     => []
 605   | ILeaf _ a => [a]
 606   | IBranch _ _ b1 b2 => (itree_to_tree b1),,(itree_to_tree b2)
 607   end.
 608
 609
 610 (*******************************************************************************)
 611 (* Extensional equality on functions                                           *)
 612
 613 Definition extensionality := fun (t1 t2:Type) => (fun (f:t1->t2) g => forall x:t1, (f x)=(g x)).
 614 Hint Transparent extensionality.
 615 Instance extensionality_Equivalence : forall t1 t2, Equivalence (extensionality t1 t2).
 616   intros; apply Build_Equivalence;
 617     intros; compute; intros; auto.
 618     rewrite H; rewrite H0; auto.
 619   Defined.
 620   Add Parametric Morphism (A B C:Type) : (fun f g => g ○ f)
 621   with signature (extensionality A B ==> extensionality B C ==> extensionality A C) as parametric_morphism_extensionality.
 622   unfold extensionality; intros; rewrite (H x1); rewrite (H0 (y x1)); auto.
 623   Defined.
 624 Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
 625   (extensionality _ _ f f') ->
 626   (extensionality _ _ g g') ->
 627   (extensionality _ _ (g ○ f) (g' ○ f')).
 628   intros.
 629   unfold extensionality.
 630   unfold extensionality in H.
 631   unfold extensionality in H0.
 632   intros.
 633   rewrite H.
 634   rewrite H0.
 635   auto.
 636   Qed.
 637
 638
 639
 640
 641
 642 CoInductive Fresh A T :=
 643 { next  : forall a:A, (T a * Fresh A T)
 644 ; split : Fresh A T * Fresh A T
 645 }.
 646
 647
 648
 649
 650
 651 Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
 652
 653
 654 (* string stuff *)
 655 Variable eol : string.
 656 Extract Constant eol  => "'\n':[]".
 657
 658 Class Monad {T:Type->Type} :=
 659 { returnM : forall {a},     a -> T a
 660 ; bindM   : forall {a}{b},  T a -> (a -> T b) -> T b
 661 }.
 662 Implicit Arguments Monad [ ].
 663 Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).
 664
 665 (* the Error monad *)
 666 Inductive OrError (T:Type) :=
 667 | Error : forall error_message:string, OrError T
 668 | OK    : T      -> OrError T.
 669 Notation "??? T" := (OrError T) (at level 10).
 670 Implicit Arguments Error [T].
 671 Implicit Arguments OK [T].
 672
 673 Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
 674   match oe with
 675     | Error s => Error s
 676     | OK    t => f t
 677   end.
 678 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
 679
 680 Open Scope string_scope.
 681 Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg :=
 682   match oe with
 683     | Error s => Error (err_msg +++ eol +++ "  " +++ s)
 684     | OK    t => f t
 685   end.
 686
 687 Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
 688
 689 Definition addErrorMessage s {T} (x:OrError T) :=
 690   x >>=[ s ] (fun y => OK y).
 691
 692 Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
 693 | Indexed_Error : forall error_message:string, Indexed f (Error error_message)
 694 | Indexed_OK    : forall t, f t -> Indexed f (OK t)
 695 .
 696
 697
 698 Require Import Coq.Arith.EqNat.
 699 Instance EqDecidableNat : EqDecidable nat.
 700   apply Build_EqDecidable.
 701   intros.
 702   apply eq_nat_dec.
 703   Defined.
 704
 705 (* for a type with decidable equality, we can maintain lists of distinct elements *)
 706 Section DistinctList.
 707   Context `{V:EqDecidable}.
 708
 709   Fixpoint addToDistinctList (cv:V)(cvl:list V) :=
 710   match cvl with
 711   | nil       => cv::nil
 712   | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl')
 713   end.
 714
 715   Fixpoint removeFromDistinctList (cv:V)(cvl:list V) :=
 716   match cvl with
 717   | nil => nil
 718   | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl')
 719   end.
 720
 721   Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) :=
 722   match cvrem with
 723   | nil         => cvl
 724   | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl)
 725   end.
 726
 727   Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) :=
 728   match cvl1 with
 729   | nil       => cvl2
 730   | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
 731   end.
 732 End DistinctList.
 733
 734 Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(vec T n).
 735   set (list2vec l) as v.
 736   destruct (eqd_dec (length l) n).
 737     rewrite e in v; apply OK; apply v.
 738     apply (Error (error_message (length l) n)).
 739     Defined.
 740
 741 (* Uniques *)
 742 Variable UniqSupply      : Type.                   Extract Inlined Constant UniqSupply     => "UniqSupply.UniqSupply".
 743 Variable Unique          : Type.                   Extract Inlined Constant Unique         => "Unique.Unique".
 744 Variable uniqFromSupply  : UniqSupply -> Unique.   Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply".
 745 Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply.
 746     Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply".
 747 Variable unique_eq       : forall u1 u2:Unique, sumbool (u1=u2) (u1≠u2).
 748     Extract Inlined Constant unique_eq => "(==)".
 749 Variable unique_toString : Unique -> string.
 750     Extract Inlined Constant unique_toString => "show".
 751 Instance EqDecidableUnique : EqDecidable Unique :=
 752   { eqd_dec := unique_eq }.
 753 Instance EqDecidableToString : ToString Unique :=
 754   { toString := unique_toString }.
 755
 756 Inductive UniqM {T:Type} : Type :=
 757  | uniqM    : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
 758  Implicit Arguments UniqM [ ].
 759
 760 Instance UniqMonad : Monad UniqM :=
 761 { returnM := fun T (x:T) => uniqM (fun u => OK (u,x))
 762 ; bindM   := fun a b (x:UniqM a) (f:a->UniqM b) =>
 763   uniqM (fun u =>
 764     match x with
 765       | uniqM fa =>
 766         match fa u with
 767           | Error s   => Error s
 768           | OK (u',va) => match f va with
 769                            | uniqM fb => fb u'
 770                          end
 771         end
 772     end)
 773 }.
 774
 775 Definition getU : UniqM Unique :=
 776   uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
 777
 778 Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity).
 779 Notation "'return' x" := (returnM x) (at level 100).
 780 Notation "'failM'  x" := (uniqM (fun _ => Error x)) (at level 100).
 781
 782
 783
 784
 785 Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".