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