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