X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=2a1a398b5576d40548733415ced4c084ad3d4c6d;hp=ad8e59092407035fc3daff58b2b4c5e7a767d6df;hb=b3214686b18b2d6f6905394494da8d1c17587bdb;hpb=112daf37524662d6d2267d3f7e50ff3522683b8f

diff --git a/src/General.v b/src/General.v
index ad8e590..2a1a398 100644
--- a/src/General.v
+++ b/src/General.v
@@ -13,15 +13,18 @@ Require Import Preamble.
 Generalizable All Variables.
 Require Import Omega.
 
-
+Definition EqDecider T := forall (n1 n2:T),  sumbool (n1=n2) (not (n1=n2)).
 Class EqDecidable (T:Type) :=
 { eqd_type           := T
 ; eqd_dec            :  forall v1 v2:T, sumbool (v1=v2) (not (v1=v2))
-; eqd_dec_reflexive  :  forall v, (eqd_dec v v) = (left _ (refl_equal _))
 }.
 Coercion eqd_type : EqDecidable >-> Sortclass.
 
 
+Class ToString (T:Type) := { toString : T -> string }.
+Instance StringToString : ToString string := { toString := fun x => x }.
+Notation "a +++ b" := (append (toString a) (toString b)) (at level 100).
+
 (*******************************************************************************)
 (* Trees                                                                       *)
 
@@ -49,7 +52,7 @@ Fixpoint mapOptionTree {a b:Type}(f:a->b)(t:@Tree ??a) : @Tree ??b :=
   match t with 
     | T_Leaf None     => T_Leaf None
     | T_Leaf (Some x) => T_Leaf (Some (f x))
-    | T_Branch l r => T_Branch (mapOptionTree f l) (mapOptionTree f r)
+    | T_Branch l r    => T_Branch (mapOptionTree f l) (mapOptionTree f r)
   end.
 Fixpoint mapTreeAndFlatten {a b:Type}(f:a->@Tree b)(t:@Tree a) : @Tree b :=
   match t with 
@@ -114,8 +117,34 @@ Lemma tree_dec_eq :
   inversion H; auto.
   Defined.
 
+Lemma mapOptionTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree ??A),
+  (mapOptionTree (g ○ f) l) = (mapOptionTree g (mapOptionTree f l)).
+  induction l.
+    destruct a.
+    reflexivity.
+    reflexivity.
+    simpl.
+    rewrite IHl1.
+    rewrite IHl2.
+    reflexivity.
+    Qed.
 
+Lemma mapOptionTree_extensional {A}{B}(f g:A->B) : (forall a, f a = g a) -> (forall t, mapOptionTree f t = mapOptionTree g t).
+  intros.
+  induction t.
+  destruct a; auto.
+  simpl; rewrite H; auto.
+  simpl; rewrite IHt1; rewrite IHt2; auto.
+  Qed.
 
+Open Scope string_scope.
+Fixpoint treeToString {T}{TT:ToString T}(t:Tree ??T) : string :=
+match t with
+  | T_Leaf None => "[]"
+  | T_Leaf (Some s) => "["+++s+++"]"
+  | T_Branch b1 b2 => treeToString b1 +++ ",," +++ treeToString b2
+end.
+Instance TreeToString {T}{TT:ToString T} : ToString (Tree ??T) := { toString := treeToString }.
 
 (*******************************************************************************)
 (* Lists                                                                       *)
