From 13441cbbe1671b1f894a8daf286c30c70b340eca Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 14 Mar 2017 21:59:44 -0400
Subject: Add firstn_skipn

---
 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 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.
-- 
cgit v1.2.3