src/General.v

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