diff options
| -rw-r--r-- | src/Util/HList.v | 17 | ||||
| -rw-r--r-- | src/Util/Tuple.v | 4 |
2 files changed, 21 insertions, 0 deletions
diff --git a/src/Util/HList.v b/src/Util/HList.v index ec9dcdd7b..c1fab2aee 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -3,6 +3,7 @@ Require Import Coq.Relations.Relation_Definitions. Require Import Coq.Lists.List. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.IffT. Require Import Crypto.Util.Tuple. Require Export Crypto.Util.FixCoqMistakes. @@ -100,6 +101,22 @@ Proof. reflexivity. Qed. +Lemma fold_right_and_True_hlist' {n A F} (xs:tuple' A n) + : iffT (List.fold_right and True (List.map F (Tuple.to_list' _ xs))) (hlist' F xs). +Proof. + induction n. + { simpl; tauto. } + { specialize (IHn (fst xs)). + destruct xs; simpl in *. + tauto. } +Qed. + +Lemma fold_right_and_True_hlist {n A F} (xs:tuple A n) + : iffT (List.fold_right and True (List.map F (Tuple.to_list _ xs))) (hlist F xs). +Proof. + destruct n; [ simpl; tauto | apply fold_right_and_True_hlist' ]. +Qed. + Module Tuple. Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n) : hlist (fun x => f x = x) xs -> Tuple.map f xs = xs. diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 79747ec2d..d1dcbca30 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -195,6 +195,10 @@ Proof. simpl @List.map. Admitted. +Lemma map_to_list {A B n ts} (f : A -> B) + : List.map f (@to_list A n ts) = @to_list B n (map f ts). +Proof. Admitted. + Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat} (Hlength : forall la lb, length la = a -> length lb = b -> length (f la lb) = c) (ta:tuple A a) (tb:tuple B b) : tuple C c |