Add Tuple and HList lemmas

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