diff options
| -rw-r--r-- | src/Util/ListUtil/Forall.v | 19 |
1 files changed, 19 insertions, 0 deletions
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. |