diff options
| -rw-r--r-- | src/Util/HList.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Util/HList.v b/src/Util/HList.v index aacefe8f3..ec9dcdd7b 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -88,6 +88,18 @@ Proof. destruct n; [ constructor | apply hlist'_impl ]. Defined. +Local Arguments Tuple.map : simpl never. +Lemma hlist_map {n A B F} {f:A -> B} (xs:tuple A n) + : hlist F (Tuple.map f xs) = hlist (fun x => F (f x)) xs. +Proof. + destruct n as [|n]; [ reflexivity | ]. + induction n; [ reflexivity | ]. + specialize (IHn (fst xs)). + destruct xs; rewrite Tuple.map_S. + simpl @hlist in *; rewrite <- IHn. + reflexivity. +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. |