Add Tuple and HList lemmas

1 files changed, 17 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.