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
 593
 594
 595 (*******************************************************************************)
 596 (* Extensional equality on functions                                           *)
 597
 598 Definition extensionality := fun (t1 t2:Type) => (fun (f:t1->t2) g => forall x:t1, (f x)=(g x)).
 599 Hint Transparent extensionality.
 600 Instance extensionality_Equivalence : forall t1 t2, Equivalence (extensionality t1 t2).
 601   intros; apply Build_Equivalence;
 602     intros; compute; intros; auto.
 603     rewrite H; rewrite H0; auto.
 604   Defined.
 605   Add Parametric Morphism (A B C:Type) : (fun f g => g ○ f)
 606   with signature (extensionality A B ==> extensionality B C ==> extensionality A C) as parametric_morphism_extensionality.
 607   unfold extensionality; intros; rewrite (H x1); rewrite (H0 (y x1)); auto.
 608   Defined.
 609 Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
 610   (extensionality _ _ f f') ->
 611   (extensionality _ _ g g') ->
 612   (extensionality _ _ (g ○ f) (g' ○ f')).
 613   intros.
 614   unfold extensionality.
 615   unfold extensionality in H.
 616   unfold extensionality in H0.
 617   intros.
 618   rewrite H.
 619   rewrite H0.
 620   auto.
 621   Qed.
 622
 623
 624
 625
 626
 627 CoInductive Fresh A T :=
 628 { next  : forall a:A, (T a * Fresh A T)
 629 ; split : Fresh A T * Fresh A T
 630 }.
 631
 632
 633
 634
 635
 636 Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
 637
 638
 639 (* string stuff *)
 640 Variable eol : string.
 641 Extract Constant eol  => "'\n':[]".
 642
 643 Class Monad {T:Type->Type} :=
 644 { returnM : forall {a},     a -> T a
 645 ; bindM   : forall {a}{b},  T a -> (a -> T b) -> T b
 646 }.
 647 Implicit Arguments Monad [ ].
 648 Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).
 649
 650 (* the Error monad *)
 651 Inductive OrError (T:Type) :=
 652 | Error : forall error_message:string, OrError T
 653 | OK    : T      -> OrError T.
 654 Notation "??? T" := (OrError T) (at level 10).
 655 Implicit Arguments Error [T].
 656 Implicit Arguments OK [T].
 657
 658 Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
 659   match oe with
 660     | Error s => Error s
 661     | OK    t => f t
 662   end.
 663 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
 664
 665 Open Scope string_scope.
 666 Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg :=
 667   match oe with
 668     | Error s => Error (err_msg +++ eol +++ "  " +++ s)
 669     | OK    t => f t
 670   end.
 671
 672 Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
 673
 674 Definition addErrorMessage s {T} (x:OrError T) :=
 675   x >>=[ s ] (fun y => OK y).
 676
 677 Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
 678 | Indexed_Error : forall error_message:string, Indexed f (Error error_message)
 679 | Indexed_OK    : forall t, f t -> Indexed f (OK t)
 680 .
 681
 682
 683 Require Import Coq.Arith.EqNat.
 684 Instance EqDecidableNat : EqDecidable nat.
 685   apply Build_EqDecidable.
 686   intros.
 687   apply eq_nat_dec.
 688   Defined.
 689
 690 (* for a type with decidable equality, we can maintain lists of distinct elements *)
 691 Section DistinctList.
 692   Context `{V:EqDecidable}.
 693
 694   Fixpoint addToDistinctList (cv:V)(cvl:list V) :=
 695   match cvl with
 696   | nil       => cv::nil
 697   | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl')
 698   end.
 699
 700   Fixpoint removeFromDistinctList (cv:V)(cvl:list V) :=
 701   match cvl with
 702   | nil => nil
 703   | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl')
 704   end.
 705
 706   Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) :=
 707   match cvrem with
 708   | nil         => cvl
 709   | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl)
 710   end.
 711
 712   Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) :=
 713   match cvl1 with
 714   | nil       => cvl2
 715   | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
 716   end.
 717 End DistinctList.
 718
 719 Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(vec T n).
 720   set (list2vec l) as v.
 721   destruct (eqd_dec (length l) n).
 722     rewrite e in v; apply OK; apply v.
 723     apply (Error (error_message (length l) n)).
 724     Defined.
 725
 726
 727
 728
 729
 730 Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".