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