From 853821e4374050d5a770ee623b24a7bf15e288ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 8 Nov 2016 11:22:11 -0500 Subject: Rename iffT, add some lemmas about tuple and hlist Some lemmas admitted --- src/Util/HList.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'src/Util/HList.v') diff --git a/src/Util/HList.v b/src/Util/HList.v index 1a23f8fd6..0ebb4cdce 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -63,3 +63,23 @@ Qed. Lemma map_is_mapt' {n A F B} (f : A -> B) {ts : tuple A (S n)} (ls : hlist' F ts) : Tuple.map f ts = mapt' (fun x _ => f x) ls. Proof. apply (@map_is_mapt (S n)). Qed. + + +Lemma hlist'_impl {n A F G} (xs:tuple' A n) + : (hlist' (fun x => F x -> G x) xs) -> (hlist' F xs -> hlist' G xs). +Proof. + induction n; simpl in *; intuition. +Defined. + +Lemma hlist_impl {n A F G} (xs:tuple A n) + : (hlist (fun x => F x -> G x) xs) -> (hlist F xs -> hlist G xs). +Proof. + destruct n; [ constructor | apply hlist'_impl ]. +Defined. + +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. + Proof. + Admitted. +End Tuple. -- cgit v1.2.3