From c19c7aa0b4efa8a2529304d4c4e46435d765699e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 10 Nov 2016 14:51:57 -0500 Subject: Add Tuple and HList lemmas --- src/Util/HList.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'src/Util/HList.v') 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. -- cgit v1.2.3