From 88548627b9776f0f05754ef35ca54199af567e30 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 9 Oct 2018 20:33:29 -0400 Subject: Add map_update_nth_ext --- src/Util/ListUtil.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/Util') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 8211d1ab7..1713d22ab 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -2165,3 +2165,13 @@ Qed. Lemma concat_fold_right_app A ls : @List.concat A ls = List.fold_right (@List.app A) nil ls. Proof. induction ls; cbn; eauto. Qed. + +Lemma map_update_nth_ext {A B n} f1 f2 f3 ls1 ls2 + : map f3 ls1 = ls2 + -> (forall x, List.In x ls1 -> f3 (f2 x) = f1 (f3 x)) + -> map f3 (@update_nth A n f2 ls1) = @update_nth B n f1 ls2. +Proof. + revert ls1 ls2; induction n as [|n IHn], ls1 as [|x1 xs1], ls2 as [|x2 xs2]; cbn; intros H0 H1; try discriminate; try reflexivity. + all: inversion H0; clear H0; subst. + all: f_equal; eauto using or_introl. +Qed. -- cgit v1.2.3