diff options
author | 2016-10-19 13:20:55 -0400 | |
---|---|---|
committer | 2016-10-19 13:20:55 -0400 | |
commit | 79c848f7b252849c8b99430eb6d7b3dd3920a88a (patch) | |
tree | 4052e43dc2ab0b13e7759782578172dbb49b51c4 | |
parent | 03403f0a6c9bcb610de0a82419f13105e82824b2 (diff) |
Add Tuple.map2
-rw-r--r-- | src/Util/ListUtil.v | 2 | ||||
-rw-r--r-- | src/Util/Tuple.v | 4 |
2 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 749b1b09f..84553d64b 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1494,6 +1494,8 @@ Proof. rewrite map2_cons, !length_cons, IHls1. auto. Qed. +Hint Rewrite @map2_length : distr_length. + Ltac simpl_list_lengths := repeat match goal with | H : appcontext[length (@nil ?A)] |- _ => rewrite (@nil_length0 A) in H diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index bcfc7be5b..c6b97415d 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -2,6 +2,7 @@ Require Import Coq.Classes.Morphisms. Require Import Coq.Relations.Relation_Definitions. Require Import Coq.Lists.List. Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.ListUtil. Require Export Crypto.Util.FixCoqMistakes. Fixpoint tuple' T n : Type := @@ -106,6 +107,9 @@ Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat} := 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)). +Definition map2 {n A B C} (f:A -> B -> C) (xs:tuple A n) (ys:tuple B n) : tuple C n + := on_tuple2 (map2 f) (fun la lb pfa pfb => eq_trans (@map2_length _ _ _ _ la lb) (eq_trans (f_equal2 _ pfa pfb) (Min.min_idempotent _))) xs ys. + 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). } |