diff options
author | Jason Gross <jgross@mit.edu> | 2019-03-07 23:47:27 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-03-07 23:47:27 -0500 |
commit | a4dd5ebe448de902df0961bf71c665198149898c (patch) | |
tree | 8fd235ee5b0871c7720522668bb801e7d3e50f93 /src/Util/ListUtil | |
parent | 9ddfac020c885bdf4f046fc0bb00117e7bdfbda8 (diff) |
Add Forall2_forall_In_combine_iff
Diffstat (limited to 'src/Util/ListUtil')
-rw-r--r-- | src/Util/ListUtil/Forall.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/Util/ListUtil/Forall.v b/src/Util/ListUtil/Forall.v index 77fa0ea11..ffc6ca9e9 100644 --- a/src/Util/ListUtil/Forall.v +++ b/src/Util/ListUtil/Forall.v @@ -200,3 +200,13 @@ Proof using Type. end | lia ]. Qed. + +Lemma Forall2_forall_In_combine_iff {A B} R xs ys + : @List.Forall2 A B R xs ys + <-> (List.length xs = List.length ys + /\ forall x y, List.In (x, y) (List.combine xs ys) -> R x y). +Proof using Type. + split; revert ys; induction xs as [|x xs IHxs], ys as [|y ys]; cbn in *; intro H. + all: inversion_clear H; split_and; + try solve [ repeat constructor; intuition (congruence + eauto) ]. +Qed. |