diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-06-25 17:16:03 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-06-25 17:16:03 -0400 |
| commit | a24262c5945566fec523304c1eb8a72ecd9a61b8 (patch) | |
| tree | 031b191120d8b7107ba27153c2a636158b013c5f /src/Util/Tuple.v | |
| parent | 75c2c8ac7f512c7baa75d0a841e45a007bd89860 (diff) | |
write and prove Tuple.map2_cps
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 5 |
1 files changed, 5 insertions, 0 deletions
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 |