X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneral.v;h=2a1a398b5576d40548733415ced4c084ad3d4c6d;hp=ffd0d29662a00a2bd143b2e5307b1f1bf40e3b39;hb=b3214686b18b2d6f6905394494da8d1c17587bdb;hpb=90316bd3f95d22815f987ccc8db23b7b04f45efe diff --git a/src/General.v b/src/General.v index ffd0d29..2a1a398 100644 --- a/src/General.v +++ b/src/General.v @@ -52,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 @@ -129,6 +129,14 @@ Lemma mapOptionTree_compose : forall A B C (f:A->B)(g:B->C)(l:Tree ??A), 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 @@ -223,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. @@ -301,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 @@ -312,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. @@ -782,4 +855,46 @@ 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.