From e91d45d8667001214e23f119f0b50294f34077a2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 6 Nov 2016 16:56:59 -0500 Subject: Add admitted lemma about tuple map, add hlist lem --- src/Util/Tuple.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Util/Tuple.v') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 7af4dfe96..7367b1460 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -136,6 +136,13 @@ Definition on_tuple {A B} (f:list A -> list B) Definition map {n A B} (f:A -> B) (xs:tuple A n) : tuple B n := on_tuple (List.map f) (fun _ => eq_trans (map_length _ _)) xs. +Lemma map_S {n A B} (f:A -> B) (xs:tuple' A n) (x:A) + : map (n:=S (S n)) f (xs, x) = (map (n:=S n) f xs, f x). +Proof. + unfold map, on_tuple. + simpl @List.map. +Admitted. + Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat} (Hlength : forall la lb, length la = a -> length lb = b -> length (f la lb) = c) (ta:tuple A a) (tb:tuple B b) : tuple C c -- cgit v1.2.3