diff options
-rw-r--r-- | src/Util/HList.v | 18 | ||||
-rw-r--r-- | src/Util/Tuple.v | 7 |
2 files changed, 25 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. diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 7af4dfe96..7367b1460 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -136,6 +136,13 @@ Definition on_tuple {A B} (f:list A -> list B) Definition map {n A B} (f:A -> B) (xs:tuple A n) : tuple B n := on_tuple (List.map f) (fun _ => eq_trans (map_length _ _)) xs. +Lemma map_S {n A B} (f:A -> B) (xs:tuple' A n) (x:A) + : map (n:=S (S n)) f (xs, x) = (map (n:=S n) f xs, f x). +Proof. + unfold map, on_tuple. + simpl @List.map. +Admitted. + Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat} (Hlength : forall la lb, length la = a -> length lb = b -> length (f la lb) = c) (ta:tuple A a) (tb:tuple B b) : tuple C c |