From 4a8952b701300f86bb75548f7665dde71d3d9c63 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 1 Aug 2018 12:57:59 -0400 Subject: Add nth_error_combine --- src/Util/ListUtil.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 390f75cd7..22b90cdc7 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -2102,3 +2102,13 @@ Lemma fold_right_push A (x y : A) (f : A -> A -> A) Proof. rewrite <- (rev_involutive ls), !fold_left_rev_right, fold_left_push with (f:=fun x y => f y x); auto. Qed. + +Lemma nth_error_combine {A B} n (ls1 : list A) (ls2 : list B) + : nth_error (combine ls1 ls2) n = match nth_error ls1 n, nth_error ls2 n with + | Some v1, Some v2 => Some (v1, v2) + | _, _ => None + end. +Proof. + revert ls2 n; induction ls1 as [|l1 ls1 IHls1], ls2, n; cbn [combine nth_error]; try reflexivity; auto. + edestruct nth_error; reflexivity. +Qed. -- cgit v1.2.3