diff options
-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). } |