diff options
| -rw-r--r-- | src/Util/CPSUtil.v | 19 | ||||
| -rw-r--r-- | src/Util/Tuple.v | 5 |
2 files changed, 24 insertions, 0 deletions
diff --git a/src/Util/CPSUtil.v b/src/Util/CPSUtil.v index 587a25290..adae0406b 100644 --- a/src/Util/CPSUtil.v +++ b/src/Util/CPSUtil.v @@ -269,6 +269,25 @@ Module Tuple. [|rewrite IHn, <-map_append,<-subst_append]; reflexivity. Qed. Hint Rewrite @map_cps_correct : uncps. + Fixpoint map2_cps {n A B C} (g:A->B->C) : + tuple A n -> tuple B n -> forall {T}, (tuple C n->T) -> T := + match n with + | O => fun _ _ _ f => f tt + | S n' => fun xs ys T f => + map2_cps g (tl xs) (tl ys) (fun zs => f (append (g (hd xs) (hd ys)) zs)) + end. + + 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). + Admitted. + Lemma map2_cps_correct {n A B C} g xs ys : forall {T} f, + @map2_cps n A B C g xs ys T f = f (map2 g xs ys). + Proof. + induction n; simpl map2_cps; intros; try destruct xs, ys; + [|rewrite IHn, <-map2_append,<-!subst_append]; reflexivity. + Qed. Hint Rewrite @map2_cps_correct : uncps. + Fixpoint mapi_with'_cps {T A B n} i (f: nat->T->A->forall {R}, (T*B->R)->R) (start:T) : Tuple.tuple' A n -> forall {R}, (T * tuple' B n -> R) -> R := 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 |