From 76fb3fbf8098bcd0c00efc99eca230d5fa1e2f14 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 3 Jul 2016 20:57:11 -0400 Subject: Tuple: lift functions from lists to tuples --- src/Util/Tuple.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'src/Util/Tuple.v') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 42a242fad..3dfbf6bab 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -88,6 +88,18 @@ Proof. eapply from_list'_to_list'; assumption. } Qed. +Definition on_tuple {A B} (f:list A -> list B) + {n m:nat} (H:forall xs, length xs = n -> length (f xs) = m) + (xs:tuple A n) : tuple B m := + from_list m (f (to_list n xs)) + (H (to_list n xs) (length_to_list xs)). + +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 + := from_list c (f (to_list a ta) (to_list b tb)) + (Hlength (to_list a ta) (to_list b tb) (length_to_list ta) (length_to_list tb)). + Fixpoint fieldwise' {A B} (n:nat) (R:A->B->Prop) (a:tuple' A n) (b:tuple' B n) {struct n} : Prop. destruct n; simpl @tuple' in *. { exact (R a b). } -- cgit v1.2.3