Add firstn_skipn

1 files changed, 16 insertions, 0 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index eb807abda..902d4cb7e 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -777,6 +777,22 @@ Hint Rewrite @skipn_skipn : simpl_skipn.
 Hint Rewrite <- @skipn_skipn : push_skipn.
 Hint Rewrite @skipn_skipn : pull_skipn.
 
+Lemma skipn_firstn {A} (ls : list A) n m
+  : skipn n (firstn m ls) = firstn (m - n) (skipn n ls).
+Proof.
+  revert n m; induction ls, m, n; simpl; autorewrite with simpl_skipn simpl_firstn; boring_list.
+Qed.
+Lemma firstn_skipn {A} (ls : list A) n m
+  : firstn n (skipn m ls) = skipn m (firstn (m + n) ls).
+Proof.
+  revert n m; induction ls, m; simpl; autorewrite with simpl_skipn simpl_firstn; boring_list.
+Qed.
+Lemma firstn_skipn' {A} (ls : list A) n m
+  : firstn n (skipn m ls) = skipn m (firstn (n + m) ls).
+Proof. rewrite firstn_skipn; do 2 f_equal; auto with arith. Qed.
+Hint Rewrite <- @firstn_skipn @firstn_skipn' : simpl_firstn.
+Hint Rewrite <- @firstn_skipn @firstn_skipn' : simpl_skipn.
+
 Lemma firstn_app_inleft : forall {A} n (xs ys : list A), (n <= length xs)%nat ->
   firstn n (xs ++ ys) = firstn n xs.
 Proof.