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.
23 Instance EqDecidableOption (T:Type)(EQDT:EqDecidable T) : EqDecidable ??T.
24 apply Build_EqDecidable.
28 destruct (eqd_dec t t0).
37 right; unfold not; intro; inversion H.
38 right; unfold not; intro; inversion H.
42 Class ToString (T:Type) := { toString : T -> string }.
43 Instance StringToString : ToString string := { toString := fun x => x }.
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 }.
55 (*******************************************************************************)
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 ].
64 Notation "a ,, b" := (@T_Branch _ a b) : tree_scope.
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.
71 Fixpoint InT {A} (a:A) (t:Tree ??A) {struct t} : Prop :=
73 | T_Leaf None => False
74 | T_Leaf (Some x) => x = a
75 | T_Branch b1 b2 => InT a b1 \/ InT a b2
78 Open Scope tree_scope.
80 Fixpoint mapTree {a b:Type}(f:a->b)(t:@Tree a) : @Tree b :=
82 | T_Leaf x => T_Leaf (f x)
83 | T_Branch l r => T_Branch (mapTree f l) (mapTree f r)
85 Fixpoint mapOptionTree {a b:Type}(f:a->b)(t:@Tree ??a) : @Tree ??b :=
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)
91 Fixpoint mapTreeAndFlatten {a b:Type}(f:a->@Tree b)(t:@Tree a) : @Tree b :=
94 | T_Branch l r => T_Branch (mapTreeAndFlatten f l) (mapTreeAndFlatten f r)
96 Fixpoint mapOptionTreeAndFlatten {a b:Type}(f:a->@Tree ??b)(t:@Tree ??a) : @Tree ??b :=
99 | T_Leaf (Some x) => f x
100 | T_Branch l r => T_Branch (mapOptionTreeAndFlatten f l) (mapOptionTreeAndFlatten f r)
102 Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tree T) :=
104 | T_Leaf x => mapLeaf x
105 | T_Branch y z => mergeBranches (treeReduce mapLeaf mergeBranches y) (treeReduce mapLeaf mergeBranches z)
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).
115 Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T :=
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)
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)).
128 induction t1; intros.
130 destruct a; destruct t2.
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.
139 right. unfold not; intro; inversion H.
141 right. unfold not; intro; inversion H.
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.
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)).
178 Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (forall t, mapOptionTree f t = mapOptionTree g t).
182 simpl; rewrite H; auto.
183 simpl; rewrite IHt1; rewrite IHt2; auto.
186 Fixpoint treeToString {T}{TT:ToString T}(t:Tree ??T) : string :=
188 | T_Leaf None => "[]"
189 | T_Leaf (Some s) => "["+++toString s+++"]"
190 | T_Branch b1 b2 => treeToString b1 +++ ",," +++ treeToString b2
192 Instance TreeToString {T}{TT:ToString T} : ToString (Tree ??T) := { toString := treeToString }.
194 (*******************************************************************************)
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 :=
201 | (T_Leaf l) => match l with
205 | (T_Branch l r) => app (leaves l) (leaves r)
207 (* weak inverse of "leaves" *)
208 Fixpoint unleaves {A:Type}(l:list A) : Tree (option A) :=
211 | (a::b) => [a],,(unleaves b)
214 (* a map over a list and the conjunction of the results *)
215 Fixpoint mapProp {A:Type} (f:A->Prop) (l:list A) : Prop :=
218 | (a::al) => f a /\ mapProp f al
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
227 | a::b => match n with
229 | S n' => fun pf => (fun list_del' => _) (list_del _ b n')
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
247 | a::b => match n with
249 | S n' => fun pf => (fun list_get' => _) (list_get _ b n')
262 Fixpoint list_ins (n:nat) {T:Type} (t:T) (l:list T) : list T :=
265 | S n' => match l with
267 | a::b => a::(list_ins n' t b)
271 Lemma list_ins_nil : forall T n x, @list_ins n T x nil = x::nil.
276 Fixpoint list_take {T:Type}(l:list T)(n:nat) :=
279 | S n' => match l with
281 | a::b => a::(list_take b n')
285 Fixpoint list_drop {T:Type}(l:list T)(n:nat) :=
288 | S n' => match l with
290 | a::b => list_drop b n'
294 Lemma list_ins_app T n κ : forall Γ, @list_ins n T κ Γ = app (list_take Γ n) (κ::(list_drop Γ n)).
307 Lemma list_take_drop T l : forall n, app (@list_take T l n) (list_drop l n) = l.
319 Lemma map_id : forall A (l:list A), (map (fun x:A => x) l) = l.
326 Lemma map_app : forall `(f:A->B) l l', map f (app l l') = app (map f l) (map f l').
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)).
342 Lemma list_cannot_be_longer_than_itself : forall `(a:A)(b:list A), b = (a::b) -> False.
346 inversion H. apply IHb in H2.
349 Lemma list_cannot_be_longer_than_itself' : forall A (b:list A) (a c:A), b = (a::c::b) -> False.
358 Lemma mapOptionTree_on_nil : forall `(f:A->B) h, [] = mapOptionTree f h -> h=[].
361 destruct o. inversion H.
366 Lemma mapOptionTree_comp a b c (f:a->b) (g:b->c) q : (mapOptionTree g (mapOptionTree f q)) = mapOptionTree (g ○ f) q.
377 Lemma leaves_unleaves {T}(t:list T) : leaves (unleaves t) = t.
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.
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.
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 }.
401 simpl in H; assert False. inversion H. inversion H0.
407 inversion H. apply map_on_nil in H2. auto.
411 inversion H. apply map_on_nil in H2. auto.
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 }.
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)).
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)).
452 (* sends a::b::c::nil to [[[[],,c],,b],,a] *)
453 Fixpoint unleaves' {A:Type}(l:list A) : Tree (option A) :=
456 | (a::b) => (unleaves' b),,[a]
459 (* sends a::b::c::nil to [[[[],,c],,b],,a] *)
460 Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A :=
463 | (a::b) => (unleaves'' b),,(T_Leaf a)
466 Lemma mapleaves {T:Type}(t:Tree ??T){Q}{f:T->Q} : leaves (mapOptionTree f t) = map f (leaves t).
476 Fixpoint filter {T:Type}(l:list ??T) : list T :=
479 | (None::b) => filter b
480 | ((Some x)::b) => x::(filter b)
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).
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).
492 Lemma in_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (v:VV)(lv:list VV), sumbool (In v lv) (not (In v lv)).
503 set (eqd_dec v a) as dec.
516 Lemma distinct_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (lv:list VV), sumbool (distinct lv) (not (distinct lv)).
519 left; apply distinct_nil.
521 set (in_decidable a lv) as dec.
523 right; unfold not; intros.
528 apply distinct_cons; auto.
536 Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
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)).
547 induction l1; intros.
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.
556 set (dec a b) as eqy.
560 right. intro. inversion H. subst. apply n. auto.
568 Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
569 apply Build_EqDecidable.
575 Fixpoint listToString {T:Type}{tst:ToString T}(l:list T) : string :=
578 | a::b => (toString a) +++ "::" +++ listToString b
581 Instance ListToString {T:Type}{tst:ToString T} : ToString (list T) :=
582 { toString := @listToString _ _ }.
585 (*******************************************************************************)
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).
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)
601 (* takeT and dropT are not exact inverses! *)
603 (* drop replaces each leaf where the flag is set with a [] *)
604 Fixpoint dropT {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
606 | tf_leaf_true x => []
607 | tf_leaf_false x => Σ
608 | tf_branch b1 b2 tb1 tb2 => (dropT tb1),,(dropT tb2)
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) :=
614 | tf_leaf_true x => Some Σ
615 | tf_leaf_false x => None
616 | tf_branch b1 b2 tb1 tb2 =>
619 | Some b1' => match takeT tb2 with
621 | Some b2' => Some (b1',,b2')
626 Definition takeT' {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T :=
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 :=
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)).
645 induction l1; intros.
650 right; unfold not; intro; apply n; inversion H; auto.
656 right; unfold not; intro; inversion H.
657 destruct (IHl1_1 l2_1 dec);
658 destruct (IHl1_2 l2_2 dec); subst.
674 Instance EqDecidableTree {T:Type}(eqd:EqDecidable T) : EqDecidable (Tree T).
675 apply Build_EqDecidable.
681 (*******************************************************************************)
682 (* Length-Indexed Lists *)
684 Inductive vec (A:Type) : nat -> Type :=
686 | vec_cons : forall n, A -> vec A n -> vec A (S n).
688 Fixpoint vec2list {n:nat}{t:Type}(v:vec t n) : list t :=
691 | vec_cons n a va => a::(vec2list va)
694 Require Import Omega.
695 Definition vec_get : forall {T:Type}{l:nat}(v:vec T l)(n:nat)(pf:lt n l), T.
710 Definition vec_zip {n:nat}{A B:Type}(va:vec A n)(vb:vec B n) : vec (A*B) n.
715 apply vec_cons; auto.
718 Definition vec_map {n:nat}{A B:Type}(f:A->B)(v:vec A n) : vec B n.
722 apply vec_cons; auto.
725 Fixpoint vec_In {A:Type} {n:nat} (a:A) (l:vec A n) : Prop :=
728 | vec_cons _ n m => (n = a) \/ vec_In a m
730 Implicit Arguments vec_nil [ A ].
731 Implicit Arguments vec_cons [ A n ].
733 Definition append_vec {n:nat}{T:Type}(v:vec T n)(t:T) : vec T (S n).
735 apply (vec_cons t vec_nil).
736 apply vec_cons; auto.
739 Definition list2vec {T:Type}(l:list T) : vec T (length l).
742 apply vec_cons; auto.
745 Definition vec_head {n:nat}{T}(v:vec T (S n)) : T.
748 Definition vec_tail {n:nat}{T}(v:vec T (S n)) : vec T n.
752 Lemma vec_chop {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l1).
757 inversion v; subst; auto.
759 inversion v; subst; auto.
762 Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (length l2).
766 apply IHl1; clear IHl1.
767 inversion v; subst; auto.
770 Lemma vec2list_len {T}{n}(v:vec T n) : length (vec2list v) = n.
776 Lemma vec2list_map_list2vec {A B}{n}(f:A->B)(v:vec A n) : map f (vec2list v) = vec2list (vec_map f v).
782 Lemma vec2list_list2vec {A}(v:list A) : vec2list (list2vec v) = v.
784 set (vec2list (list2vec (a :: v))) as q.
792 Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20).
796 (*******************************************************************************)
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).
805 Fixpoint unshape {T:Type}{Q:Type}{idx:Tree ??T}(st:@ShapedTree T Q idx) : Tree ??Q :=
809 | st_branch _ _ b1 b2 => (unshape b1),,(unshape b2)
812 Definition mapShapedTree {T}{idx:Tree ??T}{V}{Q}(f:V->Q)(st:ShapedTree V idx) : ShapedTree Q idx.
815 apply st_leaf. apply f. apply q.
816 apply st_branch; auto.
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.
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.
835 Definition build_shapedTree {T:Type}(idx:Tree ??T){Q:Type}(f:T->Q) : ShapedTree Q idx.
840 apply st_branch; auto.
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).
856 (*******************************************************************************)
857 (* Type-Indexed Lists *)
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 ].
866 Notation "a :::: b" := (@ICons _ _ _ _ a b) (at level 20).
868 Definition ilist_head {T}{F}{x}{y} : IList T F (x::y) -> F x.
875 Definition ilist_tail {T}{F}{x}{y} : IList T F (x::y) -> IList T F y.
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.
889 Lemma ilist_chop {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l1.
898 Lemma ilist_chop' {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l2.
901 inversion v; subst; auto.
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).
915 Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
918 | a::::b => a::(ilist_to_list b)
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 ].
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.
937 apply IBranch; inversion X; auto.
940 Fixpoint itree_to_tree {T}{Z}{l:Tree ??T}(il:ITree T (fun _ => Z) l) : Tree ??Z :=
944 | IBranch _ _ b1 b2 => (itree_to_tree b1),,(itree_to_tree b2)
948 (*******************************************************************************)
949 (* Extensional equality on functions *)
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.
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.
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')).
967 unfold extensionality.
968 unfold extensionality in H.
969 unfold extensionality in H0.
985 Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
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.
993 Variable eol : string.
994 Extract Constant eol => "'\n':[]".
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
1000 Implicit Arguments Monad [ ].
1001 Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).
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].
1011 Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
1013 | Error s => Error s
1016 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
1018 Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg :=
1020 | Error s => Error (err_msg +++ eol +++ " " +++ s)
1024 Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
1026 Definition addErrorMessage s {T} (x:OrError T) :=
1027 x >>=[ s ] (fun y => OK y).
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)
1035 Require Import Coq.Arith.EqNat.
1036 Instance EqDecidableNat : EqDecidable nat.
1037 apply Build_EqDecidable.
1042 (* for a type with decidable equality, we can maintain lists of distinct elements *)
1043 Section DistinctList.
1044 Context `{V:EqDecidable}.
1046 Fixpoint addToDistinctList (cv:V)(cvl:list V) :=
1049 | cv'::cvl' => if eqd_dec cv cv' then cvl' else cv'::(addToDistinctList cv cvl')
1052 Fixpoint removeFromDistinctList (cv:V)(cvl:list V) :=
1055 | cv'::cvl' => if eqd_dec cv cv' then removeFromDistinctList cv cvl' else cv'::(removeFromDistinctList cv cvl')
1058 Fixpoint removeFromDistinctList' (cvrem:list V)(cvl:list V) :=
1061 | rem::cvrem' => removeFromDistinctList rem (removeFromDistinctList' cvrem' cvl)
1064 Fixpoint mergeDistinctLists (cvl1:list V)(cvl2:list V) :=
1067 | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
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)).
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) :=
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)
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 }.
1103 Inductive UniqM {T:Type} : Type :=
1104 | uniqM : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
1105 Implicit Arguments UniqM [ ].
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) =>
1114 | Error s => Error s
1115 | OK (u',va) => match f va with
1122 Definition getU : UniqM Unique :=
1123 uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
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).
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 }
1139 Implicit Arguments FreshMonad [ ].
1140 Coercion FMT : FreshMonad >-> Funclass.
1144 Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
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' ].
1153 Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 -> t1 = t2.
1155 induction t1; intros.
1163 set (IHt1 _ H2) as q.
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
1175 | a:::v0 => ex_intro _ a (ex_intro _ v0 (refl_equal _))
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
1183 | vec_nil => refl_equal _
1187 Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
1190 set (nilVec _ v1) as v1'.
1191 set (nilVec _ v2) as v2'.
1195 set (openVec _ _ v1) as v1'.
1196 set (openVec _ _ v2) as v2'.
1207 Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
1210 set (nilVec _ v1) as v1'.
1211 set (nilVec _ v2) as v2'.
1215 set (openVec _ _ v1) as v1'.
1216 set (openVec _ _ v2) as v2'.
1227 Fixpoint mapM {M}{mon:Monad M}{T}(ml:list (M T)) : M (list T) :=
1230 | a::b => bind a' = a ; bind b' = mapM b ; return a'::b'
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
1236 | a::b => ICons a b (f a) (list_to_ilist f b)
1239 Fixpoint treeM {T}{M}{MT:Monad M}(t:Tree ??(M T)) : M (Tree ??T) :=
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')
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.
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 }.
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')
1264 Instance LatexMathToString : ToString LatexMath := { toString := fun x => match x with rawLatexMath s => s end }.
1266 Instance ToLatexLatexMath : ToLatex LatexMath := { toLatex := fun l => rawLatex ("$"+++toString l+++"$") }.
1267 Instance ToLatexMathLatex : ToLatexMath Latex := { toLatexMath := fun l => rawLatexMath ("\text{"+++toString l+++"}") }.
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 }.
1274 Fixpoint treeToLatexMath {V}{ToLatexV:ToLatexMath V}(t:Tree ??V) : LatexMath :=
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")