diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-06 17:03:30 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-06 17:03:30 -0500 |
| commit | beaf8c386549f99d0366f7c6a269ebb9ce311c5f (patch) | |
| tree | 981a79538d6d9981841bbbd1634d1e6a463f539c /src/Util/HList.v | |
| parent | e91d45d8667001214e23f119f0b50294f34077a2 (diff) | |
Add HList lemma
Diffstat (limited to 'src/Util/HList.v')
| -rw-r--r-- | src/Util/HList.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Util/HList.v b/src/Util/HList.v index 4096c54d6..120d898d9 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -49,3 +49,13 @@ Proof. destruct n as [|n]; [ reflexivity | ]. apply map'_mapt'. Qed. + +Lemma map_is_mapt {n A F B} (f : A -> B) {ts : tuple A n} (ls : hlist F ts) + : Tuple.map f ts = mapt (fun x _ => f x) ls. +Proof. + destruct n as [|n]; [ reflexivity | ]. + induction n as [|n IHn]; [ reflexivity | ]. + { unfold mapt in *; simpl @mapt' in *. + rewrite <- IHn; clear IHn. + rewrite <- (@Tuple.map_S n _ _ f); destruct ts; reflexivity. } +Qed. |