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