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