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 Fixpoint InT {A} (a:A) (t:Tree ??A) {struct t} : Prop :=
  45   match t with
  46     | T_Leaf None     => False
  47     | T_Leaf (Some x) => x = a
  48     | T_Branch b1 b2  => InT a b1 \/ InT a b2
  49   end.
  50
  51 Open Scope tree_scope.
  52
  53 Fixpoint mapTree {a b:Type}(f:a->b)(t:@Tree a) : @Tree b :=
  54   match t with
  55     | T_Leaf x     => T_Leaf (f x)
  56     | T_Branch l r => T_Branch (mapTree f l) (mapTree f r)
  57   end.
  58 Fixpoint mapOptionTree {a b:Type}(f:a->b)(t:@Tree ??a) : @Tree ??b :=
  59   match t with
  60     | T_Leaf None     => T_Leaf None
  61     | T_Leaf (Some x) => T_Leaf (Some (f x))
  62     | T_Branch l r    => T_Branch (mapOptionTree f l) (mapOptionTree f r)
  63   end.
  64 Fixpoint mapTreeAndFlatten {a b:Type}(f:a->@Tree b)(t:@Tree a) : @Tree b :=
  65   match t with
  66     | T_Leaf x        => f x
  67     | T_Branch l r    => T_Branch (mapTreeAndFlatten f l) (mapTreeAndFlatten f r)
  68   end.
  69 Fixpoint mapOptionTreeAndFlatten {a b:Type}(f:a->@Tree ??b)(t:@Tree ??a) : @Tree ??b :=
  70   match t with
  71     | T_Leaf None     => []
  72     | T_Leaf (Some x) => f x
  73     | T_Branch l r    => T_Branch (mapOptionTreeAndFlatten f l) (mapOptionTreeAndFlatten f r)
  74   end.
  75 Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tree T) :=
  76   match t with
  77   | T_Leaf x => mapLeaf x
  78   | T_Branch y z => mergeBranches (treeReduce mapLeaf mergeBranches y) (treeReduce mapLeaf mergeBranches z)
  79   end.
  80 Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
  81   forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.
  82
  83 Lemma tree_dec_eq :
  84    forall {Q}(t1 t2:Tree ??Q),
  85      (forall q1 q2:Q, sumbool (q1=q2) (not (q1=q2))) ->
  86      sumbool (t1=t2) (not (t1=t2)).
  87   intro Q.
  88   intro t1.
  89   induction t1; intros.
  90
  91   destruct a; destruct t2.
  92   destruct o.
  93   set (X q q0) as X'.
  94   inversion X'; subst.
  95   left; auto.
  96   right; unfold not; intro; apply H. inversion H0; subst. auto.
  97   right. unfold not; intro; inversion H.
  98   right. unfold not; intro; inversion H.
  99   destruct o.
 100   right. unfold not; intro; inversion H.
 101   left; auto.
 102   right. unfold not; intro; inversion H.
 103
 104   destruct t2.
 105   right. unfold not; intro; inversion H.
 106   set (IHt1_1 t2_1 X) as X1.
 107   set (IHt1_2 t2_2 X) as X2.
 108   destruct X1; destruct X2; subst.
 109   left; auto.
 110
 111   right.
 112   unfold not; intro H.
 113   apply n.
 114   inversion H; auto.
 115
 116   right.
 117   unfold not; intro H.
 118   apply n.
 119   inversion H; auto.
 120
 121   right.
 122   unfold not; intro H.
 123   apply n.
 124   inversion H; auto.
 125   Defined.
 126
 127 Lemma mapOptionTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree ??A),
 128   (mapOptionTree (g ○ f) l) = (mapOptionTree g (mapOptionTree f l)).
 129   induction l.
 130     destruct a.
 131     reflexivity.
 132     reflexivity.
 133     simpl.
 134     rewrite IHl1.
 135     rewrite IHl2.
 136     reflexivity.
 137     Qed.
 138
 139 Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (forall t, mapOptionTree f t = mapOptionTree g t).
 140   intros.
 141   induction t.
 142   destruct a; auto.
 143   simpl; rewrite H; auto.
 144   simpl; rewrite IHt1; rewrite IHt2; auto.
 145   Qed.
 146
 147 Open Scope string_scope.
 148 Fixpoint treeToString {T}{TT:ToString T}(t:Tree ??T) : string :=
 149 match t with
 150   | T_Leaf None => "[]"
 151   | T_Leaf (Some s) => "["+++s+++"]"
 152   | T_Branch b1 b2 => treeToString b1 +++ ",," +++ treeToString b2
 153 end.
 154 Instance TreeToString {T}{TT:ToString T} : ToString (Tree ??T) := { toString := treeToString }.
 155
 156 (*******************************************************************************)
 157 (* Lists                                                                       *)
 158
 159 Notation "a :: b"         := (cons a b)                               : list_scope.
 160 Open Scope list_scope.
 161 Fixpoint leaves {a:Type}(t:Tree (option a)) : list a :=
 162   match t with
 163     | (T_Leaf l)     => match l with
 164                           | None   => nil
 165                           | Some x => x::nil
 166                         end
 167     | (T_Branch l r) => app (leaves l) (leaves r)
 168   end.
 169 (* weak inverse of "leaves" *)
 170 Fixpoint unleaves {A:Type}(l:list A) : Tree (option A) :=
 171   match l with
 172     | nil    => []
 173     | (a::b) => [a],,(unleaves b)
 174   end.
 175
 176 (* a map over a list and the conjunction of the results *)
 177 Fixpoint mapProp {A:Type} (f:A->Prop) (l:list A) : Prop :=
 178   match l with
 179     | nil => True
 180     | (a::al) => f a /\ mapProp f al
 181   end.
 182
 183 Lemma map_id : forall A (l:list A), (map (fun x:A => x) l) = l.
 184   induction l.
 185   auto.
 186   simpl.
 187   rewrite IHl.
 188   auto.
 189   Defined.
 190 Lemma map_app : forall `(f:A->B) l l', map f (app l l') = app (map f l) (map f l').
 191   intros.
 192   induction l; auto.
 193   simpl.
 194   rewrite IHl.
 195   auto.
 196   Defined.
 197 Lemma map_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
 198   (map (g ○ f) l) = (map g (map f l)).
 199   intros.
 200   induction l.
 201   simpl; auto.
 202   simpl.
 203   rewrite IHl.
 204   auto.
 205   Defined.
 206 Lemma list_cannot_be_longer_than_itself : forall `(a:A)(b:list A), b = (a::b) -> False.
 207   intros.
 208   induction b.
 209   inversion H.
 210   inversion H. apply IHb in H2.
 211   auto.
 212   Defined.
 213 Lemma list_cannot_be_longer_than_itself' : forall A (b:list A) (a c:A), b = (a::c::b) -> False.
 214   induction b.
 215   intros; inversion H.
 216   intros.
 217   inversion H.
 218   apply IHb in H2.
 219   auto.
 220   Defined.
 221
 222 Lemma mapOptionTree_on_nil : forall `(f:A->B) h, [] = mapOptionTree f h -> h=[].
 223   intros.
 224   destruct h.
 225   destruct o. inversion H.
 226   auto.
 227   inversion H.
 228   Defined.
 229
 230 Lemma mapOptionTree_comp a b c (f:a->b) (g:b->c) q : (mapOptionTree g (mapOptionTree f q)) = mapOptionTree (g ○ f) q.
 231   induction q.
 232     destruct a0; simpl.
 233     reflexivity.
 234     reflexivity.
 235     simpl.
 236     rewrite IHq1.
 237     rewrite IHq2.
 238     reflexivity.
 239   Qed.
 240
 241 Lemma leaves_unleaves {T}(t:list T) : leaves (unleaves t) = t.
 242   induction t; auto.
 243   simpl.
 244   rewrite IHt; auto.
 245   Qed.
 246
 247 Lemma mapleaves' {T:Type}(t:list T){Q}{f:T->Q} : unleaves (map f t) = mapOptionTree f (unleaves t).
 248   induction t; simpl in *; auto.
 249   rewrite IHt; auto.
 250   Qed.
 251
 252 (* handy facts: map preserves the length of a list *)
 253 Lemma map_on_nil : forall A B (s1:list A) (f:A->B), nil = map f s1 -> s1=nil.
 254   intros.
 255   induction s1.
 256   auto.
 257   assert False.
 258   simpl in H.
 259   inversion H.
 260   inversion H0.
 261   Defined.
 262 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 }.
 263   induction s1.
 264   intros.
 265   simpl in H; assert False. inversion H. inversion H0.
 266   clear IHs1.
 267   intros.
 268   exists a.
 269   simpl in H.
 270   assert (s1=nil).
 271     inversion H. apply map_on_nil in H2. auto.
 272   subst.
 273   auto.
 274   assert (s1=nil).
 275     inversion H. apply map_on_nil in H2. auto.
 276   subst.
 277   simpl in H.
 278   inversion H. auto.
 279   Defined.
 280
 281 Lemma map_on_doubleton : forall A B (f:A->B) x y (s1:list A), ((x::y::nil) = map f s1) ->
 282   { z : A*A & s1=((fst z)::(snd z)::nil) & (f (fst z))=x /\ (f (snd z))=y }.
 283   intros.
 284   destruct s1.
 285   inversion H.
 286   destruct s1.
 287   inversion H.
 288   destruct s1.
 289   inversion H.
 290   exists (a,a0); auto.
 291   simpl in H.
 292   inversion H.
 293   Defined.
 294
 295
 296 Lemma mapTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree A),
 297   (mapTree (g ○ f) l) = (mapTree g (mapTree f l)).
 298   induction l.
 299     reflexivity.
 300     simpl.
 301     rewrite IHl1.
 302     rewrite IHl2.
 303     reflexivity.
 304     Defined.
 305
 306 Lemma lmap_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
 307   (map (g ○ f) l) = (map g (map f l)).
 308   intros.
 309   induction l.
 310   simpl; auto.
 311   simpl.
 312   rewrite IHl.
 313   auto.
 314   Defined.
 315
 316 (* sends a::b::c::nil to [[[[],,c],,b],,a] *)
 317 Fixpoint unleaves' {A:Type}(l:list A) : Tree (option A) :=
 318   match l with
 319     | nil    => []
 320     | (a::b) => (unleaves' b),,[a]
 321   end.
 322
 323 (* sends a::b::c::nil to [[[[],,c],,b],,a] *)
 324 Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A :=
 325   match l with
 326     | nil    => []
 327     | (a::b) => (unleaves'' b),,(T_Leaf a)
 328   end.
 329
 330 Lemma mapleaves {T:Type}(t:Tree ??T){Q}{f:T->Q} : leaves (mapOptionTree f t) = map f (leaves t).
 331   induction t.
 332   destruct a; auto.
 333   simpl.
 334   rewrite IHt1.
 335   rewrite IHt2.
 336   rewrite map_app.
 337   auto.
 338   Qed.
 339
 340 Fixpoint filter {T:Type}(l:list ??T) : list T :=
 341   match l with
 342     | nil => nil
 343     | (None::b) => filter b
 344     | ((Some x)::b) => x::(filter b)
 345   end.
 346
 347 Inductive distinct {T:Type} : list T -> Prop :=
 348 | distinct_nil  : distinct nil
 349 | distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax).
 350
 351 Inductive distinctT {T:Type} : Tree ??T -> Prop :=
 352 | distinctT_nil  : distinctT []
 353 | distinctT_leaf : forall t, distinctT [t]
 354 | distinctT_cons : forall t1 t2, (forall v, InT v t1 -> InT v t2 -> False) -> distinctT (t1,,t2).
 355
 356 Lemma in_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (v:VV)(lv:list VV), sumbool (In v lv) (not (In v lv)).
 357   intros.
 358   induction lv.
 359   right.
 360   unfold not.
 361   intros.
 362   inversion H.
 363   destruct IHlv.
 364   left.
 365   simpl.
 366   auto.
 367   set (eqd_dec v a) as dec.
 368   destruct dec.
 369   subst.
 370   left; simpl; auto.
 371   right.
 372   unfold not; intros.
 373   destruct H.
 374   subst.
 375   apply n0; auto.
 376   apply n.
 377   apply H.
 378   Defined.
 379
 380 Lemma distinct_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (lv:list VV), sumbool (distinct lv) (not (distinct lv)).
 381   intros.
 382   induction lv.
 383   left; apply distinct_nil.
 384   destruct IHlv.
 385   set (in_decidable a lv) as dec.
 386   destruct dec.
 387   right; unfold not; intros.
 388   inversion H.
 389   subst.
 390   apply H2; auto.
 391   left.
 392   apply distinct_cons; auto.
 393   right.
 394   unfold not; intros.
 395   inversion H.
 396   subst.
 397   apply n; auto.
 398   Defined.
 399
 400 Lemma distinctT_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (lv:Tree ??VV), sumbool (distinctT lv) (not (distinctT lv)).
 401   admit.
 402   Defined.
 403
 404 Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
 405   induction l; auto.
 406   simpl.
 407   omega.
 408   Qed.
 409
 410 (* decidable quality on a list of elements which have decidable equality *)
 411 Definition list_eq_dec : forall {T:Type}(l1 l2:list T)(dec:forall t1 t2:T, sumbool (eq t1 t2) (not (eq t1 t2))),
 412   sumbool (eq l1 l2) (not (eq l1 l2)).
 413   intro T.
 414   intro l1.
 415   induction l1; intros.
 416     destruct l2.
 417     left; reflexivity.
 418     right; intro H; inversion H.
 419   destruct l2 as [| b l2].
 420     right; intro H; inversion H.
 421   set (IHl1 l2 dec) as eqx.
 422     destruct eqx.
 423     subst.
 424     set (dec a b) as eqy.
 425     destruct eqy.
 426       subst.
 427       left; reflexivity.
 428       right. intro. inversion H. subst. apply n. auto.
 429     right.
 430       intro.
 431       inversion H.
 432       apply n.
 433       auto.
 434       Defined.
 435
 436 Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
 437   apply Build_EqDecidable.
 438   intros.
 439   apply list_eq_dec.
 440   apply eqd_dec.
 441   Defined.
 442
 443 (*******************************************************************************)
 444 (* Length-Indexed Lists                                                        *)
 445
 446 Inductive vec (A:Type) : nat -> Type :=
 447 | vec_nil  : vec A 0
 448 | vec_cons : forall n, A -> vec A n -> vec A (S n).
 449
 450 Fixpoint vec2list {n:nat}{t:Type}(v:vec t n) : list t :=
 451   match v with
 452     | vec_nil => nil
 453     | vec_cons n a va => a::(vec2list va)
 454   end.
 455
 456 Require Import Omega.
 457 Definition vec_get : forall {T:Type}{l:nat}(v:vec T l)(n:nat)(pf:lt n l), T.
 458   intro T.
 459   intro len.
 460   intro v.
 461   induction v; intros.
 462     assert False.
 463     inversion pf.
 464     inversion H.
 465   rename n into len.
 466     destruct n0 as [|n].
 467     exact a.
 468     apply (IHv n).
 469     omega.
 470     Defined.
 471
 472 Definition vec_zip {n:nat}{A B:Type}(va:vec A n)(vb:vec B n) : vec (A*B) n.
 473   induction n.
 474   apply vec_nil.
 475   inversion va; subst.
 476   inversion vb; subst.
 477   apply vec_cons; auto.
 478   Defined.
 479
 480 Definition vec_map {n:nat}{A B:Type}(f:A->B)(v:vec A n) : vec B n.
 481   induction n.
 482   apply vec_nil.
 483   inversion v; subst.
 484   apply vec_cons; auto.
 485   Defined.
 486
 487 Fixpoint vec_In {A:Type} {n:nat} (a:A) (l:vec A n) : Prop :=
 488   match l with
 489     | vec_nil         => False
 490     | vec_cons _ n m  => (n = a) \/ vec_In a m
 491   end.
 492 Implicit Arguments vec_nil  [ A   ].
 493 Implicit Arguments vec_cons [ A n ].
 494
 495 Definition append_vec {n:nat}{T:Type}(v:vec T n)(t:T) : vec T (S n).
 496   induction n.
 497   apply (vec_cons t vec_nil).
 498   apply vec_cons; auto.
 499   Defined.
 500
 501 Definition list2vec {T:Type}(l:list T) : vec T (length l).
 502   induction l.
 503   apply vec_nil.
 504   apply vec_cons; auto.
 505   Defined.
 506
 507 Definition vec_head {n:nat}{T}(v:vec T (S n)) : T.
 508   inversion v;  auto.
 509   Defined.
 510 Definition vec_tail {n:nat}{T}(v:vec T (S n)) : vec T n.
 511   inversion v;  auto.
 512   Defined.
 513
 514 Lemma vec_chop {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l1).
 515   induction l1.
 516   apply vec_nil.
 517   apply vec_cons.
 518   simpl in *.
 519   inversion v; subst; auto.
 520   apply IHl1.
 521   inversion v; subst; auto.
 522   Defined.
 523
 524 Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l2).
 525   induction l1.
 526   apply v.
 527   simpl in *.
 528   apply IHl1; clear IHl1.
 529   inversion v; subst; auto.
 530   Defined.
 531
 532 Lemma vec2list_len {T}{n}(v:vec T n) : length (vec2list v) = n.
 533   induction v; auto.
 534   simpl.
 535   omega.
 536   Qed.
 537
 538 Lemma vec2list_map_list2vec {A B}{n}(f:A->B)(v:vec A n) : map f (vec2list v) = vec2list (vec_map f v).
 539   induction v; auto.
 540   simpl. rewrite IHv.
 541   reflexivity.
 542   Qed.
 543
 544 Lemma vec2list_list2vec {A}(v:list A) : vec2list (list2vec v) = v.
 545   induction v; auto.
 546   set (vec2list (list2vec (a :: v))) as q.
 547   rewrite <- IHv.
 548   unfold q.
 549   clear q.
 550   simpl.
 551   reflexivity.
 552   Qed.
 553
 554 Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20).
 555
 556
 557
 558 (*******************************************************************************)
 559 (* Shaped Trees                                                                *)
 560
 561 (* a ShapedTree is a tree indexed by the shape (but not the leaf values) of another tree; isomorphic to (ITree (fun _ => Q)) *)
 562 Inductive ShapedTree {T:Type}(Q:Type) : Tree ??T -> Type :=
 563 | st_nil    : @ShapedTree T Q []
 564 | st_leaf   : forall {t}, Q -> @ShapedTree T Q [t]
 565 | st_branch : forall {t1}{t2}, @ShapedTree T Q t1 -> @ShapedTree T Q t2 -> @ShapedTree T Q (t1,,t2).
 566
 567 Fixpoint unshape {T:Type}{Q:Type}{idx:Tree ??T}(st:@ShapedTree T Q idx) : Tree ??Q :=
 568 match st with
 569 | st_nil => []
 570 | st_leaf _ q => [q]
 571 | st_branch _ _ b1 b2 => (unshape b1),,(unshape b2)
 572 end.
 573
 574 Definition mapShapedTree {T}{idx:Tree ??T}{V}{Q}(f:V->Q)(st:ShapedTree V idx) : ShapedTree Q idx.
 575   induction st.
 576   apply st_nil.
 577   apply st_leaf. apply f. apply q.
 578   apply st_branch; auto.
 579   Defined.
 580
 581 Definition zip_shapedTrees {T:Type}{Q1 Q2:Type}{idx:Tree ??T}
 582    (st1:ShapedTree Q1 idx)(st2:ShapedTree Q2 idx) : ShapedTree (Q1*Q2) idx.
 583   induction idx.
 584     destruct a.
 585     apply st_leaf; auto.
 586     inversion st1.
 587     inversion st2.
 588     auto.
 589     apply st_nil.
 590     apply st_branch; auto.
 591     inversion st1; subst; apply IHidx1; auto.
 592     inversion st2; subst; auto.
 593     inversion st2; subst; apply IHidx2; auto.
 594     inversion st1; subst; auto.
 595   Defined.
 596
 597 Definition build_shapedTree {T:Type}(idx:Tree ??T){Q:Type}(f:T->Q) : ShapedTree Q idx.
 598   induction idx.
 599   destruct a.
 600   apply st_leaf; auto.
 601   apply st_nil.
 602   apply st_branch; auto.
 603   Defined.
 604
 605 Lemma unshape_map : forall {Q}{b}(f:Q->b){T}{idx:Tree ??T}(t:ShapedTree Q idx),
 606    mapOptionTree f (unshape t) = unshape (mapShapedTree f t).
 607   intros.
 608   induction t; auto.
 609   simpl.
 610   rewrite IHt1.
 611   rewrite IHt2.
 612   reflexivity.
 613   Qed.
 614
 615
 616
 617
 618 (*******************************************************************************)
 619 (* Type-Indexed Lists                                                          *)
 620
 621 (* an indexed list *)
 622 Inductive IList (I:Type)(F:I->Type) : list I -> Type :=
 623 | INil      :                                       IList I F nil
 624 | ICons     :   forall i is, F i -> IList I F is -> IList I F (i::is).
 625 Implicit Arguments INil [ I F ].
 626 Implicit Arguments ICons [ I F ].
 627
 628 Notation "a :::: b" := (@ICons _ _ _ _ a b) (at level 20).
 629
 630 Definition ilist_head {T}{F}{x}{y} : IList T F (x::y) -> F x.
 631   intro il.
 632   inversion il.
 633   subst.
 634   apply X.
 635   Defined.
 636
 637 Definition ilist_tail {T}{F}{x}{y} : IList T F (x::y) -> IList T F y.
 638   intro il.
 639   inversion il.
 640   subst.
 641   apply X0.
 642   Defined.
 643
 644 Definition ilmap {I}{F}{G}{il:list I}(f:forall i:I, F i -> G i) : IList I F il -> IList I G il.
 645   induction il; intros; auto.
 646   apply INil.
 647   inversion X; subst.
 648   apply ICons; auto.
 649   Defined.
 650
 651 Lemma ilist_chop {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l1.
 652   induction l1; auto.
 653   apply INil.
 654   apply ICons.
 655   inversion v; auto.
 656   apply IHl1.
 657   inversion v; auto.
 658   Defined.
 659
 660 Lemma ilist_chop' {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l2.
 661   induction l1; auto.
 662   apply IHl1.
 663   inversion v; subst; auto.
 664   Defined.
 665
 666 Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
 667   match il with
 668   | INil   => nil
 669   | a::::b => a::(ilist_to_list b)
 670   end.
 671
 672 (* a tree indexed by a (Tree (option X)) *)
 673 Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type :=
 674 | INone      :                                ITree I F []
 675 | ILeaf      :  forall       i:     I, F i -> ITree I F [i]
 676 | IBranch    :  forall it1 it2:Tree ??I, ITree I F it1 -> ITree I F it2 -> ITree I F (it1,,it2).
 677 Implicit Arguments INil    [ I F ].
 678 Implicit Arguments ILeaf   [ I F ].
 679 Implicit Arguments IBranch [ I F ].
 680
 681 Definition itmap {I}{F}{G}{il:Tree ??I}(f:forall i:I, F i -> G i) : ITree I F il -> ITree I G il.
 682   induction il; intros; auto.
 683   destruct a.
 684   apply ILeaf.
 685   apply f.
 686   inversion X; auto.
 687   apply INone.
 688   apply IBranch; inversion X; auto.
 689   Defined.
 690
 691 Fixpoint itree_to_tree {T}{Z}{l:Tree ??T}(il:ITree T (fun _ => Z) l) : Tree ??Z :=
 692   match il with
 693   | INone     => []
 694   | ILeaf _ a => [a]
 695   | IBranch _ _ b1 b2 => (itree_to_tree b1),,(itree_to_tree b2)
 696   end.
 697
 698
 699 (*******************************************************************************)
 700 (* Extensional equality on functions                                           *)
 701
 702 Definition extensionality := fun (t1 t2:Type) => (fun (f:t1->t2) g => forall x:t1, (f x)=(g x)).
 703 Hint Transparent extensionality.
 704 Instance extensionality_Equivalence : forall t1 t2, Equivalence (extensionality t1 t2).
 705   intros; apply Build_Equivalence;
 706     intros; compute; intros; auto.
 707     rewrite H; rewrite H0; auto.
 708   Defined.
 709   Add Parametric Morphism (A B C:Type) : (fun f g => g ○ f)
 710   with signature (extensionality A B ==> extensionality B C ==> extensionality A C) as parametric_morphism_extensionality.
 711   unfold extensionality; intros; rewrite (H x1); rewrite (H0 (y x1)); auto.
 712   Defined.
 713 Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
 714   (extensionality _ _ f f') ->
 715   (extensionality _ _ g g') ->
 716   (extensionality _ _ (g ○ f) (g' ○ f')).
 717   intros.
 718   unfold extensionality.
 719   unfold extensionality in H.
 720   unfold extensionality in H0.
 721   intros.
 722   rewrite H.
 723   rewrite H0.
 724   auto.
 725   Qed.
 726
 727
 728
 729
 730
 731 CoInductive Fresh A T :=
 732 { next  : forall a:A, (T a * Fresh A T)
 733 ; split : Fresh A T * Fresh A T
 734 }.
 735
 736
 737
 738
 739
 740 Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
 741
 742
 743 (* string stuff *)
 744 Variable eol : string.
 745 Extract Constant eol  => "'\n':[]".
 746
 747 Class Monad {T:Type->Type} :=
 748 { returnM : forall {a},     a -> T a
 749 ; bindM   : forall {a}{b},  T a -> (a -> T b) -> T b
 750 }.
 751 Implicit Arguments Monad [ ].
 752 Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).
 753
 754 (* the Error monad *)
 755 Inductive OrError (T:Type) :=
 756 | Error : forall error_message:string, OrError T
 757 | OK    : T      -> OrError T.
 758 Notation "??? T" := (OrError T) (at level 10).
 759 Implicit Arguments Error [T].
 760 Implicit Arguments OK [T].
 761
 762 Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
 763   match oe with
 764     | Error s => Error s
 765     | OK    t => f t
 766   end.
 767 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
 768
 769 Open Scope string_scope.
 770 Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg :=
 771   match oe with
 772     | Error s => Error (err_msg +++ eol +++ "  " +++ s)
 773     | OK    t => f t
 774   end.
 775
 776 Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
 777
 778 Definition addErrorMessage s {T} (x:OrError T) :=
 779   x >>=[ s ] (fun y => OK y).
 780
 781 Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
 782 | Indexed_Error : forall error_message:string, Indexed f (Error error_message)
 783 | Indexed_OK    : forall t, f t -> Indexed f (OK t)
 784 .
 785
 786
 787 Require Import Coq.Arith.EqNat.
 788 Instance EqDecidableNat : EqDecidable nat.
 789   apply Build_EqDecidable.
 790   intros.
 791   apply eq_nat_dec.
 792   Defined.
 793
 794 (* for a type with decidable equality, we can maintain lists of distinct elements *)
 795 Section DistinctList.
 796   Context `{V:EqDecidable}.
 797
 798   Fixpoint addToDistinctList (cv:V)(cvl:list V) :=
 799   match cvl with
 800   | nil       => cv::nil
 801   | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl')
 802   end.
 803
 804   Fixpoint removeFromDistinctList (cv:V)(cvl:list V) :=
 805   match cvl with
 806   | nil => nil
 807   | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl')
 808   end.
 809
 810   Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) :=
 811   match cvrem with
 812   | nil         => cvl
 813   | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl)
 814   end.
 815
 816   Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) :=
 817   match cvl1 with
 818   | nil       => cvl2
 819   | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
 820   end.
 821 End DistinctList.
 822
 823 Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(vec T n).
 824   set (list2vec l) as v.
 825   destruct (eqd_dec (length l) n).
 826     rewrite e in v; apply OK; apply v.
 827     apply (Error (error_message (length l) n)).
 828     Defined.
 829
 830 (* Uniques *)
 831 Variable UniqSupply      : Type.                   Extract Inlined Constant UniqSupply     => "UniqSupply.UniqSupply".
 832 Variable Unique          : Type.                   Extract Inlined Constant Unique         => "Unique.Unique".
 833 Variable uniqFromSupply  : UniqSupply -> Unique.   Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply".
 834 Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply.
 835     Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply".
 836 Variable unique_eq       : forall u1 u2:Unique, sumbool (u1=u2) (u1≠u2).
 837     Extract Inlined Constant unique_eq => "(==)".
 838 Variable unique_toString : Unique -> string.
 839     Extract Inlined Constant unique_toString => "show".
 840 Instance EqDecidableUnique : EqDecidable Unique :=
 841   { eqd_dec := unique_eq }.
 842 Instance EqDecidableToString : ToString Unique :=
 843   { toString := unique_toString }.
 844
 845 Inductive UniqM {T:Type} : Type :=
 846  | uniqM    : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
 847  Implicit Arguments UniqM [ ].
 848
 849 Instance UniqMonad : Monad UniqM :=
 850 { returnM := fun T (x:T) => uniqM (fun u => OK (u,x))
 851 ; bindM   := fun a b (x:UniqM a) (f:a->UniqM b) =>
 852   uniqM (fun u =>
 853     match x with
 854       | uniqM fa =>
 855         match fa u with
 856           | Error s   => Error s
 857           | OK (u',va) => match f va with
 858                            | uniqM fb => fb u'
 859                          end
 860         end
 861     end)
 862 }.
 863
 864 Definition getU : UniqM Unique :=
 865   uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
 866
 867 Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity).
 868 Notation "'return' x" := (returnM x) (at level 100).
 869 Notation "'failM'  x" := (uniqM (fun _ => Error x)) (at level 100).
 870
 871
 872
 873
 874
 875
 876 Record FreshMonad {T:Type} :=
 877 { FMT       :  Type -> Type
 878 ; FMT_Monad :> Monad FMT
 879 ; FMT_fresh :  forall tl:list T, FMT { t:T & @In _ t tl -> False }
 880 }.
 881 Implicit Arguments FreshMonad [ ].
 882 Coercion FMT       : FreshMonad >-> Funclass.
 883
 884
 885
 886 Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
 887
 888
 889
 890
 891 Ltac eqd_dec_refl X :=
 892   destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
 893     [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].
 894
 895 Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 -> t1 = t2.
 896   intros T.
 897   induction t1; intros.
 898   destruct t2.
 899   auto.
 900   inversion H.
 901   destruct t2.
 902   inversion H.
 903   simpl in H.
 904   inversion H.
 905   set (IHt1 _ H2) as q.
 906   rewrite q.
 907   reflexivity.
 908   Qed.
 909
 910 Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
 911   admit.
 912   Defined.
 913
 914 Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
 915   admit.
 916   Defined.