From 445ff49ade0fd19c81d954f035394aae561d0958 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 30 Mar 2017 14:27:00 -0400 Subject: Get rid of list-based Tuple.map --- src/Util/HList.v | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'src/Util/HList.v') diff --git a/src/Util/HList.v b/src/Util/HList.v index 1a724f84b..2a135c75c 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -91,11 +91,10 @@ Qed. Lemma map_is_mapt {n A F B} (f : A -> B) {ts : tuple A n} (ls : hlist F ts) : Tuple.map f ts = mapt (fun x _ => f x) ls. Proof. - destruct n as [|n]; [ reflexivity | ]. + destruct n as [|n]; simpl; [ destruct ts; reflexivity | ]. induction n as [|n IHn]; [ reflexivity | ]. - { unfold mapt in *; simpl @mapt' in *. - rewrite <- IHn; clear IHn. - rewrite <- (@Tuple.map_S n _ _ f); destruct ts; reflexivity. } + { simpl in *; rewrite <- IHn; clear IHn. + reflexivity. } Qed. Lemma map_is_mapt' {n A F B} (f : A -> B) {ts : tuple A (S n)} (ls : hlist' F ts) @@ -147,7 +146,7 @@ Global Instance mapt_Proper {n A F B} : Proper ((forall_relation (fun x => pointwise_relation _ Logic.eq)) ==> forall_relation (fun ts => Logic.eq ==> Logic.eq)) - (@HList.mapt n A F B). + (@mapt n A F B). Proof. unfold forall_relation, pointwise_relation, respectful. repeat intro; subst; destruct n as [|n]; [ reflexivity | ]. -- cgit v1.2.3