src/General.v-

   1 (******************************************************************************)
   2 (* 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
  17 Class EqDecidable (T:Type) :=
  18 { eqd_type           := T
  19 ; eqd_dec            :  forall v1 v2:T, sumbool (v1=v2) (not (v1=v2))
  20 ; eqd_dec_reflexive  :  forall v, (eqd_dec v v) = (left _ (refl_equal _))
  21 }.
  22 Coercion eqd_type : EqDecidable >-> Sortclass.
  23
  24
  25 (*******************************************************************************)
  26 (* Trees                                                                       *)
  27
  28 Inductive Tree (a:Type) : Type :=
  29   | T_Leaf   : a -> Tree a
  30   | T_Branch : Tree a -> Tree a -> Tree a.
  31 Implicit Arguments T_Leaf   [ a ].
  32 Implicit Arguments T_Branch [ a ].
  33
  34 Notation "a ,, b"   := (@T_Branch _ a b)                        : tree_scope.
  35
  36 (* tree-of-option-of-X comes up a lot, so we give it special notations *)
  37 Notation "[ q ]"    := (@T_Leaf (option _) (Some q))            : tree_scope.
  38 Notation "[ ]"      := (@T_Leaf (option _) None)                : tree_scope.
  39 Notation "[]"       := (@T_Leaf (option _) None)                : tree_scope.
  40
  41 Open Scope tree_scope.
  42
  43 Fixpoint mapTree {a b:Type}(f:a->b)(t:@Tree a) : @Tree b :=
  44   match t with
  45     | T_Leaf x     => T_Leaf (f x)
  46     | T_Branch l r => T_Branch (mapTree f l) (mapTree f r)
  47   end.
  48 Fixpoint mapOptionTree {a b:Type}(f:a->b)(t:@Tree ??a) : @Tree ??b :=
  49   match t with
  50     | T_Leaf None     => T_Leaf None
  51     | T_Leaf (Some x) => T_Leaf (Some (f x))
  52     | T_Branch l r => T_Branch (mapOptionTree f l) (mapOptionTree f r)
  53   end.
  54 Fixpoint mapTreeAndFlatten {a b:Type}(f:a->@Tree b)(t:@Tree a) : @Tree b :=
  55   match t with
  56     | T_Leaf x        => f x
  57     | T_Branch l r    => T_Branch (mapTreeAndFlatten f l) (mapTreeAndFlatten f r)
  58   end.
  59 Fixpoint mapOptionTreeAndFlatten {a b:Type}(f:a->@Tree ??b)(t:@Tree ??a) : @Tree ??b :=
  60   match t with
  61     | T_Leaf None     => []
  62     | T_Leaf (Some x) => f x
  63     | T_Branch l r    => T_Branch (mapOptionTreeAndFlatten f l) (mapOptionTreeAndFlatten f r)
  64   end.
  65 Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tree T) :=
  66   match t with
  67   | T_Leaf x => mapLeaf x
  68   | T_Branch y z => mergeBranches (treeReduce mapLeaf mergeBranches y) (treeReduce mapLeaf mergeBranches z)
  69   end.
  70 Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
  71   forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.
  72
  73 Lemma tree_dec_eq :
  74    forall {Q}(t1 t2:Tree ??Q),
  75      (forall q1 q2:Q, sumbool (q1=q2) (not (q1=q2))) ->
  76      sumbool (t1=t2) (not (t1=t2)).
  77   intro Q.
  78   intro t1.
  79   induction t1; intros.
  80
  81   destruct a; destruct t2.
  82   destruct o.
  83   set (X q q0) as X'.
  84   inversion X'; subst.
  85   left; auto.
  86   right; unfold not; intro; apply H. inversion H0; subst. auto.
  87   right. unfold not; intro; inversion H.
  88   right. unfold not; intro; inversion H.
  89   destruct o.
  90   right. unfold not; intro; inversion H.
  91   left; auto.
  92   right. unfold not; intro; inversion H.
  93
  94   destruct t2.
  95   right. unfold not; intro; inversion H.
  96   set (IHt1_1 t2_1 X) as X1.
  97   set (IHt1_2 t2_2 X) as X2.
  98   destruct X1; destruct X2; subst.
  99   left; auto.
 100
 101   right.
 102   unfold not; intro H.
 103   apply n.
 104   inversion H; auto.
 105
 106   right.
 107   unfold not; intro H.
 108   apply n.
 109   inversion H; auto.
 110
 111   right.
 112   unfold not; intro H.
 113   apply n.
 114   inversion H; auto.
 115   Defined.
 116
 117
 118
 119
 120 (*******************************************************************************)
 121 (* Lists                                                                       *)
 122
 123 Notation "a :: b"         := (cons a b)                               : list_scope.
 124 Open Scope list_scope.
 125 Fixpoint leaves {a:Type}(t:Tree (option a)) : list a :=
 126   match t with
 127     | (T_Leaf l)     => match l with
 128                           | None   => nil
 129                           | Some x => x::nil
 130                         end
 131     | (T_Branch l r) => app (leaves l) (leaves r)
 132   end.
 133 (* weak inverse of "leaves" *)
 134 Fixpoint unleaves {A:Type}(l:list A) : Tree (option A) :=
 135   match l with
 136     | nil    => []
 137     | (a::b) => [a],,(unleaves b)
 138   end.
 139
 140 (* a map over a list and the conjunction of the results *)
 141 Fixpoint mapProp {A:Type} (f:A->Prop) (l:list A) : Prop :=
 142   match l with
 143     | nil => True
 144     | (a::al) => f a /\ mapProp f al
 145   end.
 146
 147 Lemma map_id : forall A (l:list A), (map (fun x:A => x) l) = l.
 148   induction l.
 149   auto.
 150   simpl.
 151   rewrite IHl.
 152   auto.
 153   Defined.
 154 Lemma map_app : forall `(f:A->B) l l', map f (app l l') = app (map f l) (map f l').
 155   intros.
 156   induction l; auto.
 157   simpl.
 158   rewrite IHl.
 159   auto.
 160   Defined.
 161 Lemma map_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
 162   (map (g ○ f) l) = (map g (map f l)).
 163   intros.
 164   induction l.
 165   simpl; auto.
 166   simpl.
 167   rewrite IHl.
 168   auto.
 169   Defined.
 170 Lemma list_cannot_be_longer_than_itself : forall `(a:A)(b:list A), b = (a::b) -> False.
 171   intros.
 172   induction b.
 173   inversion H.
 174   inversion H. apply IHb in H2.
 175   auto.
 176   Defined.
 177 Lemma list_cannot_be_longer_than_itself' : forall A (b:list A) (a c:A), b = (a::c::b) -> False.
 178   induction b.
 179   intros; inversion H.
 180   intros.
 181   inversion H.
 182   apply IHb in H2.
 183   auto.
 184   Defined.
 185
 186 Lemma mapOptionTree_on_nil : forall `(f:A->B) h, [] = mapOptionTree f h -> h=[].
 187   intros.
 188   destruct h.
 189   destruct o. inversion H.
 190   auto.
 191   inversion H.
 192   Defined.
 193
 194 Lemma mapOptionTree_comp a b c (f:a->b) (g:b->c) q : (mapOptionTree g (mapOptionTree f q)) = mapOptionTree (g ○ f) q.
 195   induction q.
 196     destruct a0; simpl.
 197     reflexivity.
 198     reflexivity.
 199     simpl.
 200     rewrite IHq1.
 201     rewrite IHq2.
 202     reflexivity.
 203   Qed.
 204
 205 (* handy facts: map preserves the length of a list *)
 206 Lemma map_on_nil : forall A B (s1:list A) (f:A->B), nil = map f s1 -> s1=nil.
 207   intros.
 208   induction s1.
 209   auto.
 210   assert False.
 211   simpl in H.
 212   inversion H.
 213   inversion H0.
 214   Defined.
 215 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 }.
 216   induction s1.
 217   intros.
 218   simpl in H; assert False. inversion H. inversion H0.
 219   clear IHs1.
 220   intros.
 221   exists a.
 222   simpl in H.
 223   assert (s1=nil).
 224     inversion H. apply map_on_nil in H2. auto.
 225   subst.
 226   auto.
 227   assert (s1=nil).
 228     inversion H. apply map_on_nil in H2. auto.
 229   subst.
 230   simpl in H.
 231   inversion H. auto.
 232   Defined.
 233
 234 Lemma map_on_doubleton : forall A B (f:A->B) x y (s1:list A), ((x::y::nil) = map f s1) ->
 235   { z : A*A & s1=((fst z)::(snd z)::nil) & (f (fst z))=x /\ (f (snd z))=y }.
 236   intros.
 237   destruct s1.
 238   inversion H.
 239   destruct s1.
 240   inversion H.
 241   destruct s1.
 242   inversion H.
 243   exists (a,a0); auto.
 244   simpl in H.
 245   inversion H.
 246   Defined.
 247
 248
 249 Lemma mapTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree A),
 250   (mapTree (g ○ f) l) = (mapTree g (mapTree f l)).
 251   induction l.
 252     reflexivity.
 253     simpl.
 254     rewrite IHl1.
 255     rewrite IHl2.
 256     reflexivity.
 257     Defined.
 258
 259 Lemma lmap_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
 260   (map (g ○ f) l) = (map g (map f l)).
 261   intros.
 262   induction l.
 263   simpl; auto.
 264   simpl.
 265   rewrite IHl.
 266   auto.
 267   Defined.
 268
 269 (* sends a::b::c::nil to [[[[],,c],,b],,a] *)
 270 Fixpoint unleaves' {A:Type}(l:list A) : Tree (option A) :=
 271   match l with
 272     | nil    => []
 273     | (a::b) => (unleaves' b),,[a]
 274   end.
 275
 276 (* sends a::b::c::nil to [[[[],,c],,b],,a] *)
 277 Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A :=
 278   match l with
 279     | nil    => []
 280     | (a::b) => (unleaves'' b),,(T_Leaf a)
 281   end.
 282
 283 Fixpoint filter {T:Type}(l:list ??T) : list T :=
 284   match l with
 285     | nil => nil
 286     | (None::b) => filter b
 287     | ((Some x)::b) => x::(filter b)
 288   end.
 289
 290 Inductive distinct {T:Type} : list T -> Prop :=
 291 | distinct_nil  : distinct nil
 292 | distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax).
 293
 294 Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
 295   induction l; auto.
 296   simpl.
 297   omega.
 298   Qed.
 299
 300 (* decidable quality on a list of elements which have decidable equality *)
 301 Definition list_eq_dec : forall {T:Type}(l1 l2:list T)(dec:forall t1 t2:T, sumbool (eq t1 t2) (not (eq t1 t2))),
 302   sumbool (eq l1 l2) (not (eq l1 l2)).
 303   intro T.
 304   intro l1.
 305   induction l1; intros.
 306     destruct l2.
 307     left; reflexivity.
 308     right; intro H; inversion H.
 309   destruct l2 as [| b l2].
 310     right; intro H; inversion H.
 311   set (IHl1 l2 dec) as eqx.
 312     destruct eqx.
 313     subst.
 314     set (dec a b) as eqy.
 315     destruct eqy.
 316       subst.
 317       left; reflexivity.
 318       right. intro. inversion H. subst. apply n. auto.
 319     right.
 320       intro.
 321       inversion H.
 322       apply n.
 323       auto.
 324       Defined.
 325
 326
 327
 328
 329 (*******************************************************************************)
 330 (* Length-Indexed Lists                                                        *)
 331
 332 Inductive vec (A:Type) : nat -> Type :=
 333 | vec_nil  : vec A 0
 334 | vec_cons : forall n, A -> vec A n -> vec A (S n).
 335
 336 Fixpoint vec2list {n:nat}{t:Type}(v:vec t n) : list t :=
 337   match v with
 338     | vec_nil => nil
 339     | vec_cons n a va => a::(vec2list va)
 340   end.
 341
 342 Require Import Omega.
 343 Definition vec_get : forall {T:Type}{l:nat}(v:vec T l)(n:nat)(pf:lt n l), T.
 344   intro T.
 345   intro len.
 346   intro v.
 347   induction v; intros.
 348     assert False.
 349     inversion pf.
 350     inversion H.
 351   rename n into len.
 352     destruct n0 as [|n].
 353     exact a.
 354     apply (IHv n).
 355     omega.
 356     Defined.
 357
 358 Definition vec_zip {n:nat}{A B:Type}(va:vec A n)(vb:vec B n) : vec (A*B) n.
 359   induction n.
 360   apply vec_nil.
 361   inversion va; subst.
 362   inversion vb; subst.
 363   apply vec_cons; auto.
 364   Defined.
 365
 366 Definition vec_map {n:nat}{A B:Type}(f:A->B)(v:vec A n) : vec B n.
 367   induction n.
 368   apply vec_nil.
 369   inversion v; subst.
 370   apply vec_cons; auto.
 371   Defined.
 372
 373 Fixpoint vec_In {A:Type} {n:nat} (a:A) (l:vec A n) : Prop :=
 374   match l with
 375     | vec_nil         => False
 376     | vec_cons _ n m  => (n = a) \/ vec_In a m
 377   end.
 378 Implicit Arguments vec_nil  [ A   ].
 379 Implicit Arguments vec_cons [ A n ].
 380
 381 Definition append_vec {n:nat}{T:Type}(v:vec T n)(t:T) : vec T (S n).
 382   induction n.
 383   apply (vec_cons t vec_nil).
 384   apply vec_cons; auto.
 385   Defined.
 386
 387 Definition list2vec {T:Type}(l:list T) : vec T (length l).
 388   induction l.
 389   apply vec_nil.
 390   apply vec_cons; auto.
 391   Defined.
 392
 393 Definition vec_head {n:nat}{T}(v:vec T (S n)) : T.
 394   inversion v;  auto.
 395   Defined.
 396 Definition vec_tail {n:nat}{T}(v:vec T (S n)) : vec T n.
 397   inversion v;  auto.
 398   Defined.
 399
 400 Lemma vec_chop {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l1).
 401   induction l1.
 402   apply vec_nil.
 403   apply vec_cons.
 404   simpl in *.
 405   inversion v; subst; auto.
 406   apply IHl1.
 407   inversion v; subst; auto.
 408   Defined.
 409
 410 Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l2).
 411   induction l1.
 412   apply v.
 413   simpl in *.
 414   apply IHl1; clear IHl1.
 415   inversion v; subst; auto.
 416   Defined.
 417
 418 Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20).
 419
 420
 421
 422 (*******************************************************************************)
 423 (* Shaped Trees                                                                *)
 424
 425 (* a ShapedTree is a tree indexed by the shape (but not the leaf values) of another tree; isomorphic to (ITree (fun _ => Q)) *)
 426 Inductive ShapedTree {T:Type}(Q:Type) : Tree ??T -> Type :=
 427 | st_nil    : @ShapedTree T Q []
 428 | st_leaf   : forall {t}, Q -> @ShapedTree T Q [t]
 429 | st_branch : forall {t1}{t2}, @ShapedTree T Q t1 -> @ShapedTree T Q t2 -> @ShapedTree T Q (t1,,t2).
 430
 431 Fixpoint unshape {T:Type}{Q:Type}{idx:Tree ??T}(st:@ShapedTree T Q idx) : Tree ??Q :=
 432 match st with
 433 | st_nil => []
 434 | st_leaf _ q => [q]
 435 | st_branch _ _ b1 b2 => (unshape b1),,(unshape b2)
 436 end.
 437
 438 Definition mapShapedTree {T}{idx:Tree ??T}{V}{Q}(f:V->Q)(st:ShapedTree V idx) : ShapedTree Q idx.
 439   induction st.
 440   apply st_nil.
 441   apply st_leaf. apply f. apply q.
 442   apply st_branch; auto.
 443   Defined.
 444
 445 Definition zip_shapedTrees {T:Type}{Q1 Q2:Type}{idx:Tree ??T}
 446    (st1:ShapedTree Q1 idx)(st2:ShapedTree Q2 idx) : ShapedTree (Q1*Q2) idx.
 447   induction idx.
 448     destruct a.
 449     apply st_leaf; auto.
 450     inversion st1.
 451     inversion st2.
 452     auto.
 453     apply st_nil.
 454     apply st_branch; auto.
 455     inversion st1; subst; apply IHidx1; auto.
 456     inversion st2; subst; auto.
 457     inversion st2; subst; apply IHidx2; auto.
 458     inversion st1; subst; auto.
 459   Defined.
 460
 461 Definition build_shapedTree {T:Type}(idx:Tree ??T){Q:Type}(f:T->Q) : ShapedTree Q idx.
 462   induction idx.
 463   destruct a.
 464   apply st_leaf; auto.
 465   apply st_nil.
 466   apply st_branch; auto.
 467   Defined.
 468
 469 Lemma unshape_map : forall {Q}{b}(f:Q->b){T}{idx:Tree ??T}(t:ShapedTree Q idx),
 470    mapOptionTree f (unshape t) = unshape (mapShapedTree f t).
 471   intros.
 472   induction t; auto.
 473   simpl.
 474   rewrite IHt1.
 475   rewrite IHt2.
 476   reflexivity.
 477   Qed.
 478
 479
 480
 481
 482 (*******************************************************************************)
 483 (* Type-Indexed Lists                                                          *)
 484
 485 (* an indexed list *)
 486 Inductive IList (I:Type)(F:I->Type) : list I -> Type :=
 487 | INil      :                                       IList I F nil
 488 | ICons     :   forall i is, F i -> IList I F is -> IList I F (i::is).
 489 Implicit Arguments INil [ I F ].
 490 Implicit Arguments ICons [ I F ].
 491
 492 (* a tree indexed by a (Tree (option X)) *)
 493 Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type :=
 494 | INone      :                                ITree I F []
 495 | ILeaf      :  forall       i:     I, F i -> ITree I F [i]
 496 | IBranch    :  forall it1 it2:Tree ??I, ITree I F it1 -> ITree I F it2 -> ITree I F (it1,,it2).
 497 Implicit Arguments INil    [ I F ].
 498 Implicit Arguments ILeaf   [ I F ].
 499 Implicit Arguments IBranch [ I F ].
 500
 501
 502
 503
 504 (*******************************************************************************)
 505 (* Extensional equality on functions                                           *)
 506
 507 Definition extensionality := fun (t1 t2:Type) => (fun (f:t1->t2) g => forall x:t1, (f x)=(g x)).
 508 Hint Transparent extensionality.
 509 Instance extensionality_Equivalence : forall t1 t2, Equivalence (extensionality t1 t2).
 510   intros; apply Build_Equivalence;
 511     intros; compute; intros; auto.
 512     rewrite H; rewrite H0; auto.
 513   Defined.
 514   Add Parametric Morphism (A B C:Type) : (fun f g => g ○ f)
 515   with signature (extensionality A B ==> extensionality B C ==> extensionality A C) as parametric_morphism_extensionality.
 516   unfold extensionality; intros; rewrite (H x1); rewrite (H0 (y x1)); auto.
 517   Defined.
 518 Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
 519   (extensionality _ _ f f') ->
 520   (extensionality _ _ g g') ->
 521   (extensionality _ _ (g ○ f) (g' ○ f')).
 522   intros.
 523   unfold extensionality.
 524   unfold extensionality in H.
 525   unfold extensionality in H0.
 526   intros.
 527   rewrite H.
 528   rewrite H0.
 529   auto.
 530   Qed.
 531
 532
 533
 534
 535
 536
 537 (* the Error monad *)
 538 Inductive OrError (T:Type) :=
 539 | Error : forall error_message:string, OrError T
 540 | OK    : T      -> OrError T.
 541 Notation "??? T" := (OrError T) (at level 10).
 542 Implicit Arguments Error [T].
 543 Implicit Arguments OK [T].
 544
 545 Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
 546   match oe with
 547     | Error s => Error s
 548     | OK    t => f t
 549   end.
 550 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
 551
 552 Fixpoint list2vecOrError {T}(l:list T)(n:nat) : ???(vec T n) :=
 553   match n as N return ???(vec _ N) with
 554     | O => match l with
 555              | nil => OK vec_nil
 556              | _   => Error "list2vecOrError: list was too long"
 557            end
 558     | S n' => match l with
 559                 | nil   => Error "list2vecOrError: list was too short"
 560                 | t::l' => list2vecOrError l' n' >>= fun l'' => OK (vec_cons t l'')
 561               end
 562   end.
 563
 564 Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
 565 | Indexed_Error : forall error_message:string, Indexed f (Error error_message)
 566 | Indexed_OK    : forall t, f t -> Indexed f (OK t)
 567 .
 568 Ltac xauto := try apply Indexed_Error; try apply Indexed_OK.
 569
 570
 571
 572
 573
 574
 575 (* for a type with decidable equality, we can maintain lists of distinct elements *)
 576 Section DistinctList.
 577   Context `{V:EqDecidable}.
 578
 579   Fixpoint addToDistinctList (cv:V)(cvl:list V) :=
 580   match cvl with
 581   | nil       => cv::nil
 582   | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl')
 583   end.
 584
 585   Fixpoint removeFromDistinctList (cv:V)(cvl:list V) :=
 586   match cvl with
 587   | nil => nil
 588   | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl')
 589   end.
 590
 591   Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) :=
 592   match cvrem with
 593   | nil         => cvl
 594   | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl)
 595   end.
 596
 597   Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) :=
 598   match cvl1 with
 599   | nil       => cvl2
 600   | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
 601   end.
 602 End DistinctList.