Rename iffT, add some lemmas about tuple and hlist

Some lemmas admitted

4 files changed, 38 insertions, 12 deletions

diff --git a/src/Util/HList.v b/src/Util/HList.v
index 1a23f8fd6..0ebb4cdce 100644
--- a/src/Util/HList.v
+++ b/src/Util/HList.v
@@ -63,3 +63,23 @@ Qed.
 Lemma map_is_mapt' {n A F B} (f : A -> B) {ts : tuple A (S n)} (ls : hlist' F ts)
   : Tuple.map f ts = mapt' (fun x _ => f x) ls.
 Proof. apply (@map_is_mapt (S n)). Qed.
+
+
+Lemma hlist'_impl {n A F G} (xs:tuple' A n)
+  : (hlist' (fun x => F x -> G x) xs) -> (hlist' F xs -> hlist' G xs).
+Proof.
+  induction n; simpl in *; intuition.
+Defined.
+
+Lemma hlist_impl {n A F G} (xs:tuple A n)
+  : (hlist (fun x => F x -> G x) xs) -> (hlist F xs -> hlist G xs).
+Proof.
+  destruct n; [ constructor | apply hlist'_impl ].
+Defined.
+
+Module Tuple.
+  Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n)
+  : hlist (fun x => f x = x) xs -> Tuple.map f xs = xs.
+  Proof.
+  Admitted.
+End Tuple.
diff --git a/src/Util/IffT.v b/src/Util/IffT.v
index fd132fbfa..f4eaa9d53 100644
--- a/src/Util/IffT.v
+++ b/src/Util/IffT.v
@@ -1,9 +1,10 @@
 Require Import Coq.Classes.RelationClasses.
-Notation iffT := (fun A B => inhabited ((A -> B) * (B -> A)))%type.
+Notation iffT A B := (((A -> B) * (B -> A)))%type.
+Notation iffTp := (fun A B => inhabited (iffT A B)).
 
-Global Instance iffT_Reflexive : Reflexive iffT | 1.
+Global Instance iffTp_Reflexive : Reflexive iffTp | 1.
 Proof. repeat constructor; intro; assumption. Defined.
-Global Instance iffT_Symmetric : Symmetric iffT | 1.
+Global Instance iffTp_Symmetric : Symmetric iffTp | 1.
 Proof. repeat (intros [?] || intro); constructor; tauto. Defined.
-Global Instance iffT_Transitive : Transitive iffT | 1.
+Global Instance iffTp_Transitive : Transitive iffTp | 1.
 Proof. repeat (intros [?] || intro); constructor; tauto. Defined.
diff --git a/src/Util/Prod.v b/src/Util/Prod.v
index fea2589be..bcd9404a6 100644
--- a/src/Util/Prod.v
+++ b/src/Util/Prod.v
@@ -76,23 +76,23 @@ Proof. repeat (intros [? ?] || intro || split); assumption. Defined.
 Global Instance iff_prod_Proper
   : Proper (iff ==> iff ==> iff) (fun A B => prod A B).
 Proof. repeat intro; tauto. Defined.
-Global Instance iff_iffT_prod_Proper
-  : Proper (iff ==> iffT ==> iffT) (fun A B => prod A B) | 1.
+Global Instance iff_iffTp_prod_Proper
+  : Proper (iff ==> iffTp ==> iffTp) (fun A B => prod A B) | 1.
 Proof.
   intros ?? [?] ?? [?]; constructor; tauto.
 Defined.
-Global Instance iffT_iff_prod_Proper
-  : Proper (iffT ==> iff ==> iffT) (fun A B => prod A B) | 1.
+Global Instance iffTp_iff_prod_Proper
+  : Proper (iffTp ==> iff ==> iffTp) (fun A B => prod A B) | 1.
 Proof.
   intros ?? [?] ?? [?]; constructor; tauto.
 Defined.
-Global Instance iffT_iffT_prod_Proper
-  : Proper (iffT ==> iffT ==> iffT) (fun A B => prod A B) | 1.
+Global Instance iffTp_iffTp_prod_Proper
+  : Proper (iffTp ==> iffTp ==> iffTp) (fun A B => prod A B) | 1.
 Proof.
   intros ?? [?] ?? [?]; constructor; tauto.
 Defined.
-Hint Extern 2 (Proper _ prod) => apply iffT_iffT_prod_Proper : typeclass_instances.
-Hint Extern 2 (Proper _ (fun A => prod A)) => refine iff_iffT_prod_Proper : typeclass_instances.
+Hint Extern 2 (Proper _ prod) => apply iffTp_iffTp_prod_Proper : typeclass_instances.
+Hint Extern 2 (Proper _ (fun A => prod A)) => refine iff_iffTp_prod_Proper : typeclass_instances.
 Hint Extern 2 (Proper _ (fun A B => prod A B)) => refine iff_prod_Proper : typeclass_instances.
 
 (** ** Useful Tactics *)
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 21abfed3a..4d97c7857 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -193,6 +193,11 @@ Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n)
 Proof.
 Admitted.
 
+Lemma map_map {n A B C} (g : B -> C) (f : A -> B) (xs:tuple A n)
+  : map g (map f xs) = map (fun x => g (f x)) xs.
+Proof.
+Admitted.
+
 Section monad.
   Context (M : Type -> Type) (bind : forall X Y, M X -> (X -> M Y) -> M Y) (ret : forall X, X -> M X).
   Fixpoint lift_monad' {n A} {struct n}