From a4dd5ebe448de902df0961bf71c665198149898c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 7 Mar 2019 23:47:27 -0500 Subject: Add Forall2_forall_In_combine_iff --- src/Util/ListUtil/Forall.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Util') 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. -- cgit v1.2.3