diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-10-09 20:33:29 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-10-09 20:33:29 -0400 |
| commit | 88548627b9776f0f05754ef35ca54199af567e30 (patch) | |
| tree | 74ee120134ef518a14a06d6cb13c66e1e6e14712 /src/Util | |
| parent | 2f836e6ca8e0f431f38d6342e10d979594de7e3e (diff) | |
Add map_update_nth_ext
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/ListUtil.v | 10 |
1 files changed, 10 insertions, 0 deletions
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. |