From e7da9779f7f64bd51a806237439fd249305eec47 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 11 Nov 2018 16:01:31 -0500 Subject: Add map_repeat, map_const --- src/Util/ListUtil.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Util') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index efaea107d..fb19ac1da 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -2205,3 +2205,10 @@ Proof. induction ls; cbn; eauto. Qed. Lemma eq_map_list_rect {A B} f (ls : list _) : @List.map A B f ls = list_rect _ nil (fun x _ rec => f x :: rec) ls. Proof. induction ls; cbn; eauto. Qed. + +Lemma map_repeat {A B} (f : A -> B) v k + : List.map f (List.repeat v k) = List.repeat (f v) k. +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. -- cgit v1.2.3