1 (*********************************************************************************************************************************)
2 (* General: general data structures *)
3 (*********************************************************************************************************************************)
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.
11 Require Import Coq.Lists.List.
12 Require Import Preamble.
13 Generalizable All Variables.
16 Definition EqDecider T := forall (n1 n2:T), sumbool (n1=n2) (not (n1=n2)).
17 Class EqDecidable (T:Type) :=
19 ; eqd_dec : forall v1 v2:T, sumbool (v1=v2) (not (v1=v2))
21 Coercion eqd_type : EqDecidable >-> Sortclass.
24 Class ToString (T:Type) := { toString : T -> string }.
25 Instance StringToString : ToString string := { toString := fun x => x }.
26 Notation "a +++ b" := (append (toString a) (toString b)) (at level 100).
28 (*******************************************************************************)
31 Inductive Tree (a:Type) : Type :=
32 | T_Leaf : a -> Tree a
33 | T_Branch : Tree a -> Tree a -> Tree a.
34 Implicit Arguments T_Leaf [ a ].
35 Implicit Arguments T_Branch [ a ].
37 Notation "a ,, b" := (@T_Branch _ a b) : tree_scope.
39 (* tree-of-option-of-X comes up a lot, so we give it special notations *)
40 Notation "[ q ]" := (@T_Leaf (option _) (Some q)) : tree_scope.
41 Notation "[ ]" := (@T_Leaf (option _) None) : tree_scope.
42 Notation "[]" := (@T_Leaf (option _) None) : tree_scope.
44 Open Scope tree_scope.
46 Fixpoint mapTree {a b:Type}(f:a->b)(t:@Tree a) : @Tree b :=
48 | T_Leaf x => T_Leaf (f x)
49 | T_Branch l r => T_Branch (mapTree f l) (mapTree f r)
51 Fixpoint mapOptionTree {a b:Type}(f:a->b)(t:@Tree ??a) : @Tree ??b :=
53 | T_Leaf None => T_Leaf None
54 | T_Leaf (Some x) => T_Leaf (Some (f x))
55 | T_Branch l r => T_Branch (mapOptionTree f l) (mapOptionTree f r)
57 Fixpoint mapTreeAndFlatten {a b:Type}(f:a->@Tree b)(t:@Tree a) : @Tree b :=
60 | T_Branch l r => T_Branch (mapTreeAndFlatten f l) (mapTreeAndFlatten f r)
62 Fixpoint mapOptionTreeAndFlatten {a b:Type}(f:a->@Tree ??b)(t:@Tree ??a) : @Tree ??b :=
65 | T_Leaf (Some x) => f x
66 | T_Branch l r => T_Branch (mapOptionTreeAndFlatten f l) (mapOptionTreeAndFlatten f r)
68 Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tree T) :=
70 | T_Leaf x => mapLeaf x
71 | T_Branch y z => mergeBranches (treeReduce mapLeaf mergeBranches y) (treeReduce mapLeaf mergeBranches z)
73 Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) :=
74 forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches tt }.
77 forall {Q}(t1 t2:Tree ??Q),
78 (forall q1 q2:Q, sumbool (q1=q2) (not (q1=q2))) ->
79 sumbool (t1=t2) (not (t1=t2)).
84 destruct a; destruct t2.
89 right; unfold not; intro; apply H. inversion H0; subst. auto.
90 right. unfold not; intro; inversion H.
91 right. unfold not; intro; inversion H.
93 right. unfold not; intro; inversion H.
95 right. unfold not; intro; inversion H.
98 right. unfold not; intro; inversion H.
99 set (IHt1_1 t2_1 X) as X1.
100 set (IHt1_2 t2_2 X) as X2.
101 destruct X1; destruct X2; subst.
120 Lemma mapOptionTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree ??A),
121 (mapOptionTree (g ○ f) l) = (mapOptionTree g (mapOptionTree f l)).
132 Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (forall t, mapOptionTree f t = mapOptionTree g t).
136 simpl; rewrite H; auto.
137 simpl; rewrite IHt1; rewrite IHt2; auto.
140 Open Scope string_scope.
141 Fixpoint treeToString {T}{TT:ToString T}(t:Tree ??T) : string :=
143 | T_Leaf None => "[]"
144 | T_Leaf (Some s) => "["+++s+++"]"
145 | T_Branch b1 b2 => treeToString b1 +++ ",," +++ treeToString b2
147 Instance TreeToString {T}{TT:ToString T} : ToString (Tree ??T) := { toString := treeToString }.
149 (*******************************************************************************)
152 Notation "a :: b" := (cons a b) : list_scope.
153 Open Scope list_scope.
154 Fixpoint leaves {a:Type}(t:Tree (option a)) : list a :=
156 | (T_Leaf l) => match l with
160 | (T_Branch l r) => app (leaves l) (leaves r)
162 (* weak inverse of "leaves" *)
163 Fixpoint unleaves {A:Type}(l:list A) : Tree (option A) :=
166 | (a::b) => [a],,(unleaves b)
169 (* a map over a list and the conjunction of the results *)
170 Fixpoint mapProp {A:Type} (f:A->Prop) (l:list A) : Prop :=
173 | (a::al) => f a /\ mapProp f al
176 Lemma map_id : forall A (l:list A), (map (fun x:A => x) l) = l.
183 Lemma map_app : forall `(f:A->B) l l', map f (app l l') = app (map f l) (map f l').
190 Lemma map_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
191 (map (g ○ f) l) = (map g (map f l)).
199 Lemma list_cannot_be_longer_than_itself : forall `(a:A)(b:list A), b = (a::b) -> False.
203 inversion H. apply IHb in H2.
206 Lemma list_cannot_be_longer_than_itself' : forall A (b:list A) (a c:A), b = (a::c::b) -> False.
215 Lemma mapOptionTree_on_nil : forall `(f:A->B) h, [] = mapOptionTree f h -> h=[].
218 destruct o. inversion H.
223 Lemma mapOptionTree_comp a b c (f:a->b) (g:b->c) q : (mapOptionTree g (mapOptionTree f q)) = mapOptionTree (g ○ f) q.
234 Lemma leaves_unleaves {T}(t:list T) : leaves (unleaves t) = t.
240 Lemma mapleaves' {T:Type}(t:list T){Q}{f:T->Q} : unleaves (map f t) = mapOptionTree f (unleaves t).
241 induction t; simpl in *; auto.
245 (* handy facts: map preserves the length of a list *)
246 Lemma map_on_nil : forall A B (s1:list A) (f:A->B), nil = map f s1 -> s1=nil.
255 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 }.
258 simpl in H; assert False. inversion H. inversion H0.
264 inversion H. apply map_on_nil in H2. auto.
268 inversion H. apply map_on_nil in H2. auto.
274 Lemma map_on_doubleton : forall A B (f:A->B) x y (s1:list A), ((x::y::nil) = map f s1) ->
275 { z : A*A & s1=((fst z)::(snd z)::nil) & (f (fst z))=x /\ (f (snd z))=y }.
289 Lemma mapTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree A),
290 (mapTree (g ○ f) l) = (mapTree g (mapTree f l)).
299 Lemma lmap_compose : forall A B C (f:A->B)(g:B->C)(l:list A),
300 (map (g ○ f) l) = (map g (map f l)).
309 (* sends a::b::c::nil to [[[[],,c],,b],,a] *)
310 Fixpoint unleaves' {A:Type}(l:list A) : Tree (option A) :=
313 | (a::b) => (unleaves' b),,[a]
316 (* sends a::b::c::nil to [[[[],,c],,b],,a] *)
317 Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A :=
320 | (a::b) => (unleaves'' b),,(T_Leaf a)
323 Lemma mapleaves {T:Type}(t:Tree ??T){Q}{f:T->Q} : leaves (mapOptionTree f t) = map f (leaves t).
333 Fixpoint filter {T:Type}(l:list ??T) : list T :=
336 | (None::b) => filter b
337 | ((Some x)::b) => x::(filter b)
340 Inductive distinct {T:Type} : list T -> Prop :=
341 | distinct_nil : distinct nil
342 | distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax).
344 Lemma in_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (v:VV)(lv:list VV), sumbool (In v lv) (not (In v lv)).
355 set (eqd_dec v a) as dec.
368 Lemma distinct_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (lv:list VV), sumbool (distinct lv) (not (distinct lv)).
371 left; apply distinct_nil.
373 set (in_decidable a lv) as dec.
375 right; unfold not; intros.
380 apply distinct_cons; auto.
388 Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
394 (* decidable quality on a list of elements which have decidable equality *)
395 Definition list_eq_dec : forall {T:Type}(l1 l2:list T)(dec:forall t1 t2:T, sumbool (eq t1 t2) (not (eq t1 t2))),
396 sumbool (eq l1 l2) (not (eq l1 l2)).
399 induction l1; intros.
402 right; intro H; inversion H.
403 destruct l2 as [| b l2].
404 right; intro H; inversion H.
405 set (IHl1 l2 dec) as eqx.
408 set (dec a b) as eqy.
412 right. intro. inversion H. subst. apply n. auto.
420 Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
421 apply Build_EqDecidable.
427 (*******************************************************************************)
428 (* Length-Indexed Lists *)
430 Inductive vec (A:Type) : nat -> Type :=
432 | vec_cons : forall n, A -> vec A n -> vec A (S n).
434 Fixpoint vec2list {n:nat}{t:Type}(v:vec t n) : list t :=
437 | vec_cons n a va => a::(vec2list va)
440 Require Import Omega.
441 Definition vec_get : forall {T:Type}{l:nat}(v:vec T l)(n:nat)(pf:lt n l), T.
456 Definition vec_zip {n:nat}{A B:Type}(va:vec A n)(vb:vec B n) : vec (A*B) n.
461 apply vec_cons; auto.
464 Definition vec_map {n:nat}{A B:Type}(f:A->B)(v:vec A n) : vec B n.
468 apply vec_cons; auto.
471 Fixpoint vec_In {A:Type} {n:nat} (a:A) (l:vec A n) : Prop :=
474 | vec_cons _ n m => (n = a) \/ vec_In a m
476 Implicit Arguments vec_nil [ A ].
477 Implicit Arguments vec_cons [ A n ].
479 Definition append_vec {n:nat}{T:Type}(v:vec T n)(t:T) : vec T (S n).
481 apply (vec_cons t vec_nil).
482 apply vec_cons; auto.
485 Definition list2vec {T:Type}(l:list T) : vec T (length l).
488 apply vec_cons; auto.
491 Definition vec_head {n:nat}{T}(v:vec T (S n)) : T.
494 Definition vec_tail {n:nat}{T}(v:vec T (S n)) : vec T n.
498 Lemma vec_chop {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l1).
503 inversion v; subst; auto.
505 inversion v; subst; auto.
508 Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l2).
512 apply IHl1; clear IHl1.
513 inversion v; subst; auto.
516 Lemma vec2list_len {T}{n}(v:vec T n) : length (vec2list v) = n.
522 Lemma vec2list_map_list2vec {A B}{n}(f:A->B)(v:vec A n) : map f (vec2list v) = vec2list (vec_map f v).
528 Lemma vec2list_list2vec {A}(v:list A) : vec2list (list2vec v) = v.
530 set (vec2list (list2vec (a :: v))) as q.
538 Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20).
542 (*******************************************************************************)
545 (* a ShapedTree is a tree indexed by the shape (but not the leaf values) of another tree; isomorphic to (ITree (fun _ => Q)) *)
546 Inductive ShapedTree {T:Type}(Q:Type) : Tree ??T -> Type :=
547 | st_nil : @ShapedTree T Q []
548 | st_leaf : forall {t}, Q -> @ShapedTree T Q [t]
549 | st_branch : forall {t1}{t2}, @ShapedTree T Q t1 -> @ShapedTree T Q t2 -> @ShapedTree T Q (t1,,t2).
551 Fixpoint unshape {T:Type}{Q:Type}{idx:Tree ??T}(st:@ShapedTree T Q idx) : Tree ??Q :=
555 | st_branch _ _ b1 b2 => (unshape b1),,(unshape b2)
558 Definition mapShapedTree {T}{idx:Tree ??T}{V}{Q}(f:V->Q)(st:ShapedTree V idx) : ShapedTree Q idx.
561 apply st_leaf. apply f. apply q.
562 apply st_branch; auto.
565 Definition zip_shapedTrees {T:Type}{Q1 Q2:Type}{idx:Tree ??T}
566 (st1:ShapedTree Q1 idx)(st2:ShapedTree Q2 idx) : ShapedTree (Q1*Q2) idx.
574 apply st_branch; auto.
575 inversion st1; subst; apply IHidx1; auto.
576 inversion st2; subst; auto.
577 inversion st2; subst; apply IHidx2; auto.
578 inversion st1; subst; auto.
581 Definition build_shapedTree {T:Type}(idx:Tree ??T){Q:Type}(f:T->Q) : ShapedTree Q idx.
586 apply st_branch; auto.
589 Lemma unshape_map : forall {Q}{b}(f:Q->b){T}{idx:Tree ??T}(t:ShapedTree Q idx),
590 mapOptionTree f (unshape t) = unshape (mapShapedTree f t).
602 (*******************************************************************************)
603 (* Type-Indexed Lists *)
605 (* an indexed list *)
606 Inductive IList (I:Type)(F:I->Type) : list I -> Type :=
607 | INil : IList I F nil
608 | ICons : forall i is, F i -> IList I F is -> IList I F (i::is).
609 Implicit Arguments INil [ I F ].
610 Implicit Arguments ICons [ I F ].
612 Notation "a :::: b" := (@ICons _ _ _ _ a b) (at level 20).
614 Definition ilist_head {T}{F}{x}{y} : IList T F (x::y) -> F x.
621 Definition ilist_tail {T}{F}{x}{y} : IList T F (x::y) -> IList T F y.
628 Definition ilmap {I}{F}{G}{il:list I}(f:forall i:I, F i -> G i) : IList I F il -> IList I G il.
629 induction il; intros; auto.
635 Lemma ilist_chop {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l1.
644 Lemma ilist_chop' {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l2.
647 inversion v; subst; auto.
650 Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
653 | a::::b => a::(ilist_to_list b)
656 (* a tree indexed by a (Tree (option X)) *)
657 Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type :=
658 | INone : ITree I F []
659 | ILeaf : forall i: I, F i -> ITree I F [i]
660 | IBranch : forall it1 it2:Tree ??I, ITree I F it1 -> ITree I F it2 -> ITree I F (it1,,it2).
661 Implicit Arguments INil [ I F ].
662 Implicit Arguments ILeaf [ I F ].
663 Implicit Arguments IBranch [ I F ].
665 Definition itmap {I}{F}{G}{il:Tree ??I}(f:forall i:I, F i -> G i) : ITree I F il -> ITree I G il.
666 induction il; intros; auto.
672 apply IBranch; inversion X; auto.
675 Fixpoint itree_to_tree {T}{Z}{l:Tree ??T}(il:ITree T (fun _ => Z) l) : Tree ??Z :=
679 | IBranch _ _ b1 b2 => (itree_to_tree b1),,(itree_to_tree b2)
683 (*******************************************************************************)
684 (* Extensional equality on functions *)
686 Definition extensionality := fun (t1 t2:Type) => (fun (f:t1->t2) g => forall x:t1, (f x)=(g x)).
687 Hint Transparent extensionality.
688 Instance extensionality_Equivalence : forall t1 t2, Equivalence (extensionality t1 t2).
689 intros; apply Build_Equivalence;
690 intros; compute; intros; auto.
691 rewrite H; rewrite H0; auto.
693 Add Parametric Morphism (A B C:Type) : (fun f g => g ○ f)
694 with signature (extensionality A B ==> extensionality B C ==> extensionality A C) as parametric_morphism_extensionality.
695 unfold extensionality; intros; rewrite (H x1); rewrite (H0 (y x1)); auto.
697 Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
698 (extensionality _ _ f f') ->
699 (extensionality _ _ g g') ->
700 (extensionality _ _ (g ○ f) (g' ○ f')).
702 unfold extensionality.
703 unfold extensionality in H.
704 unfold extensionality in H0.
715 CoInductive Fresh A T :=
716 { next : forall a:A, (T a * Fresh A T)
717 ; split : Fresh A T * Fresh A T
724 Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
728 Variable eol : string.
729 Extract Constant eol => "'\n':[]".
731 Class Monad {T:Type->Type} :=
732 { returnM : forall {a}, a -> T a
733 ; bindM : forall {a}{b}, T a -> (a -> T b) -> T b
735 Implicit Arguments Monad [ ].
736 Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).
738 (* the Error monad *)
739 Inductive OrError (T:Type) :=
740 | Error : forall error_message:string, OrError T
741 | OK : T -> OrError T.
742 Notation "??? T" := (OrError T) (at level 10).
743 Implicit Arguments Error [T].
744 Implicit Arguments OK [T].
746 Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
751 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
753 Open Scope string_scope.
754 Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg :=
756 | Error s => Error (err_msg +++ eol +++ " " +++ s)
760 Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
762 Definition addErrorMessage s {T} (x:OrError T) :=
763 x >>=[ s ] (fun y => OK y).
765 Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
766 | Indexed_Error : forall error_message:string, Indexed f (Error error_message)
767 | Indexed_OK : forall t, f t -> Indexed f (OK t)
771 Require Import Coq.Arith.EqNat.
772 Instance EqDecidableNat : EqDecidable nat.
773 apply Build_EqDecidable.
778 (* for a type with decidable equality, we can maintain lists of distinct elements *)
779 Section DistinctList.
780 Context `{V:EqDecidable}.
782 Fixpoint addToDistinctList (cv:V)(cvl:list V) :=
785 | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl')
788 Fixpoint removeFromDistinctList (cv:V)(cvl:list V) :=
791 | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl')
794 Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) :=
797 | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl)
800 Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) :=
803 | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
807 Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(vec T n).
808 set (list2vec l) as v.
809 destruct (eqd_dec (length l) n).
810 rewrite e in v; apply OK; apply v.
811 apply (Error (error_message (length l) n)).
815 Variable UniqSupply : Type. Extract Inlined Constant UniqSupply => "UniqSupply.UniqSupply".
816 Variable Unique : Type. Extract Inlined Constant Unique => "Unique.Unique".
817 Variable uniqFromSupply : UniqSupply -> Unique. Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply".
818 Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply.
819 Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply".
820 Variable unique_eq : forall u1 u2:Unique, sumbool (u1=u2) (u1≠u2).
821 Extract Inlined Constant unique_eq => "(==)".
822 Variable unique_toString : Unique -> string.
823 Extract Inlined Constant unique_toString => "show".
824 Instance EqDecidableUnique : EqDecidable Unique :=
825 { eqd_dec := unique_eq }.
826 Instance EqDecidableToString : ToString Unique :=
827 { toString := unique_toString }.
829 Inductive UniqM {T:Type} : Type :=
830 | uniqM : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
831 Implicit Arguments UniqM [ ].
833 Instance UniqMonad : Monad UniqM :=
834 { returnM := fun T (x:T) => uniqM (fun u => OK (u,x))
835 ; bindM := fun a b (x:UniqM a) (f:a->UniqM b) =>
841 | OK (u',va) => match f va with
848 Definition getU : UniqM Unique :=
849 uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
851 Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity).
852 Notation "'return' x" := (returnM x) (at level 100).
853 Notation "'failM' x" := (uniqM (fun _ => Error x)) (at level 100).
860 Record FreshMonad {T:Type} :=
862 ; FMT_Monad :> Monad FMT
863 ; FMT_fresh : forall tl:list T, FMT { t:T & @In _ t tl -> False }
865 Implicit Arguments FreshMonad [ ].
866 Coercion FMT : FreshMonad >-> Funclass.
870 Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".