From d704a3934f406c63a7d917fdb865ddf37e58d1e8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 12 Feb 2018 17:54:57 -0500 Subject: Add expand_list_correct to ListUtil --- src/Util/ListUtil.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 38678ac59..f659c7dba 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1779,3 +1779,33 @@ Proof. revert ys; induction xs as [|a xs IHxs]; destruct ys; intros; try reflexivity; []. simpl. rewrite IHxs. reflexivity. Qed. + +Definition expand_list_helper {A} (default : A) (ls : list A) (n : nat) (idx : nat) : list A + := nat_rect + (fun _ => nat -> list A) + (fun _ => nil) + (fun n' rec_call idx + => cons (List.nth_default default ls idx) (rec_call (S idx))) + n + idx. +Definition expand_list {A} (default : A) (ls : list A) (n : nat) : list A + := expand_list_helper default ls n 0. + +Lemma expand_list_helper_correct {A} (default : A) (ls : list A) (n idx : nat) (H : (idx + n <= length ls)%nat) + : expand_list_helper default ls n idx + = List.firstn n (List.skipn idx ls). +Proof. + cbv [expand_list_helper]; revert idx H. + induction n as [|n IHn]; cbn; intros. + { reflexivity. } + { rewrite IHn by omega. + erewrite (@skipn_nth_default _ idx ls) by omega. + reflexivity. } +Qed. + +Lemma expand_list_correct (n : nat) {A} (default : A) (ls : list A) (H : List.length ls = n) + : expand_list default ls n = ls. +Proof. + subst; cbv [expand_list]; rewrite expand_list_helper_correct by reflexivity. + rewrite skipn_0, firstn_all; reflexivity. +Qed. -- cgit v1.2.3