From 25bee1e1ea359593fcd3a75b044f3fb66ae85b00 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 8 Nov 2016 15:21:32 -0500
Subject: Add hlist_map

---
 src/Util/HList.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'src/Util/HList.v')

diff --git a/src/Util/HList.v b/src/Util/HList.v
index aacefe8f3..ec9dcdd7b 100644
--- a/src/Util/HList.v
+++ b/src/Util/HList.v
@@ -88,6 +88,18 @@ Proof.
   destruct n; [ constructor | apply hlist'_impl ].
 Defined.
 
+Local Arguments Tuple.map : simpl never.
+Lemma hlist_map {n A B F} {f:A -> B} (xs:tuple A n)
+  : hlist F (Tuple.map f xs) = hlist (fun x => F (f x)) xs.
+Proof.
+  destruct n as [|n]; [ reflexivity | ].
+  induction n; [ reflexivity | ].
+  specialize (IHn (fst xs)).
+  destruct xs; rewrite Tuple.map_S.
+  simpl @hlist in *; rewrite <- IHn.
+  reflexivity.
+Qed.
+
 Module Tuple.
   Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n)
   : hlist (fun x => f x = x) xs -> Tuple.map f xs = xs.
-- 
cgit v1.2.3