diff options
-rw-r--r-- | src/Util/HList.v | 20 | ||||
-rw-r--r-- | src/Util/IffT.v | 9 | ||||
-rw-r--r-- | src/Util/Prod.v | 16 | ||||
-rw-r--r-- | src/Util/Tuple.v | 5 |
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} |