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 Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
 916   match il with
 917   | INil   => nil
 918   | a::::b => a::(ilist_to_list b)
 919   end.
 920
 921 (* a tree indexed by a (Tree (option X)) *)
 922 Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type :=
 923 | INone      :                                ITree I F []
 924 | ILeaf      :  forall       i:     I, F i -> ITree I F [i]
 925 | IBranch    :  forall it1 it2:Tree ??I, ITree I F it1 -> ITree I F it2 -> ITree I F (it1,,it2).
 926 Implicit Arguments INil    [ I F ].
 927 Implicit Arguments ILeaf   [ I F ].
 928 Implicit Arguments IBranch [ I F ].
 929
 930 Definition itmap {I}{F}{G}{il:Tree ??I}(f:forall i:I, F i -> G i) : ITree I F il -> ITree I G il.
 931   induction il; intros; auto.
 932   destruct a.
 933   apply ILeaf.
 934   apply f.
 935   inversion X; auto.
 936   apply INone.
 937   apply IBranch; inversion X; auto.
 938   Defined.
 939
 940 Fixpoint itree_to_tree {T}{Z}{l:Tree ??T}(il:ITree T (fun _ => Z) l) : Tree ??Z :=
 941   match il with
 942   | INone     => []
 943   | ILeaf _ a => [a]
 944   | IBranch _ _ b1 b2 => (itree_to_tree b1),,(itree_to_tree b2)
 945   end.
 946
 947
 948 (*******************************************************************************)
 949 (* Extensional equality on functions                                           *)
 950
 951 Definition extensionality := fun (t1 t2:Type) => (fun (f:t1->t2) g => forall x:t1, (f x)=(g x)).
 952 Hint Transparent extensionality.
 953 Instance extensionality_Equivalence : forall t1 t2, Equivalence (extensionality t1 t2).
 954   intros; apply Build_Equivalence;
 955     intros; compute; intros; auto.
 956     rewrite H; rewrite H0; auto.
 957   Defined.
 958   Add Parametric Morphism (A B C:Type) : (fun f g => g ○ f)
 959   with signature (extensionality A B ==> extensionality B C ==> extensionality A C) as parametric_morphism_extensionality.
 960   unfold extensionality; intros; rewrite (H x1); rewrite (H0 (y x1)); auto.
 961   Defined.
 962 Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
 963   (extensionality _ _ f f') ->
 964   (extensionality _ _ g g') ->
 965   (extensionality _ _ (g ○ f) (g' ○ f')).
 966   intros.
 967   unfold extensionality.
 968   unfold extensionality in H.
 969   unfold extensionality in H0.
 970   intros.
 971   rewrite H.
 972   rewrite H0.
 973   auto.
 974   Qed.
 975
 976
 977
 978
 979
 980
 981
 982
 983
 984
 985 Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
 986
 987 (* boolean "not" *)
 988 Definition bnot (b:bool) : bool := if b then false else true.
 989 Definition band (b1 b2:bool) : bool := if b1 then b2 else false.
 990 Definition bor  (b1 b2:bool) : bool := if b1 then true else b2.
 991
 992 (* string stuff *)
 993 Variable eol : string.
 994 Extract Constant eol  => "'\n':[]".
 995
 996 Class Monad {T:Type->Type} :=
 997 { returnM : forall {a},     a -> T a
 998 ; bindM   : forall {a}{b},  T a -> (a -> T b) -> T b
 999 }.
1000 Implicit Arguments Monad [ ].
1001 Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).
1002
1003 (* the Error monad *)
1004 Inductive OrError (T:Type) :=
1005 | Error : forall error_message:string, OrError T
1006 | OK    : T      -> OrError T.
1007 Notation "??? T" := (OrError T) (at level 10).
1008 Implicit Arguments Error [T].
1009 Implicit Arguments OK [T].
1010
1011 Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
1012   match oe with
1013     | Error s => Error s
1014     | OK    t => f t
1015   end.
1016 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
1017
1018 Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg :=
1019   match oe with
1020     | Error s => Error (err_msg +++ eol +++ "  " +++ s)
1021     | OK    t => f t
1022   end.
1023
1024 Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
1025
1026 Definition addErrorMessage s {T} (x:OrError T) :=
1027   x >>=[ eol +++ eol +++ s ] (fun y => OK y).
1028
1029 Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
1030 | Indexed_Error : forall error_message:string, Indexed f (Error error_message)
1031 | Indexed_OK    : forall t, f t -> Indexed f (OK t)
1032 .
1033
1034
1035 Require Import Coq.Arith.EqNat.
1036 Instance EqDecidableNat : EqDecidable nat.
1037   apply Build_EqDecidable.
1038   intros.
1039   apply eq_nat_dec.
1040   Defined.
1041
1042 (* for a type with decidable equality, we can maintain lists of distinct elements *)
1043 Section DistinctList.
1044   Context `{V:EqDecidable}.
1045
1046   Fixpoint addToDistinctList (cv:V)(cvl:list V) :=
1047   match cvl with
1048   | nil       => cv::nil
1049   | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl')
1050   end.
1051
1052   Fixpoint removeFromDistinctList (cv:V)(cvl:list V) :=
1053   match cvl with
1054   | nil => nil
1055   | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl')
1056   end.
1057
1058   Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) :=
1059   match cvrem with
1060   | nil         => cvl
1061   | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl)
1062   end.
1063
1064   Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) :=
1065   match cvl1 with
1066   | nil       => cvl2
1067   | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
1068   end.
1069 End DistinctList.
1070
1071 Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(vec T n).
1072   set (list2vec l) as v.
1073   destruct (eqd_dec (length l) n).
1074     rewrite e in v; apply OK; apply v.
1075     apply (Error (error_message (length l) n)).
1076     Defined.
1077
1078 (* this makes a type function application, ensuring not to oversaturate it (though if it was undersaturated we can't fix that) *)
1079 Fixpoint split_list {T}(l:list T)(n:nat) : ???(list T * list T) :=
1080   match n with
1081     | O    => OK (nil , l)
1082     | S n' => match l with
1083                 | nil  => Error "take_list failed"
1084                 | h::t => split_list t n' >>= fun t' => let (t1,t2) := t' in OK ((h::t1),t2)
1085               end
1086     end.
1087
1088 (* Uniques *)
1089 Variable UniqSupply      : Type.                   Extract Inlined Constant UniqSupply     => "UniqSupply.UniqSupply".
1090 Variable Unique          : Type.                   Extract Inlined Constant Unique         => "Unique.Unique".
1091 Variable uniqFromSupply  : UniqSupply -> Unique.   Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply".
1092 Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply.
1093     Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply".
1094 Variable unique_eq       : forall u1 u2:Unique, sumbool (u1=u2) (u1≠u2).
1095     Extract Inlined Constant unique_eq => "(==)".
1096 Variable unique_toString : Unique -> string.
1097     Extract Inlined Constant unique_toString => "show".
1098 Instance EqDecidableUnique : EqDecidable Unique :=
1099   { eqd_dec := unique_eq }.
1100 Instance EqDecidableToString : ToString Unique :=
1101   { toString := unique_toString }.
1102
1103 Inductive UniqM {T:Type} : Type :=
1104  | uniqM    : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
1105  Implicit Arguments UniqM [ ].
1106
1107 Instance UniqMonad : Monad UniqM :=
1108 { returnM := fun T (x:T) => uniqM (fun u => OK (u,x))
1109 ; bindM   := fun a b (x:UniqM a) (f:a->UniqM b) =>
1110   uniqM (fun u =>
1111     match x with
1112       | uniqM fa =>
1113         match fa u with
1114           | Error s   => Error s
1115           | OK (u',va) => match f va with
1116                            | uniqM fb => fb u'
1117                          end
1118         end
1119     end)
1120 }.
1121
1122 Definition getU : UniqM Unique :=
1123   uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
1124
1125 Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity).
1126 Notation "'return' x" := (returnM x) (at level 100).
1127 Notation "'failM'  x" := (uniqM (fun _ => Error x)) (at level 100).
1128
1129
1130
1131
1132
1133
1134 Record FreshMonad {T:Type} :=
1135 { FMT       :  Type -> Type
1136 ; FMT_Monad :> Monad FMT
1137 ; FMT_fresh :  forall tl:list T, FMT { t:T & @In _ t tl -> False }
1138 }.
1139 Implicit Arguments FreshMonad [ ].
1140 Coercion FMT       : FreshMonad >-> Funclass.
1141
1142
1143
1144 Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
1145
1146
1147
1148
1149 Ltac eqd_dec_refl X :=
1150   destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
1151     [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].
1152
1153 Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 -> t1 = t2.
1154   intros T.
1155   induction t1; intros.
1156   destruct t2.
1157   auto.
1158   inversion H.
1159   destruct t2.
1160   inversion H.
1161   simpl in H.
1162   inversion H.
1163   set (IHt1 _ H2) as q.
1164   rewrite q.
1165   reflexivity.
1166   Qed.
1167
1168 (* adapted from Adam Chlipala's posting to the coq-club list (thanks!) *)
1169 Definition openVec A n (v: vec A (S n)) : exists a, exists v0, v = a:::v0 :=
1170   match v in vec _ N return match N return vec A N -> Prop with
1171                               | O => fun _ => True
1172                               | S n => fun v => exists a, exists v0, v = a:::v0
1173                             end v with
1174     | vec_nil => I
1175     | a:::v0 => ex_intro _ a (ex_intro _ v0 (refl_equal _))
1176   end.
1177
1178 Definition nilVec A (v: vec A O) : v = vec_nil :=
1179   match v in vec _ N return match N return vec A N -> Prop with
1180                               | O   => fun v => v = vec_nil
1181                               | S n => fun v => True
1182                             end v with
1183     | vec_nil => refl_equal _
1184     | a:::v0  => I
1185   end.
1186
1187 Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
1188   intros.
1189   induction n.
1190   set (nilVec _ v1) as v1'.
1191   set (nilVec _ v2) as v2'.
1192   subst.
1193   simpl.
1194   reflexivity.
1195   set (openVec _ _ v1) as v1'.
1196   set (openVec _ _ v2) as v2'.
1197   destruct v1'.
1198   destruct v2'.
1199   destruct H.
1200   destruct H0.
1201   subst.
1202   simpl.
1203   rewrite IHn.
1204   reflexivity.
1205   Qed.
1206
1207 Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
1208   intros.
1209   induction n.
1210   set (nilVec _ v1) as v1'.
1211   set (nilVec _ v2) as v2'.
1212   subst.
1213   simpl.
1214   reflexivity.
1215   set (openVec _ _ v1) as v1'.
1216   set (openVec _ _ v2) as v2'.
1217   destruct v1'.
1218   destruct v2'.
1219   destruct H.
1220   destruct H0.
1221   subst.
1222   simpl.
1223   rewrite IHn.
1224   reflexivity.
1225   Qed.
1226
1227 Fixpoint mapM {M}{mon:Monad M}{T}(ml:list (M T)) : M (list T) :=
1228   match ml with
1229     | nil  => return nil
1230     | a::b => bind a' = a ; bind b' = mapM b ; return a'::b'
1231   end.
1232
1233 Fixpoint list_to_ilist {T}{F}(f:forall t:T, F t) (l:list T) : IList T F l :=
1234   match l as L return IList T F L with
1235   | nil  => INil
1236   | a::b => ICons a b (f a) (list_to_ilist f b)
1237   end.
1238
1239 Fixpoint treeM {T}{M}{MT:Monad M}(t:Tree ??(M T)) : M (Tree ??T) :=
1240   match t with
1241     | T_Leaf None     => return []
1242     | T_Leaf (Some x) => bind x' = x ; return [x']
1243     | T_Branch b1 b2  => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
1244   end.
1245
1246
1247 (* escapifies any characters which might cause trouble for LaTeX *)
1248 Variable sanitizeForLatex    : string      -> string.
1249    Extract Inlined Constant sanitizeForLatex      => "sanitizeForLatex".
1250 Inductive Latex     : Type := rawLatex     : string -> Latex.
1251 Inductive LatexMath : Type := rawLatexMath : string -> LatexMath.
1252
1253 Class ToLatex (T:Type) := { toLatex : T -> Latex }.
1254 Instance ConcatenableLatex : Concatenable Latex :=
1255   { concatenate := fun l1 l2 => match l1 with rawLatex l1' => match l2 with rawLatex l2' => rawLatex (l1'+++l2') end end }.
1256 Instance LatexToString : ToString Latex := { toString := fun x => match x with rawLatex s => s end }.
1257
1258 Class ToLatexMath (T:Type) := { toLatexMath : T -> LatexMath }.
1259 Instance ConcatenableLatexMath : Concatenable LatexMath :=
1260   { concatenate := fun l1 l2 =>
1261     match l1 with rawLatexMath l1' =>
1262       match l2 with rawLatexMath l2' => rawLatexMath (l1'+++l2')
1263       end end }.
1264 Instance LatexMathToString : ToString LatexMath := { toString := fun x => match x with rawLatexMath s => s end }.
1265
1266 Instance ToLatexLatexMath : ToLatex LatexMath := { toLatex     := fun l => rawLatex     ("$"+++toString l+++"$") }.
1267 Instance ToLatexMathLatex : ToLatexMath Latex := { toLatexMath := fun l => rawLatexMath ("\text{"+++toString l+++"}") }.
1268
1269 Instance StringToLatex     : ToLatex string := { toLatex := fun x => rawLatex (sanitizeForLatex x) }.
1270 Instance StringToLatexMath : ToLatexMath  string := { toLatexMath := fun x => toLatexMath (toLatex x) }.
1271 Instance LatexToLatex          : ToLatex     Latex      := { toLatex := fun x => x }.
1272 Instance LatexMathToLatexMath  : ToLatexMath LatexMath  := { toLatexMath := fun x => x }.
1273
1274 Fixpoint treeToLatexMath {V}{ToLatexV:ToLatexMath V}(t:Tree ??V) : LatexMath :=
1275   match t with
1276     | T_Leaf None     => rawLatexMath "\langle\rangle"
1277     | T_Leaf (Some x) => (rawLatexMath "\langle")+++toLatexMath x+++(rawLatexMath "\rangle")
1278     | T_Branch b1 b2  => (rawLatexMath "\langle")+++treeToLatexMath b1+++(rawLatexMath " , ")
1279       +++treeToLatexMath b2+++(rawLatexMath "\rangle")
1280   end.