@@ -202,6 +231,17 @@ Lemma mapOptionTree_comp a b c (f:a->b) (g:b->c) q : (mapOptionTree g (mapOption
     reflexivity.
   Qed.
 
+Lemma leaves_unleaves {T}(t:list T) : leaves (unleaves t) = t.
+  induction t; auto.
+  simpl.
+  rewrite IHt; auto.
+  Qed.
+
+Lemma mapleaves' {T:Type}(t:list T){Q}{f:T->Q} : unleaves (map f t) = mapOptionTree f (unleaves t).
+  induction t; simpl in *; auto.
+  rewrite IHt; auto.
+  Qed.
+
 (* handy facts: map preserves the length of a list *)
 Lemma map_on_nil : forall A B (s1:list A) (f:A->B), nil = map f s1 -> s1=nil.
   intros.
@@ -280,6 +320,16 @@ Fixpoint unleaves'' {A:Type}(l:list ??A) : Tree ??A :=
     | (a::b) => (unleaves'' b),,(T_Leaf a)
   end.
 
+Lemma mapleaves {T:Type}(t:Tree ??T){Q}{f:T->Q} : leaves (mapOptionTree f t) = map f (leaves t).
+  induction t.
+  destruct a; auto.
+  simpl.
+  rewrite IHt1.
+  rewrite IHt2.
+  rewrite map_app.
+  auto.
+  Qed.
+
 Fixpoint filter {T:Type}(l:list ??T) : list T :=
   match l with
     | nil => nil
@@ -291,6 +341,50 @@ Inductive distinct {T:Type} : list T -> Prop :=
 | distinct_nil  : distinct nil
 | distinct_cons : forall a ax, (@In _ a ax -> False) -> distinct ax -> distinct (a::ax).
 
+Lemma in_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (v:VV)(lv:list VV), sumbool (In v lv) (not (In v lv)).
+  intros.
+  induction lv.
+  right.
+  unfold not.
+  intros.
+  inversion H.
+  destruct IHlv.
+  left.
+  simpl.
+  auto.
+  set (eqd_dec v a) as dec.
+  destruct dec.
+  subst.
+  left; simpl; auto.
+  right.
+  unfold not; intros.
+  destruct H.
+  subst.
+  apply n0; auto.
+  apply n.
+  apply H.
+  Defined.
+
+Lemma distinct_decidable {VV:Type}{eqdVV:EqDecidable VV} : forall (lv:list VV), sumbool (distinct lv) (not (distinct lv)).
+  intros.
+  induction lv.
+  left; apply distinct_nil.
+  destruct IHlv.
+  set (in_decidable a lv) as dec.
+  destruct dec.
+  right; unfold not; intros.
+  inversion H.
+  subst.
+  apply H2; auto.
+  left.
+  apply distinct_cons; auto.
+  right.
+  unfold not; intros.
+  inversion H.
+  subst.
+  apply n; auto.
+  Defined.
+
 Lemma map_preserves_length {A}{B}(f:A->B)(l:list A) : (length l) = (length (map f l)).
   induction l; auto.
   simpl.
@@ -323,8 +417,12 @@ Definition list_eq_dec : forall {T:Type}(l1 l2:list T)(dec:forall t1 t2:T, sumbo
       auto.
       Defined.
 
-
-
+Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T).
+  apply Build_EqDecidable.
+  intros.
+  apply list_eq_dec.
+  apply eqd_dec.
+  Defined.
 
 (*******************************************************************************)
 (* Length-Indexed Lists                                                        *)
@@ -415,6 +513,28 @@ Lemma vec_chop' {T}{l1 l2:list T}{Q}(v:vec Q (length (app l1 l2))) : vec Q (leng
   inversion v; subst; auto.
   Defined.
 
+Lemma vec2list_len {T}{n}(v:vec T n) : length (vec2list v) = n.
+  induction v; auto.
+  simpl.
+  omega.
+  Qed.
+
+Lemma vec2list_map_list2vec {A B}{n}(f:A->B)(v:vec A n) : map f (vec2list v) = vec2list (vec_map f v).
+  induction v; auto.
+  simpl. rewrite IHv.
+  reflexivity.
+  Qed.
+
+Lemma vec2list_list2vec {A}(v:list A) : vec2list (list2vec v) = v.
+  induction v; auto.
+  set (vec2list (list2vec (a :: v))) as q.
+  rewrite <- IHv.
+  unfold q.
+  clear q.
+  simpl.
+  reflexivity.
+  Qed.
+
 Notation "a ::: b" := (@vec_cons _ _ a b) (at level 20).
 
 
@@ -489,6 +609,50 @@ Inductive IList (I:Type)(F:I->Type) : list I -> Type :=
 Implicit Arguments INil [ I F ].
 Implicit Arguments ICons [ I F ].
 
+Notation "a :::: b" := (@ICons _ _ _ _ a b) (at level 20).
+
+Definition ilist_head {T}{F}{x}{y} : IList T F (x::y) -> F x.
+  intro il.
+  inversion il.
+  subst.
+  apply X.
+  Defined.
+
+Definition ilist_tail {T}{F}{x}{y} : IList T F (x::y) -> IList T F y.
+  intro il.
+  inversion il.
+  subst.
+  apply X0.
+  Defined.
+
+Definition ilmap {I}{F}{G}{il:list I}(f:forall i:I, F i -> G i) : IList I F il -> IList I G il.
+  induction il; intros; auto.
+  apply INil.
+  inversion X; subst.
+  apply ICons; auto.
+  Defined.
+
+Lemma ilist_chop {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l1.
+  induction l1; auto.
+  apply INil.
+  apply ICons.
+  inversion v; auto.
+  apply IHl1.
+  inversion v; auto.
+  Defined.
+
+Lemma ilist_chop' {T}{F}{l1 l2:list T}(v:IList T F (app l1 l2)) : IList T F l2.
+  induction l1; auto.
+  apply IHl1.
+  inversion v; subst; auto.
+  Defined.
+
+Fixpoint ilist_to_list {T}{Z}{l:list T}(il:IList T (fun _ => Z) l) : list Z :=
+  match il with
+  | INil   => nil
+  | a::::b => a::(ilist_to_list b)
+  end.
+
 (* a tree indexed by a (Tree (option X)) *)
 Inductive ITree (I:Type)(F:I->Type) : Tree ??I -> Type :=
 | INone      :                                ITree I F []
@@ -498,7 +662,22 @@ Implicit Arguments INil    [ I F ].
 Implicit Arguments ILeaf   [ I F ].
 Implicit Arguments IBranch [ I F ].
 
+Definition itmap {I}{F}{G}{il:Tree ??I}(f:forall i:I, F i -> G i) : ITree I F il -> ITree I G il.
+  induction il; intros; auto.
+  destruct a.
+  apply ILeaf.
+  apply f.
+  inversion X; auto.
+  apply INone.
+  apply IBranch; inversion X; auto.
+  Defined.
 
+Fixpoint itree_to_tree {T}{Z}{l:Tree ??T}(il:ITree T (fun _ => Z) l) : Tree ??Z :=
+  match il with
+  | INone     => []
+  | ILeaf _ a => [a]
+  | IBranch _ _ b1 b2 => (itree_to_tree b1),,(itree_to_tree b2)
+  end.
 
 
 (*******************************************************************************)
@@ -533,6 +712,28 @@ Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3),
 
 
 
+CoInductive Fresh A T :=
+{ next  : forall a:A, (T a * Fresh A T)
+; split : Fresh A T * Fresh A T
+}.
+
+
+
+
+
+Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
+
+
+(* string stuff *)
+Variable eol : string.
+Extract Constant eol  => "'\n':[]".
+
+Class Monad {T:Type->Type} :=
+{ returnM : forall {a},     a -> T a
+; bindM   : forall {a}{b},  T a -> (a -> T b) -> T b
+}.
+Implicit Arguments Monad [ ].
+Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).
 
 (* the Error monad *)
 Inductive OrError (T:Type) :=
@@ -549,28 +750,30 @@ Definition orErrorBind {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) :=
   end.
 Notation "a >>= b" := (@orErrorBind _ a _ b) (at level 20).
 
-Fixpoint list2vecOrError {T}(l:list T)(n:nat) : ???(vec T n) :=
-  match n as N return ???(vec _ N) with
-    | O => match l with
-             | nil => OK vec_nil
-             | _   => Error "list2vecOrError: list was too long"
-           end
-    | S n' => match l with
-                | nil   => Error "list2vecOrError: list was too short"
-                | t::l' => list2vecOrError l' n' >>= fun l'' => OK (vec_cons t l'')
-              end
+Open Scope string_scope.
+Definition orErrorBindWithMessage {T:Type} (oe:OrError T) {Q:Type} (f:T -> OrError Q) err_msg :=
+  match oe with
+    | Error s => Error (err_msg +++ eol +++ "  " +++ s)
+    | OK    t => f t
   end.
 
+Notation "a >>=[ S ] b" := (@orErrorBindWithMessage _ a _ b S) (at level 20).
+
+Definition addErrorMessage s {T} (x:OrError T) :=
+  x >>=[ s ] (fun y => OK y).
+
 Inductive Indexed {T:Type}(f:T -> Type) : ???T -> Type :=
 | Indexed_Error : forall error_message:string, Indexed f (Error error_message)
 | Indexed_OK    : forall t, f t -> Indexed f (OK t)
 .
-Ltac xauto := try apply Indexed_Error; try apply Indexed_OK.
-
-
-
 
 
+Require Import Coq.Arith.EqNat.
+Instance EqDecidableNat : EqDecidable nat.
+  apply Build_EqDecidable.
+  intros.
+  apply eq_nat_dec.
+  Defined.
 
 (* for a type with decidable equality, we can maintain lists of distinct elements *)
 Section DistinctList.
@@ -600,3 +803,98 @@ Section DistinctList.
   | cv'::cvl' => mergeDistinctLists cvl' (addToDistinctList cv' cvl2)
   end.
 End DistinctList.
