diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-08 15:34:15 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-11-08 15:34:15 -0500 |
commit | cc99ccd589ac7bdd7aeb208d709a8980a7c957cb (patch) | |
tree | d27bc054dd29c3bfb23526c1f28ad6f8f3c0914a /src | |
parent | 25bee1e1ea359593fcd3a75b044f3fb66ae85b00 (diff) |
Add map2_map{,_fst,_snd}
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/Tuple.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 4d97c7857..ea22d8ff3 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -193,6 +193,23 @@ Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n) Proof. Admitted. +Lemma map2_map {n A B C A' B'} (f:A -> B -> C) (g:A' -> A) (h:B' -> B) (xs:tuple A' n) (ys:tuple B' n) + : map2 f (map g xs) (map h ys) = map2 (fun a b => f (g a) (h b)) xs ys. +Proof. +Admitted. + +Lemma map2_map_fst {n A B C A'} (f:A -> B -> C) (g:A' -> A) (xs:tuple A' n) (ys:tuple B n) + : map2 f (map g xs) ys = map2 (fun a b => f (g a) b) xs ys. +Proof. + rewrite <- (map2_map f g (fun x => x)), map_id; reflexivity. +Qed. + +Lemma map2_map_snd {n A B C B'} (f:A -> B -> C) (g:B' -> B) (xs:tuple A n) (ys:tuple B' n) + : map2 f xs (map g ys) = map2 (fun a b => f a (g b)) xs ys. +Proof. + rewrite <- (map2_map f (fun x => x) g), map_id; reflexivity. +Qed. + Lemma map_map {n A B C} (g : B -> C) (f : A -> B) (xs:tuple A n) : map g (map f xs) = map (fun x => g (f x)) xs. Proof. |