From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Sat, 19 Mar 2011 21:15:18 +0000 (-0700)
Subject: add mapleaves to General.v
X-Git-Url: http://git.megacz.com/?a=commitdiff_plain;h=5a92232f20931ebb060082d5236239c2d2061e17;p=coq-hetmet.git

add mapleaves to General.v
---

diff --git a/src/General.v b/src/General.v
index ffd0d29..7aefcf0 100644
--- a/src/General.v
+++ b/src/General.v
@@ -301,6 +301,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