From 8f00501ac48984925832279f7d67302c09a570ec Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 19 Mar 2011 23:05:31 -0700 Subject: [PATCH] add mapOptionTree_extensional, leaves_unleaves, mapleaves --- src/General.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/General.v b/src/General.v index b0266f4..685619f 100644 --- a/src/General.v +++ b/src/General.v @@ -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. -- 1.7.10.4