From a24262c5945566fec523304c1eb8a72ecd9a61b8 Mon Sep 17 00:00:00 2001
From: jadep <jade.philipoom@gmail.com>
Date: Sun, 25 Jun 2017 17:16:03 -0400
Subject: write and prove Tuple.map2_cps

---
 src/Util/Tuple.v | 5 +++++
 1 file changed, 5 insertions(+)

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

diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 775c7cb8d..2dbc592ff 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -791,6 +791,11 @@ Lemma map_append {A B n} (f:A->B) : forall (x:tuple A n) (a:A),
   map f (append a x) = append (f a) (map f x).
 Proof. destruct n; auto using map_append'. Qed.
 
+Lemma map2_append n A B C f xs ys x y :
+  @map2 (S n) A B C f (append x xs) (append y ys)
+  = append (f x y) (map2 f xs ys).
+Proof. destruct n; [reflexivity|]. apply map2_S'. Qed.
+
 Fixpoint nth_default {A m} (d:A) n : tuple A m -> A :=
   match m, n with
   | O, _ => fun _ => d
-- 
cgit v1.2.3