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