From 8fa21b4f8e26e9eae1f1fd9061679c57f8603bc1 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 8 Nov 2016 21:49:49 -0500
Subject: Add Tuple.map2_S

---
 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 ea22d8ff3..d2c3f6d7d 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -168,6 +168,11 @@ Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat}
 Definition map2 {n A B C} (f:A -> B -> C) (xs:tuple A n) (ys:tuple B n) : tuple C n
   := on_tuple2 (map2 f) (fun la lb pfa pfb => eq_trans (@map2_length _ _ _ _ la lb) (eq_trans (f_equal2 _ pfa pfb) (Min.min_idempotent _))) xs ys.
 
+Lemma map2_S {n A B C} (f:A -> B -> C) (xs:tuple' A n) (ys:tuple' B n) (x:A) (y:B)
+  : map2 (n:=S (S n)) f (xs, x) (ys y) = (map2 (n:=S n) f xs ys, f x y).
+Proof.
+Admitted.
+
 Lemma map_map2 {n A B C D} (f:A -> B -> C) (g:C -> D) (xs:tuple A n) (ys:tuple B n)
   : map g (map2 f xs ys) = map2 (fun a b => g (f a b)) xs ys.
 Proof.
-- 
cgit v1.2.3