From ff09c2ee30773578ca9e81d0b7ded9d18a666192 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 10 Aug 2018 18:29:25 -0400 Subject: Add ListUtil.map_nth_default_seq --- src/Util/ListUtil.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 797796322..3d43bf509 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -2122,3 +2122,19 @@ Proof. rewrite combine_app_samelength, IHls1 by (rewrite ?rev_length; congruence); cbn [combine]. reflexivity. Qed. + +Lemma map_nth_default_seq {A} (d:A) n ls + : length ls = n -> List.map (List.nth_default d ls) (List.seq 0 n) = ls. +Proof. + intro; subst. + rewrite <- (List.rev_involutive ls); generalize (List.rev ls); clear ls; intro ls. + rewrite List.rev_length. + induction ls; cbn [length List.rev]; [ reflexivity | ]. + rewrite seq_snoc, List.map_app. + apply f_equal2; [ | cbn; rewrite nth_default_app, List.rev_length, Nat.sub_diag ]; + [ etransitivity; [ | eassumption ]; apply List.map_ext_in; intro; rewrite Lists.List.in_seq; + rewrite nth_default_app, List.rev_length; intros + | ]. + all: edestruct lt_dec; try (exfalso; lia). + all: reflexivity. +Qed. -- cgit v1.2.3