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 Fixpoint listToString {T:Type}{tst:ToString T}(l:list T) : string :=
 473   match l with
 474     | nil  => "nil"
 475     | a::b => (toString a) +++ "::" +++ listToString b
 476   end.
 477
 478 Instance ListToString {T:Type}{tst:ToString T} : ToString (list T) :=
 479   { toString := @listToString _ _ }.
 480
 481
 482 (*******************************************************************************)
 483 (* Tree Flags                                                                  *)
 484
 485 (* TreeFlags is effectively a tree of booleans whose shape matches that of another tree *)
 486 Inductive TreeFlags {T:Type} : Tree T -> Type :=
 487 | tf_leaf_true  : forall x, TreeFlags (T_Leaf x)
 488 | tf_leaf_false : forall x, TreeFlags (T_Leaf x)
 489 | tf_branch     : forall b1 b2, TreeFlags b1 -> TreeFlags b2 -> TreeFlags (b1,,b2).
 490
 491 (* If flags are calculated using a local condition, this will build the flags *)
 492 Fixpoint mkFlags {T}(f:T -> bool)(t:Tree T) : TreeFlags t :=
 493   match t as T return TreeFlags T with
 494     | T_Leaf x => if f x then tf_leaf_true x else tf_leaf_false x
 495     | T_Branch b1 b2 => tf_branch _ _ (mkFlags f b1) (mkFlags f b2)
 496   end.
 497
 498 (* takeT and dropT are not exact inverses! *)
 499
 500 (* drop replaces each leaf where the flag is set with a [] *)
 501 Fixpoint dropT {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
 502   match tf with
 503     | tf_leaf_true  x         => []
 504     | tf_leaf_false x         => Σ
 505     | tf_branch b1 b2 tb1 tb2 => (dropT tb1),,(dropT tb2)
 506   end.
 507
 508 (* takeT returns only those leaves for which the flag is set; all others are omitted entirely from the tree *)
 509 Fixpoint takeT {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) :=
 510   match tf with
 511     | tf_leaf_true  x         => Some Σ
 512     | tf_leaf_false x         => None
 513     | tf_branch b1 b2 tb1 tb2 =>
 514       match takeT tb1 with
 515         | None     => takeT tb2
 516         | Some b1' => match takeT tb2 with
 517                         | None     => Some b1'
 518                         | Some b2' => Some (b1',,b2')
 519                       end
 520       end
 521   end.
 522
 523 (* lift a function T->bool to a function (option T)->bool by yielding (None |-> b) *)
 524 Definition liftBoolFunc {T}(b:bool)(f:T -> bool) : ??T -> bool :=
 525   fun t =>
 526     match t with
 527       | None   => b
 528       | Some x => f x
 529     end.
 530
 531 (* decidable quality on a tree of elements which have decidable equality *)
 532 Definition tree_eq_dec : forall {T:Type}(l1 l2:Tree T)(dec:forall t1 t2:T, sumbool (eq t1 t2) (not (eq t1 t2))),
 533   sumbool (eq l1 l2) (not (eq l1 l2)).
 534   intro T.
 535   intro l1.
 536   induction l1; intros.
 537     destruct l2.
 538     destruct (dec a t).
 539     subst.
 540     left; auto.
 541     right; unfold not; intro; apply n; inversion H; auto.
 542   right.
 543     unfold not; intro.
 544     inversion H.
 545
 546   destruct l2.
 547     right; unfold not; intro; inversion H.
 548     destruct (IHl1_1 l2_1 dec);
 549     destruct (IHl1_2 l2_2 dec); subst.
 550     left; auto.
 551     right.
 552       unfold not; intro.
 553       inversion H; subst.
 554       apply n; auto.
 555     right.
 556       unfold not; intro.
 557       inversion H; subst.
 558       apply n; auto.
 559     right.
 560       unfold not; intro.
 561       inversion H; subst.
 562       apply n; auto.
 563       Defined.
 564
 565 Instance EqDecidableTree {T:Type}(eqd:EqDecidable T) : EqDecidable (Tree T).
 566   apply Build_EqDecidable.
 567   intros.
 568   apply tree_eq_dec.
 569   apply eqd_dec.
 570   Defined.
 571
 572 (*******************************************************************************)
 573 (* Length-Indexed Lists                                                        *)
 574
 575 Inductive vec (A:Type) : nat -> Type :=
 576 | vec_nil  : vec A 0
 577 | vec_cons : forall n, A -> vec A n -> vec A (S n).
 578
 579 Fixpoint vec2list {n:nat}{t:Type}(v:vec t n) : list t :=
 580   match v with
 581     | vec_nil => nil
 582     | vec_cons n a va => a::(vec2list va)
 583   end.
 584
 585 Require Import Omega.
 586 Definition vec_get : forall {T:Type}{l:nat}(v:vec T l)(n:nat)(pf:lt n l), T.
 587   intro T.
 588   intro len.
 589   intro v.
 590   induction v; intros.
 591     assert False.
 592     inversion pf.
 593     inversion H.
 594   rename n into len.
 595     destruct n0 as [|n].
 596     exact a.
 597     apply (IHv n).
 598     omega.
 599     Defined.
 600
 601 Definition vec_zip {n:nat}{A B:Type}(va:vec A n)(vb:vec B n) : vec (A*B) n.
 602   induction n.
 603   apply vec_nil.
 604   inversion va; subst.
 605   inversion vb; subst.
 606   apply vec_cons; auto.
 607   Defined.
 608
 609 Definition vec_map {n:nat}{A B:Type}(f:A->B)(v:vec A n) : vec B n.
 610   induction n.
 611   apply vec_nil.
 612   inversion v; subst.
 613   apply vec_cons; auto.
 614   Defined.
 615
 616 Fixpoint vec_In {A:Type} {n:nat} (a:A) (l:vec A n) : Prop :=
 617   match l with
 618     | vec_nil         => False
 619     | vec_cons _ n m  => (n = a) \/ vec_In a m
 620   end.
 621 Implicit Arguments vec_nil  [ A   ].
 622 Implicit Arguments vec_cons [ A n ].
 623
 624 Definition append_vec {n:nat}{T:Type}(v:vec T n)(t:T) : vec T (S n).
 625   induction n.
 626   apply (vec_cons t vec_nil).
 627   apply vec_cons; auto.
 628   Defined.
 629
 630 Definition list2vec {T:Type}(l:list T) : vec T (length l).
 631   induction l.
 632   apply vec_nil.
 633   apply vec_cons; auto.
 634   Defined.
 635
 636 Definition vec_head {n:nat}{T}(v:vec T (S n)) : T.
 637   inversion v;  auto.
 638   Defined.
 639 Definition vec_tail {n:nat}{T}(v:vec T (S n)) : vec T n.
 640   inversion v;  auto.
 641   Defined.
 642
 643 Lemma vec_chop {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l1).
 644   induction l1.
 645   apply vec_nil.
 646   apply vec_cons.
 647   simpl in *.
 648   inversion v; subst; auto.
 649   apply IHl1.
 650   inversion v; subst; auto.
 651   Defined.
 652
 653 Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l2).
 654   induction l1.
 655   apply v.
 656   simpl in *.
 657   apply IHl1; clear IHl1.
 658   inversion v; subst; auto.
 659   Defined.
 660
 661 Lemma vec2list_len {T}{n}(v:vec T n) : length (vec2list v) = n.
 662   induction v; auto.
 663   simpl.
 664   omega.
 665   Qed.
 666
 667 Lemma vec2list_map_list2vec {A B}{n}(f:A->B)(v:vec A n) : map f (vec2list v) = vec2list (vec_map f v).
 668   induction v; auto.
 669   simpl. rewrite IHv.
 670   reflexivity.
 671   Qed.
 672
 673 Lemma vec2list_list2vec {A}(v:list A) : vec2list (list2vec v) = v.
 674   induction v; auto.
 675   set (vec2list (list2vec (a :: v))) as q.
 676   rewrite <- IHv.
 677   unfold q.
 678   clear q.
 679   simpl.
 680   reflexivity.
 681   Qed.
 682
 683 Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20).
 684
 685
 686
 687 (*******************************************************************************)
 688 (* Shaped Trees                                                                *)
 689
 690 (* a ShapedTree is a tree indexed by the shape (but not the leaf values) of another tree; isomorphic to (ITree (fun _ => Q)) *)
 691 Inductive ShapedTree {T:Type}(Q:Type) : Tree ??T -> Type :=
 692 | st_nil    : @ShapedTree T Q []
 693 | st_leaf   : forall {t}, Q -> @ShapedTree T Q [t]
 694 | st_branch : forall {t1}{t2}, @ShapedTree T Q t1 -> @ShapedTree T Q t2 -> @ShapedTree T Q (t1,,t2).
 695
 696 Fixpoint unshape {T:Type}{Q:Type}{idx:Tree ??T}(st:@ShapedTree T Q idx) : Tree ??Q :=
 697 match st with
 698 | st_nil => []
 699 | st_leaf _ q => [q]
 700 | st_branch _ _ b1 b2 => (unshape b1),,(unshape b2)
 701 end.
 702
 703 Definition mapShapedTree {T}{idx:Tree ??T}{V}{Q}(f:V->Q)(st:ShapedTree V idx) : ShapedTree Q idx.
 704   induction st.
 705   apply st_nil.
 706   apply st_leaf. apply f. apply q.
 707   apply st_branch; auto.
 708   Defined.
 709
 710 Definition zip_shapedTrees {T:Type}{Q1 Q2:Type}{idx:Tree ??T}
 711    (st1:ShapedTree Q1 idx)(st2:ShapedTree Q2 idx) : ShapedTree (Q1*Q2) idx.
 712   induction idx.
 713     destruct a.
 714     apply st_leaf; auto.
 715     inversion st1.
 716     inversion st2.
 717     auto.
 718     apply st_nil.
 719     apply st_branch; auto.
 720     inversion st1; subst; apply IHidx1; auto.
 721     inversion st2; subst; auto.
 722     inversion st2; subst; apply IHidx2; auto.
 723     inversion st1; subst; auto.
 724   Defined.
 725
 726 Definition build_shapedTree {T:Type}(idx:Tree ??T){Q:Type}(f:T->Q) : ShapedTree Q idx.
 727   induction idx.
 728   destruct a.
 729   apply st_leaf; auto.
 730   apply st_nil.
 731   apply st_branch; auto.
 732   Defined.
 733
 734 Lemma unshape_map : forall {Q}{b}(f:Q->b){T}{idx:Tree ??T}(t:ShapedTree Q idx),
 735    mapOptionTree f (unshape t) = unshape (mapShapedTree f t).
 736   intros.
 737   induction t; auto.
 738   simpl.
 739   rewrite IHt1.
 740   rewrite IHt2.
 741   reflexivity.
 742   Qed.
 743
 744
 745
 746
 747 (*******************************************************************************)
 748 (* Type-Indexed Lists                                                          *)
 749
 750 (* an indexed list *)
 751 Inductive IList (I:Type)(F:I->Type) : list I -> Type :=
 752 | INil      :                                       IList I F nil
 753 | ICons     :   forall i is, F i -> IList I F is -> IList I F (i::is).
 754 Implicit Arguments INil [ I F ].
 755 Implicit Arguments ICons [ I F ].
 756
 757 Notation "a :::: b" := (@ICons _ _ _ _ a b) (at level 20).
 758
 759 Definition ilist_head {T}{F}{x}{y} : IList T F (x::y) -> F x.
 760   intro il.
 761   inversion il.
 762   subst.
 763   apply X.
 764   Defined.
 765
 766 Definition ilist_tail {T}{F}{x}{y} : IList T F (x::y) -> IList T F y.
 767   intro il.
 768   inversion il.
 769   subst.
 770   apply X0.
 771   Defined.
 772
 773 Definition ilmap {I}{F}{G}{il:list I}(f:forall i:I, F i -> G i) : IList I F il -> IList I G il.
 774   induction il; intros; auto.
 775   apply INil.
 776   inversion X; subst.
 777   apply ICons; auto.
 778   Defined.
 779
 780 Lemma ilist_chop {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l1.
 781   induction l1; auto.
 782   apply INil.
 783   apply ICons.
 784   inversion v; auto.
 785   apply IHl1.
 786   inversion v; auto.
 787   Defined.
 788
 789 Lemma ilist_chop' {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l2.
 790   induction l1; auto.
 791   apply IHl1.
 792   inversion v; subst; auto.
 793   Defined.
 794
 795 Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
 796   match il with
 797   | INil   => nil
 798   | a::::b => a::(ilist_to_list b)
 799   end.
 800
 801 (* a tree indexed by a (Tree (option X)) *)
 802 Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type :=
 803 | INone      :                                ITree I F []
 804 | ILeaf      :  forall       i:     I, F i -> ITree I F [i]
 805 | IBranch    :  forall it1 it2:Tree ??I, ITree I F it1 -> ITree I F it2 -> ITree I F (it1,,it2).
 806 Implicit Arguments INil    [ I F ].
 807 Implicit Arguments ILeaf   [ I F ].
 808 Implicit Arguments IBranch [ I F ].
 809
 810 Definition itmap {I}{F}{G}{il:Tree ??I}(f:forall i:I, F i -> G i) : ITree I F il -> ITree I G il.
 811   induction il; intros; auto.
 812   destruct a.
 813   apply ILeaf.
 814   apply f.
 815   inversion X; auto.
 816   apply INone.
 817   apply IBranch; inversion X; auto.
 818   Defined.
 819
 820 Fixpoint itree_to_tree {T}{Z}{l:Tree ??T}(il:ITree T (fun _ => Z) l) : Tree ??Z :=
 821   match il with
 822   | INone     => []
 823   | ILeaf _ a => [a]
 824   | IBranch _ _ b1 b2 => (itree_to_tree b1),,(itree_to_tree b2)
 825   end.
 826
 827
 828 (*******************************************************************************)
 829 (* Extensional equality on functions                                           *)
 830
 831 Definition extensionality := fun (t1 t2:Type) => (fun (f:t1->t2) g => forall x:t1, (f x)=(g x)).
 832 Hint Transparent extensionality.
 833 Instance extensionality_Equivalence : forall t1 t2, Equivalence (extensionality t1 t2).
 834   intros; apply Build_Equivalence;
 835     intros; compute; intros; auto.
 836     rewrite H; rewrite H0; auto.
 837   Defined.
 838   Add Parametric Morphism (A B C:Type) : (fun f g => g ○ f)
 839   with signature (extensionality A B ==> extensionality B C ==> extensionality A C) as parametric_morphism_extensionality.
 840   unfold extensionality; intros; rewrite (H x1); rewrite (H0 (y x1)); auto.
 841   Defined.
 842 Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
 843   (extensionality _ _ f f') ->
 844   (extensionality _ _ g g') ->
 845   (extensionality _ _ (g ○ f) (g' ○ f')).
 846   intros.
 847   unfold extensionality.
 848   unfold extensionality in H.
 849   unfold extensionality in H0.
 850   intros.
 851   rewrite H.
 852   rewrite H0.
 853   auto.
 854   Qed.
 855
 856
 857
 858
 859
 860
 861
 862
 863
 864
 865 Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
 866
 867 (* boolean "not" *)
 868 Definition bnot (b:bool) : bool := if b then false else true.
 869 Definition band (b1 b2:bool) : bool := if b1 then b2 else false.
 870 Definition bor  (b1 b2:bool) : bool := if b1 then true else b2.
 871
 872 (* string stuff *)
 873 Variable eol : string.
 874 Extract Constant eol  => "'\n':[]".
 875
 876 Class Monad {T:Type->Type} :=
 877 { returnM : forall {a},     a -> T a
 878 ; bindM   : forall {a}{b},  T a -> (a -> T b) -> T b
 879 }.
 880 Implicit Arguments Monad [ ].
 881 Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).
 882
 883 (* the Error monad *)
 884 Inductive OrError (T:Type) :=
 885 | Error : forall error_message:string, OrError T
 886 | OK    : T      -> OrError T.
 887 Notation "??? T" := (OrError T) (at level 10).
 888 Implicit Arguments Error [T].
 889 Implicit Arguments OK [T].
 890
 891 Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
 892   match oe with
 893     | Error s => Error s
 894     | OK    t => f t
 895   end.
 896 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
 897
 898 Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg :=
 899   match oe with
 900     | Error s => Error (err_msg +++ eol +++ "  " +++ s)
 901     | OK    t => f t
 902   end.
 903
 904 Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
 905
 906 Definition addErrorMessage s {T} (x:OrError T) :=
 907   x >>=[ s ] (fun y => OK y).
 908
 909 Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
 910 | Indexed_Error : forall error_message:string, Indexed f (Error error_message)
 911 | Indexed_OK    : forall t, f t -> Indexed f (OK t)
 912 .
 913
 914
 915 Require Import Coq.Arith.EqNat.
 916 Instance EqDecidableNat : EqDecidable nat.
 917   apply Build_EqDecidable.
 918   intros.
 919   apply eq_nat_dec.
 920   Defined.
 921
 922 (* for a type with decidable equality, we can maintain lists of distinct elements *)
 923 Section DistinctList.
 924   Context `{V:EqDecidable}.
 925
 926   Fixpoint addToDistinctList (cv:V)(cvl:list V) :=
 927   match cvl with
 928   | nil       => cv::nil
 929   | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl')
 930   end.
 931
 932   Fixpoint removeFromDistinctList (cv:V)(cvl:list V) :=
 933   match cvl with
 934   | nil => nil
 935   | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl')
 936   end.
 937
 938   Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) :=
 939   match cvrem with
 940   | nil         => cvl
 941   | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl)
 942   end.
 943
 944   Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) :=
 945   match cvl1 with
 946   | nil       => cvl2
 947   | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
 948   end.
 949 End DistinctList.
 950
 951 Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(vec T n).
 952   set (list2vec l) as v.
 953   destruct (eqd_dec (length l) n).
 954     rewrite e in v; apply OK; apply v.
 955     apply (Error (error_message (length l) n)).
 956     Defined.
 957
 958 (* this makes a type function application, ensuring not to oversaturate it (though if it was undersaturated we can't fix that) *)
 959 Fixpoint split_list {T}(l:list T)(n:nat) : ???(list T * list T) :=
 960   match n with
 961     | O    => OK (nil , l)
 962     | S n' => match l with
 963                 | nil  => Error "take_list failed"
 964                 | h::t => split_list t n' >>= fun t' => let (t1,t2) := t' in OK ((h::t1),t2)
 965               end
 966     end.
 967
 968 (* Uniques *)
 969 Variable UniqSupply      : Type.                   Extract Inlined Constant UniqSupply     => "UniqSupply.UniqSupply".
 970 Variable Unique          : Type.                   Extract Inlined Constant Unique         => "Unique.Unique".
 971 Variable uniqFromSupply  : UniqSupply -> Unique.   Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply".
 972 Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply.
 973     Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply".
 974 Variable unique_eq       : forall u1 u2:Unique, sumbool (u1=u2) (u1≠u2).
 975     Extract Inlined Constant unique_eq => "(==)".
 976 Variable unique_toString : Unique -> string.
 977     Extract Inlined Constant unique_toString => "show".
 978 Instance EqDecidableUnique : EqDecidable Unique :=
 979   { eqd_dec := unique_eq }.
 980 Instance EqDecidableToString : ToString Unique :=
 981   { toString := unique_toString }.
 982
 983 Inductive UniqM {T:Type} : Type :=
 984  | uniqM    : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
 985  Implicit Arguments UniqM [ ].
 986
 987 Instance UniqMonad : Monad UniqM :=
 988 { returnM := fun T (x:T) => uniqM (fun u => OK (u,x))
 989 ; bindM   := fun a b (x:UniqM a) (f:a->UniqM b) =>
 990   uniqM (fun u =>
 991     match x with
 992       | uniqM fa =>
 993         match fa u with
 994           | Error s   => Error s
 995           | OK (u',va) => match f va with
 996                            | uniqM fb => fb u'
 997                          end
 998         end
 999     end)
1000 }.
1001
1002 Definition getU : UniqM Unique :=
1003   uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
1004
1005 Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity).
1006 Notation "'return' x" := (returnM x) (at level 100).
1007 Notation "'failM'  x" := (uniqM (fun _ => Error x)) (at level 100).
1008
1009
1010
1011
1012
1013
1014 Record FreshMonad {T:Type} :=
1015 { FMT       :  Type -> Type
1016 ; FMT_Monad :> Monad FMT
1017 ; FMT_fresh :  forall tl:list T, FMT { t:T & @In _ t tl -> False }
1018 }.
1019 Implicit Arguments FreshMonad [ ].
1020 Coercion FMT       : FreshMonad >-> Funclass.
1021
1022
1023
1024 Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
1025
1026
1027
1028
1029 Ltac eqd_dec_refl X :=
1030   destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
1031     [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].
1032
1033 Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 -> t1 = t2.
1034   intros T.
1035   induction t1; intros.
1036   destruct t2.
1037   auto.
1038   inversion H.
1039   destruct t2.
1040   inversion H.
1041   simpl in H.
1042   inversion H.
1043   set (IHt1 _ H2) as q.
1044   rewrite q.
1045   reflexivity.
1046   Qed.
1047
1048 (* adapted from Adam Chlipala's posting to the coq-club list (thanks!) *)
1049 Definition openVec A n (v: vec A (S n)) : exists a, exists v0, v = a:::v0 :=
1050   match v in vec _ N return match N return vec A N -> Prop with
1051                               | O => fun _ => True
1052                               | S n => fun v => exists a, exists v0, v = a:::v0
1053                             end v with
1054     | vec_nil => I
1055     | a:::v0 => ex_intro _ a (ex_intro _ v0 (refl_equal _))
1056   end.
1057
1058 Definition nilVec A (v: vec A O) : v = vec_nil :=
1059   match v in vec _ N return match N return vec A N -> Prop with
1060                               | O   => fun v => v = vec_nil
1061                               | S n => fun v => True
1062                             end v with
1063     | vec_nil => refl_equal _
1064     | a:::v0  => I
1065   end.
1066
1067 Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
1068   intros.
1069   induction n.
1070   set (nilVec _ v1) as v1'.
1071   set (nilVec _ v2) as v2'.
1072   subst.
1073   simpl.
1074   reflexivity.
1075   set (openVec _ _ v1) as v1'.
1076   set (openVec _ _ v2) as v2'.
1077   destruct v1'.
1078   destruct v2'.
1079   destruct H.
1080   destruct H0.
1081   subst.
1082   simpl.
1083   rewrite IHn.
1084   reflexivity.
1085   Qed.
1086
1087 Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
1088   intros.
1089   induction n.
1090   set (nilVec _ v1) as v1'.
1091   set (nilVec _ v2) as v2'.
1092   subst.
1093   simpl.
1094   reflexivity.
1095   set (openVec _ _ v1) as v1'.
1096   set (openVec _ _ v2) as v2'.
1097   destruct v1'.
1098   destruct v2'.
1099   destruct H.
1100   destruct H0.
1101   subst.
1102   simpl.
1103   rewrite IHn.
1104   reflexivity.
1105   Qed.
1106
1107 Fixpoint mapM {M}{mon:Monad M}{T}(ml:list (M T)) : M (list T) :=
1108   match ml with
1109     | nil  => return nil
1110     | a::b => bind a' = a ; bind b' = mapM b ; return a'::b'
1111   end.
1112
1113 Fixpoint list_to_ilist {T}{F}(f:forall t:T, F t) (l:list T) : IList T F l :=
1114   match l as L return IList T F L with
1115   | nil  => INil
1116   | a::b => ICons a b (f a) (list_to_ilist f b)
1117   end.
1118
1119 Fixpoint treeM {T}{M}{MT:Monad M}(t:Tree ??(M T)) : M (Tree ??T) :=
1120   match t with
1121     | T_Leaf None     => return []
1122     | T_Leaf (Some x) => bind x' = x ; return [x']
1123     | T_Branch b1 b2  => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
1124   end.
1125
1126
1127 (* escapifies any characters which might cause trouble for LaTeX *)
1128 Variable sanitizeForLatex    : string      -> string.
1129    Extract Inlined Constant sanitizeForLatex      => "sanitizeForLatex".
1130 Inductive Latex     : Type := rawLatex     : string -> Latex.
1131 Inductive LatexMath : Type := rawLatexMath : string -> LatexMath.
1132
1133 Class ToLatex (T:Type) := { toLatex : T -> Latex }.
1134 Instance ConcatenableLatex : Concatenable Latex :=
1135   { concatenate := fun l1 l2 => match l1 with rawLatex l1' => match l2 with rawLatex l2' => rawLatex (l1'+++l2') end end }.
1136 Instance LatexToString : ToString Latex := { toString := fun x => match x with rawLatex s => s end }.
1137
1138 Class ToLatexMath (T:Type) := { toLatexMath : T -> LatexMath }.
1139 Instance ConcatenableLatexMath : Concatenable LatexMath :=
1140   { concatenate := fun l1 l2 =>
1141     match l1 with rawLatexMath l1' =>
1142       match l2 with rawLatexMath l2' => rawLatexMath (l1'+++l2')
1143       end end }.
1144 Instance LatexMathToString : ToString LatexMath := { toString := fun x => match x with rawLatexMath s => s end }.
1145
1146 Instance ToLatexLatexMath : ToLatex LatexMath := { toLatex     := fun l => rawLatex     ("$"+++toString l+++"$") }.
1147 Instance ToLatexMathLatex : ToLatexMath Latex := { toLatexMath := fun l => rawLatexMath ("\text{"+++toString l+++"}") }.
1148
1149 Instance StringToLatex     : ToLatex string := { toLatex := fun x => rawLatex (sanitizeForLatex x) }.
1150 Instance StringToLatexMath : ToLatexMath  string := { toLatexMath := fun x => toLatexMath (toLatex x) }.
1151 Instance LatexToLatex          : ToLatex     Latex      := { toLatex := fun x => x }.
1152 Instance LatexMathToLatexMath  : ToLatexMath LatexMath  := { toLatexMath := fun x => x }.
1153
1154 Fixpoint treeToLatexMath {V}{ToLatexV:ToLatexMath V}(t:Tree ??V) : LatexMath :=
1155   match t with
1156     | T_Leaf None     => rawLatexMath "\langle\rangle"
1157     | T_Leaf (Some x) => (rawLatexMath "\langle")+++toLatexMath x+++(rawLatexMath "\rangle")
1158     | T_Branch b1 b2  => (rawLatexMath "\langle")+++treeToLatexMath b1+++(rawLatexMath " , ")
1159       +++treeToLatexMath b2+++(rawLatexMath "\rangle")
1160   end.