diff options
Diffstat (limited to 'src/Util/HList.v')
-rw-r--r-- | src/Util/HList.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/Util/HList.v b/src/Util/HList.v index 8013e8b15..4096c54d6 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -31,3 +31,21 @@ Definition mapt {n A F B} (f : forall x : A, F x -> B) | 0 => fun ts v => tt | S n' => @mapt' n' A F B f end. + +Lemma map'_mapt' {n A F B C} (g : B -> C) (f : forall x : A, F x -> B) + {ts : tuple' A n} (ls : hlist' F ts) + : Tuple.map (n:=S n) g (mapt' f ls) = mapt' (fun x v => g (f x v)) ls. +Proof. + induction n as [|n IHn]; [ reflexivity | ]. + { simpl @mapt' in *. + rewrite <- IHn. + rewrite Tuple.map_S; reflexivity. } +Qed. + +Lemma map_mapt {n A F B C} (g : B -> C) (f : forall x : A, F x -> B) + {ts : tuple A n} (ls : hlist F ts) + : Tuple.map g (mapt f ls) = mapt (fun x v => g (f x v)) ls. +Proof. + destruct n as [|n]; [ reflexivity | ]. + apply map'_mapt'. +Qed. |