diff options
Diffstat (limited to 'src/Util/ListUtil.v')
-rw-r--r-- | src/Util/ListUtil.v | 16 |
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. |