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