diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-11-11 16:01:31 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-11-11 16:01:31 -0500 |
| commit | e7da9779f7f64bd51a806237439fd249305eec47 (patch) | |
| tree | 519ba6e173648297a6c7d32a886a81bbe0601481 /src/Util | |
| parent | db9921705a8038507335117ecaaeace1f3ac0b80 (diff) | |
Add map_repeat, map_const
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/ListUtil.v | 7 |
1 files changed, 7 insertions, 0 deletions
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. |