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