Add admitted lemma about tuple map, add hlist lem

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