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 (*******************************************************************************)
  25 (* Trees                                                                       *)
  26
  27 Inductive Tree (a:Type) : Type :=
  28   | T_Leaf   : a -> Tree a
  29   | T_Branch : Tree a -> Tree a -> Tree a.
  30 Implicit Arguments T_Leaf   [ a ].
  31 Implicit Arguments T_Branch [ a ].
  32
  33 Notation "a ,, b"   := (@T_Branch _ a b)                        : tree_scope.
  34
  35 (* tree-of-option-of-X comes up a lot, so we give it special notations *)
  36 Notation "[ q ]"    := (@T_Leaf (option _) (Some q))            : tree_scope.
  37 Notation "[ ]"      := (@T_Leaf (option _) None)                : tree_scope.
  38 Notation "[]"       := (@T_Leaf (option _) None)                : tree_scope.
  39
  40 Open Scope tree_scope.
  41
  42 Fixpoint mapTree {a b:Type}(f:a->b)(t:@Tree a) : @Tree b :=
  43   match t with
  44     | T_Leaf x     => T_Leaf (f x)
  45     | T_Branch l r => T_Branch (mapTree f l) (mapTree f r)
  46   end.
  47 Fixpoint mapOptionTree {a b:Type}(f:a->b)(t:@Tree ??a) : @Tree ??b :=
  48   match t with
  49     | T_Leaf None     => T_Leaf None
  50     | T_Leaf (Some x) => T_Leaf (Some (f x))
  51     | T_Branch l r => T_Branch (mapOptionTree f l) (mapOptionTree f r)
  52   end.
  53 Fixpoint mapTreeAndFlatten {a b:Type}(f:a->@Tree b)(t:@Tree a) : @Tree b :=
  54   match t with
  55     | T_Leaf x        => f x
  56     | T_Branch l r    => T_Branch (mapTreeAndFlatten f l) (mapTreeAndFlatten f r)
  57   end.
  58 Fixpoint mapOptionTreeAndFlatten {a b:Type}(f:a->@Tree ??b)(t:@Tree ??a) : @Tree ??b :=
  59   match t with
  60     | T_Leaf None     => []
  61     | T_Leaf (Some x) => f x
  62     | T_Branch l r    => T_Branch (mapOptionTreeAndFlatten f l) (mapOptionTreeAndFlatten f r)
  63   end.
  64 Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tree T) :=
  65   match t with
  66   | T_Leaf x => mapLeaf x
  67   | T_Branch y z => mergeBranches (treeReduce mapLeaf mergeBranches y) (treeReduce mapLeaf mergeBranches z)
  68   end.
  69 Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
  70   forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.
  71
  72 Lemma tree_dec_eq :
  73    forall {Q}(t1 t2:Tree ??Q),
  74      (forall q1 q2:Q, sumbool (q1=q2) (not (q1=q2))) ->
  75      sumbool (t1=t2) (not (t1=t2)).
  76   intro Q.
  77   intro t1.
  78   induction t1; intros.
  79
  80   destruct a; destruct t2.
  81   destruct o.
  82   set (X q q0) as X'.
  83   inversion X'; subst.
  84   left; auto.
  85   right; unfold not; intro; apply H. inversion H0; subst. auto.
  86   right. unfold not; intro; inversion H.
  87   right. unfold not; intro; inversion H.
  88   destruct o.
  89   right. unfold not; intro; inversion H.
  90   left; auto.
  91   right. unfold not; intro; inversion H.
  92
  93   destruct t2.
  94   right. unfold not; intro; inversion H.
  95   set (IHt1_1 t2_1 X) as X1.
  96   set (IHt1_2 t2_2 X) as X2.
  97   destruct X1; destruct X2; subst.
  98   left; auto.
  99
 100   right.
 101   unfold not; intro H.
 102   apply n.
 103   inversion H; auto.
 104
 105   right.
 106   unfold not; intro H.
 107   apply n.
 108   inversion H; auto.
 109
 110   right.
 111   unfold not; intro H.
 112   apply n.
 113   inversion H; auto.
 114   Defined.
 115
 116 Lemma mapOptionTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree ??A),
 117   (mapOptionTree (g ○ f) l) = (mapOptionTree g (mapOptionTree f l)).
 118   induction l.
 119     destruct a.
 120     reflexivity.
 121     reflexivity.
 122     simpl.
 123     rewrite IHl1.
 124     rewrite IHl2.
 125     reflexivity.
 126     Qed.
 127
 128
 129
 130 (*******************************************************************************)
 131 (* Lists                                                                       *)
 132
 133 Notation "a :: b"         := (cons a b)                               : list_scope.
 134 Open Scope list_scope.
 135 Fixpoint leaves {a:Type}(t:Tree (option a)) : list a :=
 136   match t with
 137     | (T_Leaf l)     => match l with
 138                           | None   => nil
 139                           | Some x => x::nil
 140                         end
 141     | (T_Branch l r) => app (leaves l) (leaves r)
 142   end.
 143 (* weak inverse of "leaves" *)
 144 Fixpoint unleaves {A:Type}(l:list A) : Tree (option A) :=
 145   match l with
 146     | nil    => []
 147     | (a::b) => [a],,(unleaves b)
 148   end.
 149
 150 (* a map over a list and the conjunction of the results *)
 151 Fixpoint mapProp {A:Type} (f:A->Prop) (l:list A) : Prop :=
 152   match l with
 153     | nil => True
 154     | (a::al) => f a /\ mapProp f al
 155   end.
 156
 157 Lemma map_id : forall A (l:list A), (map (fun x:A => x) l) = l.
 158   induction l.
 159   auto.
 160   simpl.
 161   rewrite IHl.
 162   auto.
 163   Defined.
 164 Lemma map_app : forall `(f:A->B) l l', map f (app l l') = app (map f l) (map f l').
 165   intros.
 166   induction l; auto.
 167   simpl.
 168   rewrite IHl.
 169   auto.
 170   Defined.
 171 Lemma map_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
 172   (map (g ○ f) l) = (map g (map f l)).
 173   intros.
 174   induction l.
 175   simpl; auto.
 176   simpl.
 177   rewrite IHl.
 178   auto.
 179   Defined.
 180 Lemma list_cannot_be_longer_than_itself : forall `(a:A)(b:list A), b = (a::b) -> False.
 181   intros.
 182   induction b.
 183   inversion H.
 184   inversion H. apply IHb in H2.
 185   auto.
 186   Defined.
 187 Lemma list_cannot_be_longer_than_itself' : forall A (b:list A) (a c:A), b = (a::c::b) -> False.
 188   induction b.
 189   intros; inversion H.
 190   intros.
 191   inversion H.
 192   apply IHb in H2.
 193   auto.
 194   Defined.
 195
 196 Lemma mapOptionTree_on_nil : forall `(f:A->B) h, [] = mapOptionTree f h -> h=[].
 197   intros.
 198   destruct h.
 199   destruct o. inversion H.
 200   auto.
 201   inversion H.
 202   Defined.
 203
 204 Lemma mapOptionTree_comp a b c (f:a->b) (g:b->c) q : (mapOptionTree g (mapOptionTree f q)) = mapOptionTree (g ○ f) q.
 205   induction q.
 206     destruct a0; simpl.
 207     reflexivity.
 208     reflexivity.
 209     simpl.
 210     rewrite IHq1.
 211     rewrite IHq2.
 212     reflexivity.
 213   Qed.
 214
 215 (* handy facts: map preserves the length of a list *)
 216 Lemma map_on_nil : forall A B (s1:list A) (f:A->B), nil = map f s1 -> s1=nil.
 217   intros.
 218   induction s1.
 219   auto.
 220   assert False.
 221   simpl in H.
 222   inversion H.
 223   inversion H0.
 224   Defined.
 225 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 }.
 226   induction s1.
 227   intros.
 228   simpl in H; assert False. inversion H. inversion H0.
 229   clear IHs1.
 230   intros.
 231   exists a.
 232   simpl in H.
 233   assert (s1=nil).
 234     inversion H. apply map_on_nil in H2. auto.
 235   subst.
 236   auto.
 237   assert (s1=nil).
 238     inversion H. apply map_on_nil in H2. auto.
 239   subst.
 240   simpl in H.
 241   inversion H. auto.
 242   Defined.
 243
 244 Lemma map_on_doubleton : forall A B (f:A->B) x y (s1:list A), ((x::y::nil) = map f s1) ->
 245   { z : A*A & s1=((fst z)::(snd z)::nil) & (f (fst z))=x /\ (f (snd z))=y }.
 246   intros.
 247   destruct s1.
 248   inversion H.
 249   destruct s1.
 250   inversion H.
 251   destruct s1.
 252   inversion H.
 253   exists (a,a0); auto.
 254   simpl in H.
 255   inversion H.
 256   Defined.
 257
 258
 259 Lemma mapTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree A),
 260   (mapTree (g ○ f) l) = (mapTree g (mapTree f l)).
 261   induction l.
 262     reflexivity.
 263     simpl.
 264     rewrite IHl1.
 265     rewrite IHl2.
 266     reflexivity.
 267     Defined.
 268
 269 Lemma lmap_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
 270   (map (g ○ f) l) = (map g (map f l)).
 271   intros.
 272   induction l.
 273   simpl; auto.
 274   simpl.
 275   rewrite IHl.
 276   auto.
 277   Defined.
 278
 279 (* sends a::b::c::nil to [[[[],,c],,b],,a] *)
 280 Fixpoint unleaves' {A:Type}(l:list A) : Tree (option A) :=
 281   match l with
 282     | nil    => []
 283     | (a::b) => (unleaves' b),,[a]
 284   end.
 285
 286 (* sends a::b::c::nil to [[[[],,c],,b],,a] *)
 287 Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A :=
 288   match l with
 289     | nil    => []
 290     | (a::b) => (unleaves'' b),,(T_Leaf a)
 291   end.
 292
 293 Fixpoint filter {T:Type}(l:list ??T) : list T :=
 294   match l with
 295     | nil => nil
 296     | (None::b) => filter b
 297     | ((Some x)::b) => x::(filter b)
 298   end.
 299
 300 Inductive distinct {T:Type} : list T -> Prop :=
 301 | distinct_nil  : distinct nil
 302 | distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax).
 303
 304 Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
 305   induction l; auto.
 306   simpl.
 307   omega.
 308   Qed.
 309
 310 (* decidable quality on a list of elements which have decidable equality *)
 311 Definition list_eq_dec : forall {T:Type}(l1 l2:list T)(dec:forall t1 t2:T, sumbool (eq t1 t2) (not (eq t1 t2))),
 312   sumbool (eq l1 l2) (not (eq l1 l2)).
 313   intro T.
 314   intro l1.
 315   induction l1; intros.
 316     destruct l2.
 317     left; reflexivity.
 318     right; intro H; inversion H.
 319   destruct l2 as [| b l2].
 320     right; intro H; inversion H.
 321   set (IHl1 l2 dec) as eqx.
 322     destruct eqx.
 323     subst.
 324     set (dec a b) as eqy.
 325     destruct eqy.
 326       subst.
 327       left; reflexivity.
 328       right. intro. inversion H. subst. apply n. auto.
 329     right.
 330       intro.
 331       inversion H.
 332       apply n.
 333       auto.
 334       Defined.
 335
 336 Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
 337   apply Build_EqDecidable.
 338   intros.
 339   apply list_eq_dec.
 340   apply eqd_dec.
 341   Defined.
 342
 343 (*******************************************************************************)
 344 (* Length-Indexed Lists                                                        *)
 345
 346 Inductive vec (A:Type) : nat -> Type :=
 347 | vec_nil  : vec A 0
 348 | vec_cons : forall n, A -> vec A n -> vec A (S n).
 349
 350 Fixpoint vec2list {n:nat}{t:Type}(v:vec t n) : list t :=
 351   match v with
 352     | vec_nil => nil
 353     | vec_cons n a va => a::(vec2list va)
 354   end.
 355
 356 Require Import Omega.
 357 Definition vec_get : forall {T:Type}{l:nat}(v:vec T l)(n:nat)(pf:lt n l), T.
 358   intro T.
 359   intro len.
 360   intro v.
 361   induction v; intros.
 362     assert False.
 363     inversion pf.
 364     inversion H.
 365   rename n into len.
 366     destruct n0 as [|n].
 367     exact a.
 368     apply (IHv n).
 369     omega.
 370     Defined.
 371
 372 Definition vec_zip {n:nat}{A B:Type}(va:vec A n)(vb:vec B n) : vec (A*B) n.
 373   induction n.
 374   apply vec_nil.
 375   inversion va; subst.
 376   inversion vb; subst.
 377   apply vec_cons; auto.
 378   Defined.
 379
 380 Definition vec_map {n:nat}{A B:Type}(f:A->B)(v:vec A n) : vec B n.
 381   induction n.
 382   apply vec_nil.
 383   inversion v; subst.
 384   apply vec_cons; auto.
 385   Defined.
 386
 387 Fixpoint vec_In {A:Type} {n:nat} (a:A) (l:vec A n) : Prop :=
 388   match l with
 389     | vec_nil         => False
 390     | vec_cons _ n m  => (n = a) \/ vec_In a m
 391   end.
 392 Implicit Arguments vec_nil  [ A   ].
 393 Implicit Arguments vec_cons [ A n ].
 394
 395 Definition append_vec {n:nat}{T:Type}(v:vec T n)(t:T) : vec T (S n).
 396   induction n.
 397   apply (vec_cons t vec_nil).
 398   apply vec_cons; auto.
 399   Defined.
 400
 401 Definition list2vec {T:Type}(l:list T) : vec T (length l).
 402   induction l.
 403   apply vec_nil.
 404   apply vec_cons; auto.
 405   Defined.
 406
 407 Definition vec_head {n:nat}{T}(v:vec T (S n)) : T.
 408   inversion v;  auto.
 409   Defined.
 410 Definition vec_tail {n:nat}{T}(v:vec T (S n)) : vec T n.
 411   inversion v;  auto.
 412   Defined.
 413
 414 Lemma vec_chop {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l1).
 415   induction l1.
 416   apply vec_nil.
 417   apply vec_cons.
 418   simpl in *.
 419   inversion v; subst; auto.
 420   apply IHl1.
 421   inversion v; subst; auto.
 422   Defined.
 423
 424 Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l2).
 425   induction l1.
 426   apply v.
 427   simpl in *.
 428   apply IHl1; clear IHl1.
 429   inversion v; subst; auto.
 430   Defined.
 431
 432 Lemma vec2list_len {T}{n}(v:vec T n) : length (vec2list v) = n.
 433   induction v; auto.
 434   simpl.
 435   omega.
 436   Qed.
 437
 438 Lemma vec2list_map_list2vec {A B}{n}(f:A->B)(v:vec A n) : map f (vec2list v) = vec2list (vec_map f v).
 439   induction v; auto.
 440   simpl. rewrite IHv.
 441   reflexivity.
 442   Qed.
 443
 444 Lemma vec2list_list2vec {A}(v:list A) : vec2list (list2vec v) = v.
 445   induction v; auto.
 446   set (vec2list (list2vec (a :: v))) as q.
 447   rewrite <- IHv.
 448   unfold q.
 449   clear q.
 450   simpl.
 451   reflexivity.
 452   Qed.
 453
 454 Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20).
 455
 456
 457
 458 (*******************************************************************************)
 459 (* Shaped Trees                                                                *)
 460
 461 (* a ShapedTree is a tree indexed by the shape (but not the leaf values) of another tree; isomorphic to (ITree (fun _ => Q)) *)
 462 Inductive ShapedTree {T:Type}(Q:Type) : Tree ??T -> Type :=
 463 | st_nil    : @ShapedTree T Q []
 464 | st_leaf   : forall {t}, Q -> @ShapedTree T Q [t]
 465 | st_branch : forall {t1}{t2}, @ShapedTree T Q t1 -> @ShapedTree T Q t2 -> @ShapedTree T Q (t1,,t2).
 466
 467 Fixpoint unshape {T:Type}{Q:Type}{idx:Tree ??T}(st:@ShapedTree T Q idx) : Tree ??Q :=
 468 match st with
 469 | st_nil => []
 470 | st_leaf _ q => [q]
 471 | st_branch _ _ b1 b2 => (unshape b1),,(unshape b2)
 472 end.
 473
 474 Definition mapShapedTree {T}{idx:Tree ??T}{V}{Q}(f:V->Q)(st:ShapedTree V idx) : ShapedTree Q idx.
 475   induction st.
 476   apply st_nil.
 477   apply st_leaf. apply f. apply q.
 478   apply st_branch; auto.
 479   Defined.
 480
 481 Definition zip_shapedTrees {T:Type}{Q1 Q2:Type}{idx:Tree ??T}
 482    (st1:ShapedTree Q1 idx)(st2:ShapedTree Q2 idx) : ShapedTree (Q1*Q2) idx.
 483   induction idx.
 484     destruct a.
 485     apply st_leaf; auto.
 486     inversion st1.
 487     inversion st2.
 488     auto.
 489     apply st_nil.
 490     apply st_branch; auto.
 491     inversion st1; subst; apply IHidx1; auto.
 492     inversion st2; subst; auto.
 493     inversion st2; subst; apply IHidx2; auto.
 494     inversion st1; subst; auto.
 495   Defined.
 496
 497 Definition build_shapedTree {T:Type}(idx:Tree ??T){Q:Type}(f:T->Q) : ShapedTree Q idx.
 498   induction idx.
 499   destruct a.
 500   apply st_leaf; auto.
 501   apply st_nil.
 502   apply st_branch; auto.
 503   Defined.
 504
 505 Lemma unshape_map : forall {Q}{b}(f:Q->b){T}{idx:Tree ??T}(t:ShapedTree Q idx),
 506    mapOptionTree f (unshape t) = unshape (mapShapedTree f t).
 507   intros.
 508   induction t; auto.
 509   simpl.
 510   rewrite IHt1.
 511   rewrite IHt2.
 512   reflexivity.
 513   Qed.
 514
 515
 516
 517
 518 (*******************************************************************************)
 519 (* Type-Indexed Lists                                                          *)
 520
 521 (* an indexed list *)
 522 Inductive IList (I:Type)(F:I->Type) : list I -> Type :=
 523 | INil      :                                       IList I F nil
 524 | ICons     :   forall i is, F i -> IList I F is -> IList I F (i::is).
 525 Implicit Arguments INil [ I F ].
 526 Implicit Arguments ICons [ I F ].
 527
 528 (* a tree indexed by a (Tree (option X)) *)
 529 Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type :=
 530 | INone      :                                ITree I F []
 531 | ILeaf      :  forall       i:     I, F i -> ITree I F [i]
 532 | IBranch    :  forall it1 it2:Tree ??I, ITree I F it1 -> ITree I F it2 -> ITree I F (it1,,it2).
 533 Implicit Arguments INil    [ I F ].
 534 Implicit Arguments ILeaf   [ I F ].
 535 Implicit Arguments IBranch [ I F ].
 536
 537
 538
 539
 540 (*******************************************************************************)
 541 (* Extensional equality on functions                                           *)
 542
 543 Definition extensionality := fun (t1 t2:Type) => (fun (f:t1->t2) g => forall x:t1, (f x)=(g x)).
 544 Hint Transparent extensionality.
 545 Instance extensionality_Equivalence : forall t1 t2, Equivalence (extensionality t1 t2).
 546   intros; apply Build_Equivalence;
 547     intros; compute; intros; auto.
 548     rewrite H; rewrite H0; auto.
 549   Defined.
 550   Add Parametric Morphism (A B C:Type) : (fun f g => g ○ f)
 551   with signature (extensionality A B ==> extensionality B C ==> extensionality A C) as parametric_morphism_extensionality.
 552   unfold extensionality; intros; rewrite (H x1); rewrite (H0 (y x1)); auto.
 553   Defined.
 554 Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
 555   (extensionality _ _ f f') ->
 556   (extensionality _ _ g g') ->
 557   (extensionality _ _ (g ○ f) (g' ○ f')).
 558   intros.
 559   unfold extensionality.
 560   unfold extensionality in H.
 561   unfold extensionality in H0.
 562   intros.
 563   rewrite H.
 564   rewrite H0.
 565   auto.
 566   Qed.
 567
 568
 569
 570 Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
 571
 572
 573
 574 (* the Error monad *)
 575 Inductive OrError (T:Type) :=
 576 | Error : forall error_message:string, OrError T
 577 | OK    : T      -> OrError T.
 578 Notation "??? T" := (OrError T) (at level 10).
 579 Implicit Arguments Error [T].
 580 Implicit Arguments OK [T].
 581
 582 Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
 583   match oe with
 584     | Error s => Error s
 585     | OK    t => f t
 586   end.
 587 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
 588
 589 Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
 590 | Indexed_Error : forall error_message:string, Indexed f (Error error_message)
 591 | Indexed_OK    : forall t, f t -> Indexed f (OK t)
 592 .
 593
 594
 595 Require Import Coq.Arith.EqNat.
 596 Instance EqDecidableNat : EqDecidable nat.
 597   apply Build_EqDecidable.
 598   intros.
 599   apply eq_nat_dec.
 600   Defined.
 601
 602 (* for a type with decidable equality, we can maintain lists of distinct elements *)
 603 Section DistinctList.
 604   Context `{V:EqDecidable}.
 605
 606   Fixpoint addToDistinctList (cv:V)(cvl:list V) :=
 607   match cvl with
 608   | nil       => cv::nil
 609   | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl')
 610   end.
 611
 612   Fixpoint removeFromDistinctList (cv:V)(cvl:list V) :=
 613   match cvl with
 614   | nil => nil
 615   | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl')
 616   end.
 617
 618   Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) :=
 619   match cvrem with
 620   | nil         => cvl
 621   | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl)
 622   end.
 623
 624   Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) :=
 625   match cvl1 with
 626   | nil       => cvl2
 627   | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
 628   end.
 629 End DistinctList.
 630
 631 Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(vec T n).
 632   set (list2vec l) as v.
 633   destruct (eqd_dec (length l) n).
 634     rewrite e in v; apply OK; apply v.
 635     apply (Error (error_message (length l) n)).
 636     Defined.