From beaf8c386549f99d0366f7c6a269ebb9ce311c5f Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 6 Nov 2016 17:03:30 -0500
Subject: Add HList lemma

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

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

diff --git a/src/Util/HList.v b/src/Util/HList.v
index 4096c54d6..120d898d9 100644
--- a/src/Util/HList.v
+++ b/src/Util/HList.v
@@ -49,3 +49,13 @@ Proof.
   destruct n as [|n]; [ reflexivity | ].
   apply map'_mapt'.
 Qed.
+
+Lemma map_is_mapt {n A F B} (f : A -> B) {ts : tuple A n} (ls : hlist F ts)
+  : Tuple.map f ts = mapt (fun x _ => f x) ls.
+Proof.
+  destruct n as [|n]; [ reflexivity | ].
+  induction n as [|n IHn]; [ reflexivity | ].
+  { unfold mapt in *; simpl @mapt' in *.
+    rewrite <- IHn; clear IHn.
+    rewrite <- (@Tuple.map_S n _ _ f); destruct ts; reflexivity. }
+Qed.
-- 
cgit v1.2.3