From b13cb39473dd93136ee36691f226f1924baff9a4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 8 Mar 2019 19:48:02 -0500 Subject: Add Forall2_Proper instances --- src/Util/ListUtil/Forall.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'src/Util') diff --git a/src/Util/ListUtil/Forall.v b/src/Util/ListUtil/Forall.v index d9adfffa6..56243e461 100644 --- a/src/Util/ListUtil/Forall.v +++ b/src/Util/ListUtil/Forall.v @@ -217,3 +217,22 @@ Proof using Type. all: inversion_clear H; split_and; try solve [ repeat constructor; intuition (congruence + eauto) ]. Qed. + +Global Instance Forall2_Proper_impl {A B} + : Proper (pointwise_relation _ (pointwise_relation _ Basics.impl) ==> eq ==> eq ==> Basics.impl) + (@List.Forall2 A B) | 10. +Proof. + cbv [Basics.impl respectful pointwise_relation]. + repeat intro; subst; rewrite Forall2_forall_In_combine_iff in *. + destruct_head'_and; split; eauto. +Qed. + +Global Instance Forall2_Proper_iff {A B} + : Proper (pointwise_relation _ (pointwise_relation _ iff) ==> eq ==> eq ==> iff) + (@List.Forall2 A B) | 10. +Proof. + cbv [respectful pointwise_relation]. + repeat intro; subst; rewrite !Forall2_forall_In_combine_iff in *. + split_iff. + repeat (split || destruct_head'_and); eauto. +Qed. -- cgit v1.2.3