From e91d45d8667001214e23f119f0b50294f34077a2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 6 Nov 2016 16:56:59 -0500 Subject: Add admitted lemma about tuple map, add hlist lem --- src/Util/HList.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'src/Util/HList.v') 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. -- cgit v1.2.3