From f42021b5ddd1f6bafe0c0b42944d39d5fc36dc25 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 6 Dec 2018 13:07:07 -0500 Subject: Add Forall2_update_nth --- src/Util/ListUtil.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'src/Util') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 60899696d..9f6658c42 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -2189,3 +2189,19 @@ Proof. induction k; cbn; f_equal; assumption. Qed. Lemma map_const {A B} (v : B) (ls : list A) : List.map (fun _ => v) ls = List.repeat v (List.length ls). Proof. induction ls; cbn; f_equal; assumption. Qed. + +Lemma Forall2_update_nth {A B f g n R ls1 ls2} + : @List.Forall2 A B R ls1 ls2 + -> (forall v1, nth_error ls1 n = Some v1 -> forall v2, nth_error ls2 n = Some v2 -> R v1 v2 -> R (f v1) (g v2)) + -> @List.Forall2 A B R (update_nth n f ls1) (update_nth n g ls2). +Proof using Type. + intro H; revert n; induction H, n; cbn [nth_error update_nth]. + all: repeat first [ progress intros + | progress specialize_by_assumption + | assumption + | match goal with + | [ |- List.Forall2 _ _ _ ] => constructor + | [ H : forall x, Some _ = Some x -> _ |- _ ] => specialize (H _ eq_refl) + | [ IH : forall n : nat, _, H : forall v1, nth_error ?l ?n = Some v1 -> _ |- _ ] => specialize (IH n H) + end ]. +Qed. -- cgit v1.2.3