+
+Lemma list2vecOrFail {T}(l:list T)(n:nat)(error_message:nat->nat->string) : ???(vec T n).
+  set (list2vec l) as v.
+  destruct (eqd_dec (length l) n).
+    rewrite e in v; apply OK; apply v.
+    apply (Error (error_message (length l) n)).
+    Defined.
+
+(* Uniques *)
+Variable UniqSupply      : Type.                   Extract Inlined Constant UniqSupply     => "UniqSupply.UniqSupply".
+Variable Unique          : Type.                   Extract Inlined Constant Unique         => "Unique.Unique".
+Variable uniqFromSupply  : UniqSupply -> Unique.   Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply".
+Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply.
+    Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply".
+Variable unique_eq       : forall u1 u2:Unique, sumbool (u1=u2) (u1≠u2).
+    Extract Inlined Constant unique_eq => "(==)".
+Variable unique_toString : Unique -> string.
+    Extract Inlined Constant unique_toString => "show".
+Instance EqDecidableUnique : EqDecidable Unique :=
+  { eqd_dec := unique_eq }.
+Instance EqDecidableToString : ToString Unique :=
+  { toString := unique_toString }.
+
+Inductive UniqM {T:Type} : Type :=
+ | uniqM    : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
+ Implicit Arguments UniqM [ ].
+
+Instance UniqMonad : Monad UniqM :=
+{ returnM := fun T (x:T) => uniqM (fun u => OK (u,x))
+; bindM   := fun a b (x:UniqM a) (f:a->UniqM b) =>
+  uniqM (fun u =>
+    match x with
+      | uniqM fa =>
+        match fa u with
+          | Error s   => Error s
+          | OK (u',va) => match f va with
+                           | uniqM fb => fb u'
+                         end
+        end
+    end)
+}.
+
+Definition getU : UniqM Unique :=
+  uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
+
+Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity).
+Notation "'return' x" := (returnM x) (at level 100).
+Notation "'failM'  x" := (uniqM (fun _ => Error x)) (at level 100).
+
+
+
+
+
+
+Record FreshMonad {T:Type} :=
+{ FMT       :  Type -> Type
+; FMT_Monad :> Monad FMT
+; FMT_fresh :  forall tl:list T, FMT { t:T & @In _ t tl -> False }
+}.
+Implicit Arguments FreshMonad [ ].
+Coercion FMT       : FreshMonad >-> Funclass.
+
+
+
+Variable Prelude_error : forall {A}, string -> A.   Extract Inlined Constant Prelude_error => "Prelude.error".
+
+
+
+
+Ltac eqd_dec_refl X :=
+  destruct (eqd_dec X X) as [eqd_dec1 | eqd_dec2];
+    [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ].
+
+Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 -> t1 = t2.
+  intros T.
+  induction t1; intros.
+  destruct t2.
+  auto.
+  inversion H.
+  destruct t2.
+  inversion H.
+  simpl in H.
+  inversion H.
+  set (IHt1 _ H2) as q.
+  rewrite q.
+  reflexivity.
+  Qed.
+
+Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1.
+  admit.
+  Defined.
+
+Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2.
+  admit.
+  Defined.