diff options
author | Jason Gross <jgross@mit.edu> | 2019-03-08 19:48:02 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-03-08 19:48:02 -0500 |
commit | b13cb39473dd93136ee36691f226f1924baff9a4 (patch) | |
tree | 9a3f37a3ca66362a20655663f0eca6395f64c451 /src | |
parent | 8fd63ce4a8bca37f98d7e9044d2b0ffc0278f2e1 (diff) |
Add Forall2_Proper instances
Diffstat (limited to 'src')
-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. |